equal
deleted
inserted
replaced
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.*) |
117 (*Attach a suffix, provided we have a name to start with.*) |
118 fun suffix_thm "" _ th = th |
118 fun suffix_thm "" _ = I |
119 | suffix_thm a b th = Thm.name_thm (a^b, th); |
119 | suffix_thm a b = PureThy.put_name_hint (a^b); |
120 |
120 |
121 (* iffs: addition of rules to simpsets and clasets simultaneously *) |
121 (* iffs: addition of rules to simpsets and clasets simultaneously *) |
122 |
122 |
123 (*Takes (possibly conditional) theorems of the form A<->B to |
123 (*Takes (possibly conditional) theorems of the form A<->B to |
124 the Safe Intr rule B==>A and |
124 the Safe Intr rule B==>A and |
127 Failing other cases, A is added as a Safe Intr rule*) |
127 Failing other cases, A is added as a Safe Intr rule*) |
128 local |
128 local |
129 |
129 |
130 fun addIff decls1 decls2 simp ((cs, ss), th) = |
130 fun addIff decls1 decls2 simp ((cs, ss), th) = |
131 let |
131 let |
132 val name = Thm.name_of_thm th; |
132 val name = PureThy.get_name_hint th; |
133 val n = nprems_of th; |
133 val n = nprems_of th; |
134 val (elim, intro) = if n = 0 then decls1 else decls2; |
134 val (elim, intro) = if n = 0 then decls1 else decls2; |
135 val zero_rotate = zero_var_indexes o rotate_prems n; |
135 val zero_rotate = zero_var_indexes o rotate_prems n; |
136 in |
136 in |
137 (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS iffD2))]), |
137 (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS iffD2))]), |