src/Pure/Isar/element.ML
changeset 29603 b660ee46f2f6
parent 29578 8c4e961fcb08
child 30211 556d1810cdad
child 30240 5b25fee0362c
     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