68 (fn [prem] => [rewtac prem, rtac refl 1]); |
68 (fn [prem] => [rewtac prem, rtac refl 1]); |
69 |
69 |
70 val eq_sym_conv = prover "(x=y) = (y=x)"; |
70 val eq_sym_conv = prover "(x=y) = (y=x)"; |
71 |
71 |
72 val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))"; |
72 val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))"; |
73 val conj_commute = prover "(P&Q) = (Q&P)"; |
|
74 val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))"; |
|
75 val conj_comms = [conj_commute, conj_left_commute]; |
|
76 |
73 |
77 val if_True = prove_goalw HOL.thy [if_def] "if(True,x,y) = x" |
74 val if_True = prove_goalw HOL.thy [if_def] "if(True,x,y) = x" |
78 (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]); |
75 (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]); |
79 |
76 |
80 val if_False = prove_goalw HOL.thy [if_def] "if(False,x,y) = y" |
77 val if_False = prove_goalw HOL.thy [if_def] "if(False,x,y) = y" |
91 (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1), |
88 (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1), |
92 rtac (if_P RS ssubst) 2, |
89 rtac (if_P RS ssubst) 2, |
93 rtac (if_not_P RS ssubst) 1, |
90 rtac (if_not_P RS ssubst) 1, |
94 REPEAT(fast_tac HOL_cs 1) ]); |
91 REPEAT(fast_tac HOL_cs 1) ]); |
95 |
92 |
|
93 val if_bool_eq = prove_goal HOL.thy "if(P,Q,R) = ((P-->Q) & (~P-->R))" |
|
94 (fn _ => [rtac expand_if 1]); |
|
95 |
96 infix addcongs; |
96 infix addcongs; |
97 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
97 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
98 |
98 |
99 val mksimps_pairs = |
99 val mksimps_pairs = |
100 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
100 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
101 ("All", [spec]), ("True", []), ("False", [])]; |
101 ("All", [spec]), ("True", []), ("False", []), |
|
102 ("if", [if_bool_eq RS iffD1])]; |
102 |
103 |
103 fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all; |
104 fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all; |
104 |
105 |
105 val HOL_ss = empty_ss |
106 val HOL_ss = empty_ss |
106 setmksimps (mksimps mksimps_pairs) |
107 setmksimps (mksimps mksimps_pairs) |
149 val let_weak_cong = prove_goal HOL.thy |
150 val let_weak_cong = prove_goal HOL.thy |
150 "a = b ==> (let x=a in t(x)) = (let x=b in t(x))" |
151 "a = b ==> (let x=a in t(x)) = (let x=b in t(x))" |
151 (fn [prem] => [rtac (prem RS arg_cong) 1]); |
152 (fn [prem] => [rtac (prem RS arg_cong) 1]); |
152 |
153 |
153 end; |
154 end; |
|
155 |
|
156 fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]); |
|
157 |
|
158 prove "conj_commute" "(P&Q) = (Q&P)"; |
|
159 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
|
160 val conj_comms = [conj_commute, conj_left_commute]; |
|
161 |
|
162 prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; |
|
163 prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; |