Drule.read_instantiate;
authorwenzelm
Wed Jun 11 18:02:00 2008 +0200 (2008-06-11)
changeset 2715356b6cdce22f1
parent 27152 192954a9a549
child 27154 026f3db3f5c6
Drule.read_instantiate;
src/HOL/Bali/Basis.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Prolog/prolog.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOLCF/Tools/domain/domain_library.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/HOL/Bali/Basis.thy	Wed Jun 11 18:01:36 2008 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Wed Jun 11 18:02:00 2008 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4  
     1.5  ML {*
     1.6  fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[@{thm not_None_eq}])
     1.7 - (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
     1.8 + (Drule.read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
     1.9  *}
    1.10  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
    1.11  
     2.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jun 11 18:01:36 2008 +0200
     2.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jun 11 18:02:00 2008 +0200
     2.3 @@ -51,7 +51,7 @@
     2.4  val deriv_tac =
     2.5    SUBGOAL (fn (prem,i) =>
     2.6     (resolve_tac @{thms deriv_rulesI} i) ORELSE
     2.7 -    ((rtac (read_instantiate [("f",get_fun_name prem)]
     2.8 +    ((rtac (Drule.read_instantiate [("f",get_fun_name prem)]
     2.9                       @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));;
    2.10  
    2.11  val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
     3.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 11 18:01:36 2008 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 11 18:02:00 2008 +0200
     3.3 @@ -48,7 +48,7 @@
     3.4           then SOME perm_bool else NONE
     3.5       | _ => NONE);
     3.6  
     3.7 -val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE;
     3.8 +val allE_Nil = Drule.read_instantiate_sg (the_context()) [("x", "[]")] allE;
     3.9  
    3.10  fun transp ([] :: _) = []
    3.11    | transp xs = map hd xs :: transp (map tl xs);
     4.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Jun 11 18:01:36 2008 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Jun 11 18:02:00 2008 +0200
     4.3 @@ -155,7 +155,7 @@
     4.4  val perm_simproc =
     4.5    Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
     4.6  
     4.7 -val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE;
     4.8 +val allE_Nil = Drule.read_instantiate_sg (the_context()) [("x", "[]")] allE;
     4.9  
    4.10  val meta_spec = thm "meta_spec";
    4.11  
     5.1 --- a/src/HOL/Prolog/prolog.ML	Wed Jun 11 18:01:36 2008 +0200
     5.2 +++ b/src/HOL/Prolog/prolog.ML	Wed Jun 11 18:02:00 2008 +0200
     5.3 @@ -52,7 +52,7 @@
     5.4  
     5.5  fun atomizeD thm = let
     5.6      fun at  thm = case concl_of thm of
     5.7 -      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
     5.8 +      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (Drule.read_instantiate [("x",
     5.9                                          "?"^(if s="P" then "PP" else s))] spec))
    5.10      | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    5.11      | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
     6.1 --- a/src/HOL/Tools/TFL/post.ML	Wed Jun 11 18:01:36 2008 +0200
     6.2 +++ b/src/HOL/Tools/TFL/post.ML	Wed Jun 11 18:02:00 2008 +0200
     6.3 @@ -152,7 +152,7 @@
     6.4    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
     6.5  
     6.6  (*Strip off the outer !P*)
     6.7 -val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
     6.8 +val spec'= Drule.read_instantiate [("x","P::?'b=>bool")] spec;
     6.9  
    6.10  fun tracing true _ = ()
    6.11    | tracing false msg = writeln msg;
     7.1 --- a/src/HOL/Tools/meson.ML	Wed Jun 11 18:01:36 2008 +0200
     7.2 +++ b/src/HOL/Tools/meson.ML	Wed Jun 11 18:02:00 2008 +0200
     7.3 @@ -646,7 +646,7 @@
     7.4  (*Rules to convert the head literal into a negated assumption. If the head
     7.5    literal is already negated, then using notEfalse instead of notEfalse'
     7.6    prevents a double negation.*)
     7.7 -val notEfalse = read_instantiate [("R","False")] notE;
     7.8 +val notEfalse = Drule.read_instantiate [("R","False")] notE;
     7.9  val notEfalse' = rotate_prems 1 notEfalse;
    7.10  
    7.11  fun negated_asm_of_head th =
     8.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Jun 11 18:01:36 2008 +0200
     8.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Jun 11 18:02:00 2008 +0200
     8.3 @@ -24,10 +24,10 @@
     8.4    (* ------------------------------------------------------------------------- *)
     8.5    (* Useful Theorems                                                           *)
     8.6    (* ------------------------------------------------------------------------- *)
     8.7 -  val EXCLUDED_MIDDLE  = rotate_prems 1 (read_instantiate [("R","False")] notE);
     8.8 +  val EXCLUDED_MIDDLE  = rotate_prems 1 (Drule.read_instantiate [("R","False")] notE);
     8.9    val REFL_THM         = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
    8.10    val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
    8.11 -  val ssubst_em  = read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em);
    8.12 +  val ssubst_em  = Drule.read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em);
    8.13  
    8.14    (* ------------------------------------------------------------------------- *)
    8.15    (* Useful Functions                                                          *)
     9.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Wed Jun 11 18:01:36 2008 +0200
     9.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Wed Jun 11 18:02:00 2008 +0200
     9.3 @@ -24,7 +24,7 @@
     9.4  fun upd_second f (x,y,z) = (  x, f y,   z);
     9.5  fun upd_third  f (x,y,z) = (  x,   y, f z);
     9.6  
     9.7 -fun atomize thm = let val r_inst = read_instantiate;
     9.8 +fun atomize thm = let val r_inst = Drule.read_instantiate;
     9.9      fun at  thm = case concl_of thm of
    9.10        _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    9.11      | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec))
    10.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Jun 11 18:01:36 2008 +0200
    10.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Jun 11 18:02:00 2008 +0200
    10.3 @@ -884,7 +884,7 @@
    10.4      else (* infinite case *)
    10.5        let
    10.6          fun one_finite n dn =
    10.7 -          read_instantiate_sg thy
    10.8 +          Drule.read_instantiate_sg thy
    10.9              [("P",dn^"_finite "^x_name n)] excluded_middle;
   10.10          val finites = mapn one_finite 1 dnames;
   10.11  
    11.1 --- a/src/ZF/ind_syntax.ML	Wed Jun 11 18:01:36 2008 +0200
    11.2 +++ b/src/ZF/ind_syntax.ML	Wed Jun 11 18:02:00 2008 +0200
    11.3 @@ -51,7 +51,7 @@
    11.4  (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
    11.5    read_instantiate replaces a propositional variable by a formula variable*)
    11.6  val equals_CollectD =
    11.7 -    read_instantiate [("W","?Q")]
    11.8 +    Drule.read_instantiate [("W","?Q")]
    11.9          (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
   11.10  
   11.11