1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML Sat Dec 14 07:26:45 2013 +0800
1.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML Sat Dec 14 07:45:30 2013 +0800
1.3 @@ -459,7 +459,7 @@
1.4
1.5 fun bnf_of ctxt =
1.6 Symtab.lookup (Data.get (Context.Proof ctxt))
1.7 - #> Option.map (morph_bnf (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
1.8 + #> Option.map (morph_bnf (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
1.9
1.10
1.11 (* Utilities *)
2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Sat Dec 14 07:26:45 2013 +0800
2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Sat Dec 14 07:45:30 2013 +0800
2.3 @@ -156,7 +156,7 @@
2.4 sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
2.5
2.6 val transfer_fp_sugar =
2.7 - morph_fp_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
2.8 + morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
2.9
2.10 structure Data = Generic_Data
2.11 (
2.12 @@ -344,7 +344,7 @@
2.13 (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs));
2.14
2.15 val transfer_lfp_sugar_thms =
2.16 - morph_lfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
2.17 + morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
2.18
2.19 type gfp_sugar_thms =
2.20 ((thm list * thm) list * Args.src list)
2.21 @@ -368,7 +368,7 @@
2.22 map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs));
2.23
2.24 val transfer_gfp_sugar_thms =
2.25 - morph_gfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
2.26 + morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
2.27
2.28 fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
2.29
3.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML Sat Dec 14 07:26:45 2013 +0800
3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML Sat Dec 14 07:45:30 2013 +0800
3.3 @@ -370,7 +370,7 @@
3.4 xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
3.5 xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
3.6 rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
3.7 - |> morph_fp_result (Morphism.term_morphism (singleton (Variable.polymorphic lthy))));
3.8 + |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
3.9 in
3.10 (fp_res, lthy)
3.11 end;
4.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Sat Dec 14 07:26:45 2013 +0800
4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Sat Dec 14 07:45:30 2013 +0800
4.3 @@ -52,7 +52,7 @@
4.4 Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt));
4.5
4.6 val transfer_n2m_sugar =
4.7 - morph_n2m_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
4.8 + morph_n2m_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
4.9
4.10 fun n2m_sugar_of ctxt =
4.11 Typtab.lookup (Data.get (Context.Proof ctxt))
4.12 @@ -127,7 +127,7 @@
4.13 fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
4.14 let
4.15 val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
4.16 - val phi = Morphism.term_morphism (Term.subst_TVars rho);
4.17 + val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
4.18 in
4.19 morph_ctr_sugar phi (nth ctr_sugars index)
4.20 end;
5.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sat Dec 14 07:26:45 2013 +0800
5.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sat Dec 14 07:45:30 2013 +0800
5.3 @@ -125,7 +125,7 @@
5.4 case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
5.5
5.6 val transfer_ctr_sugar =
5.7 - morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
5.8 + morph_ctr_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
5.9
5.10 structure Data = Generic_Data
5.11 (
6.1 --- a/src/HOL/Tools/Function/function_common.ML Sat Dec 14 07:26:45 2013 +0800
6.2 +++ b/src/HOL/Tools/Function/function_common.ML Sat Dec 14 07:45:30 2013 +0800
6.3 @@ -189,8 +189,11 @@
6.4 let
6.5 fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
6.6 in
6.7 - Morphism.thm_morphism f $> Morphism.term_morphism term
6.8 - $> Morphism.typ_morphism (Logic.type_map term)
6.9 + Morphism.morphism "lift_morphism"
6.10 + {binding = [],
6.11 + typ = [Logic.type_map term],
6.12 + term = [term],
6.13 + fact = [map f]}
6.14 end
6.15
6.16 fun import_function_data t ctxt =
7.1 --- a/src/HOL/Tools/Function/function_elims.ML Sat Dec 14 07:26:45 2013 +0800
7.2 +++ b/src/HOL/Tools/Function/function_elims.ML Sat Dec 14 07:45:30 2013 +0800
7.3 @@ -33,118 +33,121 @@
7.4
7.5 local
7.6
7.7 -fun propagate_tac i thm =
7.8 - let fun inspect eq = case eq of
7.9 - Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) =>
7.10 - if Logic.occs (Free x, t) then raise Match else true
7.11 - | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) =>
7.12 - if Logic.occs (Free x, t) then raise Match else false
7.13 - | _ => raise Match;
7.14 - fun mk_eq thm = (if inspect (prop_of thm) then
7.15 - [thm RS eq_reflection]
7.16 - else
7.17 - [Thm.symmetric (thm RS eq_reflection)])
7.18 - handle Match => [];
7.19 - val ss = Simplifier.global_context (Thm.theory_of_thm thm) empty_ss
7.20 - |> Simplifier.set_mksimps (K mk_eq)
7.21 +fun propagate_tac ctxt i =
7.22 + let
7.23 + fun inspect eq =
7.24 + (case eq of
7.25 + Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) =>
7.26 + if Logic.occs (Free x, t) then raise Match else true
7.27 + | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) =>
7.28 + if Logic.occs (Free x, t) then raise Match else false
7.29 + | _ => raise Match);
7.30 + fun mk_eq thm =
7.31 + (if inspect (prop_of thm) then [thm RS eq_reflection]
7.32 + else [Thm.symmetric (thm RS eq_reflection)])
7.33 + handle Match => [];
7.34 + val simpset =
7.35 + empty_simpset ctxt
7.36 + |> Simplifier.set_mksimps (K mk_eq);
7.37 in
7.38 - asm_lr_simp_tac ss i thm
7.39 + asm_lr_simp_tac simpset i
7.40 end;
7.41
7.42 -val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+}
7.43 -val boolE = @{thms HOL.TrueE HOL.FalseE}
7.44 -val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+}
7.45 -val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}
7.46 +val eq_boolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+};
7.47 +val boolE = @{thms HOL.TrueE HOL.FalseE};
7.48 +val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+};
7.49 +val eq_bool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False};
7.50
7.51 fun bool_subst_tac ctxt i =
7.52 - REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i)
7.53 - THEN REPEAT (dresolve_tac boolD i)
7.54 - THEN REPEAT (eresolve_tac boolE i)
7.55 + REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eq_bool i)
7.56 + THEN REPEAT (dresolve_tac boolD i)
7.57 + THEN REPEAT (eresolve_tac boolE i)
7.58
7.59 fun mk_bool_elims ctxt elim =
7.60 - let val tac = ALLGOALS (bool_subst_tac ctxt)
7.61 - fun mk_bool_elim b =
7.62 - elim
7.63 - |> Thm.forall_elim b
7.64 - |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1))
7.65 - |> Tactic.rule_by_tactic ctxt tac
7.66 + let
7.67 + val tac = ALLGOALS (bool_subst_tac ctxt);
7.68 + fun mk_bool_elim b =
7.69 + elim
7.70 + |> Thm.forall_elim b
7.71 + |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eq_boolI 1))
7.72 + |> Tactic.rule_by_tactic ctxt tac;
7.73 in
7.74 - map mk_bool_elim [@{cterm True}, @{cterm False}]
7.75 + map mk_bool_elim [@{cterm True}, @{cterm False}]
7.76 end;
7.77
7.78 in
7.79
7.80 fun mk_partial_elim_rules ctxt result =
7.81 let
7.82 - val thy = Proof_Context.theory_of ctxt;
7.83 + val thy = Proof_Context.theory_of ctxt;
7.84 + val cert = cterm_of thy;
7.85
7.86 - val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
7.87 - termination, domintros, ...} = result;
7.88 - val n_fs = length fs;
7.89 + val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
7.90 + val n_fs = length fs;
7.91
7.92 - fun mk_partial_elim_rule (idx,f) =
7.93 - let fun mk_funeq 0 T (acc_vars, acc_lhs) =
7.94 - let val y = Free("y",T) in
7.95 - (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T)
7.96 - end
7.97 - | mk_funeq n (Type(@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) =
7.98 - let val xn = Free ("x" ^ Int.toString n,S) in
7.99 - mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn)
7.100 - end
7.101 - | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f]))
7.102 + fun mk_partial_elim_rule (idx, f) =
7.103 + let
7.104 + fun mk_funeq 0 T (acc_vars, acc_lhs) =
7.105 + let val y = Free("y", T)
7.106 + in (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T) end
7.107 + | mk_funeq n (Type (@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) =
7.108 + let val xn = Free ("x" ^ Int.toString n, S)
7.109 + in mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) end
7.110 + | mk_funeq _ _ _ = raise TERM ("Not a function.", [f]);
7.111
7.112 - val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl
7.113 - |> HOLogic.dest_Trueprop
7.114 - |> dest_funprop |> fst |> fst) = f)
7.115 - psimps
7.116 + val f_simps =
7.117 + filter (fn r =>
7.118 + (prop_of r |> Logic.strip_assums_concl
7.119 + |> HOLogic.dest_Trueprop
7.120 + |> dest_funprop |> fst |> fst) = f)
7.121 + psimps;
7.122
7.123 - val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl
7.124 - |> HOLogic.dest_Trueprop
7.125 - |> snd o fst o dest_funprop |> length;
7.126 - val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([],f)
7.127 - val (rhs_var, arg_vars) = case free_vars of x::xs => (x, rev xs)
7.128 - val args = HOLogic.mk_tuple arg_vars;
7.129 - val domT = R |> dest_Free |> snd |> hd o snd o dest_Type
7.130 + val arity =
7.131 + hd f_simps
7.132 + |> prop_of
7.133 + |> Logic.strip_assums_concl
7.134 + |> HOLogic.dest_Trueprop
7.135 + |> snd o fst o dest_funprop
7.136 + |> length;
7.137 + val (free_vars, prop, ranT) = mk_funeq arity (fastype_of f) ([], f);
7.138 + val (rhs_var, arg_vars) = (case free_vars of x :: xs => (x, rev xs));
7.139 + val args = HOLogic.mk_tuple arg_vars;
7.140 + val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
7.141
7.142 - val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
7.143 + val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
7.144
7.145 - val cprop = cterm_of thy prop
7.146 + val cprop = cert prop;
7.147
7.148 - val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
7.149 - val asms_thms = map Thm.assume asms;
7.150 + val asms = [cprop, cert (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
7.151 + val asms_thms = map Thm.assume asms;
7.152
7.153 - fun prep_subgoal i =
7.154 - REPEAT (eresolve_tac @{thms Pair_inject} i)
7.155 - THEN Method.insert_tac (case asms_thms of
7.156 - thm::thms => (thm RS sym) :: thms) i
7.157 - THEN propagate_tac i
7.158 - THEN TRY
7.159 - ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
7.160 - THEN bool_subst_tac ctxt i;
7.161 + fun prep_subgoal_tac i =
7.162 + REPEAT (eresolve_tac @{thms Pair_inject} i)
7.163 + THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
7.164 + THEN propagate_tac ctxt i
7.165 + THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
7.166 + THEN bool_subst_tac ctxt i;
7.167
7.168 - val tac = ALLGOALS prep_subgoal;
7.169 + val elim_stripped =
7.170 + nth cases idx
7.171 + |> Thm.forall_elim @{cterm "P::bool"}
7.172 + |> Thm.forall_elim (cert args)
7.173 + |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
7.174 + |> fold_rev Thm.implies_intr asms
7.175 + |> Thm.forall_intr (cert rhs_var);
7.176
7.177 - val elim_stripped =
7.178 - nth cases idx
7.179 - |> Thm.forall_elim @{cterm "P::bool"}
7.180 - |> Thm.forall_elim (cterm_of thy args)
7.181 - |> Tactic.rule_by_tactic ctxt tac
7.182 - |> fold_rev Thm.implies_intr asms
7.183 - |> Thm.forall_intr (cterm_of thy rhs_var)
7.184 + val bool_elims =
7.185 + (case ranT of
7.186 + Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
7.187 + | _ => []);
7.188
7.189 - val bool_elims = (case ranT of
7.190 - Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
7.191 - | _ => []);
7.192 -
7.193 - fun unstrip rl =
7.194 - rl |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm
7.195 - (map (cterm_of thy) arg_vars))
7.196 - |> Thm.forall_intr @{cterm "P::bool"}
7.197 -
7.198 - in
7.199 - map unstrip (elim_stripped :: bool_elims)
7.200 - end;
7.201 -
7.202 + fun unstrip rl =
7.203 + rl
7.204 + |> fold_rev (Thm.forall_intr o cert) arg_vars
7.205 + |> Thm.forall_intr @{cterm "P::bool"};
7.206 + in
7.207 + map unstrip (elim_stripped :: bool_elims)
7.208 + end;
7.209 in
7.210 map_index mk_partial_elim_rule fs
7.211 end;
8.1 --- a/src/Pure/Isar/class_declaration.ML Sat Dec 14 07:26:45 2013 +0800
8.2 +++ b/src/Pure/Isar/class_declaration.ML Sat Dec 14 07:45:30 2013 +0800
8.3 @@ -64,7 +64,7 @@
8.4
8.5 (* canonical interpretation *)
8.6 val base_morph = inst_morph
8.7 - $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class))
8.8 + $> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class))
8.9 $> Element.satisfy_morphism (the_list some_witn);
8.10 val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups);
8.11
9.1 --- a/src/Pure/Isar/element.ML Sat Dec 14 07:26:45 2013 +0800
9.2 +++ b/src/Pure/Isar/element.ML Sat Dec 14 07:45:30 2013 +0800
9.3 @@ -391,7 +391,7 @@
9.4 in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
9.5
9.6 fun instT_morphism thy env =
9.7 - Morphism.morphism
9.8 + Morphism.morphism "Element.instT"
9.9 {binding = [],
9.10 typ = [instT_type env],
9.11 term = [instT_term env],
9.12 @@ -434,7 +434,7 @@
9.13 end;
9.14
9.15 fun inst_morphism thy (envT, env) =
9.16 - Morphism.morphism
9.17 + Morphism.morphism "Element.inst"
9.18 {binding = [],
9.19 typ = [instT_type envT],
9.20 term = [inst_term (envT, env)],
9.21 @@ -449,14 +449,14 @@
9.22 NONE => I
9.23 | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
9.24
9.25 -val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
9.26 +val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm;
9.27
9.28
9.29 (* rewriting with equalities *)
9.30
9.31 fun eq_morphism _ [] = NONE
9.32 | eq_morphism thy thms =
9.33 - SOME (Morphism.morphism
9.34 + SOME (Morphism.morphism "Element.eq_morphism"
9.35 {binding = [],
9.36 typ = [],
9.37 term = [Raw_Simplifier.rewrite_term thy thms []],
10.1 --- a/src/Pure/Isar/expression.ML Sat Dec 14 07:26:45 2013 +0800
10.2 +++ b/src/Pure/Isar/expression.ML Sat Dec 14 07:45:30 2013 +0800
10.3 @@ -171,7 +171,7 @@
10.4
10.5 (* Instantiation morphism *)
10.6
10.7 -fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
10.8 +fun inst_morphism (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
10.9 let
10.10 (* parameters *)
10.11 val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
10.12 @@ -192,7 +192,7 @@
10.13 val inst = Symtab.make insts'';
10.14 in
10.15 (Element.inst_morphism (Proof_Context.theory_of ctxt) (instT, inst) $>
10.16 - Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
10.17 + Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
10.18 end;
10.19
10.20
10.21 @@ -299,7 +299,7 @@
10.22 let
10.23 val thy = Proof_Context.theory_of ctxt;
10.24 val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
10.25 - val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
10.26 + val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst) ctxt;
10.27 in (loc, morph) end;
10.28
10.29 fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
10.30 @@ -368,7 +368,7 @@
10.31 val insts' = insts @ [(loc, (prfx, inst''))];
10.32 val (insts'', _, _, _) = check_autofix insts' [] [] ctxt;
10.33 val inst''' = insts'' |> List.last |> snd |> snd;
10.34 - val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
10.35 + val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
10.36 val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
10.37 in (i + 1, insts', ctxt'') end;
10.38
10.39 @@ -513,7 +513,8 @@
10.40 val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
10.41 val exp_typ = Logic.type_map exp_term;
10.42 val export' =
10.43 - Morphism.morphism {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
10.44 + Morphism.morphism "Expression.prep_goal"
10.45 + {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
10.46 in ((propss, deps, export'), goal_ctxt) end;
10.47
10.48 in
11.1 --- a/src/Pure/Isar/local_theory.ML Sat Dec 14 07:26:45 2013 +0800
11.2 +++ b/src/Pure/Isar/local_theory.ML Sat Dec 14 07:45:30 2013 +0800
11.3 @@ -189,7 +189,8 @@
11.4
11.5 fun standard_morphism lthy ctxt =
11.6 Proof_Context.norm_export_morphism lthy ctxt $>
11.7 - Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
11.8 + Morphism.binding_morphism "Local_Theory.standard_binding"
11.9 + (Name_Space.transform_binding (naming_of lthy));
11.10
11.11 fun standard_form lthy ctxt x =
11.12 Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
12.1 --- a/src/Pure/Isar/proof_context.ML Sat Dec 14 07:26:45 2013 +0800
12.2 +++ b/src/Pure/Isar/proof_context.ML Sat Dec 14 07:45:30 2013 +0800
12.3 @@ -762,7 +762,7 @@
12.4
12.5 fun norm_export_morphism inner outer =
12.6 export_morphism inner outer $>
12.7 - Morphism.thm_morphism Goal.norm_result;
12.8 + Morphism.thm_morphism "Proof_Context.norm_export" Goal.norm_result;
12.9
12.10
12.11
13.1 --- a/src/Pure/ROOT.ML Sat Dec 14 07:26:45 2013 +0800
13.2 +++ b/src/Pure/ROOT.ML Sat Dec 14 07:45:30 2013 +0800
13.3 @@ -328,6 +328,7 @@
13.4 toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
13.5 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
13.6 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
13.7 +toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
13.8
13.9 if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
13.10
14.1 --- a/src/Pure/assumption.ML Sat Dec 14 07:26:45 2013 +0800
14.2 +++ b/src/Pure/assumption.ML Sat Dec 14 07:45:30 2013 +0800
14.3 @@ -121,6 +121,9 @@
14.4 val thm = export false inner outer;
14.5 val term = export_term inner outer;
14.6 val typ = Logic.type_map term;
14.7 - in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [map thm]} end;
14.8 + in
14.9 + Morphism.morphism "Assumption.export"
14.10 + {binding = [], typ = [typ], term = [term], fact = [map thm]}
14.11 + end;
14.12
14.13 end;
15.1 --- a/src/Pure/morphism.ML Sat Dec 14 07:26:45 2013 +0800
15.2 +++ b/src/Pure/morphism.ML Sat Dec 14 07:45:30 2013 +0800
15.3 @@ -16,23 +16,24 @@
15.4 signature MORPHISM =
15.5 sig
15.6 include BASIC_MORPHISM
15.7 - type 'a funs = ('a -> 'a) list
15.8 + exception MORPHISM of string * exn
15.9 + val pretty: morphism -> Pretty.T
15.10 val binding: morphism -> binding -> binding
15.11 val typ: morphism -> typ -> typ
15.12 val term: morphism -> term -> term
15.13 val fact: morphism -> thm list -> thm list
15.14 val thm: morphism -> thm -> thm
15.15 val cterm: morphism -> cterm -> cterm
15.16 - val morphism:
15.17 - {binding: binding funs,
15.18 - typ: typ funs,
15.19 - term: term funs,
15.20 - fact: thm list funs} -> morphism
15.21 - val binding_morphism: (binding -> binding) -> morphism
15.22 - val typ_morphism: (typ -> typ) -> morphism
15.23 - val term_morphism: (term -> term) -> morphism
15.24 - val fact_morphism: (thm list -> thm list) -> morphism
15.25 - val thm_morphism: (thm -> thm) -> morphism
15.26 + val morphism: string ->
15.27 + {binding: (binding -> binding) list,
15.28 + typ: (typ -> typ) list,
15.29 + term: (term -> term) list,
15.30 + fact: (thm list -> thm list) list} -> morphism
15.31 + val binding_morphism: string -> (binding -> binding) -> morphism
15.32 + val typ_morphism: string -> (typ -> typ) -> morphism
15.33 + val term_morphism: string -> (term -> term) -> morphism
15.34 + val fact_morphism: string -> (thm list -> thm list) -> morphism
15.35 + val thm_morphism: string -> (thm -> thm) -> morphism
15.36 val transfer_morphism: theory -> morphism
15.37 val identity: morphism
15.38 val compose: morphism -> morphism -> morphism
15.39 @@ -43,17 +44,31 @@
15.40 structure Morphism: MORPHISM =
15.41 struct
15.42
15.43 -type 'a funs = ('a -> 'a) list;
15.44 -fun apply fs = fold_rev (fn f => fn x => f x) fs;
15.45 +(* named functions *)
15.46 +
15.47 +type 'a funs = (string * ('a -> 'a)) list;
15.48 +
15.49 +exception MORPHISM of string * exn;
15.50 +
15.51 +fun app (name, f) x = f x
15.52 + handle exn => if Exn.is_interrupt exn then reraise exn else raise MORPHISM (name, exn);
15.53 +
15.54 +fun apply fs = fold_rev app fs;
15.55 +
15.56 +
15.57 +(* type morphism *)
15.58
15.59 datatype morphism = Morphism of
15.60 - {binding: binding funs,
15.61 + {names: string list,
15.62 + binding: binding funs,
15.63 typ: typ funs,
15.64 term: term funs,
15.65 fact: thm list funs};
15.66
15.67 type declaration = morphism -> Context.generic -> Context.generic;
15.68
15.69 +fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
15.70 +
15.71 fun binding (Morphism {binding, ...}) = apply binding;
15.72 fun typ (Morphism {typ, ...}) = apply typ;
15.73 fun term (Morphism {term, ...}) = apply term;
15.74 @@ -61,22 +76,36 @@
15.75 val thm = singleton o fact;
15.76 val cterm = Drule.cterm_rule o thm;
15.77
15.78 -val morphism = Morphism;
15.79
15.80 -fun binding_morphism binding = morphism {binding = [binding], typ = [], term = [], fact = []};
15.81 -fun typ_morphism typ = morphism {binding = [], typ = [typ], term = [], fact = []};
15.82 -fun term_morphism term = morphism {binding = [], typ = [], term = [term], fact = []};
15.83 -fun fact_morphism fact = morphism {binding = [], typ = [], term = [], fact = [fact]};
15.84 -fun thm_morphism thm = morphism {binding = [], typ = [], term = [], fact = [map thm]};
15.85 -val transfer_morphism = thm_morphism o Thm.transfer;
15.86 +fun morphism a {binding, typ, term, fact} =
15.87 + Morphism {
15.88 + names = if a = "" then [] else [a],
15.89 + binding = map (pair a) binding,
15.90 + typ = map (pair a) typ,
15.91 + term = map (pair a) term,
15.92 + fact = map (pair a) fact};
15.93
15.94 -val identity = morphism {binding = [], typ = [], term = [], fact = []};
15.95 +fun binding_morphism a binding = morphism a {binding = [binding], typ = [], term = [], fact = []};
15.96 +fun typ_morphism a typ = morphism a {binding = [], typ = [typ], term = [], fact = []};
15.97 +fun term_morphism a term = morphism a {binding = [], typ = [], term = [term], fact = []};
15.98 +fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]};
15.99 +fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
15.100 +val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
15.101 +
15.102 +val identity = morphism "" {binding = [], typ = [], term = [], fact = []};
15.103 +
15.104 +
15.105 +(* morphism combinators *)
15.106
15.107 fun compose
15.108 - (Morphism {binding = binding1, typ = typ1, term = term1, fact = fact1})
15.109 - (Morphism {binding = binding2, typ = typ2, term = term2, fact = fact2}) =
15.110 - morphism {binding = binding1 @ binding2, typ = typ1 @ typ2,
15.111 - term = term1 @ term2, fact = fact1 @ fact2};
15.112 + (Morphism {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1})
15.113 + (Morphism {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2}) =
15.114 + Morphism {
15.115 + names = names1 @ names2,
15.116 + binding = binding1 @ binding2,
15.117 + typ = typ1 @ typ2,
15.118 + term = term1 @ term2,
15.119 + fact = fact1 @ fact2};
15.120
15.121 fun phi1 $> phi2 = compose phi2 phi1;
15.122
16.1 --- a/src/Pure/variable.ML Sat Dec 14 07:26:45 2013 +0800
16.2 +++ b/src/Pure/variable.ML Sat Dec 14 07:45:30 2013 +0800
16.3 @@ -461,7 +461,9 @@
16.4 val fact = export inner outer;
16.5 val term = singleton (export_terms inner outer);
16.6 val typ = Logic.type_map term;
16.7 - in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [fact]} end;
16.8 + in
16.9 + Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]}
16.10 + end;
16.11
16.12
16.13