| DISP | bexp_df |  exp== exp |
| ABS | bexp | exp == rec(B. + B  B + B B + B + Exp Exp + Exp Exp) |
| THM | bexp_wf | exp   |
| DISP | bexp_atom_df | Bexp(<b:bool:*>)== Bexp(<b>) |
| ABS | bexp_atom | Bexp(b) == inl b |
| THM | bexp_atom_wf |  b:. Bexp(b) exp |
| DISP | andbexp_df | <b1:bexp:*> AND <b2:bexp:*>== <b1> AND <b2> |
| ABS | andbexp | b1 AND b2 == inr (inl <b1, b2> ) |
| THM | andbexp_wf | b1,b2:exp. b1 AND b2 exp |
| DISP | orbexp_df | <b1:bexp:*> OR <b2:bexp:*>== <b1> OR <b2> |
| ABS | orbexp | b1 OR b2 == inr inr (inl <b1, b2> ) |
| THM | orbexp_wf | b1,b2:exp. b1 OR b2 exp |
| DISP | notbexp_df | NOT <b:bexp:*>== NOT <b> |
| ABS | notbexp | NOT b == inr inr inr (inl b ) |
| THM | notbexp_wf | b:exp. NOT b exp |
| DISP | ltexp_df | <e1:exp:*> < <e2:exp:*>== <e1> < <e2> |
| ABS | ltexp | e1 < e2 == inr inr inr inr (inl <e1, e2> ) |
| THM | ltexp_wf | e1,e2:Exp. e1 < e2 exp |
| DISP | eqexp_df | <e1:exp:*> == <e2:exp:*>== <e1> == <e2> |
| ABS | eqexp | e1 == e2 == inr inr inr inr inr <e1, e2> |
| THM | eqexp_wf | e1,e2:Exp. e1 == e2 exp |
| DISP | bexp_cases_df | {[SOFT}{->0}case <b:b:*> {\\}of {->0}Bexp(<atm:var>)  
<atom_case:atom_case:*> {\\}<a1:var> AND <a2:var>
<and_case:and_case:*> {\\}<o1:var> OR <o2:var> <or_case:or_case:*>
{\\}NOT <n:var> <not_case:not_case:*> {\\}<l1:var> < <l2:var>
<lt_case:lt_case:*> {\\}<e1:var> == <e2:var> <eq_case:eq_case:*>
{<-}{<-}{]}
== case <b>
of Bexp(<atm>) <atom_case>
<a1> AND <a2> <and_case>
<o1> OR <o2> <or_case>
NOT <n> <not_case>
<l1> < <l2> <lt_case>
<e1> == <e2> <eq_case> |
| ABS | bexp_cases | case b
of Bexp(atm) atom_case[atm]
a1 AND a2 and_case[a1; a2]
o1 OR o2 or_case[o1; o2]
NOT n not_case[n]
l1 < l2 lt_case[l1; l2]
e1 == e2 eq_case[e1; e2] ==
case b
of inl(atm) => atom_case[atm]
| inr(natm) => case natm
of inl(aa) => let <a1,a2> = aa in and_case[a1; a2]
| inr(na) => case na
of inl(oo) => let <o1,o2> = oo
in
or_case[o1; o2]
| inr(no) => case no
of inl(n) => not_case[n]
| inr(nn) => case nn
of inl(ll)
=> let <l1,l2> = ll
in
lt_case[l1; l2]
| inr(ee)
=> let <e1,e2> = ee
in
eq_case[e1; e2] |
| THM | bexp_cases_wf | T:. atom_case: T. and_case,or_case:exp exp T.
not_case:exp T. lt_case,eq_case:Exp Exp T. b:exp.
case b
of Bexp(atm) atom_case[atm]
a1 AND a2 and_case[a1;a2]
o1 OR o2 or_case[o1;o2]
NOT n not_case[n]
l1 < l2 lt_case[l1;l2]
e1 == e2 eq_case[e1;e2] T |
| ML | bexp_cases_eval1 | let bexp_cases_atomC =
SimpleMacroC `exp_cases_atom`
 case Bexp(x)
