# HG changeset patch # User wenzelm # Date 1232573208 -3600 # Node ID b660ee46f2f665892ffe86b5a8ba1bf97e852275 # Parent f1583c12b5d0e3d89a70df50ac06f34782b0e4ca eliminated obsolete var morphism; simplified map_ctxt: just one version, without var; removed obsolete params_of, prems_of, facts_of; removed obsolete rename operations; tuned; diff -r f1583c12b5d0 -r b660ee46f2f6 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Wed Jan 21 20:24:44 2009 +0100 +++ b/src/Pure/Isar/element.ML Wed Jan 21 22:26:48 2009 +0100 @@ -23,20 +23,12 @@ val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) -> (Attrib.binding * ('fact * Attrib.src list) list) list -> (Attrib.binding * ('c * Attrib.src list) list) list - val map_ctxt': {binding: binding -> binding, - var: binding * mixfix -> binding * mixfix, - typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c, - attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt - val map_ctxt: {binding: binding -> binding, - var: binding * mixfix -> binding * mixfix, - typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c, - attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt + val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b, + pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} -> + ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt val map_ctxt_attrib: (Attrib.src -> Attrib.src) -> ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt val morph_ctxt: morphism -> context_i -> context_i - val params_of: context_i -> (string * typ) list - val prems_of: context_i -> term list - val facts_of: theory -> context_i -> (Attrib.binding * (thm list * Attrib.src list) list) list val pretty_stmt: Proof.context -> statement_i -> Pretty.T list val pretty_ctxt: Proof.context -> context_i -> Pretty.T list val pretty_statement: Proof.context -> string -> thm -> Pretty.T @@ -51,14 +43,6 @@ val morph_witness: morphism -> witness -> witness val conclude_witness: witness -> thm val pretty_witness: Proof.context -> witness -> Pretty.T - val rename: (string * (string * mixfix option)) list -> string -> string - val rename_var_name: (string * (string * mixfix option)) list -> - string * mixfix -> string * mixfix - val rename_var: (string * (string * mixfix option)) list -> - binding * mixfix -> binding * mixfix - val rename_term: (string * (string * mixfix option)) list -> term -> term - val rename_thm: (string * (string * mixfix option)) list -> thm -> thm - val rename_morphism: (string * (string * mixfix option)) list -> morphism val instT_type: typ Symtab.table -> typ -> typ val instT_term: typ Symtab.table -> term -> term val instT_thm: theory -> typ Symtab.table -> thm -> thm @@ -109,53 +93,29 @@ fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts'); -fun map_ctxt' {binding, var, typ, term, pat, fact, attrib} = - fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => - let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end)) +fun map_ctxt {binding, typ, term, pattern, fact, attrib} = + fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx))) | Constrains xs => Constrains (xs |> map (fn (x, T) => - let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end)) + (Binding.base_name (binding (Binding.name x)), typ T))) | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => - ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pat ps))))) + ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps))))) | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => - ((binding a, map attrib atts), (term t, map pat ps)))) + ((binding a, map attrib atts), (term t, map pattern ps)))) | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) => ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))); -fun map_ctxt {binding, var, typ, term, fact, attrib} = - map_ctxt' {binding = binding, var = var, typ = typ, term = term, pat = term, - fact = fact, attrib = attrib} - fun map_ctxt_attrib attrib = - map_ctxt {binding = I, var = I, typ = I, term = I, fact = I, attrib = attrib}; + map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib}; fun morph_ctxt phi = map_ctxt {binding = Morphism.binding phi, - var = Morphism.var phi, typ = Morphism.typ phi, term = Morphism.term phi, + pattern = Morphism.term phi, fact = Morphism.fact phi, attrib = Args.morph_values phi}; -(* logical content *) - -fun params_of (Fixes fixes) = fixes |> map - (fn (x, SOME T, _) => (Binding.base_name x, T) - | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Binding.display x), [])) - | params_of _ = []; - -fun prems_of (Assumes asms) = maps (map fst o snd) asms - | prems_of (Defines defs) = map (fst o snd) defs - | prems_of _ = []; - -fun assume thy t = Assumption.assume (Thm.cterm_of thy t); - -fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms - | facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs - | facts_of _ (Notes (_, facts)) = facts - | facts_of _ _ = []; - - (** pretty printing **) @@ -165,9 +125,8 @@ map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys; fun pretty_name_atts ctxt (b, atts) sep = - let - val name = Binding.display b; - in if name = "" andalso null atts then [] + let val name = Binding.display b in + if name = "" andalso null atts then [] else [Pretty.block (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))] end; @@ -307,6 +266,7 @@ Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ => Tactic.rtac Drule.protectI 1 THEN tac))); + local val refine_witness = @@ -320,8 +280,7 @@ val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss @ [map (rpair []) eq_props]; fun after_qed' thmss = - let - val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss); + let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss); in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end; in proof after_qed' propss #> refine_witness #> Seq.hd end; @@ -340,7 +299,8 @@ cmd NONE after_qed' (map (pair (Binding.empty, [])) propss)) (fn wits => fn _ => after_qed wits) wit_propss []; -end; (*local*) +end; + fun compose_witness (Witness (_, th)) r = let @@ -398,50 +358,6 @@ end; -(* rename *) - -fun rename ren x = - (case AList.lookup (op =) ren (x: string) of - NONE => x - | SOME (x', _) => x'); - -fun rename_var_name ren (x, mx) = - (case (AList.lookup (op =) ren x, mx) of - (NONE, _) => (x, mx) - | (SOME (x', NONE), Structure) => (x', mx) - | (SOME (x', SOME _), Structure) => - error ("Attempt to change syntax of structure parameter " ^ quote x) - | (SOME (x', NONE), _) => (x', NoSyn) - | (SOME (x', SOME mx'), _) => (x', mx')); - -fun rename_var ren (b, mx) = - let - val x = Binding.base_name b; - val (x', mx') = rename_var_name ren (x, mx); - in (Binding.name x', mx') end; - -fun rename_term ren (Free (x, T)) = Free (rename ren x, T) - | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u - | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t) - | rename_term _ a = a; - -fun rename_thm ren th = - let - val thy = Thm.theory_of_thm th; - val subst = (Thm.fold_terms o Term.fold_aterms) - (fn Free (x, T) => - let val x' = rename ren x - in if x = x' then I else insert (eq_fst (op =)) ((x, T), Free (x', T)) end - | _ => I) th []; - in - if null subst then th - else th |> hyps_rule (instantiate_frees thy subst) - end; - -fun rename_morphism ren = Morphism.morphism - {binding = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)}; - - (* instantiate types *) fun instT_type env = @@ -467,7 +383,7 @@ fun instT_morphism thy env = let val thy_ref = Theory.check_thy thy in Morphism.morphism - {binding = I, var = I, + {binding = I, typ = instT_type env, term = instT_term env, fact = map (fn th => instT_thm (Theory.deref thy_ref) env th)} @@ -516,7 +432,7 @@ fun inst_morphism thy envs = let val thy_ref = Theory.check_thy thy in Morphism.morphism - {binding = I, var = I, + {binding = I, typ = instT_type (#1 envs), term = inst_term envs, fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)} @@ -530,15 +446,15 @@ NONE => I | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm)); -fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns); - -fun satisfy_facts witns = facts_map (morph_ctxt (satisfy_morphism witns)); +val satisfy_morphism = Morphism.thm_morphism o satisfy_thm; +val satisfy_facts = facts_map o morph_ctxt o satisfy_morphism; (* rewriting with equalities *) fun eq_morphism thy thms = Morphism.morphism - {binding = I, var = I, typ = I, + {binding = I, + typ = I, term = MetaSimplifier.rewrite_term thy thms [], fact = map (MetaSimplifier.rewrite_rule thms)}; @@ -555,18 +471,16 @@ val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer; val exp_term = Drule.term_rule thy (singleton exp_fact); val exp_typ = Logic.type_map exp_term; - val morphism = - Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; + val morphism = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact}; in facts_map (morph_ctxt morphism) facts end; (* transfer to theory using closure *) fun transfer_morphism thy = - let val thy_ref = Theory.check_thy thy in - Morphism.morphism {binding = I, var = I, typ = I, term = I, - fact = map (fn th => transfer (Theory.deref thy_ref) th)} - end; + let val thy_ref = Theory.check_thy thy + in Morphism.thm_morphism (fn th => transfer (Theory.deref thy_ref) th) end; + (** activate in context, return elements and facts **) @@ -613,11 +527,14 @@ if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name) else name; -fun prep_facts prep_name get intern ctxt elem = elem |> map_ctxt - {var = I, typ = I, term = I, - binding = Binding.map_base prep_name, - fact = get ctxt, - attrib = intern (ProofContext.theory_of ctxt)}; +fun prep_facts prep_name get intern ctxt = + map_ctxt + {binding = Binding.map_base prep_name, + typ = I, + term = I, + pattern = I, + fact = get ctxt, + attrib = intern (ProofContext.theory_of ctxt)}; in