equal
deleted
inserted
replaced
112 fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", |
112 fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", |
113 CHANGED o Simplifier.asm_full_simp_tac ss)); |
113 CHANGED o Simplifier.asm_full_simp_tac ss)); |
114 fun cs addss' ss = Classical.addbefore (cs, ("asm_full_simp_tac", |
114 fun cs addss' ss = Classical.addbefore (cs, ("asm_full_simp_tac", |
115 CHANGED o Simplifier.asm_lr_simp_tac ss)); |
115 CHANGED o Simplifier.asm_lr_simp_tac ss)); |
116 |
116 |
117 (*Attach a suffix, provided we have a name to start with.*) |
|
118 fun suffix_thm "" _ = I |
|
119 | suffix_thm a b = PureThy.put_name_hint (a^b); |
|
120 |
|
121 (* iffs: addition of rules to simpsets and clasets simultaneously *) |
117 (* iffs: addition of rules to simpsets and clasets simultaneously *) |
122 |
118 |
123 (*Takes (possibly conditional) theorems of the form A<->B to |
119 (*Takes (possibly conditional) theorems of the form A<->B to |
124 the Safe Intr rule B==>A and |
120 the Safe Intr rule B==>A and |
125 the Safe Destruct rule A==>B. |
121 the Safe Destruct rule A==>B. |
132 val name = PureThy.get_name_hint th; |
128 val name = PureThy.get_name_hint th; |
133 val n = nprems_of th; |
129 val n = nprems_of th; |
134 val (elim, intro) = if n = 0 then decls1 else decls2; |
130 val (elim, intro) = if n = 0 then decls1 else decls2; |
135 val zero_rotate = zero_var_indexes o rotate_prems n; |
131 val zero_rotate = zero_var_indexes o rotate_prems n; |
136 in |
132 in |
137 (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS iffD2))]), |
133 (elim (intro (cs, [zero_rotate (th RS iffD2)]), |
138 [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS iffD1)))]) |
134 [Tactic.make_elim (zero_rotate (th RS iffD1))]) |
139 handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS notE))]) |
135 handle THM _ => (elim (cs, [zero_rotate (th RS notE)]) |
140 handle THM _ => intro (cs, [th])), |
136 handle THM _ => intro (cs, [th])), |
141 simp (ss, [th])) |
137 simp (ss, [th])) |
142 end; |
138 end; |
143 |
139 |
144 fun delIff delcs delss ((cs, ss), th) = |
140 fun delIff delcs delss ((cs, ss), th) = |