91 REPEAT(fast_tac HOL_cs 1) ]); |
91 REPEAT(fast_tac HOL_cs 1) ]); |
92 |
92 |
93 val if_bool_eq = prove_goal HOL.thy "if(P,Q,R) = ((P-->Q) & (~P-->R))" |
93 val if_bool_eq = prove_goal HOL.thy "if(P,Q,R) = ((P-->Q) & (~P-->R))" |
94 (fn _ => [rtac expand_if 1]); |
94 (fn _ => [rtac expand_if 1]); |
95 |
95 |
96 infix addcongs; |
96 (*Add congruence rules for = (instead of ==) *) |
|
97 infix 4 addcongs; |
97 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
98 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
|
99 |
|
100 (*Add a simpset to a classical set!*) |
|
101 infix 4 addss; |
|
102 fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; |
98 |
103 |
99 val mksimps_pairs = |
104 val mksimps_pairs = |
100 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
105 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
101 ("All", [spec]), ("True", []), ("False", []), |
106 ("All", [spec]), ("True", []), ("False", []), |
102 ("if", [if_bool_eq RS iffD1])]; |
107 ("if", [if_bool_eq RS iffD1])]; |