--- a/src/HOL/Import/Import_Setup.thy Thu Jan 16 12:12:32 2025 +0100
+++ b/src/HOL/Import/Import_Setup.thy Thu Jan 16 12:41:55 2025 +0100
@@ -3,7 +3,7 @@
Author: Alexander Krauss, QAware GmbH
*)
-section \<open>Importer machinery and required theorems\<close>
+section \<open>Importer machinery\<close>
theory Import_Setup
imports Main
@@ -11,19 +11,6 @@
begin
ML_file \<open>import_data.ML\<close>
-
-lemma light_ex_imp_nonempty: "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
- by auto
-
-lemma typedef_hol2hollight:
- "type_definition Rep Abs (Collect P) \<Longrightarrow> Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
- by (metis type_definition.Rep_inverse type_definition.Abs_inverse
- type_definition.Rep mem_Collect_eq)
-
-lemma ext2: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
- by (rule ext)
-
ML_file \<open>import_rule.ML\<close>
end
-
--- a/src/HOL/Import/import_rule.ML Thu Jan 16 12:12:32 2025 +0100
+++ b/src/HOL/Import/import_rule.ML Thu Jan 16 12:41:55 2025 +0100
@@ -152,7 +152,7 @@
val th3 = implies_elim_all th2
val th4 = Thm.forall_intr cv th3
val i = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
- [SOME ll, SOME lr] @{thm ext2}
+ [SOME ll, SOME lr] @{lemma "(\<And>x. f x = g x) \<Longrightarrow> f = g" by (rule ext)}
in
meta_mp i th4
end
@@ -193,6 +193,12 @@
end
| NONE => def' constname rhs thy
+fun typedef_hol2hollight nty oty rep abs pred a r =
+ Thm.instantiate' [SOME nty, SOME oty] [SOME rep, SOME abs, SOME pred, SOME a, SOME r]
+ @{lemma "type_definition Rep Abs (Collect P) \<Longrightarrow> Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
+ by (metis type_definition.Rep_inverse type_definition.Abs_inverse
+ type_definition.Rep mem_Collect_eq)}
+
fun typedef_hollight th thy =
let
val (th_s, cn) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
@@ -201,15 +207,16 @@
val P = Thm.dest_arg cn
val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
in
- Thm.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
- SOME (Thm.global_cterm_of thy (Free ("a", Thm.typ_of nty))),
- SOME (Thm.global_cterm_of thy (Free ("r", Thm.typ_of oty)))] @{thm typedef_hol2hollight}
+ typedef_hol2hollight nty oty rept abst P
+ (Thm.global_cterm_of thy (Free ("a", Thm.typ_of nty)))
+ (Thm.global_cterm_of thy (Free ("r", Thm.typ_of oty)))
end
fun tydef' tycname abs_name rep_name cP ct td_th thy =
let
val ctT = Thm.ctyp_of_cterm ct
- val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
+ val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct]
+ @{lemma "P t \<Longrightarrow> \<exists>x. x \<in> Collect P" by auto}
val th2 = meta_mp nonempty td_th
val c =
case Thm.concl_of th2 of
@@ -233,11 +240,9 @@
val rept = Thm.dest_arg th_s
val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
val typedef_th =
- Thm.instantiate'
- [SOME nty, SOME oty]
- [SOME rept, SOME abst, SOME cP, SOME (Thm.global_cterm_of thy' (Free ("a", aty))),
- SOME (Thm.global_cterm_of thy' (Free ("r", Thm.typ_of ctT)))]
- @{thm typedef_hol2hollight}
+ typedef_hol2hollight nty oty rept abst cP
+ (Thm.global_cterm_of thy' (Free ("a", aty)))
+ (Thm.global_cterm_of thy' (Free ("r", Thm.typ_of ctT)))
val th4 = typedef_th OF [#type_definition (#2 typedef_info)]
in
(th4, thy')