get_thm(s): Name;
authorwenzelm
Mon Jun 20 22:13:59 2005 +0200 (2005-06-20)
changeset 164861a12cdb6ee6b
parent 16485 77ae3bfa8b76
child 16487 2060ebae96f9
get_thm(s): Name;
src/HOL/Algebra/ringsimp.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Library/word_setup.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.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/Isar/find_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/Algebra/ringsimp.ML	Mon Jun 20 22:13:58 2005 +0200
     1.2 +++ b/src/HOL/Algebra/ringsimp.ML	Mon Jun 20 22:13:59 2005 +0200
     1.3 @@ -82,9 +82,9 @@
     1.4        ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
     1.5         "\nCommutative rings in proof context: " ^ commas comm_rings);
     1.6      val simps =
     1.7 -      List.concat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules", NONE))
     1.8 +      List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".ring_simprules")))
     1.9          non_comm_rings) @
    1.10 -      List.concat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules", NONE))
    1.11 +      List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".cring_simprules")))
    1.12          comm_rings);
    1.13    in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
    1.14    end;
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Jun 20 22:13:58 2005 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Jun 20 22:13:59 2005 +0200
     2.3 @@ -401,7 +401,7 @@
     2.4  fun dom_rng (Type("fun",[dom,rng])) = (dom,rng)
     2.5    | dom_rng _ = raise ERR "dom_rng" "Not a functional type"
     2.6  
     2.7 -fun mk_thy_const thy Thy Name Ty = Const(intern_const_name Thy Name thy,Ty)
     2.8 +fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
     2.9  
    2.10  local
    2.11      fun get_type sg thyname name =
    2.12 @@ -409,12 +409,12 @@
    2.13  	    SOME ty => ty
    2.14  	  | NONE => raise ERR "get_type" (name ^ ": No such constant")
    2.15  in
    2.16 -fun prim_mk_const thy Thy Name =
    2.17 +fun prim_mk_const thy Thy Nam =
    2.18      let
    2.19 -	val name = intern_const_name Thy Name thy
    2.20 +	val name = intern_const_name Thy Nam thy
    2.21  	val cmaps = HOL4ConstMaps.get thy
    2.22      in
    2.23 -	case StringPair.lookup(cmaps,(Thy,Name)) of
    2.24 +	case StringPair.lookup(cmaps,(Thy,Nam)) of
    2.25  	    SOME(_,_,SOME ty) => Const(name,ty)
    2.26  	  | _ => Const(name,get_type (sign_of thy) Thy name)
    2.27      end
    2.28 @@ -1236,10 +1236,10 @@
    2.29  	    SOME (SOME thmname) =>
    2.30  	    let
    2.31  		val _ = message ("Looking for " ^ thmname)
    2.32 -		val th1 = (SOME (transform_error (PureThy.get_thm thy) (thmname, NONE))
    2.33 +		val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
    2.34  			   handle ERROR_MESSAGE _ =>
    2.35  				  (case split_name thmname of
    2.36 -				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (listname, NONE),idx-1))
    2.37 +				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx-1))
    2.38  							       handle _ => NONE)
    2.39  				     | NONE => NONE))
    2.40  	    in
     3.1 --- a/src/HOL/Library/word_setup.ML	Mon Jun 20 22:13:58 2005 +0200
     3.2 +++ b/src/HOL/Library/word_setup.ML	Mon Jun 20 22:13:59 2005 +0200
     3.3 @@ -24,7 +24,7 @@
     3.4      fun add_word thy =
     3.5  	let
     3.6   (*lcp**	    val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
     3.7 -	    val fast2_th = PureThy.get_thm thy ("Word.fast_bv_to_nat_def", NONE)
     3.8 +	    val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
     3.9   (*lcp**	    fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
    3.10  		if num_is_usable t
    3.11  		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
     4.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 20 22:13:58 2005 +0200
     4.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 20 22:13:59 2005 +0200
     4.3 @@ -984,8 +984,8 @@
     4.4  	 val s =  post_last_dot(fst(qtn a));
     4.5  	 fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t)))))  = t |
     4.6  	 param_types _ = error "malformed induct-theorem in preprocess_td";	
     4.7 -	 val pl = param_types (concl_of (get_thm sg (s ^ ".induct", NONE)));		
     4.8 -         val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (s ^ ".induct", NONE)));
     4.9 +	 val pl = param_types (concl_of (get_thm sg (Name (s ^ ".induct"))));		
    4.10 +         val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (Name (s ^ ".induct"))));
    4.11  	 val ntl = new_types l;
    4.12          in 
    4.13          ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
     5.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Jun 20 22:13:58 2005 +0200
     5.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Jun 20 22:13:59 2005 +0200
     5.3 @@ -339,7 +339,7 @@
     5.4                                   val eq_ct = cterm_of sg eq_t;
     5.5                                   val Datatype_thy = theory "Datatype";
     5.6                                   val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
     5.7 -                                   map (get_thm Datatype_thy o rpair NONE)
     5.8 +                                   map (get_thm Datatype_thy o Name)
     5.9                                       ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
    5.10                               in (case (#distinct (datatype_info_err sg tname1)) of
    5.11                                   QuickAndDirty => SOME (Thm.invoke_oracle
    5.12 @@ -644,7 +644,7 @@
    5.13        Theory.parent_path |>>>
    5.14        add_and_get_axiomss "inject" new_type_names
    5.15          (DatatypeProp.make_injs descr sorts);
    5.16 -    val size_thms = if no_size then [] else get_thms thy3 ("size", NONE);
    5.17 +    val size_thms = if no_size then [] else get_thms thy3 (Name "size");
    5.18      val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
    5.19        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
    5.20  
     6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jun 20 22:13:58 2005 +0200
     6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jun 20 22:13:59 2005 +0200
     6.3 @@ -57,7 +57,7 @@
     6.4  
     6.5      val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
     6.6           In0_eq, In1_eq, In0_not_In1, In1_not_In0,
     6.7 -         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o rpair NONE)
     6.8 +         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o Name)
     6.9          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
    6.10           "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
    6.11           "Lim_inject", "Suml_inject", "Sumr_inject"];
    6.12 @@ -261,9 +261,9 @@
    6.13      (* get axioms from theory *)
    6.14  
    6.15      val newT_iso_axms = map (fn s =>
    6.16 -      (get_thm thy4 ("Abs_" ^ s ^ "_inverse", NONE),
    6.17 -       get_thm thy4 ("Rep_" ^ s ^ "_inverse", NONE),
    6.18 -       get_thm thy4 ("Rep_" ^ s, NONE))) new_type_names;
    6.19 +      (get_thm thy4 (Name ("Abs_" ^ s ^ "_inverse")),
    6.20 +       get_thm thy4 (Name ("Rep_" ^ s ^ "_inverse")),
    6.21 +       get_thm thy4 (Name ("Rep_" ^ s)))) new_type_names;
    6.22  
    6.23      (*------------------------------------------------*)
    6.24      (* prove additional theorems:                     *)
     7.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Jun 20 22:13:58 2005 +0200
     7.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Jun 20 22:13:59 2005 +0200
     7.3 @@ -614,11 +614,11 @@
     7.4  
     7.5      val sum_case_rewrites =
     7.6        (if Context.theory_name thy = "Datatype" then
     7.7 -        PureThy.get_thms thy ("sum.cases", NONE)
     7.8 +        PureThy.get_thms thy (Name "sum.cases")
     7.9        else
    7.10          (case ThyInfo.lookup_theory "Datatype" of
    7.11            NONE => []
    7.12 -        | SOME thy' => PureThy.get_thms thy' ("sum.cases", NONE)))
    7.13 +        | SOME thy' => PureThy.get_thms thy' (Name "sum.cases")))
    7.14        |> map mk_meta_eq;
    7.15  
    7.16      val (preds, ind_prems, mutual_ind_concl, factors) =
     8.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Jun 20 22:13:58 2005 +0200
     8.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Jun 20 22:13:59 2005 +0200
     8.3 @@ -97,7 +97,7 @@
     8.4  fun prove_nonempty thy cset goal (witn1_tac, witn_names, witn_thms, witn2_tac) =
     8.5    let
     8.6      val is_def = Logic.is_equals o #prop o Thm.rep_thm;
     8.7 -    val thms = PureThy.get_thmss thy (map (rpair NONE) witn_names) @ witn_thms;
     8.8 +    val thms = PureThy.get_thmss thy (map Name witn_names) @ witn_thms;
     8.9      val tac =
    8.10        witn1_tac THEN
    8.11        TRY (rewrite_goals_tac (List.filter is_def thms)) THEN
     9.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Jun 20 22:13:58 2005 +0200
     9.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Jun 20 22:13:59 2005 +0200
     9.3 @@ -98,7 +98,7 @@
     9.4  fun unqualify s = implode(rev(afpl(rev(explode s))));
     9.5  val q_atypstr = act_name thy atyp;
     9.6  val uq_atypstr = unqualify q_atypstr;
     9.7 -val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct", NONE));
     9.8 +val prem = prems_of (get_thm thy (Name (uq_atypstr ^ ".induct")));
     9.9  in
    9.10  extract_constrs thy prem
    9.11  handle malformed =>
    9.12 @@ -284,7 +284,7 @@
    9.13  let
    9.14  fun left_of (( _ $ left) $ _) = left |
    9.15  left_of _ = raise malformed;
    9.16 -val aut_def = concl_of (get_thm thy (aut_name ^ "_def", NONE));
    9.17 +val aut_def = concl_of (get_thm thy (Name (aut_name ^ "_def")));
    9.18  in
    9.19  (#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def))))
    9.20  handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
    10.1 --- a/src/HOLCF/domain/interface.ML	Mon Jun 20 22:13:58 2005 +0200
    10.2 +++ b/src/HOLCF/domain/interface.ML	Mon Jun 20 22:13:59 2005 +0200
    10.3 @@ -12,10 +12,10 @@
    10.4  
    10.5  (* --- generation of bindings for axioms and theorems in .thy.ML - *)
    10.6  
    10.7 -  fun get      dname name   = "get_thm thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", NONE)";
    10.8 +  fun get      dname name   = "get_thm thy (PureThy.Name " ^ Library.quote (dname ^ "." ^ name) ^ ")";
    10.9    fun gen_vals dname name   = "val "^ name ^ " = get_thm" ^ 
   10.10  			(if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
   10.11 -			" thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", NONE);";
   10.12 +			" thy (PureThy.Name " ^ Library.quote (dname ^ "." ^ name) ^ ");";
   10.13    fun gen_vall       name l = "val "^name^" = "^ mk_list l^";";
   10.14    val rews = "iso_rews @ when_rews @\n\
   10.15   	   \  con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\
    11.1 --- a/src/HOLCF/domain/theorems.ML	Mon Jun 20 22:13:58 2005 +0200
    11.2 +++ b/src/HOLCF/domain/theorems.ML	Mon Jun 20 22:13:59 2005 +0200
    11.3 @@ -63,7 +63,7 @@
    11.4  
    11.5  (* ----- getting the axioms and definitions --------------------------------- *)
    11.6  
    11.7 -local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
    11.8 +local fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)) in
    11.9  val ax_abs_iso    = ga "abs_iso"  dname;
   11.10  val ax_rep_iso    = ga "rep_iso"  dname;
   11.11  val ax_when_def   = ga "when_def" dname;
   11.12 @@ -352,7 +352,7 @@
   11.13  
   11.14  (* ----- getting the composite axiom and definitions ------------------------ *)
   11.15  
   11.16 -local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
   11.17 +local fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)) in
   11.18  val axs_reach      = map (ga "reach"     ) dnames;
   11.19  val axs_take_def   = map (ga "take_def"  ) dnames;
   11.20  val axs_finite_def = map (ga "finite_def") dnames;
   11.21 @@ -360,8 +360,8 @@
   11.22  val ax_bisim_def   =      ga "bisim_def" comp_dnam;
   11.23  end; (* local *)
   11.24  
   11.25 -local fun gt  s dn = get_thm  thy (dn ^ "." ^ s, NONE);
   11.26 -      fun gts s dn = get_thms thy (dn ^ "." ^ s, NONE) in
   11.27 +local fun gt  s dn = get_thm  thy (Name (dn ^ "." ^ s));
   11.28 +      fun gts s dn = get_thms thy (Name (dn ^ "." ^ s)) in
   11.29  val cases     =       map (gt  "casedist" ) dnames;
   11.30  val con_rews  = List.concat (map (gts "con_rews" ) dnames);
   11.31  val copy_rews = List.concat (map (gts "copy_rews") dnames);
    12.1 --- a/src/Pure/Isar/find_theorems.ML	Mon Jun 20 22:13:58 2005 +0200
    12.2 +++ b/src/Pure/Isar/find_theorems.ML	Mon Jun 20 22:13:59 2005 +0200
    12.3 @@ -38,7 +38,7 @@
    12.4    | read_criterion _ Intro = Intro
    12.5    | read_criterion _ Elim = Elim
    12.6    | read_criterion _ Dest = Dest
    12.7 -  | read_criterion ctxt (Simp str) = 
    12.8 +  | read_criterion ctxt (Simp str) =
    12.9        Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]))
   12.10    | read_criterion ctxt (Pattern str) =
   12.11        Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
   12.12 @@ -70,15 +70,15 @@
   12.13      val sg = ProofContext.sign_of ctxt;
   12.14      val tsig = Sign.tsig_of sg;
   12.15  
   12.16 -    val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg;    
   12.17 +    val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg;
   12.18  
   12.19 -    fun matches pat = 
   12.20 -      is_nontrivial pat andalso 
   12.21 +    fun matches pat =
   12.22 +      is_nontrivial pat andalso
   12.23        Pattern.matches tsig (if po then (pat,obj) else (obj,pat))
   12.24        handle Pattern.MATCH => false;
   12.25  
   12.26      val match_thm = matches o extract_term o Thm.prop_of
   12.27 -  in       
   12.28 +  in
   12.29      List.exists match_thm (extract_thms thm)
   12.30    end;
   12.31  
   12.32 @@ -93,7 +93,7 @@
   12.33  
   12.34  (*filter that just looks for a string in the name,
   12.35    substring match only (no regexps are performed)*)
   12.36 -fun filter_name str_pat ((name, _), _) = is_substring str_pat name;
   12.37 +fun filter_name str_pat (thmref, _) = is_substring str_pat (PureThy.name_of_thmref thmref);
   12.38  
   12.39  
   12.40  (* filter intro/elim/dest rules *)
   12.41 @@ -121,8 +121,8 @@
   12.42        hd o Logic.strip_imp_prems);
   12.43      val prems = Logic.prems_of_goal goal 1;
   12.44    in
   12.45 -    prems |> 
   12.46 -    List.exists (fn prem => 
   12.47 +    prems |>
   12.48 +    List.exists (fn prem =>
   12.49        is_matching_thm extract_elim ctxt true prem thm
   12.50        andalso (check_thm ctxt) thm)
   12.51    end;
    13.1 --- a/src/Pure/Proof/extraction.ML	Mon Jun 20 22:13:58 2005 +0200
    13.2 +++ b/src/Pure/Proof/extraction.ML	Mon Jun 20 22:13:59 2005 +0200
    13.3 @@ -115,7 +115,7 @@
    13.4              Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems')
    13.5          in SOME (Envir.norm_term env'' (inc (ren tm2)))
    13.6          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
    13.7 -          (sort (Int.compare o pairself fst)
    13.8 +          (sort (int_ord o pairself fst)
    13.9              (Net.match_term rules (Pattern.eta_contract tm)))
   13.10        end;
   13.11  
   13.12 @@ -774,7 +774,7 @@
   13.13      (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
   13.14       (fn xs => Toplevel.theory (fn thy => add_realizers
   13.15         (map (fn (((a, vs), s1), s2) =>
   13.16 -         (PureThy.get_thm thy (a, NONE), (vs, s1, s2))) xs) thy)));
   13.17 +         (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
   13.18  
   13.19  val realizabilityP =
   13.20    OuterSyntax.command "realizability"
   13.21 @@ -789,7 +789,7 @@
   13.22  val extractP =
   13.23    OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
   13.24      (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
   13.25 -      (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair NONE)) xs) thy)));
   13.26 +      (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
   13.27  
   13.28  val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
   13.29  
    14.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Jun 20 22:13:58 2005 +0200
    14.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Jun 20 22:13:59 2005 +0200
    14.3 @@ -523,7 +523,7 @@
    14.4  
    14.5  (* standard sections *)
    14.6  
    14.7 -fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (" ^ Library.quote ax ^ ", NONE);";
    14.8 +fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (PureThy.Name " ^ Library.quote ax ^ ");";
    14.9  val mk_vals = cat_lines o map mk_val;
   14.10  
   14.11  fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs)
    15.1 --- a/src/Pure/axclass.ML	Mon Jun 20 22:13:58 2005 +0200
    15.2 +++ b/src/Pure/axclass.ML	Mon Jun 20 22:13:59 2005 +0200
    15.3 @@ -417,7 +417,7 @@
    15.4    Pretty.string_of_arity (Sign.pp thy) (t, Ss, [c]));
    15.5  
    15.6  fun witnesses thy names thms =
    15.7 -  PureThy.get_thmss thy (map (rpair NONE) names) @
    15.8 +  PureThy.get_thmss thy (map Name names) @
    15.9    thms @
   15.10    List.filter is_def (map snd (axioms_of thy));
   15.11  
    16.1 --- a/src/Pure/goals.ML	Mon Jun 20 22:13:58 2005 +0200
    16.2 +++ b/src/Pure/goals.ML	Mon Jun 20 22:13:59 2005 +0200
    16.3 @@ -315,7 +315,7 @@
    16.4  fun get_thmx f get thy name =
    16.5    (case get_first (get_thm_locale name) (get_scope thy) of
    16.6      SOME thm => f thm
    16.7 -  | NONE => get thy (name, NONE));
    16.8 +  | NONE => get thy (Name name));
    16.9  
   16.10  val get_thm = get_thmx I PureThy.get_thm;
   16.11  val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
    17.1 --- a/src/Pure/proof_general.ML	Mon Jun 20 22:13:58 2005 +0200
    17.2 +++ b/src/Pure/proof_general.ML	Mon Jun 20 22:13:59 2005 +0200
    17.3 @@ -715,7 +715,7 @@
    17.4  
    17.5  local
    17.6   val topthy = Toplevel.theory_of o Toplevel.get_state
    17.7 - fun pthm thy name = print_thm (get_thm thy (name, NONE))
    17.8 + fun pthm thy name = print_thm (get_thm thy (Name name))
    17.9  
   17.10   fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
   17.11  in