src/Provers/clasimp.ML
changeset 21709 9cfd9eb9faec
parent 21646 c07b5b0e8492
child 21963 416a5338d2bb
equal deleted inserted replaced
21708:45e7491bea47 21709:9cfd9eb9faec
   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) =