119 Also ~A goes to the Safe Elim rule A ==> ?R |
119 Also ~A goes to the Safe Elim rule A ==> ?R |
120 Failing other cases, A is added as a Safe Intr rule*) |
120 Failing other cases, A is added as a Safe Intr rule*) |
121 local |
121 local |
122 |
122 |
123 fun addIff dest elim intro simp ((cs, ss), th) = |
123 fun addIff dest elim intro simp ((cs, ss), th) = |
124 ( dest (intro (cs, [zero_var_indexes (th RS Data.iffD2)]), |
124 let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in |
125 [zero_var_indexes (rotate_prems (nprems_of th) |
125 (dest (intro (cs, [zero_rotate (th RS Data.iffD2)]), [zero_rotate (th RS Data.iffD1)]) |
126 (th RS Data.iffD1))]) |
126 handle THM _ => (elim (cs, [zero_rotate (th RS Data.notE)]) |
127 handle THM _ => (elim (cs, [zero_var_indexes (th RS Data.notE )]) |
127 handle THM _ => intro (cs, [th])), |
128 handle THM _ => intro (cs, [th])), |
128 simp (ss, [th])) |
129 simp (ss, [th])); |
129 end; |
130 |
130 |
131 fun delIff ((cs, ss), th) = |
131 fun delIff ((cs, ss), th) = |
132 ( Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2), |
132 let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in |
133 Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))]) |
133 (Classical.delrules (cs, [zero_rotate (th RS Data.iffD2), |
134 handle THM _ => (Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)]) |
134 Data.cla_make_elim (zero_rotate (th RS Data.iffD1))]) |
135 handle THM _ => Classical.delrules (cs, [th])), |
135 handle THM _ => (Classical.delrules (cs, [zero_rotate (th RS Data.notE)]) |
136 Simplifier.delsimps (ss, [th])); |
136 handle THM _ => Classical.delrules (cs, [th])), |
|
137 Simplifier.delsimps (ss, [th])) |
|
138 end; |
137 |
139 |
138 fun store_clasimp (cs, ss) = |
140 fun store_clasimp (cs, ss) = |
139 (Classical.claset_ref () := cs; Simplifier.simpset_ref () := ss); |
141 (Classical.claset_ref () := cs; Simplifier.simpset_ref () := ss); |
140 |
142 |
141 in |
143 in |