disallow hyps in export;
authorwenzelm
Fri Jun 29 14:19:52 2018 +0200 (13 months ago)
changeset 685396740e3611a86
parent 68538 0903c4c8b455
child 68540 000a0e062529
disallow hyps in export;
handle extra shyps as explicit sort constraints;
src/Pure/Thy/export_theory.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Fri Jun 29 14:02:14 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Jun 29 14:19:52 2018 +0200
     1.3 @@ -102,6 +102,12 @@
     1.4  
     1.5      (* axioms and facts *)
     1.6  
     1.7 +    val standard_prop_of =
     1.8 +      Thm.transfer thy #>
     1.9 +      Thm.check_hyps (Context.Theory thy) #>
    1.10 +      Drule.sort_constraint_intr_shyps #>
    1.11 +      Thm.full_prop_of;
    1.12 +
    1.13      val encode_props =
    1.14        let open XML.Encode Term_XML.Encode
    1.15        in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
    1.16 @@ -114,7 +120,7 @@
    1.17        in encode_props (typargs, args, props') end;
    1.18  
    1.19      val export_axiom = export_props o single;
    1.20 -    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
    1.21 +    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of;
    1.22  
    1.23      val _ =
    1.24        export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
     2.1 --- a/src/Pure/drule.ML	Fri Jun 29 14:02:14 2018 +0200
     2.2 +++ b/src/Pure/drule.ML	Fri Jun 29 14:19:52 2018 +0200
     2.3 @@ -98,6 +98,8 @@
     2.4    val is_sort_constraint: term -> bool
     2.5    val sort_constraintI: thm
     2.6    val sort_constraint_eq: thm
     2.7 +  val sort_constraint_intr: indexname * sort -> thm -> thm
     2.8 +  val sort_constraint_intr_shyps: thm -> thm
     2.9    val with_subgoal: int -> (thm -> thm) -> thm -> thm
    2.10    val comp_no_flatten: thm * int -> int -> thm -> thm
    2.11    val rename_bvars: (string * string) list -> thm -> thm
    2.12 @@ -647,6 +649,26 @@
    2.13          (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
    2.14        (implies_intr_list [A, C] (Thm.assume A)));
    2.15  
    2.16 +val sort_constraint_eq' = Thm.symmetric sort_constraint_eq;
    2.17 +
    2.18 +fun sort_constraint_intr tvar thm =
    2.19 +  Thm.equal_elim
    2.20 +    (Thm.instantiate
    2.21 +      ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))],
    2.22 +       [((("A", 0), propT), Thm.cprop_of thm)])
    2.23 +      sort_constraint_eq') thm;
    2.24 +
    2.25 +fun sort_constraint_intr_shyps raw_thm =
    2.26 +  let val thm = Thm.strip_shyps raw_thm in
    2.27 +    (case Thm.extra_shyps thm of
    2.28 +      [] => thm
    2.29 +    | shyps =>
    2.30 +        let
    2.31 +          val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm []));
    2.32 +          val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps;
    2.33 +        in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end)
    2.34 +  end;
    2.35 +
    2.36  end;
    2.37  
    2.38