# HG changeset patch # User oheimb # Date 902931649 -7200 # Node ID 22029546d109ea678adceab7f861b7dfe23c982b # Parent b8598e4fb73eaa92c40b630ce0787bc86e40719f renamed mk_meta_eq to meta_eq diff -r b8598e4fb73e -r 22029546d109 src/HOL/Modelcheck/MCSyn.ML --- a/src/HOL/Modelcheck/MCSyn.ML Wed Aug 12 16:16:49 1998 +0200 +++ b/src/HOL/Modelcheck/MCSyn.ML Wed Aug 12 16:20:49 1998 +0200 @@ -26,7 +26,7 @@ local val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; - val rew = mk_meta_eq pair_eta_expand; + val rew = meta_eq pair_eta_expand; fun proc _ _ (Abs _) = Some rew | proc _ _ _ = None; diff -r b8598e4fb73e -r 22029546d109 src/HOL/Prod.ML --- a/src/HOL/Prod.ML Wed Aug 12 16:16:49 1998 +0200 +++ b/src/HOL/Prod.ML Wed Aug 12 16:20:49 1998 +0200 @@ -153,7 +153,7 @@ local val split_eta_pat = Thm.read_cterm (sign_of thy) ("split (%x. split (%y. f x y))", HOLogic.termTVar); - val split_eta_meta_eq = standard (mk_meta_eq cond_split_eta); + val split_eta_meta_eq = standard (meta_eq cond_split_eta); fun Pair_pat 0 (Bound 0) = true | Pair_pat k (Const ("Pair", _) $ Bound m $ t) = m = k andalso Pair_pat (k-1) t @@ -176,7 +176,7 @@ val ct = cterm_of (sign_of thy) (HOLogic.mk_Trueprop (HOLogic.mk_eq (atom_fun s,fvar))); val ss = HOL_basic_ss addsimps [cond_split_eta]; - in Some (mk_meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end) + in Some (meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end) | None => None) | proc _ _ _ = None; @@ -435,7 +435,7 @@ Cannot use this rule directly -- it loops!*) local val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT)); - val unit_meta_eq = standard (mk_meta_eq unit_eq); + val unit_meta_eq = standard (meta_eq unit_eq); fun proc _ _ t = if HOLogic.is_unit t then None else Some unit_meta_eq; diff -r b8598e4fb73e -r 22029546d109 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Aug 12 16:16:49 1998 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Aug 12 16:20:49 1998 +0200 @@ -329,7 +329,7 @@ (take (length newTs, reccomb_names))); val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @ - (map mk_meta_eq primrec_thms)) (cterm_of (sign_of thy2) t) + (map meta_eq primrec_thms)) (cterm_of (sign_of thy2) t) (fn _ => [rtac refl 1]))) (DatatypeProp.make_cases new_type_names descr sorts thy2); @@ -399,7 +399,7 @@ val cert = cterm_of (sign_of thy2); val distinct_lemma' = cterm_instantiate [(cert distinct_f, cert f)] distinct_lemma; - val rewrites = ord_defs @ (map mk_meta_eq case_thms) + val rewrites = ord_defs @ (map meta_eq case_thms) in (map (fn t => prove_goalw_cterm rewrites (cert t) (fn _ => [rtac refl 1])) (rev ts')) @ [standard distinct_lemma'] @@ -490,7 +490,7 @@ (size_names ~~ recTs ~~ def_names ~~ reccomb_names)); val size_def_thms = map (get_axiom thy') def_names; - val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; + val rewrites = size_def_thms @ map meta_eq primrec_thms; val size_thms = map (fn t => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t) (fn _ => [rtac refl 1])) diff -r b8598e4fb73e -r 22029546d109 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Aug 12 16:16:49 1998 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Aug 12 16:20:49 1998 +0200 @@ -317,7 +317,7 @@ (* prove characteristic equations *) - val rewrites = def_thms @ (map mk_meta_eq rec_rewrites); + val rewrites = def_thms @ (map meta_eq rec_rewrites); val char_thms' = map (fn eqn => prove_goalw_cterm rewrites (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns; @@ -381,7 +381,7 @@ val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds); - val rewrites = map mk_meta_eq iso_char_thms; + val rewrites = map meta_eq iso_char_thms; val inj_thms' = map (fn r => r RS injD) inj_thms; val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5) @@ -430,7 +430,7 @@ fun prove_constr_rep_thm eqn = let val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms; - val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms) + val rewrites = constr_defs @ (map (meta_eq o #2) newT_iso_axms) in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ => [resolve_tac inj_thms 1, rewrite_goals_tac rewrites, @@ -524,7 +524,7 @@ [REPEAT (eresolve_tac Abs_inverse_thms 1), simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1, DEPTH_SOLVE_1 (ares_tac [prem] 1)])) - (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); + (prems ~~ (constr_defs @ (map meta_eq iso_char_thms))))]); val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6; diff -r b8598e4fb73e -r 22029546d109 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Wed Aug 12 16:16:49 1998 +0200 +++ b/src/HOL/Tools/inductive_package.ML Wed Aug 12 16:20:49 1998 +0200 @@ -341,14 +341,14 @@ HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $ nth_elem (find_index_eq c cs, preds))))) (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac - (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), + (map meta_eq [sum_case_Inl, sum_case_Inr]), rtac refl 1])) cs; val induct = prove_goalw_cterm [] (cterm_of sign (Logic.list_implies (ind_prems, ind_concl))) (fn prems => [rtac (impI RS allI) 1, DETERM (etac (mono RS (fp_def RS def_induct)) 1), - rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)), + rewrite_goals_tac (map meta_eq (vimage_Int::vimage_simps)), fold_goals_tac rec_sets_defs, (*This CollectE and disjE separates out the introduction rules*) REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])), @@ -356,7 +356,7 @@ some premise involves disjunction.*) REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] ORELSE' hyp_subst_tac)), - rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), + rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]), EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); @@ -366,7 +366,7 @@ REPEAT (EVERY [REPEAT (resolve_tac [conjI, impI] 1), TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1, - rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), + rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]), atac 1])]) in standard (split_rule (induct RS lemma)) @@ -451,7 +451,7 @@ prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; val raw_induct = if no_ind then TrueI else if coind then standard (rule_by_tactic - (rewrite_tac [mk_meta_eq vimage_Un] THEN + (rewrite_tac [meta_eq vimage_Un] THEN fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) else prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def diff -r b8598e4fb73e -r 22029546d109 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Wed Aug 12 16:16:49 1998 +0200 +++ b/src/HOL/Tools/primrec_package.ML Wed Aug 12 16:20:49 1998 +0200 @@ -221,7 +221,7 @@ (if eq_set (names1, names2) then Theory.add_defs_i defs' else primrec_err ("functions " ^ commas names2 ^ "\nare not mutually recursive")); - val rewrites = (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs'); + val rewrites = (map meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs'); val _ = writeln ("Proving equations for primrec function(s)\n" ^ commas names1 ^ " ..."); val char_thms = map (fn t => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t) diff -r b8598e4fb73e -r 22029546d109 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Wed Aug 12 16:16:49 1998 +0200 +++ b/src/HOL/arith_data.ML Wed Aug 12 16:20:49 1998 +0200 @@ -56,7 +56,7 @@ val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; fun prove_conv expand_tac norm_tac sg (t, u) = - mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u))) + meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u))) (K [expand_tac, norm_tac])) handle ERROR => error ("The error(s) above occurred while trying to prove " ^ (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));