1.1 --- a/src/Pure/Isar/element.ML Wed Jan 21 20:24:44 2009 +0100
1.2 +++ b/src/Pure/Isar/element.ML Wed Jan 21 22:26:48 2009 +0100
1.3 @@ -23,20 +23,12 @@
1.4 val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
1.5 (Attrib.binding * ('fact * Attrib.src list) list) list ->
1.6 (Attrib.binding * ('c * Attrib.src list) list) list
1.7 - val map_ctxt': {binding: binding -> binding,
1.8 - var: binding * mixfix -> binding * mixfix,
1.9 - typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c,
1.10 - attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
1.11 - val map_ctxt: {binding: binding -> binding,
1.12 - var: binding * mixfix -> binding * mixfix,
1.13 - typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
1.14 - attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
1.15 + val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
1.16 + pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} ->
1.17 + ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
1.18 val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
1.19 ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
1.20 val morph_ctxt: morphism -> context_i -> context_i
1.21 - val params_of: context_i -> (string * typ) list
1.22 - val prems_of: context_i -> term list
1.23 - val facts_of: theory -> context_i -> (Attrib.binding * (thm list * Attrib.src list) list) list
1.24 val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
1.25 val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
1.26 val pretty_statement: Proof.context -> string -> thm -> Pretty.T
1.27 @@ -51,14 +43,6 @@
1.28 val morph_witness: morphism -> witness -> witness
1.29 val conclude_witness: witness -> thm
1.30 val pretty_witness: Proof.context -> witness -> Pretty.T
1.31 - val rename: (string * (string * mixfix option)) list -> string -> string
1.32 - val rename_var_name: (string * (string * mixfix option)) list ->
1.33 - string * mixfix -> string * mixfix
1.34 - val rename_var: (string * (string * mixfix option)) list ->
1.35 - binding * mixfix -> binding * mixfix
1.36 - val rename_term: (string * (string * mixfix option)) list -> term -> term
1.37 - val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
1.38 - val rename_morphism: (string * (string * mixfix option)) list -> morphism
1.39 val instT_type: typ Symtab.table -> typ -> typ
1.40 val instT_term: typ Symtab.table -> term -> term
1.41 val instT_thm: theory -> typ Symtab.table -> thm -> thm
1.42 @@ -109,53 +93,29 @@
1.43
1.44 fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
1.45
1.46 -fun map_ctxt' {binding, var, typ, term, pat, fact, attrib} =
1.47 - fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
1.48 - let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
1.49 +fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
1.50 + fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
1.51 | Constrains xs => Constrains (xs |> map (fn (x, T) =>
1.52 - let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
1.53 + (Binding.base_name (binding (Binding.name x)), typ T)))
1.54 | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
1.55 - ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pat ps)))))
1.56 + ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
1.57 | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
1.58 - ((binding a, map attrib atts), (term t, map pat ps))))
1.59 + ((binding a, map attrib atts), (term t, map pattern ps))))
1.60 | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
1.61 ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
1.62
1.63 -fun map_ctxt {binding, var, typ, term, fact, attrib} =
1.64 - map_ctxt' {binding = binding, var = var, typ = typ, term = term, pat = term,
1.65 - fact = fact, attrib = attrib}
1.66 -
1.67 fun map_ctxt_attrib attrib =
1.68 - map_ctxt {binding = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
1.69 + map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
1.70
1.71 fun morph_ctxt phi = map_ctxt
1.72 {binding = Morphism.binding phi,
1.73 - var = Morphism.var phi,
1.74 typ = Morphism.typ phi,
1.75 term = Morphism.term phi,
1.76 + pattern = Morphism.term phi,
1.77 fact = Morphism.fact phi,
1.78 attrib = Args.morph_values phi};
1.79
1.80
1.81 -(* logical content *)
1.82 -
1.83 -fun params_of (Fixes fixes) = fixes |> map
1.84 - (fn (x, SOME T, _) => (Binding.base_name x, T)
1.85 - | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Binding.display x), []))
1.86 - | params_of _ = [];
1.87 -
1.88 -fun prems_of (Assumes asms) = maps (map fst o snd) asms
1.89 - | prems_of (Defines defs) = map (fst o snd) defs
1.90 - | prems_of _ = [];
1.91 -
1.92 -fun assume thy t = Assumption.assume (Thm.cterm_of thy t);
1.93 -
1.94 -fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms
1.95 - | facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs
1.96 - | facts_of _ (Notes (_, facts)) = facts
1.97 - | facts_of _ _ = [];
1.98 -
1.99 -
1.100
1.101 (** pretty printing **)
1.102
1.103 @@ -165,9 +125,8 @@
1.104 map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
1.105
1.106 fun pretty_name_atts ctxt (b, atts) sep =
1.107 - let
1.108 - val name = Binding.display b;
1.109 - in if name = "" andalso null atts then []
1.110 + let val name = Binding.display b in
1.111 + if name = "" andalso null atts then []
1.112 else [Pretty.block
1.113 (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
1.114 end;
1.115 @@ -307,6 +266,7 @@
1.116 Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
1.117 Tactic.rtac Drule.protectI 1 THEN tac)));
1.118
1.119 +
1.120 local
1.121
1.122 val refine_witness =
1.123 @@ -320,8 +280,7 @@
1.124 val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss
1.125 @ [map (rpair []) eq_props];
1.126 fun after_qed' thmss =
1.127 - let
1.128 - val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
1.129 + let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
1.130 in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
1.131 in proof after_qed' propss #> refine_witness #> Seq.hd end;
1.132
1.133 @@ -340,7 +299,8 @@
1.134 cmd NONE after_qed' (map (pair (Binding.empty, [])) propss))
1.135 (fn wits => fn _ => after_qed wits) wit_propss [];
1.136
1.137 -end; (*local*)
1.138 +end;
1.139 +
1.140
1.141 fun compose_witness (Witness (_, th)) r =
1.142 let
1.143 @@ -398,50 +358,6 @@
1.144 end;
1.145
1.146
1.147 -(* rename *)
1.148 -
1.149 -fun rename ren x =
1.150 - (case AList.lookup (op =) ren (x: string) of
1.151 - NONE => x
1.152 - | SOME (x', _) => x');
1.153 -
1.154 -fun rename_var_name ren (x, mx) =
1.155 - (case (AList.lookup (op =) ren x, mx) of
1.156 - (NONE, _) => (x, mx)
1.157 - | (SOME (x', NONE), Structure) => (x', mx)
1.158 - | (SOME (x', SOME _), Structure) =>
1.159 - error ("Attempt to change syntax of structure parameter " ^ quote x)
1.160 - | (SOME (x', NONE), _) => (x', NoSyn)
1.161 - | (SOME (x', SOME mx'), _) => (x', mx'));
1.162 -
1.163 -fun rename_var ren (b, mx) =
1.164 - let
1.165 - val x = Binding.base_name b;
1.166 - val (x', mx') = rename_var_name ren (x, mx);
1.167 - in (Binding.name x', mx') end;
1.168 -
1.169 -fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
1.170 - | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
1.171 - | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
1.172 - | rename_term _ a = a;
1.173 -
1.174 -fun rename_thm ren th =
1.175 - let
1.176 - val thy = Thm.theory_of_thm th;
1.177 - val subst = (Thm.fold_terms o Term.fold_aterms)
1.178 - (fn Free (x, T) =>
1.179 - let val x' = rename ren x
1.180 - in if x = x' then I else insert (eq_fst (op =)) ((x, T), Free (x', T)) end
1.181 - | _ => I) th [];
1.182 - in
1.183 - if null subst then th
1.184 - else th |> hyps_rule (instantiate_frees thy subst)
1.185 - end;
1.186 -
1.187 -fun rename_morphism ren = Morphism.morphism
1.188 - {binding = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)};
1.189 -
1.190 -
1.191 (* instantiate types *)
1.192
1.193 fun instT_type env =
1.194 @@ -467,7 +383,7 @@
1.195 fun instT_morphism thy env =
1.196 let val thy_ref = Theory.check_thy thy in
1.197 Morphism.morphism
1.198 - {binding = I, var = I,
1.199 + {binding = I,
1.200 typ = instT_type env,
1.201 term = instT_term env,
1.202 fact = map (fn th => instT_thm (Theory.deref thy_ref) env th)}
1.203 @@ -516,7 +432,7 @@
1.204 fun inst_morphism thy envs =
1.205 let val thy_ref = Theory.check_thy thy in
1.206 Morphism.morphism
1.207 - {binding = I, var = I,
1.208 + {binding = I,
1.209 typ = instT_type (#1 envs),
1.210 term = inst_term envs,
1.211 fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)}
1.212 @@ -530,15 +446,15 @@
1.213 NONE => I
1.214 | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
1.215
1.216 -fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns);
1.217 -
1.218 -fun satisfy_facts witns = facts_map (morph_ctxt (satisfy_morphism witns));
1.219 +val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
1.220 +val satisfy_facts = facts_map o morph_ctxt o satisfy_morphism;
1.221
1.222
1.223 (* rewriting with equalities *)
1.224
1.225 fun eq_morphism thy thms = Morphism.morphism
1.226 - {binding = I, var = I, typ = I,
1.227 + {binding = I,
1.228 + typ = I,
1.229 term = MetaSimplifier.rewrite_term thy thms [],
1.230 fact = map (MetaSimplifier.rewrite_rule thms)};
1.231
1.232 @@ -555,18 +471,16 @@
1.233 val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer;
1.234 val exp_term = Drule.term_rule thy (singleton exp_fact);
1.235 val exp_typ = Logic.type_map exp_term;
1.236 - val morphism =
1.237 - Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
1.238 + val morphism = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
1.239 in facts_map (morph_ctxt morphism) facts end;
1.240
1.241
1.242 (* transfer to theory using closure *)
1.243
1.244 fun transfer_morphism thy =
1.245 - let val thy_ref = Theory.check_thy thy in
1.246 - Morphism.morphism {binding = I, var = I, typ = I, term = I,
1.247 - fact = map (fn th => transfer (Theory.deref thy_ref) th)}
1.248 - end;
1.249 + let val thy_ref = Theory.check_thy thy
1.250 + in Morphism.thm_morphism (fn th => transfer (Theory.deref thy_ref) th) end;
1.251 +
1.252
1.253
1.254 (** activate in context, return elements and facts **)
1.255 @@ -613,11 +527,14 @@
1.256 if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
1.257 else name;
1.258
1.259 -fun prep_facts prep_name get intern ctxt elem = elem |> map_ctxt
1.260 - {var = I, typ = I, term = I,
1.261 - binding = Binding.map_base prep_name,
1.262 - fact = get ctxt,
1.263 - attrib = intern (ProofContext.theory_of ctxt)};
1.264 +fun prep_facts prep_name get intern ctxt =
1.265 + map_ctxt
1.266 + {binding = Binding.map_base prep_name,
1.267 + typ = I,
1.268 + term = I,
1.269 + pattern = I,
1.270 + fact = get ctxt,
1.271 + attrib = intern (ProofContext.theory_of ctxt)};
1.272
1.273 in
1.274