Nuprl Theory boolean_expression

(only non hidden objects are presented)

 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()== Bexp() ABS bexp_atom Bexp(b) == inl b THM bexp_atom_wf b:. Bexp(b) exp DISP andbexp_df AND == AND ABS andbexp b1 AND b2 == inr (inl ) THM andbexp_wf b1,b2:exp. b1 AND b2 exp DISP orbexp_df OR == OR ABS orbexp b1 OR b2 == inr inr (inl ) THM orbexp_wf b1,b2:exp. b1 OR b2 exp DISP notbexp_df NOT == NOT ABS notbexp NOT b == inr inr inr (inl b ) THM notbexp_wf b:exp. NOT b exp DISP ltexp_df < == < ABS ltexp e1 < e2 == inr inr inr inr (inl ) THM ltexp_wf e1,e2:Exp. e1 < e2 exp DISP eqexp_df == == == ABS eqexp e1 == e2 == inr inr inr inr inr THM eqexp_wf e1,e2:Exp. e1 == e2 exp DISP bexp_cases_df {[SOFT}{->0}case {\\}of {->0}Bexp() {\\} AND {\\} OR {\\}NOT {\\} < {\\} == {<-}{<-}{]} == case of Bexp() AND OR NOT < == 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 = aa in and_case[a1; a2] | inr(na) => case na of inl(oo) => let = oo in or_case[o1; o2] | inr(no) => case no of inl(n) => not_case[n] | inr(nn) => case nn of inl(ll) => let = ll in lt_case[l1; l2] | inr(ee) => let = 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 []()== []() 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]

the other theories