Adapted to modified interface of PureThy.get_thm(s).
authorberghofe
Mon Jan 24 17:59:48 2005 +0100 (2005-01-24 ago)
changeset 154571fbd4aba46e3
parent 15456 956d6acacf89
child 15458 9c292e3e0ca1
Adapted to modified interface of PureThy.get_thm(s).
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/domain/interface.ML
src/HOLCF/domain/theorems.ML
src/Pure/Proof/extraction.ML
src/Pure/Thy/thy_parse.ML
src/Pure/axclass.ML
src/Pure/goals.ML
src/Pure/proof_general.ML
     1.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jan 24 17:56:18 2005 +0100
     1.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jan 24 17:59:48 2005 +0100
     1.3 @@ -981,8 +981,8 @@
     1.4  	 val s =  post_last_dot(fst(qtn a));
     1.5  	 fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t)))))  = t |
     1.6  	 param_types _ = error "malformed induct-theorem in preprocess_td";	
     1.7 -	 val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct")));		
     1.8 -         val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct")));
     1.9 +	 val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct", None)));		
    1.10 +         val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct", None)));
    1.11  	 val ntl = new_types l;
    1.12          in 
    1.13          ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Jan 24 17:56:18 2005 +0100
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Jan 24 17:59:48 2005 +0100
     2.3 @@ -51,8 +51,8 @@
     2.4         induction : thm,
     2.5         size : thm list,
     2.6         simps : thm list}
     2.7 -  val rep_datatype : string list option -> (xstring * Args.src list) list list ->
     2.8 -    (xstring * Args.src list) list list -> xstring * Args.src list -> theory -> theory *
     2.9 +  val rep_datatype : string list option -> (thmref * Args.src list) list list ->
    2.10 +    (thmref * Args.src list) list list -> thmref * Args.src list -> theory -> theory *
    2.11        {distinct : thm list list,
    2.12         inject : thm list list,
    2.13         exhaustion : thm list,
    2.14 @@ -355,7 +355,7 @@
    2.15                                   val eq_ct = cterm_of sg eq_t;
    2.16                                   val Datatype_thy = theory "Datatype";
    2.17                                   val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
    2.18 -                                   map (get_thm Datatype_thy)
    2.19 +                                   map (get_thm Datatype_thy o rpair None)
    2.20                                       ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
    2.21                               in (case (#distinct (datatype_info_sg_err sg tname1)) of
    2.22                                   QuickAndDirty => Some (Thm.invoke_oracle
    2.23 @@ -583,21 +583,7 @@
    2.24          (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
    2.25            (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
    2.26  
    2.27 -    val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
    2.28 -      replicate (length descr') HOLogic.typeS);
    2.29 -
    2.30 -    val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
    2.31 -      map (fn (_, cargs) =>
    2.32 -        let
    2.33 -          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    2.34 -          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
    2.35 -
    2.36 -          fun mk_argT (dt, T) =
    2.37 -            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
    2.38 -
    2.39 -          val argTs = Ts @ map mk_argT recs
    2.40 -        in argTs ---> nth_elem (i, rec_result_Ts)
    2.41 -        end) constrs) descr');
    2.42 +    val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
    2.43  
    2.44      val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
    2.45      val reccomb_names = if length descr' = 1 then [big_reccomb_name] else
    2.46 @@ -674,7 +660,7 @@
    2.47        Theory.parent_path |>>>
    2.48        add_and_get_axiomss "inject" new_type_names
    2.49          (DatatypeProp.make_injs descr sorts);
    2.50 -    val size_thms = if no_size then [] else get_thms thy3 "size";
    2.51 +    val size_thms = if no_size then [] else get_thms thy3 ("size", None);
    2.52      val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
    2.53        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
    2.54  
     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jan 24 17:56:18 2005 +0100
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jan 24 17:59:48 2005 +0100
     3.3 @@ -57,7 +57,7 @@
     3.4  
     3.5      val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
     3.6           In0_eq, In1_eq, In0_not_In1, In1_not_In0,
     3.7 -         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy)
     3.8 +         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o rpair None)
     3.9          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
    3.10           "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
    3.11           "Lim_inject", "Suml_inject", "Sumr_inject"];
    3.12 @@ -261,9 +261,9 @@
    3.13      (* get axioms from theory *)
    3.14  
    3.15      val newT_iso_axms = map (fn s =>
    3.16 -      (get_thm thy4 ("Abs_" ^ s ^ "_inverse"),
    3.17 -       get_thm thy4 ("Rep_" ^ s ^ "_inverse"),
    3.18 -       get_thm thy4 ("Rep_" ^ s))) new_type_names;
    3.19 +      (get_thm thy4 ("Abs_" ^ s ^ "_inverse", None),
    3.20 +       get_thm thy4 ("Rep_" ^ s ^ "_inverse", None),
    3.21 +       get_thm thy4 ("Rep_" ^ s, None))) new_type_names;
    3.22  
    3.23      (*------------------------------------------------*)
    3.24      (* prove additional theorems:                     *)
     4.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Jan 24 17:56:18 2005 +0100
     4.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Jan 24 17:59:48 2005 +0100
     4.3 @@ -101,7 +101,7 @@
     4.4  fun prove_nonempty thy cset goal (witn1_tac, witn_names, witn_thms, witn2_tac) =
     4.5    let
     4.6      val is_def = Logic.is_equals o #prop o Thm.rep_thm;
     4.7 -    val thms = PureThy.get_thmss thy witn_names @ witn_thms;
     4.8 +    val thms = PureThy.get_thmss thy (map (rpair None) witn_names) @ witn_thms;
     4.9      val tac =
    4.10        witn1_tac THEN
    4.11        TRY (rewrite_goals_tac (filter is_def thms)) THEN
     5.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Jan 24 17:56:18 2005 +0100
     5.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Jan 24 17:59:48 2005 +0100
     5.3 @@ -98,7 +98,7 @@
     5.4  fun unqualify s = implode(rev(afpl(rev(explode s))));
     5.5  val q_atypstr = act_name thy atyp;
     5.6  val uq_atypstr = unqualify q_atypstr;
     5.7 -val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct"));
     5.8 +val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct", None));
     5.9  in
    5.10  extract_constrs thy prem
    5.11  handle malformed =>
    5.12 @@ -284,7 +284,7 @@
    5.13  let
    5.14  fun left_of (( _ $ left) $ _) = left |
    5.15  left_of _ = raise malformed;
    5.16 -val aut_def = concl_of(get_thm thy (aut_name ^ "_def"));
    5.17 +val aut_def = concl_of (get_thm thy (aut_name ^ "_def", None));
    5.18  in
    5.19  (#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def))))
    5.20  handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
     6.1 --- a/src/HOLCF/domain/interface.ML	Mon Jan 24 17:56:18 2005 +0100
     6.2 +++ b/src/HOLCF/domain/interface.ML	Mon Jan 24 17:59:48 2005 +0100
     6.3 @@ -12,10 +12,10 @@
     6.4  
     6.5  (* --- generation of bindings for axioms and theorems in .thy.ML - *)
     6.6  
     6.7 -  fun get      dname name   = "get_thm thy " ^ Library.quote (dname^"."^name);
     6.8 +  fun get      dname name   = "get_thm thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", None)";
     6.9    fun gen_vals dname name   = "val "^ name ^ " = get_thm" ^ 
    6.10  			(if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
    6.11 -			" thy " ^ Library.quote (dname^"."^name)^";";
    6.12 +			" thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", None);";
    6.13    fun gen_vall       name l = "val "^name^" = "^ mk_list l^";";
    6.14    val rews = "iso_rews @ when_rews @\n\
    6.15   	   \  con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\
     7.1 --- a/src/HOLCF/domain/theorems.ML	Mon Jan 24 17:56:18 2005 +0100
     7.2 +++ b/src/HOLCF/domain/theorems.ML	Mon Jan 24 17:59:48 2005 +0100
     7.3 @@ -65,7 +65,7 @@
     7.4  
     7.5  (* ----- getting the axioms and definitions --------------------------------- *)
     7.6  
     7.7 -local fun ga s dn = get_thm thy (dn^"."^s) in
     7.8 +local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in
     7.9  val ax_abs_iso    = ga "abs_iso"  dname;
    7.10  val ax_rep_iso    = ga "rep_iso"  dname;
    7.11  val ax_when_def   = ga "when_def" dname;
    7.12 @@ -341,7 +341,7 @@
    7.13  
    7.14  (* ----- getting the composite axiom and definitions ------------------------ *)
    7.15  
    7.16 -local fun ga s dn = get_thm thy (dn^"."^s) in
    7.17 +local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in
    7.18  val axs_reach      = map (ga "reach"     ) dnames;
    7.19  val axs_take_def   = map (ga "take_def"  ) dnames;
    7.20  val axs_finite_def = map (ga "finite_def") dnames;
    7.21 @@ -349,8 +349,8 @@
    7.22  val ax_bisim_def   =      ga "bisim_def" comp_dnam;
    7.23  end; (* local *)
    7.24  
    7.25 -local fun gt  s dn = get_thm  thy (dn^"."^s);
    7.26 -      fun gts s dn = get_thms thy (dn^"."^s) in
    7.27 +local fun gt  s dn = get_thm  thy (dn ^ "." ^ s, None);
    7.28 +      fun gts s dn = get_thms thy (dn ^ "." ^ s, None) in
    7.29  val cases     =       map (gt  "casedist" ) dnames;
    7.30  val con_rews  = flat (map (gts "con_rews" ) dnames);
    7.31  val copy_rews = flat (map (gts "copy_rews") dnames);
     8.1 --- a/src/Pure/Proof/extraction.ML	Mon Jan 24 17:56:18 2005 +0100
     8.2 +++ b/src/Pure/Proof/extraction.ML	Mon Jan 24 17:59:48 2005 +0100
     8.3 @@ -734,7 +734,7 @@
     8.4      (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
     8.5       (fn xs => Toplevel.theory (fn thy => add_realizers
     8.6         (map (fn (((a, vs), s1), s2) =>
     8.7 -         (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
     8.8 +         (PureThy.get_thm thy (a, None), (vs, s1, s2))) xs) thy)));
     8.9  
    8.10  val realizabilityP =
    8.11    OuterSyntax.command "realizability"
    8.12 @@ -749,7 +749,7 @@
    8.13  val extractP =
    8.14    OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
    8.15      (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
    8.16 -      (fn thy => extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
    8.17 +      (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair None)) xs) thy)));
    8.18  
    8.19  val parsers = [realizersP, realizabilityP, typeofP, extractP];
    8.20  
     9.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Jan 24 17:56:18 2005 +0100
     9.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Jan 24 17:59:48 2005 +0100
     9.3 @@ -523,7 +523,7 @@
     9.4  
     9.5  (* standard sections *)
     9.6  
     9.7 -fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ Library.quote ax ^ ";";
     9.8 +fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (" ^ Library.quote ax ^ ", None);";
     9.9  val mk_vals = cat_lines o map mk_val;
    9.10  
    9.11  fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs)
    10.1 --- a/src/Pure/axclass.ML	Mon Jan 24 17:56:18 2005 +0100
    10.2 +++ b/src/Pure/axclass.ML	Mon Jan 24 17:59:48 2005 +0100
    10.3 @@ -64,7 +64,7 @@
    10.4  val is_def = Logic.is_equals o #prop o rep_thm;
    10.5  
    10.6  fun witnesses thy names thms =
    10.7 -  PureThy.get_thmss thy names @ thms @ filter is_def (map snd (axioms_of thy));
    10.8 +  PureThy.get_thmss thy (map (rpair None) names) @ thms @ filter is_def (map snd (axioms_of thy));
    10.9  
   10.10  
   10.11  
    11.1 --- a/src/Pure/goals.ML	Mon Jan 24 17:56:18 2005 +0100
    11.2 +++ b/src/Pure/goals.ML	Mon Jan 24 17:59:48 2005 +0100
    11.3 @@ -330,7 +330,7 @@
    11.4  fun get_thmx f get thy name =
    11.5    (case get_first (get_thm_locale name) (get_scope thy) of
    11.6      Some thm => f thm
    11.7 -  | None => get thy name);
    11.8 +  | None => get thy (name, None));
    11.9  
   11.10  val get_thm = get_thmx I PureThy.get_thm;
   11.11  val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
    12.1 --- a/src/Pure/proof_general.ML	Mon Jan 24 17:56:18 2005 +0100
    12.2 +++ b/src/Pure/proof_general.ML	Mon Jan 24 17:59:48 2005 +0100
    12.3 @@ -685,7 +685,7 @@
    12.4  
    12.5  local
    12.6   val topthy = Toplevel.theory_of o Toplevel.get_state
    12.7 - val pthm = print_thm oo get_thm
    12.8 + fun pthm thy name = print_thm (get_thm thy (name, None))
    12.9  
   12.10   fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
   12.11  in