--- a/etc/build.props Fri Jan 17 12:17:37 2025 +0100
+++ b/etc/build.props Fri Jan 17 21:30:08 2025 +0100
@@ -27,6 +27,7 @@
src/Pure/Admin/component_eptcs.scala \
src/Pure/Admin/component_foiltex.scala \
src/Pure/Admin/component_fonts.scala \
+ src/Pure/Admin/component_hol_light.scala \
src/Pure/Admin/component_hugo.scala \
src/Pure/Admin/component_javamail.scala \
src/Pure/Admin/component_jcef.scala \
--- a/etc/settings Fri Jan 17 12:17:37 2025 +0100
+++ b/etc/settings Fri Jan 17 21:30:08 2025 +0100
@@ -164,7 +164,7 @@
ISABELLE_OPAM_ROOT="$USER_HOME/.opam"
-ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.12.0"
+ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.14.1"
###
--- a/lib/Tools/ocaml_setup Fri Jan 17 12:17:37 2025 +0100
+++ b/lib/Tools/ocaml_setup Fri Jan 17 21:30:08 2025 +0100
@@ -2,20 +2,6 @@
#
# Author: Makarius
#
-# DESCRIPTION: setup OCaml via OPAM
-
-set -e
+# DESCRIPTION: setup OCaml for Isabelle via OPAM
-if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]
-then
- isabelle_opam switch -y "$ISABELLE_OCAML_VERSION"
-elif [ -e "$ISABELLE_OPAM_ROOT/config" ]
-then
- isabelle_opam switch create -y "$ISABELLE_OCAML_VERSION"
-else
- mkdir -p "$ISABELLE_OPAM_ROOT"
- cd "$ISABELLE_OPAM_ROOT"
- isabelle_opam init -y --disable-sandboxing --no-setup --compiler="$ISABELLE_OCAML_VERSION"
-fi
-
-isabelle_opam install -y zarith
+isabelle ocaml_setup_base && isabelle_opam install -y zarith
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocaml_setup_base Fri Jan 17 21:30:08 2025 +0100
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: setup OCaml base compiler via OPAM
+
+set -e
+
+if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]
+then
+ isabelle_opam switch -y "$ISABELLE_OCAML_VERSION"
+elif [ -e "$ISABELLE_OPAM_ROOT/config" ]
+then
+ isabelle_opam switch create -y "$ISABELLE_OCAML_VERSION"
+else
+ mkdir -p "$ISABELLE_OPAM_ROOT"
+ cd "$ISABELLE_OPAM_ROOT"
+ isabelle_opam init -y --disable-sandboxing --no-setup --compiler="$ISABELLE_OCAML_VERSION"
+fi
--- a/src/HOL/Import/Import_Setup.thy Fri Jan 17 12:17:37 2025 +0100
+++ b/src/HOL/Import/Import_Setup.thy Fri Jan 17 21:30:08 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,22 +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:
- assumes a: "type_definition Rep Abs (Collect P)"
- shows "Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
- by (metis type_definition.Rep_inverse type_definition.Abs_inverse
- type_definition.Rep a mem_Collect_eq)
-
-lemma ext2:
- "(\<And>x. f x = g x) \<Longrightarrow> f = g"
- by auto
-
ML_file \<open>import_rule.ML\<close>
end
-
--- a/src/HOL/Import/import_data.ML Fri Jan 17 12:17:37 2025 +0100
+++ b/src/HOL/Import/import_data.ML Fri Jan 17 21:30:08 2025 +0100
@@ -7,11 +7,10 @@
signature IMPORT_DATA =
sig
- val get_const_map : string -> theory -> string option
- val get_typ_map : string -> theory -> string option
- val get_const_def : string -> theory -> thm option
- val get_typ_def : string -> theory -> thm option
-
+ val get_const_map : theory -> string -> string option
+ val get_typ_map : theory -> string -> string option
+ val get_const_def : theory -> string -> thm option
+ val get_typ_def : theory -> string -> thm option
val add_const_map : string -> string -> theory -> theory
val add_const_map_cmd : string -> string -> theory -> theory
val add_typ_map : string -> string -> theory -> theory
@@ -25,114 +24,110 @@
structure Data = Theory_Data
(
- type T = {const_map: string Symtab.table, ty_map: string Symtab.table,
- const_def: thm Symtab.table, ty_def: thm Symtab.table}
- val empty = {const_map = Symtab.empty, ty_map = Symtab.empty,
- const_def = Symtab.empty, ty_def = Symtab.empty}
+ type T =
+ {const_map: string Symtab.table, ty_map: string Symtab.table,
+ const_def: thm Symtab.table, ty_def: thm Symtab.table}
+ val empty =
+ {const_map = Symtab.empty, ty_map = Symtab.empty,
+ const_def = Symtab.empty, ty_def = Symtab.empty}
fun merge
({const_map = cm1, ty_map = tm1, const_def = cd1, ty_def = td1},
{const_map = cm2, ty_map = tm2, const_def = cd2, ty_def = td2}) : T =
{const_map = Symtab.merge (K true) (cm1, cm2), ty_map = Symtab.merge (K true) (tm1, tm2),
- const_def = Symtab.merge (K true) (cd1, cd2), ty_def = Symtab.merge (K true) (td1, td2)
- }
+ const_def = Symtab.merge (K true) (cd1, cd2), ty_def = Symtab.merge (K true) (td1, td2)}
)
-fun get_const_map s thy = Symtab.lookup (#const_map (Data.get thy)) s
-
-fun get_typ_map s thy = Symtab.lookup (#ty_map (Data.get thy)) s
-
-fun get_const_def s thy = Symtab.lookup (#const_def (Data.get thy)) s
+val get_const_map = Symtab.lookup o #const_map o Data.get
+val get_typ_map = Symtab.lookup o #ty_map o Data.get
+val get_const_def = Symtab.lookup o #const_def o Data.get
+val get_typ_def = Symtab.lookup o #ty_def o Data.get
-fun get_typ_def s thy = Symtab.lookup (#ty_def (Data.get thy)) s
-
-fun add_const_map s1 s2 thy =
+fun add_const_map c d =
Data.map (fn {const_map, ty_map, const_def, ty_def} =>
- {const_map = (Symtab.update (s1, s2) const_map), ty_map = ty_map,
- const_def = const_def, ty_def = ty_def}) thy
+ {const_map = Symtab.update (c, d) const_map, ty_map = ty_map,
+ const_def = const_def, ty_def = ty_def})
-fun add_const_map_cmd s1 raw_s2 thy =
+fun add_const_map_cmd c s thy =
let
val ctxt = Proof_Context.init_global thy
- val Const (s2, _) = Proof_Context.read_const {proper = true, strict = false} ctxt raw_s2
- in add_const_map s1 s2 thy end
+ val d = dest_Const_name (Proof_Context.read_const {proper = true, strict = false} ctxt s)
+ in add_const_map c d thy end
-fun add_typ_map s1 s2 thy =
+fun add_typ_map c d =
Data.map (fn {const_map, ty_map, const_def, ty_def} =>
- {const_map = const_map, ty_map = (Symtab.update (s1, s2) ty_map),
- const_def = const_def, ty_def = ty_def}) thy
+ {const_map = const_map, ty_map = (Symtab.update (c, d) ty_map),
+ const_def = const_def, ty_def = ty_def})
-fun add_typ_map_cmd s1 raw_s2 thy =
+fun add_typ_map_cmd c s thy =
let
val ctxt = Proof_Context.init_global thy
- val Type (s2, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt raw_s2
- in add_typ_map s1 s2 thy end
+ val d = dest_Type_name (Proof_Context.read_type_name {proper = true, strict = false} ctxt s)
+ in add_typ_map c d thy end
-fun add_const_def s th name_opt thy =
+fun add_const_def c th name_opt thy =
let
- val th = Thm.legacy_freezeT th
- val name = case name_opt of
- NONE => dest_Const_name (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th))))
- | SOME n => n
- val thy' = add_const_map s name thy
+ val th' = Thm.legacy_freezeT th
+ val d =
+ (case name_opt of
+ NONE => dest_Const_name (#1 (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))))
+ | SOME d => d)
in
- Data.map (fn {const_map, ty_map, const_def, ty_def} =>
+ thy
+ |> add_const_map c d
+ |> Data.map (fn {const_map, ty_map, const_def, ty_def} =>
{const_map = const_map, ty_map = ty_map,
- const_def = (Symtab.update (s, th) const_def), ty_def = ty_def}) thy'
+ const_def = (Symtab.update (c, th') const_def), ty_def = ty_def})
end
-fun add_typ_def tyname absname repname th thy =
+fun add_typ_def type_name abs_name rep_name th thy =
let
- val th = Thm.legacy_freezeT th
- val (l, _) = dest_comb (HOLogic.dest_Trueprop (Thm.prop_of th))
- val (l, abst) = dest_comb l
- val (_, rept) = dest_comb l
- val absn = dest_Const_name abst
- val repn = dest_Const_name rept
- val nty = domain_type (fastype_of rept)
- val ntyn = dest_Type_name nty
- val thy2 = add_typ_map tyname ntyn thy
- val thy3 = add_const_map absname absn thy2
- val thy4 = add_const_map repname repn thy3
+ val th' = Thm.legacy_freezeT th
+ val \<^Const_>\<open>type_definition A _ for rep abs _\<close> = HOLogic.dest_Trueprop (Thm.prop_of th')
in
- Data.map (fn {const_map, ty_map, const_def, ty_def} =>
+ thy
+ |> add_typ_map type_name (dest_Type_name A)
+ |> add_const_map abs_name (dest_Const_name abs)
+ |> add_const_map rep_name (dest_Const_name rep)
+ |> Data.map (fn {const_map, ty_map, const_def, ty_def} =>
{const_map = const_map, ty_map = ty_map,
- const_def = const_def, ty_def = (Symtab.update (tyname, th) ty_def)}) thy4
+ const_def = const_def, ty_def = (Symtab.update (type_name, th') ty_def)})
end
-val _ = Theory.setup
- (Attrib.setup \<^binding>\<open>import_const\<close>
+val _ =
+ Theory.setup (Attrib.setup \<^binding>\<open>import_const\<close>
(Scan.lift Parse.name --
Scan.option (Scan.lift \<^keyword>\<open>:\<close> |-- Args.const {proper = true, strict = false}) >>
(fn (s1, s2) => Thm.declaration_attribute
(fn th => Context.mapping (add_const_def s1 th s2) I)))
- "declare a theorem as an equality that maps the given constant")
+ "declare a theorem as an equality that maps the given constant")
-val _ = Theory.setup
- (Attrib.setup \<^binding>\<open>import_type\<close>
+val _ =
+ Theory.setup (Attrib.setup \<^binding>\<open>import_type\<close>
(Scan.lift (Parse.name -- Parse.name -- Parse.name) >>
(fn ((tyname, absname), repname) => Thm.declaration_attribute
(fn th => Context.mapping (add_typ_def tyname absname repname th) I)))
- "declare a type_definition theorem as a map for an imported type with abs and rep")
+ "declare a type_definition theorem as a map for an imported type with abs and rep")
val _ =
Outer_Syntax.command \<^command_keyword>\<open>import_type_map\<close>
"map external type name to existing Isabelle/HOL type name"
((Parse.name --| \<^keyword>\<open>:\<close>) -- Parse.type_const >>
- (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
+ (fn (c, d) => Toplevel.theory (add_typ_map_cmd c d)))
val _ =
Outer_Syntax.command \<^command_keyword>\<open>import_const_map\<close>
"map external const name to existing Isabelle/HOL const name"
((Parse.name --| \<^keyword>\<open>:\<close>) -- Parse.const >>
- (fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
+ (fn (c, d) => Toplevel.theory (add_const_map_cmd c d)))
-(* Initial type and constant maps, for types and constants that are not
- defined, which means their definitions do not appear in the proof dump *)
-val _ = Theory.setup
- (add_typ_map "bool" \<^type_name>\<open>bool\<close> #>
- add_typ_map "fun" \<^type_name>\<open>fun\<close> #>
- add_typ_map "ind" \<^type_name>\<open>ind\<close> #>
- add_const_map "=" \<^const_name>\<open>HOL.eq\<close> #>
- add_const_map "@" \<^const_name>\<open>Eps\<close>)
+(*Initial type and constant maps, for types and constants that are not
+ defined, which means their definitions do not appear in the proof dump.*)
+val _ =
+ Theory.setup
+ (add_typ_map "bool" \<^type_name>\<open>bool\<close> #>
+ add_typ_map "fun" \<^type_name>\<open>fun\<close> #>
+ add_typ_map "ind" \<^type_name>\<open>ind\<close> #>
+ add_const_map "=" \<^const_name>\<open>HOL.eq\<close> #>
+ add_const_map "@" \<^const_name>\<open>Eps\<close>)
end
--- a/src/HOL/Import/import_rule.ML Fri Jan 17 12:17:37 2025 +0100
+++ b/src/HOL/Import/import_rule.ML Fri Jan 17 21:30:08 2025 +0100
@@ -18,33 +18,25 @@
val conj2 : thm -> thm
val refl : cterm -> thm
val abs : cterm -> thm -> thm
- val mdef : string -> theory -> thm
+ val mdef : theory -> string -> thm
val def : string -> cterm -> theory -> thm * theory
- val mtydef : string -> theory -> thm
+ val mtydef : theory -> string -> thm
val tydef :
string -> string -> string -> cterm -> cterm -> thm -> theory -> thm * theory
- val inst_type : (ctyp * ctyp) list -> thm -> theory -> thm
+ val inst_type : (ctyp * ctyp) list -> thm -> thm
val inst : (cterm * cterm) list -> thm -> thm
-
- type state
- val init_state : state
- val process_line : string -> (theory * state) -> (theory * state)
- val process_file : Path.T -> theory -> theory
+ val import_file : Path.T -> theory -> theory
end
structure Import_Rule: IMPORT_RULE =
struct
-val init_state = ((Inttab.empty, 0), (Inttab.empty, 0), (Inttab.empty, 0))
-
-type state = (ctyp Inttab.table * int) * (cterm Inttab.table * int) * (thm Inttab.table * int)
-
fun implies_elim_all th = implies_elim_list th (map Thm.assume (cprems_of th))
fun meta_mp th1 th2 =
let
val th1a = implies_elim_all th1
- val th1b = Thm.implies_intr (strip_imp_concl (Thm.cprop_of th2)) th1a
+ val th1b = Thm.implies_intr (Thm.cconcl_of th2) th1a
val th2a = implies_elim_all th2
val th3 = Thm.implies_elim th1b th2a
in
@@ -53,20 +45,19 @@
fun meta_eq_to_obj_eq th =
let
- val (tml, tmr) = Thm.dest_binop (strip_imp_concl (Thm.cprop_of th))
- val cty = Thm.ctyp_of_cterm tml
- val i = Thm.instantiate' [SOME cty] [SOME tml, SOME tmr]
- @{thm meta_eq_to_obj_eq}
+ val (t, u) = Thm.dest_equals (Thm.cconcl_of th)
+ val A = Thm.ctyp_of_cterm t
+ val rl = Thm.instantiate' [SOME A] [SOME t, SOME u] @{thm meta_eq_to_obj_eq}
in
- Thm.implies_elim i th
+ Thm.implies_elim rl th
end
fun beta ct = meta_eq_to_obj_eq (Thm.beta_conversion false ct)
fun eq_mp th1 th2 =
let
- val (tm1l, tm1r) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1)))
- val i1 = Thm.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
+ val (Q, P) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th1))
+ val i1 = Thm.instantiate' [] [SOME Q, SOME P] @{thm iffD1}
val i2 = meta_mp i1 th1
in
meta_mp i2 th2
@@ -74,13 +65,12 @@
fun comb th1 th2 =
let
- val t1c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1))
- val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
- val (cf, cg) = Thm.dest_binop t1c
- val (cx, cy) = Thm.dest_binop t2c
- val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_cterm cf)
- val i1 = Thm.instantiate' [SOME fd, SOME fr]
- [SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong}
+ val t1 = Thm.dest_arg (Thm.cconcl_of th1)
+ val t2 = Thm.dest_arg (Thm.cconcl_of th2)
+ val (f, g) = Thm.dest_binop t1
+ val (x, y) = Thm.dest_binop t2
+ val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm f)
+ val i1 = Thm.instantiate' [SOME A, SOME B] [SOME f, SOME g, SOME x, SOME y] @{thm cong}
val i2 = meta_mp i1 th1
in
meta_mp i2 th2
@@ -88,10 +78,10 @@
fun trans th1 th2 =
let
- val t1c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1))
- val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
- val (r, s) = Thm.dest_binop t1c
- val (_, t) = Thm.dest_binop t2c
+ val t1 = Thm.dest_arg (Thm.cconcl_of th1)
+ val t2 = Thm.dest_arg (Thm.cconcl_of th2)
+ val (r, s) = Thm.dest_binop t1
+ val t = Thm.dest_arg t2
val ty = Thm.ctyp_of_cterm r
val i1 = Thm.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
val i2 = meta_mp i1 th1
@@ -101,14 +91,13 @@
fun deduct th1 th2 =
let
- val th1c = strip_imp_concl (Thm.cprop_of th1)
- val th2c = strip_imp_concl (Thm.cprop_of th2)
+ val th1c = Thm.cconcl_of th1
+ val th2c = Thm.cconcl_of th2
val th1a = implies_elim_all th1
val th2a = implies_elim_all th2
val th1b = Thm.implies_intr th2c th1a
val th2b = Thm.implies_intr th1c th2a
- val i = Thm.instantiate' []
- [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
+ val i = Thm.instantiate' [] [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
val i1 = Thm.implies_elim i (Thm.assume (Thm.cprop_of th2b))
val i2 = Thm.implies_elim i1 th1b
val i3 = Thm.implies_intr (Thm.cprop_of th2b) i2
@@ -119,102 +108,115 @@
fun conj1 th =
let
- val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
- val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
+ val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th))
+ val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct1}
in
meta_mp i th
end
fun conj2 th =
let
- val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
- val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
+ val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th))
+ val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct2}
in
meta_mp i th
end
-fun refl ctm =
- let
- val cty = Thm.ctyp_of_cterm ctm
- in
- Thm.instantiate' [SOME cty] [SOME ctm] @{thm refl}
- end
+fun refl t =
+ let val A = Thm.ctyp_of_cterm t
+ in Thm.instantiate' [SOME A] [SOME t] @{thm refl} end
-fun abs cv th =
+fun abs x th =
let
val th1 = implies_elim_all th
- val (tl, tr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1)))
- val (ll, lr) = (Thm.lambda cv tl, Thm.lambda cv tr)
- val (al, ar) = (Thm.apply ll cv, Thm.apply lr cv)
+ val (tl, tr) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th1))
+ val (f, g) = (Thm.lambda x tl, Thm.lambda x tr)
+ val (al, ar) = (Thm.apply f x, Thm.apply g x)
val bl = beta al
val br = meta_eq_to_obj_eq (Thm.symmetric (Thm.beta_conversion false ar))
- val th2 = trans (trans bl th1) br
- 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}
+ val th2 =
+ trans (trans bl th1) br
+ |> implies_elim_all
+ |> Thm.forall_intr x
+ val i =
+ Thm.instantiate' [SOME (Thm.ctyp_of_cterm x), SOME (Thm.ctyp_of_cterm tl)]
+ [SOME f, SOME g] @{lemma "(\<And>x. f x = g x) \<Longrightarrow> f = g" by (rule ext)}
in
- meta_mp i th4
+ meta_mp i th2
end
-fun freezeT thy thm =
+fun freezeT thy th =
let
- val tvars = Term.add_tvars (Thm.prop_of thm) []
- val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars
+ fun add (v as ((a, _), S)) tvars =
+ if TVars.defined tvars v then tvars
+ else TVars.add (v, Thm.global_ctyp_of thy (TFree (a, S))) tvars
+ val tyinst =
+ TVars.build (Thm.prop_of th |> (fold_types o fold_atyps) (fn TVar v => add v | _ => I))
in
- Thm.instantiate (TVars.make (tvars ~~ map (Thm.global_ctyp_of thy) tfrees), Vars.empty) thm
+ Thm.instantiate (tyinst, Vars.empty) th
end
-fun def' constname rhs thy =
+fun freeze thy = freezeT thy #> (fn th =>
let
- val rhs = Thm.term_of rhs
- val typ = type_of rhs
- val constbinding = Binding.name constname
- val thy1 = Sign.add_consts [(constbinding, typ, NoSyn)] thy
- val eq = Logic.mk_equals (Const (Sign.full_name thy1 constbinding, typ), rhs)
- val (thm, thy2) = Global_Theory.add_def (Binding.suffix_name "_hldef" constbinding, eq) thy1
- val def_thm = freezeT thy1 thm
+ val vars = Vars.build (th |> Thm.add_vars)
+ val inst = vars |> Vars.map (fn _ => fn v =>
+ let
+ val Var ((x, _), _) = Thm.term_of v
+ val ty = Thm.ctyp_of_cterm v
+ in Thm.free (x, ty) end)
+ in
+ Thm.instantiate (TVars.empty, inst) th
+ end)
+
+fun def' c rhs thy =
+ let
+ val b = Binding.name c
+ val ty = type_of rhs
+ val thy1 = Sign.add_consts [(b, ty, NoSyn)] thy
+ val eq = Logic.mk_equals (Const (Sign.full_name thy1 b, ty), rhs)
+ val (th, thy2) = Global_Theory.add_def (Binding.suffix_name "_hldef" b, eq) thy1
+ val def_thm = freezeT thy1 th
in
(meta_eq_to_obj_eq def_thm, thy2)
end
-fun mdef name thy =
- case Import_Data.get_const_def name thy of
+fun mdef thy name =
+ (case Import_Data.get_const_def thy name of
SOME th => th
- | NONE => error ("constant mapped but no definition: " ^ name)
+ | NONE => error ("Constant mapped, but no definition: " ^ quote name))
+
+fun def c rhs thy =
+ if is_some (Import_Data.get_const_def thy c) then
+ (warning ("Const mapped, but def provided: " ^ quote c); (mdef thy c, thy))
+ else def' c (Thm.term_of rhs) thy
-fun def constname rhs thy =
- case Import_Data.get_const_def constname thy of
- SOME _ =>
- let
- val () = warning ("Const mapped but def provided: " ^ constname)
- in
- (mdef constname thy, thy)
- end
- | NONE => def' constname rhs thy
+fun typedef_hol2hollight A B rep abs pred a r =
+ Thm.instantiate' [SOME A, SOME B] [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 =
+fun typedef_hollight th =
let
- val (th_s, cn) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
- val (th_s, abst) = Thm.dest_comb th_s
- val rept = Thm.dest_arg th_s
- val P = Thm.dest_arg cn
- val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
+ val ((rep, abs), P) =
+ Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
+ |>> (Thm.dest_comb #>> Thm.dest_arg)
+ ||> Thm.dest_arg
+ val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep)
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 A B rep abs P (Thm.free ("a", A)) (Thm.free ("r", B))
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
- _ $ (Const(\<^const_name>\<open>Ex\<close>,_) $ Abs(_,_,Const(\<^const_name>\<open>Set.member\<close>,_) $ _ $ c)) => c
- | _ => error "type_introduction: bad type definition theorem"
+ (case Thm.concl_of th2 of
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>Ex _ for \<open>Abs (_, _, \<^Const_>\<open>Set.member _ for _ c\<close>)\<close>\<close>\<close> => c
+ | _ => raise THM ("type_introduction: bad type definition theorem", 0, [th2]))
val tfrees = Term.add_tfrees c []
val tnames = sort_strings (map fst tfrees)
val typedef_bindings =
@@ -226,54 +228,33 @@
(Typedef.add_typedef {overloaded = false}
(Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
(SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1)) thy
- val aty = #abs_type (#1 typedef_info)
+ val aty = Thm.global_ctyp_of thy' (#abs_type (#1 typedef_info))
val th = freezeT thy' (#type_definition (#2 typedef_info))
- val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
- val (th_s, abst) = Thm.dest_comb th_s
- 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}
- val th4 = typedef_th OF [#type_definition (#2 typedef_info)]
+ val (rep, abs) =
+ Thm.dest_comb (#1 (Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)))) |>> Thm.dest_arg
+ val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep)
+ val typedef_th = typedef_hol2hollight A B rep abs cP (Thm.free ("a", aty)) (Thm.free ("r", ctT))
in
- (th4, thy')
+ (typedef_th OF [#type_definition (#2 typedef_info)], thy')
end
-fun mtydef name thy =
- case Import_Data.get_typ_def name thy of
- SOME thn => meta_mp (typedef_hollight thn thy) thn
- | NONE => error ("type mapped but no tydef thm registered: " ^ name)
+fun mtydef thy name =
+ (case Import_Data.get_typ_def thy name of
+ SOME th => meta_mp (typedef_hollight th) th
+ | NONE => error ("Type mapped, but no tydef thm registered: " ^ quote name))
fun tydef tycname abs_name rep_name P t td_th thy =
- case Import_Data.get_typ_def tycname thy of
- SOME _ =>
- let
- val () = warning ("Type mapped but proofs provided: " ^ tycname)
- in
- (mtydef tycname thy, thy)
- end
- | NONE => tydef' tycname abs_name rep_name P t td_th thy
+ if is_some (Import_Data.get_typ_def thy tycname) then
+ (warning ("Type mapped but proofs provided: " ^ quote tycname); (mtydef thy tycname, thy))
+ else tydef' tycname abs_name rep_name P t td_th thy
-fun inst_type lambda th thy =
+fun inst_type lambda =
let
- fun assoc _ [] = error "assoc"
- | assoc x ((x',y)::rest) = if x = x' then y else assoc x rest
- val lambda = map (fn (a, b) => (Thm.typ_of a, b)) lambda
- val tys_before = Term.add_tfrees (Thm.prop_of th) []
- val th1 = Thm.varifyT_global th
- val tys_after = Term.add_tvars (Thm.prop_of th1) []
val tyinst =
- map2 (fn bef => fn iS =>
- (case try (assoc (TFree bef)) lambda of
- SOME cty => (iS, cty)
- | NONE => (iS, Thm.global_ctyp_of thy (TFree bef))))
- tys_before tys_after
+ TFrees.build (lambda |> fold (fn (a, b) =>
+ TFrees.add (Term.dest_TFree (Thm.typ_of a), b)))
in
- Thm.instantiate (TVars.make tyinst, Vars.empty) th1
+ Thm.instantiate_frees (tyinst, Frees.empty)
end
fun inst sigma th =
@@ -284,167 +265,181 @@
|> forall_elim_list rng
end
-fun transl_dotc #"." = "dot"
- | transl_dotc c = Char.toString c
-val transl_dot = String.translate transl_dotc
+val make_name = String.translate (fn #"." => "dot" | c => Char.toString c)
+
+fun make_free (x, ty) = Free (make_name x, ty)
-fun transl_qmc #"?" = "t"
- | transl_qmc c = Char.toString c
-val transl_qm = String.translate transl_qmc
+fun make_tfree a =
+ let val b = "'" ^ String.translate (fn #"?" => "t" | c => Char.toString c) a
+ in TFree (b, \<^sort>\<open>type\<close>) end
-fun getconstname s thy =
- case Import_Data.get_const_map s thy of
- SOME s => s
- | NONE => Sign.full_name thy (Binding.name (transl_dot s))
-fun gettyname s thy =
- case Import_Data.get_typ_map s thy of
- SOME s => s
- | NONE => Sign.full_name thy (Binding.name s)
+fun make_type thy (c, args) =
+ let
+ val d =
+ (case Import_Data.get_typ_map thy c of
+ SOME d => d
+ | NONE => Sign.full_bname thy (make_name c))
+ in Type (d, args) end
+
+fun make_const thy (c, ty) =
+ let
+ val d =
+ (case Import_Data.get_const_map thy c of
+ SOME d => d
+ | NONE => Sign.full_bname thy (make_name c))
+ in Const (d, ty) end
+
+
+datatype state =
+ State of theory * (ctyp Inttab.table * int) * (cterm Inttab.table * int) * (thm Inttab.table * int)
+
+fun init_state thy = State (thy, (Inttab.empty, 0), (Inttab.empty, 0), (Inttab.empty, 0))
-fun get (map, no) s =
- case Int.fromString s of
- NONE => error "Import_Rule.get: not a number"
- | SOME i => (case Inttab.lookup map (Int.abs i) of
- NONE => error "Import_Rule.get: lookup failed"
- | SOME res => (res, (if i < 0 then Inttab.delete (Int.abs i) map else map, no)))
+fun get (tab, no) s =
+ (case Int.fromString s of
+ NONE => raise Fail "get: not a number"
+ | SOME i =>
+ (case Inttab.lookup tab (Int.abs i) of
+ NONE => raise Fail "get: lookup failed"
+ | SOME res => (res, (if i < 0 then Inttab.delete (Int.abs i) tab else tab, no))))
-fun getty i (thy, (tyi, tmi, thi)) = let val (i, tyi) = (get tyi i) in (i, (thy, (tyi, tmi, thi))) end
-fun gettm i (thy, (tyi, tmi, thi)) = let val (i, tmi) = (get tmi i) in (i, (thy, (tyi, tmi, thi))) end
-fun getth i (thy, (tyi, tmi, thi)) = let val (i, thi) = (get thi i) in (i, (thy, (tyi, tmi, thi))) end
-fun set (map, no) v = (Inttab.update_new (no + 1, v) map, no + 1)
-fun setty v (thy, (tyi, tmi, thi)) = (thy, (set tyi v, tmi, thi))
-fun settm v (thy, (tyi, tmi, thi)) = (thy, (tyi, set tmi v, thi))
-fun setth v (thy, (tyi, tmi, thi)) = (thy, (tyi, tmi, set thi v))
+fun get_theory (State (thy, _, _, _)) = thy;
+fun map_theory f (State (thy, a, b, c)) = State (f thy, a, b, c);
+fun map_theory_result f (State (thy, a, b, c)) =
+ let val (res, thy') = f thy in (res, State (thy', a, b, c)) end;
+
+fun ctyp_of (State (thy, _, _, _)) = Thm.global_ctyp_of thy;
+fun cterm_of (State (thy, _, _, _)) = Thm.global_cterm_of thy;
+
+fun typ i (State (thy, a, b, c)) = let val (i, a') = get a i in (i, State (thy, a', b, c)) end
+fun term i (State (thy, a, b, c)) = let val (i, b') = get b i in (i, State (thy, a, b', c)) end
+fun thm i (State (thy, a, b, c)) = let val (i, c') = get c i in (i, State (thy, a, b, c')) end
-fun last_thm (_, _, (map, no)) =
- case Inttab.lookup map no of
- NONE => error "Import_Rule.last_thm: lookup failed"
- | SOME thm => thm
+fun set (tab, no) v = (Inttab.update_new (no + 1, v) tab, no + 1)
+fun set_typ ty (State (thy, a, b, c)) = State (thy, set a ty, b, c)
+fun set_term tm (State (thy, a, b, c)) = State (thy, a, set b tm, c)
+fun set_thm th (State (thy, a, b, c)) = State (thy, a, b, set c th)
+
+fun last_thm (State (_, _, _, (tab, no))) =
+ case Inttab.lookup tab no of
+ NONE => raise Fail "last_thm: lookup failed"
+ | SOME th => th
-fun listLast (h1 :: (h2 :: t)) = apfst (fn t => h1 :: h2 :: t) (listLast t)
- | listLast [p] = ([], p)
- | listLast [] = error "listLast: empty"
+fun list_last (x :: y :: zs) = apfst (fn t => x :: y :: t) (list_last zs)
+ | list_last [x] = ([], x)
+ | list_last [] = raise Fail "list_last: empty"
-fun pairList (h1 :: (h2 :: t)) = ((h1, h2) :: pairList t)
- | pairList [] = []
- | pairList _ = error "pairList: odd list length"
+fun pair_list (x :: y :: zs) = ((x, y) :: pair_list zs)
+ | pair_list [] = []
+ | pair_list _ = raise Fail "pair_list: odd list length"
-fun store_thm binding thm thy =
+fun store_thm binding th0 thy =
let
val ctxt = Proof_Context.init_global thy
- val thm = Drule.export_without_context_open thm
- val tvs = Term.add_tvars (Thm.prop_of thm) []
+ val th = Drule.export_without_context_open th0
+ val tvs = Term.add_tvars (Thm.prop_of th) []
val tns = map (fn (_, _) => "'") tvs
val nms = Name.variants (Variable.names_of ctxt) tns
val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
- val thm' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) thm
+ val th' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) th
in
- snd (Global_Theory.add_thm ((binding, thm'), []) thy)
- end
-
-fun log_timestamp () =
- let
- val time = Time.now ()
- val millis = nth (space_explode "." (Time.fmt 3 time)) 1
- in
- Date.fmt "%d.%m.%Y %H:%M:%S." (Date.fromTimeLocal time) ^ millis
+ snd (Global_Theory.add_thm ((binding, th'), []) thy)
end
-fun process_line str tstate =
+fun parse_line s =
+ (case String.tokens (fn x => x = #"\n" orelse x = #" ") s of
+ [] => raise Fail "parse_line: empty"
+ | cmd :: args =>
+ (case String.explode cmd of
+ [] => raise Fail "parse_line: empty command"
+ | c :: cs => (c, String.implode cs :: args)))
+
+fun process_line str =
let
- fun process tstate (#"R", [t]) = gettm t tstate |>> refl |-> setth
- | process tstate (#"B", [t]) = gettm t tstate |>> beta |-> setth
- | process tstate (#"1", [th]) = getth th tstate |>> conj1 |-> setth
- | process tstate (#"2", [th]) = getth th tstate |>> conj2 |-> setth
- | process tstate (#"H", [t]) =
- gettm t tstate |>> Thm.apply \<^cterm>\<open>Trueprop\<close> |>> Thm.trivial |-> setth
- | process tstate (#"A", [_, t]) =
- gettm t tstate |>> Thm.apply \<^cterm>\<open>Trueprop\<close> |>> Skip_Proof.make_thm_cterm |-> setth
- | process tstate (#"C", [th1, th2]) =
- getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => comb t1 t2) |-> setth
- | process tstate (#"T", [th1, th2]) =
- getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => trans t1 t2) |-> setth
- | process tstate (#"E", [th1, th2]) =
- getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => eq_mp t1 t2) |-> setth
- | process tstate (#"D", [th1, th2]) =
- getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => deduct t1 t2) |-> setth
- | process tstate (#"L", [t, th]) =
- gettm t tstate ||>> (fn ti => getth th ti) |>> (fn (tm, th) => abs tm th) |-> setth
- | process (thy, state) (#"M", [s]) =
+ fun process (#"R", [t]) = term t #>> refl #-> set_thm
+ | process (#"B", [t]) = term t #>> beta #-> set_thm
+ | process (#"1", [th]) = thm th #>> conj1 #-> set_thm
+ | process (#"2", [th]) = thm th #>> conj2 #-> set_thm
+ | process (#"H", [t]) = term t #>> Thm.apply \<^cterm>\<open>Trueprop\<close> #>> Thm.trivial #-> set_thm
+ | process (#"A", [_, t]) =
+ term t #>> Thm.apply \<^cterm>\<open>Trueprop\<close> #>> Skip_Proof.make_thm_cterm #-> set_thm
+ | process (#"C", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry comb #-> set_thm
+ | process (#"T", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry trans #-> set_thm
+ | process (#"E", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry eq_mp #-> set_thm
+ | process (#"D", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry deduct #-> set_thm
+ | process (#"L", [t, th]) = term t ##>> (fn ti => thm th ti) #>> uncurry abs #-> set_thm
+ | process (#"M", [s]) = (fn state =>
let
- val ctxt = Proof_Context.init_global thy
- val thm = freezeT thy (Global_Theory.get_thm thy s)
- val ((_, [th']), _) = Variable.import true [thm] ctxt
+ val thy = get_theory state
+ val th = Global_Theory.get_thm thy s
in
- setth th' (thy, state)
- end
- | process (thy, state) (#"Q", l) =
+ set_thm (freeze thy th) state
+ end)
+ | process (#"Q", l) = (fn state =>
let
- val (tys, th) = listLast l
- val (th, tstate) = getth th (thy, state)
- val (tys, tstate) = fold_map getty tys tstate
- in
- setth (inst_type (pairList tys) th thy) tstate
- end
- | process tstate (#"S", l) =
- let
- val (tms, th) = listLast l
- val (th, tstate) = getth th tstate
- val (tms, tstate) = fold_map gettm tms tstate
+ val (tys, th) = list_last l
+ val (th, state1) = thm th state
+ val (tys, state2) = fold_map typ tys state1
in
- setth (inst (pairList tms) th) tstate
- end
- | process tstate (#"F", [name, t]) =
+ set_thm (inst_type (pair_list tys) th) state2
+ end)
+ | process (#"S", l) = (fn state =>
let
- val (tm, (thy, state)) = gettm t tstate
- val (th, thy) = def (transl_dot name) tm thy
+ val (tms, th) = list_last l
+ val (th, state1) = thm th state
+ val (tms, state2) = fold_map term tms state1
in
- setth th (thy, state)
- end
- | process (thy, state) (#"F", [name]) = setth (mdef name thy) (thy, state)
- | process tstate (#"Y", [name, absname, repname, t1, t2, th]) =
+ set_thm (inst (pair_list tms) th) state2
+ end)
+ | process (#"F", [name, t]) = (fn state =>
let
- val (th, tstate) = getth th tstate
- val (t1, tstate) = gettm t1 tstate
- val (t2, (thy, state)) = gettm t2 tstate
- val (th, thy) = tydef name absname repname t1 t2 th thy
+ val (tm, state1) = term t state
in
- setth th (thy, state)
- end
- | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state)
- | process (thy, state) (#"t", [n]) =
- setty (Thm.global_ctyp_of thy (TFree ("'" ^ (transl_qm n), \<^sort>\<open>type\<close>))) (thy, state)
- | process (thy, state) (#"a", n :: l) =
- fold_map getty l (thy, state) |>>
- (fn tys => Thm.global_ctyp_of thy (Type (gettyname n thy, map Thm.typ_of tys))) |-> setty
- | process (thy, state) (#"v", [n, ty]) =
- getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (Free (transl_dot n, Thm.typ_of ty))) |-> settm
- | process (thy, state) (#"c", [n, ty]) =
- getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (Const (getconstname n thy, Thm.typ_of ty))) |-> settm
- | process tstate (#"f", [t1, t2]) =
- gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.apply t1 t2) |-> settm
- | process tstate (#"l", [t1, t2]) =
- gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm
- | process (thy, state) (#"+", [s]) =
- (store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state)
- | process _ (c, _) = error ("process: unknown command: " ^ String.implode [c])
-
- fun parse_line s =
- case String.tokens (fn x => (x = #"\n" orelse x = #" ")) s of
- [] => error "parse_line: empty"
- | h :: t => (case String.explode h of
- [] => error "parse_line: empty command"
- | sh :: st => (sh, (String.implode st) :: t))
+ state1
+ |> map_theory_result (def (make_name name) tm)
+ |-> set_thm
+ end)
+ | process (#"F", [name]) = (fn state => set_thm (mdef (get_theory state) name) state)
+ | process (#"Y", [name, absname, repname, t1, t2, th]) = (fn state =>
+ let
+ val (th, state1) = thm th state
+ val (t1, state2) = term t1 state1
+ val (t2, state3) = term t2 state2
+ in
+ state3
+ |> map_theory_result (tydef name absname repname t1 t2 th)
+ |-> set_thm
+ end)
+ | process (#"Y", [name, _, _]) = (fn state => set_thm (mtydef (get_theory state) name) state)
+ | process (#"t", [n]) = (fn state => set_typ (ctyp_of state (make_tfree n)) state)
+ | process (#"a", n :: l) = (fn state =>
+ fold_map typ l state
+ |>> (fn tys => ctyp_of state (make_type (get_theory state) (n, map Thm.typ_of tys)))
+ |-> set_typ)
+ | process (#"v", [n, ty]) = (fn state =>
+ typ ty state |>> (fn ty => cterm_of state (make_free (n, Thm.typ_of ty))) |-> set_term)
+ | process (#"c", [n, ty]) = (fn state =>
+ typ ty state |>> (fn ty =>
+ cterm_of state (make_const (get_theory state) (n, Thm.typ_of ty))) |-> set_term)
+ | process (#"f", [t1, t2]) = term t1 ##>> term t2 #>> uncurry Thm.apply #-> set_term
+ | process (#"l", [t1, t2]) = term t1 ##>> term t2 #>> uncurry Thm.lambda #-> set_term
+ | process (#"+", [s]) = (fn state =>
+ map_theory (store_thm (Binding.name (make_name s)) (last_thm state)) state)
+ | process (c, _) = raise Fail ("process: unknown command: " ^ String.str c)
in
- process tstate (parse_line str)
+ process (parse_line str)
end
-fun process_file path thy =
- #1 (fold process_line (File.read_lines path) (thy, init_state))
+fun import_file path0 thy =
+ let
+ val path = File.absolute_path (Resources.master_directory thy + path0)
+ val lines =
+ if Path.is_zst path then Bytes.read path |> Zstd.uncompress |> Bytes.trim_split_lines
+ else File.read_lines path
+ in get_theory (fold process_line lines (init_state thy)) end
-val _ = Outer_Syntax.command \<^command_keyword>\<open>import_file\<close>
- "import a recorded proof file"
- (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
-
+val _ =
+ Outer_Syntax.command \<^command_keyword>\<open>import_file\<close> "import recorded proofs from HOL Light"
+ (Parse.path >> (fn name => Toplevel.theory (fn thy => import_file (Path.explode name) thy)))
end
--- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Jan 17 12:17:37 2025 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Jan 17 21:30:08 2025 +0100
@@ -13,7 +13,7 @@
val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,
{lines = fdl_lines, pos = fdl_pos, ...},
{lines = rls_lines, pos = rls_pos, ...}], thy') = files thy;
- val path = fst (Path.split_ext src_path);
+ val path = Path.drop_ext src_path;
in
SPARK_VCs.set_vcs
(snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/component_hol_light.scala Fri Jan 17 21:30:08 2025 +0100
@@ -0,0 +1,268 @@
+/* Title: Pure/Admin/component_hol_light.scala
+ Author: Makarius
+
+Build component for HOL-Light, with export of facts and proofs, offline
+optimization, and import to Isabelle/HOL.
+*/
+
+package isabelle
+
+
+object Component_HOL_Light {
+ /* resources */
+
+ val default_hol_light_url = "https://github.com/jrh13/hol-light.git"
+ val default_hol_light_rev = "Release-3.0.0"
+
+ val default_hol_light_patched_url = "https://gitlab.inria.fr/hol-light-isabelle/hol-light.git"
+ val default_hol_light_patched_rev = "master"
+
+ val default_import_url = "https://gitlab.inria.fr/hol-light-isabelle/import.git"
+ val default_import_rev = "master"
+
+ def hol_light_dirs(base_dir: Path): (Path, Path) =
+ (base_dir + Path.basic("hol-light"), base_dir + Path.basic("hol-light-patched"))
+
+ val patched_files: List[Path] =
+ List("fusion.ml", "statements.ml", "stage1.ml", "stage2.ml").map(Path.explode)
+
+ def make_patch(base_dir: Path): String = {
+ val (dir1, dir2) = hol_light_dirs(Path.current)
+ (for (path <- patched_files) yield {
+ val path1 = dir1 + path
+ val path2 = dir2 + path
+ if ((base_dir + path1).is_file || (base_dir + path2).is_file) {
+ Isabelle_System.make_patch(base_dir, path1, path2)
+ }
+ else ""
+ }).mkString
+ }
+
+ def build_hol_light_import(
+ only_offline: Boolean = false,
+ progress: Progress = new Progress,
+ target_dir: Path = Path.current,
+ hol_light_url: String = default_hol_light_url,
+ hol_light_rev: String = default_hol_light_rev,
+ hol_light_patched_url: String = default_hol_light_patched_url,
+ hol_light_patched_rev: String = default_hol_light_patched_rev,
+ import_url: String = default_import_url,
+ import_rev: String = default_import_rev
+ ): Unit = {
+ /* system */
+
+ if (!only_offline) {
+ Linux.check_system()
+ Isabelle_System.require_command("buffer", test = "-i /dev/null")
+ Isabelle_System.require_command("patch")
+ }
+
+
+ /* component */
+
+ val component_name = "hol_light_import-" + Date.Format.alt_date(Date.now())
+ val component_dir = Components.Directory(target_dir + Path.basic(component_name)).create()
+
+ val platform = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
+ val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform))
+
+
+ /* settings */
+
+ component_dir.write_settings("""
+HOL_LIGHT_IMPORT="$COMPONENT"
+HOL_LIGTH_BUNDLE="$HOL_LIGHT_IMPORT/bundle/proofs"
+HOL_LIGHT_OFFLINE="$HOL_LIGHT_IMPORT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}/offline"
+""")
+
+
+ /* README */
+
+ File.write(component_dir.README,
+ """Author: Cezary Kaliszyk, University of Innsbruck, 2013
+Author: Alexander Krauss, QAware GmbH, 2013
+Author: Sophie Tourret, INRIA, 2024
+Author: Stéphane Glondu, INRIA, 2024
+LICENSE (export tools): BSD-3 from Isabelle
+LICENSE (HOL Light proofs): BSD-2 from HOL Light
+
+
+This is an export of primitive proofs from HOL Light """ + hol_light_rev + """.
+
+The original repository """ + hol_light_url + """
+has been patched in 2 stages. The overall export process works like this:
+
+ make
+
+ patch -p1 < patches/stage1.patch
+ ./ocaml-hol -I +compiler-libs stage1.ml
+
+ patch -p1 < patches/stage2.patch
+ export MAXTMS=10000
+ ./ocaml-hol -I +compiler-libs stage2.ml
+
+ gzip -d proofs.gz
+ > maps.lst
+ x86_64-linux/offline
+
+
+ Makarius
+ """ + Date.Format.date(Date.now()) + "\n")
+
+
+ Isabelle_System.with_tmp_dir("build") { tmp_dir =>
+
+ /* OCaml setup */
+
+ progress.echo("Setup OCaml ...")
+
+ progress.bash(
+ if (only_offline) "isabelle ocaml_setup_base"
+ else "isabelle ocaml_setup && isabelle ocaml_opam install -y camlp5",
+ echo = progress.verbose).check
+
+ val opam_env = Isabelle_System.bash("isabelle ocaml_opam env").check.out
+
+
+ /* repository clones */
+
+ val (hol_light_dir, hol_light_patched_dir) = hol_light_dirs(tmp_dir)
+ val import_dir = tmp_dir + Path.basic("import")
+
+ if (!only_offline) {
+ Isabelle_System.git_clone(hol_light_url, hol_light_dir, checkout = hol_light_rev,
+ progress = progress)
+
+ Isabelle_System.git_clone(
+ hol_light_patched_url, hol_light_patched_dir, checkout = hol_light_patched_rev,
+ progress = progress)
+ }
+
+ Isabelle_System.git_clone(import_url, import_dir, checkout = import_rev, progress = progress)
+
+
+ /* "offline" tool */
+
+ progress.echo("Building offline tool ...")
+
+ val offline_path = Path.explode("offline")
+ val offline_exe = offline_path.platform_exe
+ val import_offline_dir = import_dir + offline_path
+
+ Isabelle_System.copy_dir(import_offline_dir, component_dir.path)
+ (component_dir.path + Path.explode("offline/.gitignore")).file.delete
+
+ progress.bash("make", cwd = import_offline_dir, echo = progress.verbose).check
+ Isabelle_System.copy_file(import_offline_dir + offline_exe, platform_dir + offline_exe)
+ File.set_executable(platform_dir + offline_exe)
+
+
+ if (!only_offline) {
+
+ /* patches */
+
+ progress.echo("Preparing patches ...")
+
+ val patches_dir = Isabelle_System.make_directory(component_dir.path + Path.basic("patches"))
+ val patch1 = patches_dir + Path.basic("stage1.patch")
+ val patch2 = patches_dir + Path.basic("stage2.patch")
+
+ Isabelle_System.bash("git reset --hard origin/stdlib/isabelle-export-base",
+ cwd = hol_light_patched_dir).check
+
+ File.write(patch1, make_patch(tmp_dir))
+
+ Isabelle_System.bash("patch -p1 < " + File.bash_path(patch1), cwd = hol_light_dir).check
+
+ Isabelle_System.bash("git reset --hard origin/stdlib/isabelle-export",
+ cwd = hol_light_patched_dir).check
+
+ File.write(patch2, make_patch(tmp_dir))
+
+
+ /* export */
+
+ progress.echo("Exporting proofs ...")
+ progress.bash(
+ Library.make_lines("set -e", opam_env,
+ "make",
+ "./ocaml-hol -I +compiler-libs stage1.ml",
+ "patch -p1 < " + File.bash_path(patch2),
+ "export MAXTMS=10000",
+ "./ocaml-hol -I +compiler-libs stage2.ml",
+ "gzip -d proofs.gz",
+ "> maps.lst",
+ File.bash_path(platform_dir + offline_exe) + " proofs"
+ ),
+ cwd = hol_light_dir, echo = progress.verbose).check
+
+ val bundle_dir = Isabelle_System.make_directory(component_dir.path + Path.explode("bundle"))
+ Isabelle_System.copy_file(hol_light_dir + Path.explode("proofs"), bundle_dir)
+ }
+ }
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("component_hol_light_import", "build Isabelle component for HOL Light import",
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var only_offline = false
+ var hol_light_url = default_hol_light_url
+ var hol_light_patched_url = default_hol_light_patched_url
+ var hol_light_rev = default_hol_light_rev
+ var hol_light_patched_rev = default_hol_light_patched_rev
+ var import_url = default_import_url
+ var import_rev = default_import_rev
+ var verbose = false
+
+ val getopts = Getopts("""
+Usage: isabelle component_hol_light_import [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default ".")
+ -O only build the "offline" tool
+ -U URL git URL for original HOL Light repository, default:
+ """ + default_hol_light_url + """
+ -V URL git URL for patched HOL Light repository, default:
+ """ + default_hol_light_patched_url + """
+ -W URL git URL for import repository, default:
+ """ + default_import_url + """
+ -r REV revision or branch to checkout HOL Light (default: """ +
+ default_hol_light_rev + """)
+ -s REV revision or branch to checkout HOL-Light-to-Isabelle (default: """ +
+ default_hol_light_patched_rev + """)
+ -t REV revision or branch to checkout import (default: """ +
+ default_import_rev + """)
+ -v verbose
+
+ Build Isabelle component for HOL Light import.
+""",
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "O" -> (_ => only_offline = true),
+ "U:" -> (arg => hol_light_url = arg),
+ "V:" -> (arg => hol_light_patched_url = arg),
+ "W:" -> (arg => import_url = arg),
+ "r:" -> (arg => hol_light_rev = arg),
+ "s:" -> (arg => hol_light_patched_rev = arg),
+ "t:" -> (arg => import_rev = arg),
+ "v" -> (_ => verbose = true))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress(verbose = verbose)
+
+ build_hol_light_import(
+ only_offline = only_offline, progress = progress, target_dir = target_dir,
+ hol_light_url = hol_light_url,
+ hol_light_rev = hol_light_rev,
+ hol_light_patched_url = hol_light_patched_url,
+ hol_light_patched_rev = hol_light_patched_rev,
+ import_url = import_url,
+ import_rev = import_rev)
+ })
+}
--- a/src/Pure/General/path.ML Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Pure/General/path.ML Fri Jan 17 21:30:08 2025 +0100
@@ -33,7 +33,10 @@
val ext: string -> T -> T
val platform_exe: T -> T
val split_ext: T -> T * string
- val exe: T -> T
+ val drop_ext: T -> T
+ val get_ext: T -> string
+ val is_xz: T -> bool
+ val is_zst: T -> bool
val expand: T -> T
val file_name: T -> string
eqtype binding
@@ -213,7 +216,11 @@
([], _) => (Path [Basic s], "")
| (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
-val exe = ML_System.platform_is_windows ? ext "exe";
+val drop_ext = #1 o split_ext;
+val get_ext = #2 o split_ext;
+
+fun is_xz path = get_ext path = "xz";
+fun is_zst path = get_ext path = "zst";
(* expand variables *)
--- a/src/Pure/ROOT.ML Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Pure/ROOT.ML Fri Jan 17 21:30:08 2025 +0100
@@ -1,6 +1,6 @@
(* Title: Pure/ROOT.ML
Author: Makarius
- UUID: b5c84e7e-c43b-4cf5-9644-a1f387b61ab4
+ UUID: e075658d-0c3c-4076-892c-37ce2c40df8e
Main entry point for the Isabelle/Pure bootstrap process.
--- a/src/Pure/System/isabelle_system.scala Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Pure/System/isabelle_system.scala Fri Jan 17 21:30:08 2025 +0100
@@ -495,13 +495,24 @@
}
def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
- with_tmp_file("patch") { patch =>
+ val lines =
Isabelle_System.bash(
- "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) +
- " > " + File.bash_path(patch),
- cwd = base_dir).check_rc(_ <= 1)
- File.read(patch)
- }
+ "diff -Nru" + if_proper(diff_options, " " + diff_options) + " -- " +
+ File.bash_path(src) + " " + File.bash_path(dst),
+ cwd = base_dir).check_rc(Process_Result.RC.regular).out_lines
+ Library.terminate_lines(lines)
+ }
+
+ def git_clone(url: String, target: Path,
+ checkout: String = "HEAD",
+ ssh: SSH.System = SSH.Local,
+ progress: Progress = new Progress
+ ): Unit = {
+ progress.echo("Cloning " + quote(url) + " ...")
+ bash(
+ "git clone --quiet --no-checkout " + Bash.string(url) + " . && " +
+ "git checkout --quiet --detach " + Bash.string(checkout),
+ ssh = ssh, cwd = ssh.make_directory(target)).check
}
def open(arg: String): Unit =
--- a/src/Pure/System/isabelle_tool.scala Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Pure/System/isabelle_tool.scala Fri Jan 17 21:30:08 2025 +0100
@@ -180,6 +180,7 @@
Component_Elm.isabelle_tool,
Component_Foiltex.isabelle_tool,
Component_Fonts.isabelle_tool,
+ Component_HOL_Light.isabelle_tool,
Component_Hugo.isabelle_tool,
Component_Javamail.isabelle_tool,
Component_JCEF.isabelle_tool,
--- a/src/Pure/System/process_result.scala Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Pure/System/process_result.scala Fri Jan 17 21:30:08 2025 +0100
@@ -18,6 +18,8 @@
val interrupt = 130
val timeout = 142
+ val regular: Set[Int] = Set(ok, error)
+
private def text(rc: Int): String = {
val txt =
rc match {
--- a/src/Pure/Tools/generated_files.ML Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Pure/Tools/generated_files.ML Fri Jan 17 21:30:08 2025 +0100
@@ -253,7 +253,7 @@
val (path, pos) = Path.dest_binding binding;
val file_type =
- get_file_type thy (#2 (Path.split_ext path))
+ get_file_type thy (Path.get_ext path)
handle ERROR msg => error (msg ^ Position.here pos);
val header = #make_comment file_type " generated by Isabelle ";
@@ -343,7 +343,8 @@
export |> List.app (fn (bindings, executable) =>
bindings |> List.app (fn binding0 =>
let
- val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
+ val binding = binding0
+ |> Path.map_binding (executable = SOME true ? Path.platform_exe);
val (path, pos) = Path.dest_binding binding;
val content =
(case try Bytes.read (dir + path) of
--- a/src/Pure/library.scala Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Pure/library.scala Fri Jan 17 21:30:08 2025 +0100
@@ -147,6 +147,8 @@
def cat_lines(lines: IterableOnce[String]): String =
lines.iterator.mkString("\n")
+ def make_lines(lines: String*): String = cat_lines(lines)
+
def split_lines(str: String): List[String] = space_explode('\n', str)
def prefix_lines(prfx: String, str: String): String =
--- a/src/Pure/thm.ML Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Pure/thm.ML Fri Jan 17 21:30:08 2025 +0100
@@ -49,6 +49,7 @@
val dest_abs_fresh: string -> cterm -> cterm * cterm
val dest_abs_global: cterm -> cterm * cterm
val rename_tvar: indexname -> ctyp -> ctyp
+ val free: string * ctyp -> cterm
val var: indexname * ctyp -> cterm
val apply: cterm -> cterm -> cterm
val lambda_name: string * cterm -> cterm -> cterm
@@ -340,6 +341,9 @@
val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else ();
in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end;
+fun free (x, Ctyp {cert, T, maxidx, sorts}) =
+ Cterm {cert = cert, t = Free (x, T), T = T, maxidx = maxidx, sorts = sorts};
+
fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) =
if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)])
else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts};
--- a/src/Tools/VSCode/src/component_vscodium.scala Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Tools/VSCode/src/component_vscodium.scala Fri Jan 17 21:30:08 2025 +0100
@@ -81,12 +81,7 @@
def get_vscodium_repository(build_dir: Path, progress: Progress = new Progress): Unit = {
progress.echo("Getting VSCodium repository ...")
- Isabelle_System.bash(
- List(
- "set -e",
- "git clone -n " + Bash.string(vscodium_repository) + " .",
- "git checkout -q " + Bash.string(version)
- ).mkString("\n"), cwd = build_dir).check
+ Isabelle_System.git_clone(vscodium_repository, build_dir, checkout = version)
progress.echo("Getting VSCode repository ...")
Isabelle_System.bash(environment + "\n" + "./get_repo.sh", cwd = build_dir).check
@@ -286,13 +281,13 @@
progress.echo("Prepare ...")
Isabelle_System.with_copy_dir(vscode_dir, vscode_dir.orig) {
progress.bash(
- List(
+ Library.make_lines(
"set -e",
platform_info.environment,
"./prepare_vscode.sh",
// enforce binary diff of code.xpm
"cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm"
- ).mkString("\n"), cwd = build_dir, echo = progress.verbose).check
+ ), cwd = build_dir, echo = progress.verbose).check
Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base,
diff_options = "--exclude=.git --exclude=node_modules")
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Jan 17 12:17:37 2025 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Jan 17 21:30:08 2025 +0100
@@ -45,6 +45,8 @@
.replace('\t',' ')
lazy val gui_text: String = Library.string_builder(line_range.length * 2) { s =>
+ val style = GUI.Style_HTML
+
// see also HyperSearchResults.highlightString
s ++= "<html><b>"
s ++= line.toString
@@ -58,15 +60,15 @@
var last = plain_start
for (range <- JEdit_Lib.search_text(buffer, search_range, regex)) {
val next = range.start - line_start
- if (last < next) s ++= line_text.substring(last, next)
+ if (last < next) s ++= style.make_text(line_text.substring(last, next))
s ++= "<span style=\""
s ++= highlight_style
s ++= "\">"
- s ++= line_text.substring(next, next + range.length)
+ s ++= style.make_text(line_text.substring(next, next + range.length))
s ++= "</span>"
last = range.stop - line_start
}
- if (last < plain_stop) s ++= line_text.substring(last)
+ if (last < plain_stop) s ++= style.make_text(line_text.substring(last))
s ++= "</html>"
}
override def toString: String = gui_text