renamed mk_meta_eq to mk_eq
authoroheimb
Thu Sep 24 17:17:14 1998 +0200 (1998-09-24)
changeset 5553ae42b36a50c2
parent 5552 dcd3e7711cac
child 5554 3cae5d6510c2
renamed mk_meta_eq to mk_eq
src/HOL/Integ/simproc.ML
src/HOL/Modelcheck/MCSyn.ML
src/HOL/Prod.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/arith_data.ML
src/Provers/splitter.ML
src/ZF/OrdQuant.ML
src/ZF/indrule.ML
src/ZF/simpdata.ML
     1.1 --- a/src/HOL/Integ/simproc.ML	Thu Sep 24 17:16:06 1998 +0200
     1.2 +++ b/src/HOL/Integ/simproc.ML	Thu Sep 24 17:17:14 1998 +0200
     1.3 @@ -79,7 +79,7 @@
     1.4  	handle ERROR =>
     1.5  	error("The error(s) above occurred while trying to prove " ^
     1.6  	      string_of_cterm ct)
     1.7 -  in Some (meta_eq thm) end
     1.8 +  in Some (mk_meta_eq thm) end
     1.9    handle Cancel => None;
    1.10  
    1.11  
     2.1 --- a/src/HOL/Modelcheck/MCSyn.ML	Thu Sep 24 17:16:06 1998 +0200
     2.2 +++ b/src/HOL/Modelcheck/MCSyn.ML	Thu Sep 24 17:17:14 1998 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4  
     2.5  local
     2.6    val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))];
     2.7 -  val rew = meta_eq pair_eta_expand;
     2.8 +  val rew = mk_meta_eq pair_eta_expand;
     2.9  
    2.10    fun proc _ _ (Abs _) = Some rew
    2.11      | proc _ _ _ = None;
     3.1 --- a/src/HOL/Prod.ML	Thu Sep 24 17:16:06 1998 +0200
     3.2 +++ b/src/HOL/Prod.ML	Thu Sep 24 17:17:14 1998 +0200
     3.3 @@ -153,7 +153,7 @@
     3.4  local
     3.5    val split_eta_pat = Thm.read_cterm (sign_of thy) 
     3.6  		("split (%x. split (%y. f x y))", HOLogic.termTVar);
     3.7 -  val split_eta_meta_eq = standard (meta_eq cond_split_eta);
     3.8 +  val split_eta_meta_eq = standard (mk_meta_eq cond_split_eta);
     3.9    fun  Pair_pat 0      (Bound 0) = true
    3.10    |    Pair_pat k      (Const ("Pair",  _) $ Bound m $ t) = 
    3.11  			m = k andalso Pair_pat (k-1) t
    3.12 @@ -176,7 +176,7 @@
    3.13  			 val ct   = cterm_of sg (HOLogic.mk_Trueprop
    3.14  				   (HOLogic.mk_eq (atom_fun s,fvar)));
    3.15  			 val ss   = HOL_basic_ss addsimps [cond_split_eta];
    3.16 -         in Some (meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)
    3.17 +         in Some (mk_meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)
    3.18  	| None => None)
    3.19    |   proc _ _ _ = None;
    3.20  
    3.21 @@ -434,7 +434,7 @@
    3.22    Cannot use this rule directly -- it loops!*)
    3.23  local
    3.24    val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT));
    3.25 -  val unit_meta_eq = standard (meta_eq unit_eq);
    3.26 +  val unit_meta_eq = standard (mk_meta_eq unit_eq);
    3.27    fun proc _ _ t =
    3.28      if HOLogic.is_unit t then None
    3.29      else Some unit_meta_eq;
     4.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Sep 24 17:16:06 1998 +0200
     4.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Sep 24 17:17:14 1998 +0200
     4.3 @@ -329,7 +329,7 @@
     4.4            (take (length newTs, reccomb_names)));
     4.5  
     4.6      val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
     4.7 -      (map meta_eq primrec_thms)) (cterm_of (sign_of thy2) t)
     4.8 +      (map mk_meta_eq primrec_thms)) (cterm_of (sign_of thy2) t)
     4.9          (fn _ => [rtac refl 1])))
    4.10            (DatatypeProp.make_cases new_type_names descr sorts thy2);
    4.11  
    4.12 @@ -399,7 +399,7 @@
    4.13              val cert = cterm_of (sign_of thy2);
    4.14              val distinct_lemma' = cterm_instantiate
    4.15                [(cert distinct_f, cert f)] distinct_lemma;
    4.16 -            val rewrites = ord_defs @ (map meta_eq case_thms)
    4.17 +            val rewrites = ord_defs @ (map mk_meta_eq case_thms)
    4.18            in
    4.19              (map (fn t => prove_goalw_cterm rewrites (cert t)
    4.20                (fn _ => [rtac refl 1])) (rev ts')) @ [standard distinct_lemma']
    4.21 @@ -490,7 +490,7 @@
    4.22              (size_names ~~ recTs ~~ def_names ~~ reccomb_names));
    4.23  
    4.24      val size_def_thms = map (get_axiom thy') def_names;
    4.25 -    val rewrites = size_def_thms @ map meta_eq primrec_thms;
    4.26 +    val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
    4.27  
    4.28      val size_thms = map (fn t => prove_goalw_cterm rewrites
    4.29        (cterm_of (sign_of thy') t) (fn _ => [rtac refl 1]))
     5.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 24 17:16:06 1998 +0200
     5.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 24 17:17:14 1998 +0200
     5.3 @@ -317,7 +317,7 @@
     5.4  
     5.5          (* prove characteristic equations *)
     5.6  
     5.7 -        val rewrites = def_thms @ (map meta_eq rec_rewrites);
     5.8 +        val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
     5.9          val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
    5.10            (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
    5.11  
    5.12 @@ -381,7 +381,7 @@
    5.13  
    5.14          val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
    5.15  
    5.16 -        val rewrites = map meta_eq iso_char_thms;
    5.17 +        val rewrites = map mk_meta_eq iso_char_thms;
    5.18          val inj_thms' = map (fn r => r RS injD) inj_thms;
    5.19  
    5.20          val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
    5.21 @@ -430,7 +430,7 @@
    5.22      fun prove_constr_rep_thm eqn =
    5.23        let
    5.24          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
    5.25 -        val rewrites = constr_defs @ (map (meta_eq o #2) newT_iso_axms)
    5.26 +        val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    5.27        in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ =>
    5.28          [resolve_tac inj_thms 1,
    5.29           rewrite_goals_tac rewrites,
    5.30 @@ -524,7 +524,7 @@
    5.31             [REPEAT (eresolve_tac Abs_inverse_thms 1),
    5.32              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
    5.33              DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
    5.34 -              (prems ~~ (constr_defs @ (map meta_eq iso_char_thms))))]);
    5.35 +              (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
    5.36  
    5.37      val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
    5.38  
     6.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Sep 24 17:16:06 1998 +0200
     6.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Sep 24 17:17:14 1998 +0200
     6.3 @@ -341,14 +341,14 @@
     6.4             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
     6.5               nth_elem (find_index_eq c cs, preds)))))
     6.6          (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
     6.7 -           (map meta_eq [sum_case_Inl, sum_case_Inr]),
     6.8 +           (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
     6.9            rtac refl 1])) cs;
    6.10  
    6.11      val induct = prove_goalw_cterm [] (cterm_of sign
    6.12        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
    6.13          [rtac (impI RS allI) 1,
    6.14           DETERM (etac (mono RS (fp_def RS def_induct)) 1),
    6.15 -         rewrite_goals_tac (map meta_eq (vimage_Int::vimage_simps)),
    6.16 +         rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)),
    6.17           fold_goals_tac rec_sets_defs,
    6.18           (*This CollectE and disjE separates out the introduction rules*)
    6.19           REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
    6.20 @@ -356,7 +356,7 @@
    6.21             some premise involves disjunction.*)
    6.22           REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
    6.23                       ORELSE' hyp_subst_tac)),
    6.24 -         rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
    6.25 +         rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    6.26           EVERY (map (fn prem =>
    6.27             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    6.28  
    6.29 @@ -366,7 +366,7 @@
    6.30           REPEAT (EVERY
    6.31             [REPEAT (resolve_tac [conjI, impI] 1),
    6.32              TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
    6.33 -            rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
    6.34 +            rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    6.35              atac 1])])
    6.36  
    6.37    in standard (split_rule (induct RS lemma))
    6.38 @@ -451,7 +451,7 @@
    6.39        prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
    6.40      val raw_induct = if no_ind then TrueI else
    6.41        if coind then standard (rule_by_tactic
    6.42 -        (rewrite_tac [meta_eq vimage_Un] THEN
    6.43 +        (rewrite_tac [mk_meta_eq vimage_Un] THEN
    6.44            fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
    6.45        else
    6.46          prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
     7.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Sep 24 17:16:06 1998 +0200
     7.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Sep 24 17:17:14 1998 +0200
     7.3 @@ -221,7 +221,7 @@
     7.4        (if eq_set (names1, names2) then Theory.add_defs_i defs'
     7.5         else primrec_err ("functions " ^ commas names2 ^
     7.6           "\nare not mutually recursive"));
     7.7 -    val rewrites = (map meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
     7.8 +    val rewrites = (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
     7.9      val _ = writeln ("Proving equations for primrec function(s)\n" ^
    7.10        commas names1 ^ " ...");
    7.11      val char_thms = map (fn t => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
     8.1 --- a/src/HOL/arith_data.ML	Thu Sep 24 17:16:06 1998 +0200
     8.2 +++ b/src/HOL/arith_data.ML	Thu Sep 24 17:17:14 1998 +0200
     8.3 @@ -56,7 +56,7 @@
     8.4  val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
     8.5  
     8.6  fun prove_conv expand_tac norm_tac sg (t, u) =
     8.7 -  meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
     8.8 +  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
     8.9      (K [expand_tac, norm_tac]))
    8.10    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    8.11      (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
     9.1 --- a/src/Provers/splitter.ML	Thu Sep 24 17:16:06 1998 +0200
     9.2 +++ b/src/Provers/splitter.ML	Thu Sep 24 17:17:14 1998 +0200
     9.3 @@ -11,7 +11,7 @@
     9.4  signature SPLITTER_DATA =
     9.5  sig
     9.6    structure Simplifier: SIMPLIFIER
     9.7 -  val mk_meta_eq    : thm -> thm
     9.8 +  val mk_eq         : thm -> thm
     9.9    val meta_eq_to_iff: thm (* "x == y ==> x = y"                    *)
    9.10    val iffD          : thm (* "[| P = Q; Q |] ==> P"                *)
    9.11    val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
    9.12 @@ -47,7 +47,7 @@
    9.13  
    9.14  fun split_format_err() = error("Wrong format for split rule");
    9.15  
    9.16 -fun split_thm_info thm = case concl_of (Data.mk_meta_eq thm) of
    9.17 +fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
    9.18       Const("==", _)$(Var _$t)$c =>
    9.19          (case strip_comb t of
    9.20             (Const(a,_),_) => (a,case c of (Const(s,_)$_)=>s=const_not|_=> false)
    9.21 @@ -288,7 +288,7 @@
    9.22  
    9.23  fun split_tac [] i = no_tac
    9.24    | split_tac splits i =
    9.25 -  let val splits = map Data.mk_meta_eq splits;
    9.26 +  let val splits = map Data.mk_eq splits;
    9.27        fun const(thm) =
    9.28              (case concl_of thm of _$(t as _$lhs)$_ =>
    9.29                 (case strip_comb lhs of (Const(a,_),args) =>
    10.1 --- a/src/ZF/OrdQuant.ML	Thu Sep 24 17:16:06 1998 +0200
    10.2 +++ b/src/ZF/OrdQuant.ML	Thu Sep 24 17:17:14 1998 +0200
    10.3 @@ -98,7 +98,7 @@
    10.4  val Ord_atomize = atomize (("oall", [ospec])::ZF_conn_pairs, 
    10.5                             ZF_mem_pairs);
    10.6  
    10.7 -simpset_ref() := simpset() setmksimps (map mk_meta_eq o Ord_atomize o gen_all)
    10.8 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
    10.9                          addsimps [oall_simp, ltD RS beta]
   10.10                          addcongs [oall_cong, oex_cong, OUN_cong];
   10.11  
    11.1 --- a/src/ZF/indrule.ML	Thu Sep 24 17:16:06 1998 +0200
    11.2 +++ b/src/ZF/indrule.ML	Thu Sep 24 17:17:14 1998 +0200
    11.3 @@ -85,7 +85,7 @@
    11.4    simplifications.  If the premises get simplified, then the proofs could 
    11.5    fail.  *)
    11.6  val min_ss = empty_ss
    11.7 -      setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
    11.8 +      setmksimps (map mk_eq o ZF_atomize o gen_all)
    11.9        setSolver  (fn prems => resolve_tac (triv_rls@prems) 
   11.10                                ORELSE' assume_tac
   11.11                                ORELSE' etac FalseE);
    12.1 --- a/src/ZF/simpdata.ML	Thu Sep 24 17:16:06 1998 +0200
    12.2 +++ b/src/ZF/simpdata.ML	Thu Sep 24 17:17:14 1998 +0200
    12.3 @@ -105,7 +105,7 @@
    12.4  
    12.5  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    12.6  
    12.7 -simpset_ref() := simpset() setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
    12.8 +simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
    12.9                             addsplits [split_if];
   12.10  
   12.11  val ZF_ss = simpset();