src/Pure/Isar/theory_target.ML
changeset 21611 fc95ff1fe738
parent 21594 2859c94d67d4
child 21613 ae3bb930b50f
     1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Nov 30 14:17:36 2006 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Nov 30 14:17:37 2006 +0100
     1.3 @@ -73,47 +73,16 @@
     1.4    in
     1.5      lthy'
     1.6      |> is_loc ? LocalTheory.abbrevs Syntax.default_mode abbrs
     1.7 -    |> LocalDefs.add_defs defs
     1.8 -    |>> map (apsnd snd)
     1.9 +    |> LocalDefs.add_defs defs |>> map (apsnd snd)
    1.10    end;
    1.11  
    1.12  
    1.13 -(* axioms *)
    1.14 -
    1.15 -local
    1.16 -
    1.17 -fun add_axiom hyps (name, prop) thy =
    1.18 -  let
    1.19 -    val name' = if name = "" then "axiom_" ^ serial_string () else name;
    1.20 -    val prop' = Logic.list_implies (hyps, prop);
    1.21 -    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
    1.22 -    val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
    1.23 -    val prems = map (Thm.assume o Thm.cterm_of thy') hyps;
    1.24 -  in (Drule.implies_elim_list axm prems, thy') end;
    1.25 -
    1.26 -in
    1.27 -
    1.28 -fun axioms kind specs lthy =
    1.29 -  let
    1.30 -    val hyps = map Thm.term_of (Assumption.assms_of lthy);
    1.31 -    fun axiom ((name, atts), props) thy = thy
    1.32 -      |> fold_map (add_axiom hyps) (PureThy.name_multi name props)
    1.33 -      |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.34 -  in
    1.35 -    lthy
    1.36 -    |> fold (fold Variable.declare_term o snd) specs
    1.37 -    |> LocalTheory.theory_result (fold_map axiom specs)
    1.38 -    |-> LocalTheory.notes kind
    1.39 -  end;
    1.40 -
    1.41 -end;
    1.42 -
    1.43 -
    1.44  (* defs *)
    1.45  
    1.46  local
    1.47  
    1.48  infix also;
    1.49 +
    1.50  fun eq1 also eq2 =
    1.51    eq2 COMP (eq1 COMP (Drule.incr_indexes2 eq1 eq2 transitive_thm));
    1.52  
    1.53 @@ -159,61 +128,118 @@
    1.54  end;
    1.55  
    1.56  
    1.57 +(* axioms *)
    1.58 +
    1.59 +local
    1.60 +
    1.61 +fun add_axiom hyps (name, prop) thy =
    1.62 +  let
    1.63 +    val name' = if name = "" then "axiom_" ^ serial_string () else name;
    1.64 +    val prop' = Logic.list_implies (hyps, prop);
    1.65 +    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
    1.66 +    val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
    1.67 +    val prems = map (Thm.assume o Thm.cterm_of thy') hyps;
    1.68 +  in (Drule.implies_elim_list axm prems, thy') end;
    1.69 +
    1.70 +in
    1.71 +
    1.72 +fun axioms kind specs lthy =
    1.73 +  let
    1.74 +    val hyps = map Thm.term_of (Assumption.assms_of lthy);
    1.75 +    fun axiom ((name, atts), props) thy = thy
    1.76 +      |> fold_map (add_axiom hyps) (PureThy.name_multi name props)
    1.77 +      |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.78 +  in
    1.79 +    lthy
    1.80 +    |> fold (fold Variable.declare_term o snd) specs
    1.81 +    |> LocalTheory.theory_result (fold_map axiom specs)
    1.82 +    |-> LocalTheory.notes kind
    1.83 +  end;
    1.84 +
    1.85 +end;
    1.86 +
    1.87 +
    1.88  (* notes *)
    1.89  
    1.90 -(* FIXME
    1.91 -fun import_export inner outer (name, raw_th) =
    1.92 +fun import_export_proof ctxt (name, raw_th) =
    1.93    let
    1.94 -    val th = norm_hhf_protect raw_th;
    1.95 -    val (defs, th') = LocalDefs.export inner outer th;
    1.96 -    val n = Thm.nprems_of th' - Thm.nprems_of th;
    1.97 +    val thy = ProofContext.theory_of ctxt;
    1.98 +    val thy_ctxt = ProofContext.init thy;
    1.99 +    val certT = Thm.ctyp_of thy;
   1.100 +    val cert = Thm.cterm_of thy;
   1.101  
   1.102 -    val result = PureThy.name_thm true (name, th');  (* FIXME proper thm definition!? *)
   1.103 -
   1.104 +    (*export assumes/defines*)
   1.105 +    val th = Goal.norm_result raw_th;
   1.106 +    val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
   1.107      val concl_conv = Tactic.rewrite true defs (Thm.cprop_of th);
   1.108 -    val assms = map (Tactic.rewrite_rule defs o Thm.assume) (Assumption.assms_of inner);
   1.109 +    val assms = map (Tactic.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
   1.110 +    val nprems = Thm.nprems_of th' - Thm.nprems_of th;
   1.111 +
   1.112 +    (*export fixes*)
   1.113 +    val tfrees = map TFree (Drule.fold_terms Term.add_tfrees th' []);
   1.114 +    val frees = map Free (Drule.fold_terms Term.add_frees th' []);
   1.115 +    val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
   1.116 +      |> Variable.export ctxt thy_ctxt
   1.117 +      |> Drule.zero_var_indexes_list;
   1.118 +
   1.119 +    (*thm definition*)
   1.120 +    val result = PureThy.name_thm true (name, th'');
   1.121 +
   1.122 +    (*import fixes*)
   1.123 +    val (tvars, vars) =
   1.124 +      chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
   1.125 +      |>> map Logic.dest_type;
   1.126 +
   1.127 +    val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
   1.128 +    val inst = filter (is_Var o fst) (vars ~~ frees);
   1.129 +    val cinstT = map (pairself certT o apfst TVar) instT;
   1.130 +    val cinst = map (pairself (cert o Term.map_types (TermSubst.instantiateT instT))) inst;
   1.131 +    val result' = Thm.instantiate (cinstT, cinst) result;
   1.132 +
   1.133 +    (*import assumes/defines*)
   1.134      val assm_tac = FIRST' (map (fn assm => Tactic.compose_tac (false, assm, 0)) assms);
   1.135 -    val reimported_result =
   1.136 -      (case SINGLE (Seq.INTERVAL assm_tac 1 n) result of
   1.137 -        NONE => raise THM ("Failed to re-import result", 0, [result])
   1.138 -      | SOME res => res) COMP (concl_conv COMP_INCR Drule.equal_elim_rule2);
   1.139 -    val _ = reimported_result COMP (th COMP_INCR Drule.remdups_rl) handle THM _ =>
   1.140 -      (warning "FIXME"; asm_rl);
   1.141 -  in (reimported_result, result) end;
   1.142 -*)
   1.143 -fun import_export inner outer (_, th) =
   1.144 -  (singleton (ProofContext.standard inner) th, Assumption.export false inner outer th);
   1.145 +    val result'' =
   1.146 +      (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
   1.147 +        NONE => raise THM ("Failed to re-import result", 0, [result'])
   1.148 +      | SOME res => res) COMP (concl_conv COMP_INCR Drule.equal_elim_rule2)
   1.149 +      |> Goal.norm_result
   1.150 +      |> Goal.close_result;
   1.151 +
   1.152 +    val _ = result'' COMP (th COMP_INCR Drule.remdups_rl);  (* FIXME *)
   1.153 +  in (result'', result) end;
   1.154 +
   1.155 +fun import_export ctxt (_, raw_th) =
   1.156 +  let
   1.157 +    val thy_ctxt = ProofContext.init (ProofContext.theory_of ctxt);
   1.158 +    val result'' = Goal.close_result (Goal.norm_result raw_th);
   1.159 +    val result = Goal.norm_result (singleton (ProofContext.export ctxt thy_ctxt) result'');
   1.160 +  in (result'', result) end;
   1.161  
   1.162  fun notes loc kind facts lthy =
   1.163    let
   1.164      val is_loc = loc <> "";
   1.165      val thy = ProofContext.theory_of lthy;
   1.166 -    val thy_ctxt = ProofContext.init thy;
   1.167  
   1.168      val facts' = facts
   1.169        |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (fst a)) bs))
   1.170 -      |> PureThy.map_facts (import_export lthy thy_ctxt);
   1.171 -    val local_facts = facts'
   1.172 -      |> PureThy.map_facts #1
   1.173 -      |> Element.facts_map (Element.morph_ctxt (Morphism.thm_morphism Drule.local_standard));
   1.174 -    val global_facts = facts'
   1.175 -      |> PureThy.map_facts #2
   1.176 -      |> Element.generalize_facts lthy thy_ctxt
   1.177 -      |> PureThy.map_facts Drule.local_standard
   1.178 +      |> PureThy.map_facts (import_export lthy);
   1.179 +    val local_facts = PureThy.map_facts #1 facts'
   1.180 +      |> Attrib.map_facts (Attrib.attribute_i thy);
   1.181 +    val target_facts = PureThy.map_facts #1 facts'
   1.182 +      |> is_loc ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy));
   1.183 +    val global_facts = PureThy.map_facts #2 facts'
   1.184        |> Attrib.map_facts (if is_loc then K I else Attrib.attribute_i thy);
   1.185    in
   1.186 -    lthy |> LocalTheory.theory (fn thy => thy
   1.187 -      |> Sign.qualified_names
   1.188 -      |> PureThy.note_thmss_i kind global_facts |> #2
   1.189 -      |> Sign.restore_naming thy)
   1.190 +    lthy |> LocalTheory.theory
   1.191 +      (Sign.qualified_names
   1.192 +        #> PureThy.note_thmss_i kind global_facts #> snd
   1.193 +        #> Sign.restore_naming thy)
   1.194  
   1.195 -    |> is_loc ? (fn lthy' => lthy' |> LocalTheory.target
   1.196 -      (Locale.add_thmss loc kind
   1.197 -        (Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy')) local_facts)))
   1.198 +    |> is_loc ? LocalTheory.target (Locale.add_thmss loc kind target_facts)
   1.199  
   1.200      |> ProofContext.set_stmt true
   1.201      |> ProofContext.qualified_names
   1.202 -    |> ProofContext.note_thmss_i kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
   1.203 +    |> ProofContext.note_thmss_i kind local_facts
   1.204      ||> ProofContext.restore_naming lthy
   1.205      ||> ProofContext.restore_stmt lthy
   1.206    end;
   1.207 @@ -221,19 +247,19 @@
   1.208  
   1.209  (* target declarations *)
   1.210  
   1.211 -fun decl _ "" f =
   1.212 +fun target_decl _ "" f =
   1.213        LocalTheory.theory (Context.theory_map (f Morphism.identity)) #>
   1.214        LocalTheory.target (Context.proof_map (f Morphism.identity))
   1.215 -  | decl add loc f =
   1.216 +  | target_decl add loc f =
   1.217        LocalTheory.target (add loc (Context.proof_map o f));
   1.218  
   1.219 -val type_syntax = decl Locale.add_type_syntax;
   1.220 -val term_syntax = decl Locale.add_term_syntax;
   1.221 -val declaration = decl Locale.add_declaration;
   1.222 +val type_syntax = target_decl Locale.add_type_syntax;
   1.223 +val term_syntax = target_decl Locale.add_term_syntax;
   1.224 +val declaration = target_decl Locale.add_declaration;
   1.225  
   1.226  fun target_morphism loc lthy =
   1.227    ProofContext.export_morphism lthy (LocalTheory.target_of lthy) $>
   1.228 -  Morphism.thm_morphism Drule.local_standard;
   1.229 +  Morphism.thm_morphism (Goal.close_result o Goal.norm_result);
   1.230  
   1.231  fun target_name "" lthy = Sign.full_name (ProofContext.theory_of lthy)
   1.232    | target_name _ lthy = ProofContext.full_name (LocalTheory.target_of lthy);