renamed mk_meta_eq to meta_eq
authoroheimb
Wed Aug 12 16:20:49 1998 +0200 (1998-08-12)
changeset 530322029546d109
parent 5302 b8598e4fb73e
child 5304 c133f16febc7
renamed mk_meta_eq to meta_eq
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
     1.1 --- a/src/HOL/Modelcheck/MCSyn.ML	Wed Aug 12 16:16:49 1998 +0200
     1.2 +++ b/src/HOL/Modelcheck/MCSyn.ML	Wed Aug 12 16:20:49 1998 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  local
     1.6    val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))];
     1.7 -  val rew = mk_meta_eq pair_eta_expand;
     1.8 +  val rew = meta_eq pair_eta_expand;
     1.9  
    1.10    fun proc _ _ (Abs _) = Some rew
    1.11      | proc _ _ _ = None;
     2.1 --- a/src/HOL/Prod.ML	Wed Aug 12 16:16:49 1998 +0200
     2.2 +++ b/src/HOL/Prod.ML	Wed Aug 12 16:20:49 1998 +0200
     2.3 @@ -153,7 +153,7 @@
     2.4  local
     2.5    val split_eta_pat = Thm.read_cterm (sign_of thy) 
     2.6  		("split (%x. split (%y. f x y))", HOLogic.termTVar);
     2.7 -  val split_eta_meta_eq = standard (mk_meta_eq cond_split_eta);
     2.8 +  val split_eta_meta_eq = standard (meta_eq cond_split_eta);
     2.9    fun  Pair_pat 0      (Bound 0) = true
    2.10    |    Pair_pat k      (Const ("Pair",  _) $ Bound m $ t) = 
    2.11  			m = k andalso Pair_pat (k-1) t
    2.12 @@ -176,7 +176,7 @@
    2.13  			 val ct   = cterm_of (sign_of thy) (HOLogic.mk_Trueprop
    2.14  				   (HOLogic.mk_eq (atom_fun s,fvar)));
    2.15  			 val ss   = HOL_basic_ss addsimps [cond_split_eta];
    2.16 -         in Some (mk_meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)
    2.17 +         in Some (meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)
    2.18  	| None => None)
    2.19    |   proc _ _ _ = None;
    2.20  
    2.21 @@ -435,7 +435,7 @@
    2.22    Cannot use this rule directly -- it loops!*)
    2.23  local
    2.24    val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT));
    2.25 -  val unit_meta_eq = standard (mk_meta_eq unit_eq);
    2.26 +  val unit_meta_eq = standard (meta_eq unit_eq);
    2.27    fun proc _ _ t =
    2.28      if HOLogic.is_unit t then None
    2.29      else Some unit_meta_eq;
     3.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Aug 12 16:16:49 1998 +0200
     3.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Aug 12 16:20:49 1998 +0200
     3.3 @@ -329,7 +329,7 @@
     3.4            (take (length newTs, reccomb_names)));
     3.5  
     3.6      val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
     3.7 -      (map mk_meta_eq primrec_thms)) (cterm_of (sign_of thy2) t)
     3.8 +      (map meta_eq primrec_thms)) (cterm_of (sign_of thy2) t)
     3.9          (fn _ => [rtac refl 1])))
    3.10            (DatatypeProp.make_cases new_type_names descr sorts thy2);
    3.11  
    3.12 @@ -399,7 +399,7 @@
    3.13              val cert = cterm_of (sign_of thy2);
    3.14              val distinct_lemma' = cterm_instantiate
    3.15                [(cert distinct_f, cert f)] distinct_lemma;
    3.16 -            val rewrites = ord_defs @ (map mk_meta_eq case_thms)
    3.17 +            val rewrites = ord_defs @ (map meta_eq case_thms)
    3.18            in
    3.19              (map (fn t => prove_goalw_cterm rewrites (cert t)
    3.20                (fn _ => [rtac refl 1])) (rev ts')) @ [standard distinct_lemma']
    3.21 @@ -490,7 +490,7 @@
    3.22              (size_names ~~ recTs ~~ def_names ~~ reccomb_names));
    3.23  
    3.24      val size_def_thms = map (get_axiom thy') def_names;
    3.25 -    val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
    3.26 +    val rewrites = size_def_thms @ map meta_eq primrec_thms;
    3.27  
    3.28      val size_thms = map (fn t => prove_goalw_cterm rewrites
    3.29        (cterm_of (sign_of thy') t) (fn _ => [rtac refl 1]))
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Aug 12 16:16:49 1998 +0200
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Aug 12 16:20:49 1998 +0200
     4.3 @@ -317,7 +317,7 @@
     4.4  
     4.5          (* prove characteristic equations *)
     4.6  
     4.7 -        val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
     4.8 +        val rewrites = def_thms @ (map meta_eq rec_rewrites);
     4.9          val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
    4.10            (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
    4.11  
    4.12 @@ -381,7 +381,7 @@
    4.13  
    4.14          val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
    4.15  
    4.16 -        val rewrites = map mk_meta_eq iso_char_thms;
    4.17 +        val rewrites = map meta_eq iso_char_thms;
    4.18          val inj_thms' = map (fn r => r RS injD) inj_thms;
    4.19  
    4.20          val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
    4.21 @@ -430,7 +430,7 @@
    4.22      fun prove_constr_rep_thm eqn =
    4.23        let
    4.24          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
    4.25 -        val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    4.26 +        val rewrites = constr_defs @ (map (meta_eq o #2) newT_iso_axms)
    4.27        in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ =>
    4.28          [resolve_tac inj_thms 1,
    4.29           rewrite_goals_tac rewrites,
    4.30 @@ -524,7 +524,7 @@
    4.31             [REPEAT (eresolve_tac Abs_inverse_thms 1),
    4.32              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
    4.33              DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
    4.34 -              (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
    4.35 +              (prems ~~ (constr_defs @ (map meta_eq iso_char_thms))))]);
    4.36  
    4.37      val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
    4.38  
     5.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Aug 12 16:16:49 1998 +0200
     5.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Aug 12 16:20:49 1998 +0200
     5.3 @@ -341,14 +341,14 @@
     5.4             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
     5.5               nth_elem (find_index_eq c cs, preds)))))
     5.6          (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
     5.7 -           (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
     5.8 +           (map meta_eq [sum_case_Inl, sum_case_Inr]),
     5.9            rtac refl 1])) cs;
    5.10  
    5.11      val induct = prove_goalw_cterm [] (cterm_of sign
    5.12        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
    5.13          [rtac (impI RS allI) 1,
    5.14           DETERM (etac (mono RS (fp_def RS def_induct)) 1),
    5.15 -         rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)),
    5.16 +         rewrite_goals_tac (map meta_eq (vimage_Int::vimage_simps)),
    5.17           fold_goals_tac rec_sets_defs,
    5.18           (*This CollectE and disjE separates out the introduction rules*)
    5.19           REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
    5.20 @@ -356,7 +356,7 @@
    5.21             some premise involves disjunction.*)
    5.22           REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
    5.23                       ORELSE' hyp_subst_tac)),
    5.24 -         rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    5.25 +         rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
    5.26           EVERY (map (fn prem =>
    5.27             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    5.28  
    5.29 @@ -366,7 +366,7 @@
    5.30           REPEAT (EVERY
    5.31             [REPEAT (resolve_tac [conjI, impI] 1),
    5.32              TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
    5.33 -            rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    5.34 +            rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
    5.35              atac 1])])
    5.36  
    5.37    in standard (split_rule (induct RS lemma))
    5.38 @@ -451,7 +451,7 @@
    5.39        prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
    5.40      val raw_induct = if no_ind then TrueI else
    5.41        if coind then standard (rule_by_tactic
    5.42 -        (rewrite_tac [mk_meta_eq vimage_Un] THEN
    5.43 +        (rewrite_tac [meta_eq vimage_Un] THEN
    5.44            fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
    5.45        else
    5.46          prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
     6.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Aug 12 16:16:49 1998 +0200
     6.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Aug 12 16:20:49 1998 +0200
     6.3 @@ -221,7 +221,7 @@
     6.4        (if eq_set (names1, names2) then Theory.add_defs_i defs'
     6.5         else primrec_err ("functions " ^ commas names2 ^
     6.6           "\nare not mutually recursive"));
     6.7 -    val rewrites = (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
     6.8 +    val rewrites = (map meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
     6.9      val _ = writeln ("Proving equations for primrec function(s)\n" ^
    6.10        commas names1 ^ " ...");
    6.11      val char_thms = map (fn t => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
     7.1 --- a/src/HOL/arith_data.ML	Wed Aug 12 16:16:49 1998 +0200
     7.2 +++ b/src/HOL/arith_data.ML	Wed Aug 12 16:20:49 1998 +0200
     7.3 @@ -56,7 +56,7 @@
     7.4  val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
     7.5  
     7.6  fun prove_conv expand_tac norm_tac sg (t, u) =
     7.7 -  mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
     7.8 +  meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
     7.9      (K [expand_tac, norm_tac]))
    7.10    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    7.11      (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));