more antiquotations;
authorwenzelm
Wed Mar 19 22:47:38 2008 +0100 (2008-03-19 ago)
changeset 26340a85fe32e7b2f
parent 26339 7825c83c9eff
child 26341 2f5a4367a39e
more antiquotations;
eliminated change_claset/simpset;
src/HOL/Product_Type.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Product_Type.thy	Wed Mar 19 22:47:35 2008 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Mar 19 22:47:38 2008 +0100
     1.3 @@ -322,7 +322,7 @@
     1.4    ?P(a, b)"} which cannot be solved by reflexivity.
     1.5  *}
     1.6  
     1.7 -ML_setup {*
     1.8 +ML {*
     1.9    (* replace parameters of product type by individual component parameters *)
    1.10    val safe_full_simp_tac = generic_simp_tac true (true, false, false);
    1.11    local (* filtering with exists_paired_all is an essential optimization *)
    1.12 @@ -332,7 +332,7 @@
    1.13        | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
    1.14        | exists_paired_all _ = false;
    1.15      val ss = HOL_basic_ss
    1.16 -      addsimps [thm "split_paired_all", thm "unit_all_eq2", thm "unit_abs_eta_conv"]
    1.17 +      addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}]
    1.18        addsimprocs [unit_eq_proc];
    1.19    in
    1.20      val split_all_tac = SUBGOAL (fn (t, i) =>
    1.21 @@ -340,10 +340,12 @@
    1.22      val unsafe_split_all_tac = SUBGOAL (fn (t, i) =>
    1.23        if exists_paired_all t then full_simp_tac ss i else no_tac);
    1.24      fun split_all th =
    1.25 -   if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
    1.26 +   if exists_paired_all (Thm.prop_of th) then full_simplify ss th else th;
    1.27    end;
    1.28 +*}
    1.29  
    1.30 -change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
    1.31 +declaration {* fn _ =>
    1.32 +  Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))
    1.33  *}
    1.34  
    1.35  lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))"
    1.36 @@ -541,7 +543,7 @@
    1.37  declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
    1.38  declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
    1.39  
    1.40 -ML_setup {*
    1.41 +ML {*
    1.42  local (* filtering with exists_p_split is an essential optimization *)
    1.43    fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true
    1.44      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
    1.45 @@ -552,9 +554,12 @@
    1.46  val split_conv_tac = SUBGOAL (fn (t, i) =>
    1.47      if exists_p_split t then safe_full_simp_tac ss i else no_tac);
    1.48  end;
    1.49 +*}
    1.50 +
    1.51  (* This prevents applications of splitE for already splitted arguments leading
    1.52     to quite time-consuming computations (in particular for nested tuples) *)
    1.53 -change_claset (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac));
    1.54 +declaration {* fn _ =>
    1.55 +  Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
    1.56  *}
    1.57  
    1.58  lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
     2.1 --- a/src/HOL/Transitive_Closure.thy	Wed Mar 19 22:47:35 2008 +0100
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Mar 19 22:47:38 2008 +0100
     2.3 @@ -618,18 +618,18 @@
     2.4  
     2.5  subsection {* Setup of transitivity reasoner *}
     2.6  
     2.7 -ML_setup {*
     2.8 +ML {*
     2.9  
    2.10  structure Trancl_Tac = Trancl_Tac_Fun (
    2.11    struct
    2.12 -    val r_into_trancl = thm "trancl.r_into_trancl";
    2.13 -    val trancl_trans  = thm "trancl_trans";
    2.14 -    val rtrancl_refl = thm "rtrancl.rtrancl_refl";
    2.15 -    val r_into_rtrancl = thm "r_into_rtrancl";
    2.16 -    val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    2.17 -    val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
    2.18 -    val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
    2.19 -    val rtrancl_trans = thm "rtrancl_trans";
    2.20 +    val r_into_trancl = @{thm trancl.r_into_trancl};
    2.21 +    val trancl_trans  = @{thm trancl_trans};
    2.22 +    val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
    2.23 +    val r_into_rtrancl = @{thm r_into_rtrancl};
    2.24 +    val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
    2.25 +    val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
    2.26 +    val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
    2.27 +    val rtrancl_trans = @{thm rtrancl_trans};
    2.28  
    2.29    fun decomp (Trueprop $ t) =
    2.30      let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
    2.31 @@ -645,14 +645,14 @@
    2.32  
    2.33  structure Tranclp_Tac = Trancl_Tac_Fun (
    2.34    struct
    2.35 -    val r_into_trancl = thm "tranclp.r_into_trancl";
    2.36 -    val trancl_trans  = thm "tranclp_trans";
    2.37 -    val rtrancl_refl = thm "rtranclp.rtrancl_refl";
    2.38 -    val r_into_rtrancl = thm "r_into_rtranclp";
    2.39 -    val trancl_into_rtrancl = thm "tranclp_into_rtranclp";
    2.40 -    val rtrancl_trancl_trancl = thm "rtranclp_tranclp_tranclp";
    2.41 -    val trancl_rtrancl_trancl = thm "tranclp_rtranclp_tranclp";
    2.42 -    val rtrancl_trans = thm "rtranclp_trans";
    2.43 +    val r_into_trancl = @{thm tranclp.r_into_trancl};
    2.44 +    val trancl_trans  = @{thm tranclp_trans};
    2.45 +    val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
    2.46 +    val r_into_rtrancl = @{thm r_into_rtranclp};
    2.47 +    val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
    2.48 +    val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
    2.49 +    val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
    2.50 +    val rtrancl_trans = @{thm rtranclp_trans};
    2.51  
    2.52    fun decomp (Trueprop $ t) =
    2.53      let fun dec (rel $ a $ b) =
    2.54 @@ -665,13 +665,14 @@
    2.55      in dec t end;
    2.56  
    2.57    end);
    2.58 +*}
    2.59  
    2.60 -change_simpset (fn ss => ss
    2.61 -  addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    2.62 -  addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
    2.63 -  addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
    2.64 -  addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)));
    2.65 -
    2.66 +declaration {* fn _ =>
    2.67 +  Simplifier.map_ss (fn ss => ss
    2.68 +    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    2.69 +    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
    2.70 +    addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
    2.71 +    addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)))
    2.72  *}
    2.73  
    2.74  (* Optional methods *)