of Bexp(b) atom_case[b]
a1 AND a2 and_case[a1; a2]
o1 OR o2 or_case[o1; o2]
NOT n not_case[n]
l1 < l2 lt_case[l1; l2]
e1 == e2 eq_case[e1; e2]
atom_case[x] ``bexp_cases bexp_atom``
;;
let bexp_cases_andC =
SimpleMacroC `exp_cases_and`
case x AND y
of Bexp(b) atom_case[b]
a1 AND a2 and_case[a1; a2]
o1 OR o2 or_case[o1; o2]
NOT n not_case[n]
l1 < l2 lt_case[l1; l2]
e1 == e2 eq_case[e1; e2]
and_case[x; y] ``bexp_cases andbexp``
;;
let bexp_cases_orC =
SimpleMacroC `exp_cases_or`
case x OR y
of Bexp(b) atom_case[b]
a1 AND a2 and_case[a1; a2]
o1 OR o2 or_case[o1; o2]
NOT n not_case[n]
l1 < l2 lt_case[l1; l2]
e1 == e2 eq_case[e1; e2]
or_case[x; y] ``bexp_cases orbexp``
;;
let bexp_cases_notC =
SimpleMacroC `exp_cases_not`
case NOT x
of Bexp(b) atom_case[b]
a1 AND a2 and_case[a1; a2]
o1 OR o2 or_case[o1; o2]
NOT n not_case[n]
l1 < l2 lt_case[l1; l2]
e1 == e2 eq_case[e1; e2]
not_case[x] ``bexp_cases notbexp``
;; |
| ML | bexp_cases_eval2 | let bexp_cases_ltC =
SimpleMacroC `exp_cases_lt`
case x < y
of Bexp(b) atom_case[b]
a1 AND a2 and_case[a1; a2]
o1 OR o2 or_case[o1; o2]
NOT n not_case[n]
l1 < l2 lt_case[l1; l2]
e1 == e2 eq_case[e1; e2]
lt_case[x; y] ``bexp_cases ltexp``
;;
let bexp_cases_eqC =
SimpleMacroC `exp_cases_eq`
case x == y
of Bexp(b) atom_case[b]
a1 AND a2 and_case[a1; a2]
o1 OR o2 or_case[o1; o2]
NOT n not_case[n]
l1 < l2 lt_case[l1; l2]
e1 == e2 eq_case[e1; e2]
eq_case[x; y] ``bexp_cases eqexp``
;;
let bexp_casesC =
FirstC [bexp_cases_atomC;
bexp_cases_andC;
bexp_cases_orC;
bexp_cases_notC;
bexp_cases_ltC;
bexp_cases_eqC]
;;
add_AbReduce_conv `bexp_cases` bexp_casesC
;; |
| THM | bexp_ind_tp | P:exp 
(b:. P[Bexp(b)])
  (b1,b2:exp. P[b1] P[b2] P[b1 AND b2])
(b1,b2:exp. P[b1] P[b2] P[b1 OR b2])
(b:exp. P[b] P[NOT b])
(e1,e2:Exp. P[e1 < e2])
(e1,e2:Exp. P[e1 == e2])
{b:exp. P[b]} |
| ML | bexp_ind_tac | let BexpInd i p = ByAnalogyWith1 `bexp_ind_tp` [`hr`, int_to_arg i] p;
; |
| DISP | bexpval_df | [<bex:bexp:*>](<m:m:*>)== [<bex>](<m>) |
| ML | bexpval_ml | [bex](m)
==r case bex
of Bexp(atm) atm
b1 AND b2 [b1](m)   [b2](m)
b1 OR b2 [b1](m)  [b2](m)
NOT b  [b](m)
e1 < e2 [e1] <z [e2]
e1 == e2 ([e1] = [e2]) |
| THM | bexpval_wf | b:exp. m:Atom  . [b](m) |
| ML | bexpval_eval | let bexpvalC =
RecUnfoldC `bexpval` ANDTHENC bexp_casesC
;;
add_AbReduce_conv `bexpval` bexpvalC
;; |