--- a/NEWS Thu Jan 23 13:42:58 2025 +0100
+++ b/NEWS Fri Jan 24 10:22:17 2025 +0100
@@ -324,6 +324,10 @@
Variable.variant_names or Variable.focus_params, instead of
Logic.goal_params etc.
+* Antiquotation \<^instantiate>\<open>(no_beta) x = t in \<dots>\<close> is like
+\<^instantiate>\<open>x = t in \<dots>\<close>, but without implicit beta-normalization.
+This is occasionally useful for low-level applications.
+
* Antiquotation \<^bundle>\<open>name\<close> inlines a formally checked bundle name.
* The new operation Pattern.rewrite_term_yoyo alternates top-down,
--- a/src/CCL/Wfd.thy Thu Jan 23 13:42:58 2025 +0100
+++ b/src/CCL/Wfd.thy Fri Jan 24 10:22:17 2025 +0100
@@ -424,9 +424,9 @@
| get_bno l n (Bound m) = (m-length(l),n)
(* Not a great way of identifying induction hypothesis! *)
-fun could_IH x = Term.could_unify(x,hd (Thm.prems_of @{thm rcallT})) orelse
- Term.could_unify(x,hd (Thm.prems_of @{thm rcall2T})) orelse
- Term.could_unify(x,hd (Thm.prems_of @{thm rcall3T}))
+fun could_IH x = Term.could_unify(x,hd (Thm.take_prems_of 1 @{thm rcallT})) orelse
+ Term.could_unify(x,hd (Thm.take_prems_of 1 @{thm rcall2T})) orelse
+ Term.could_unify(x,hd (Thm.take_prems_of 1 @{thm rcall3T}))
fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
let val bvs = bvars Bi []
--- a/src/FOLP/simp.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/FOLP/simp.ML Fri Jan 24 10:22:17 2025 +0100
@@ -83,9 +83,7 @@
biresolve_tac ctxt (Net.unify_term net
(lhs_of (Logic.strip_assums_concl prem))) i);
-fun nth_subgoal i thm = nth (Thm.prems_of thm) (i - 1);
-
-fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm);
+fun goal_concl i thm = Logic.strip_assums_concl (Thm.prem_of thm i);
fun lhs_of_eq i thm = lhs_of(goal_concl i thm)
and rhs_of_eq i thm = rhs_of(goal_concl i thm);
@@ -370,7 +368,7 @@
(*Select subgoal i from proof state; substitute parameters, for printing*)
fun prepare_goal i st =
- let val subgi = nth_subgoal i st
+ let val subgi = Thm.prem_of st i
val params = rev (Logic.strip_params subgi)
in variants_abs (params, Logic.strip_assums_concl subgi) end;
@@ -425,7 +423,7 @@
(*NB: the "Adding rewrites:" trace will look strange because assumptions
are represented by rules, generalized over their parameters*)
fun add_asms(ss,thm,a,anet,ats,cs) =
- let val As = strip_varify(nth_subgoal i thm, a, []);
+ let val As = strip_varify(Thm.prem_of thm i, a, []);
val thms = map (Thm.trivial o Thm.cterm_of ctxt) As;
val new_rws = maps mk_rew_rules thms;
val rwrls = map mk_trans (maps mk_rew_rules thms);
@@ -532,7 +530,7 @@
fun find_subst ctxt T =
let fun find (thm::thms) =
- let val (Const(_,cT), va, vb) = dest_red(hd(Thm.prems_of thm));
+ let val (Const(_,cT), va, vb) = dest_red(Thm.prem_of thm 1);
val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (Thm.concl_of thm, []));
val eqT::_ = binder_types cT
in if Sign.typ_instance (Proof_Context.theory_of ctxt) (T,eqT) then SOME(thm,va,vb,P)
--- a/src/HOL/Analysis/measurable.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Analysis/measurable.ML Fri Jan 24 10:22:17 2025 +0100
@@ -125,7 +125,7 @@
| _ => raise (TERM ("not a measurability predicate", [t])))
fun not_measurable_prop n thm =
- if length (Thm.prems_of thm) < n then false
+ if Thm.nprems_of thm < n then false
else
(case nth_hol_goal thm n of
\<^Const_>\<open>Set.member _ for _ \<^Const_>\<open>sets _ for _\<close>\<close> => false
--- a/src/HOL/Analysis/normarith.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Analysis/normarith.ML Fri Jan 24 10:22:17 2025 +0100
@@ -359,7 +359,7 @@
val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (Thm.chyps_of th1)
val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
- val cps = map (swap o Thm.dest_equals) (cprems_of th11)
+ val cps = map (swap o Thm.dest_equals) (Thm.cprems_of th11)
val th12 = Drule.instantiate_normalize (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) cps)) th11
val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
in hd (Variable.export ctxt' ctxt [th13])
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Jan 24 10:22:17 2025 +0100
@@ -930,7 +930,7 @@
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
@@ -953,7 +953,7 @@
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
@@ -975,7 +975,7 @@
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
@@ -1000,7 +1000,7 @@
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
@@ -1019,7 +1019,7 @@
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim
@@ -1041,7 +1041,7 @@
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val rth = Thm.implies_elim
--- a/src/HOL/HOL.thy Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/HOL.thy Fri Jan 24 10:22:17 2025 +0100
@@ -2177,7 +2177,7 @@
fun wrong_prem \<^Const_>\<open>All _ for \<open>Abs (_, _, t)\<close>\<close> = wrong_prem t
| wrong_prem (Bound _) = true
| wrong_prem _ = false;
- val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
+ val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.take_prems_of 1);
fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp];
in
fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt];
--- a/src/HOL/HOLCF/Cfun.thy Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Fri Jan 24 10:22:17 2025 +0100
@@ -144,7 +144,7 @@
simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \<open>
K (fn ctxt => fn ct =>
let
- val f = #2 (Thm.dest_comb (#2 (Thm.dest_comb ct)));
+ val f = Thm.dest_arg (Thm.dest_arg ct);
val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2});
val rules = Named_Theorems.get ctxt \<^named_theorems>\<open>cont2cont\<close>;
--- a/src/HOL/Import/HOL_Light_Maps.thy Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy Fri Jan 24 10:22:17 2025 +0100
@@ -17,7 +17,7 @@
lemma [import_const "/\\"]:
"(\<and>) = (\<lambda>p q. (\<lambda>f. f p q :: bool) = (\<lambda>f. f True True))"
- by metis
+ by (metis (full_types))
lemma [import_const "==>"]:
"(\<longrightarrow>) = (\<lambda>(p::bool) q::bool. (p \<and> q) = p)"
@@ -123,6 +123,17 @@
"\<forall>P. P 0 \<and> (\<forall>n. P n \<longrightarrow> P (Suc n)) \<longrightarrow> (\<forall>n. P n)"
by (auto intro: nat.induct)
+lemma num_Axiom:
+ "\<forall>(e::'A) f. \<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
+ apply (intro allI)
+ subgoal for e f
+ apply (rule ex1I [where a = "Nat.rec_nat e (\<lambda>a b. f b a)"])
+ apply simp
+ apply (rule ext)
+ subgoal for fn x by (induct x) simp_all
+ done
+ done
+
lemma [import_const NUMERAL]: "id = (\<lambda>x :: nat. x)"
by auto
@@ -131,13 +142,13 @@
lemma [import_const BIT0]:
"bit0 = (SOME fn. fn (id 0) = id 0 \<and> (\<forall>n. fn (Suc n) = Suc (Suc (fn n))))"
apply (auto intro!: some_equality[symmetric])
- apply (auto simp add: fun_eq_iff)
- apply (induct_tac x)
- apply auto
+ subgoal for fn
+ apply (rule ext)
+ subgoal for x by (induct x) simp_all
+ done
done
-definition [import_const BIT1, simp]:
- "bit1 = (\<lambda>x. Suc (bit0 x))"
+definition [import_const BIT1, simp]: "bit1 = (\<lambda>x. Suc (bit0 x))"
definition [simp]: "pred n = n - 1"
@@ -181,9 +192,7 @@
"min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
by (simp add: fun_eq_iff)
-definition even
-where
- "even = Parity.even"
+definition even where "even = Parity.even"
lemma EVEN[import_const "EVEN" : even]:
"even (id 0::nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
@@ -298,7 +307,7 @@
"list_all2 (P::'t18495 \<Rightarrow> 't18502 \<Rightarrow> bool) [] (l2::'t18502 list) = (l2 = []) \<and>
list_all2 P ((h1::'t18495) # (t1::'t18495 list)) l2 =
(if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))"
- by simp (induct_tac l2, simp_all)
+ by simp (induct l2, simp_all)
lemma FILTER[import_const FILTER : filter]:
"filter (P::'t18680 \<Rightarrow> bool) [] = [] \<and>
@@ -311,18 +320,19 @@
by simp
lemma WF[import_const WF : wfP]:
- "\<forall>u. wfP u \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
+ "\<forall>R. wfP R \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. R y x \<longrightarrow> \<not> P y)))"
proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
- fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
- assume a: "xa \<in> Q"
- assume "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
- then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
- then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
-next
- fix x P and xa :: 'A and z
- assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
- then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
+ fix R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and P :: "'a \<Rightarrow> bool" and x z :: "'a"
+ {
+ fix Q
+ assume a: "x \<in> Q"
+ assume "\<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. R y x \<longrightarrow> \<not> P y))"
+ then have "(\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>x. (\<lambda>x. x \<in> Q) x \<and> (\<forall>y. R y x \<longrightarrow> y \<notin> Q))" by auto
+ with a show "\<exists>x\<in>Q. \<forall>y. R y x \<longrightarrow> y \<notin> Q" by auto
+ next
+ assume "P x" "z \<in> {a. P a}" "\<And>y. R y z \<Longrightarrow> y \<notin> {a. P a}"
+ then show "\<exists>x. P x \<and> (\<forall>y. R y x \<longrightarrow> \<not> P y)" by auto
+ }
qed auto
end
-
--- a/src/HOL/Import/Import_Setup.thy Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Import/Import_Setup.thy Fri Jan 24 10:22:17 2025 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/Import/Import_Setup.thy
Author: Cezary Kaliszyk, University of Innsbruck
Author: Alexander Krauss, QAware GmbH
+ Author: Makarius
*)
section \<open>Importer machinery\<close>
@@ -11,6 +12,17 @@
begin
ML_file \<open>import_data.ML\<close>
+
+text \<open>
+ Initial type and constant maps, for types and constants that are not
+ defined, which means their definitions do not appear in the proof dump.
+\<close>
+import_type_map bool : bool
+import_type_map "fun" : "fun"
+import_type_map ind : ind
+import_const_map "=" : HOL.eq
+import_const_map "@" : Eps
+
ML_file \<open>import_rule.ML\<close>
end
--- a/src/HOL/Import/import_data.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Import/import_data.ML Fri Jan 24 10:22:17 2025 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/Import/import_data.ML
Author: Cezary Kaliszyk, University of Innsbruck
Author: Alexander Krauss, QAware GmbH
+ Author: Makarius
Importer data.
*)
@@ -97,15 +98,15 @@
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)))
+ (fn (c, d) => Thm.declaration_attribute
+ (fn th => Context.mapping (add_const_def c th d) I)))
"declare a theorem as an equality that maps the given constant")
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)))
+ (fn ((c, abs), rep) => Thm.declaration_attribute
+ (fn th => Context.mapping (add_typ_def c abs rep th) I)))
"declare a type_definition theorem as a map for an imported type with abs and rep")
val _ =
@@ -120,14 +121,4 @@
((Parse.name --| \<^keyword>\<open>:\<close>) -- Parse.const >>
(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>)
-
end
--- a/src/HOL/Import/import_rule.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Import/import_rule.ML Fri Jan 24 10:22:17 2025 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/Import/import_rule.ML
Author: Cezary Kaliszyk, University of Innsbruck
Author: Alexander Krauss, QAware GmbH
+ Author: Makarius
Importer proof rules and processing of lines and files.
@@ -9,141 +10,111 @@
signature IMPORT_RULE =
sig
- val beta : cterm -> thm
- val eq_mp : thm -> thm -> thm
- val comb : thm -> thm -> thm
- val trans : thm -> thm -> thm
- val deduct : thm -> thm -> thm
- val conj1 : thm -> thm
- val conj2 : thm -> thm
- val refl : cterm -> thm
- val abs : cterm -> thm -> thm
- val mdef : theory -> string -> thm
- val def : string -> cterm -> theory -> thm * theory
- val mtydef : theory -> string -> thm
- val tydef :
- string -> string -> string -> cterm -> cterm -> thm -> theory -> thm * theory
- val inst_type : (ctyp * ctyp) list -> thm -> thm
- val inst : (cterm * cterm) list -> thm -> thm
+ val trace : bool Config.T
val import_file : Path.T -> theory -> theory
end
structure Import_Rule: IMPORT_RULE =
struct
-fun implies_elim_all th = implies_elim_list th (map Thm.assume (cprems_of th))
+(* tracing *)
+
+val trace = Attrib.setup_config_bool \<^binding>\<open>import_trace\<close> (K false)
+
+type name = {hol: string, isabelle: string}
+
+fun print_name {hol, isabelle} =
+ if hol = isabelle then quote hol
+ else quote hol ^ " = " ^ quote isabelle
-fun meta_mp th1 th2 =
+fun print_item kind name =
+ Markup.markup Markup.keyword1 kind ^ " " ^ print_name name
+
+fun tracing_item thy kind name =
+ if Config.get_global thy trace then tracing (print_item kind name) else ()
+
+
+
+(** primitive rules of HOL Light **)
+
+fun to_obj_eq th =
let
- val th1a = implies_elim_all th1
- val th1b = Thm.implies_intr (Thm.cconcl_of th2) th1a
- val th2a = implies_elim_all th2
- val th3 = Thm.implies_elim th1b th2a
+ val (t, u) = Thm.dest_equals (Thm.cprop_of th)
+ val A = Thm.ctyp_of_cterm t
+ val rl = \<^instantiate>\<open>(no_beta) 'a = A and t and u in lemma \<open>t \<equiv> u \<Longrightarrow> t = u\<close> by simp\<close>
in
- implies_intr_hyps th3
+ Thm.implies_elim rl th
end
-fun meta_eq_to_obj_eq th =
+fun to_meta_eq th =
let
- val (t, u) = Thm.dest_equals (Thm.cconcl_of th)
+ val (t, u) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_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}
+ val rl = \<^instantiate>\<open>(no_beta) 'a = A and t and u in lemma \<open>t = u \<Longrightarrow> t \<equiv> u\<close> by simp\<close>
in
Thm.implies_elim rl th
end
-fun beta ct = meta_eq_to_obj_eq (Thm.beta_conversion false ct)
+
+(* basic logic *)
+
+fun refl t =
+ \<^instantiate>\<open>(no_beta) 'a = \<open>Thm.ctyp_of_cterm t\<close> and t in lemma \<open>t = t\<close> by (fact refl)\<close>
+
+fun trans th1 th2 =
+ Thm.transitive (to_meta_eq th1) (to_meta_eq th2) |> to_obj_eq
+
+fun mk_comb th1 th2 =
+ Thm.combination (to_meta_eq th1) (to_meta_eq th2) |> to_obj_eq
+
+fun abs x th =
+ to_meta_eq th |> Thm.abstract_rule (Term.term_name (Thm.term_of x)) x |> to_obj_eq
+
+fun beta t = Thm.beta_conversion false t |> to_obj_eq
+
+val assume = Thm.assume_cterm o HOLogic.mk_judgment
fun eq_mp th1 th2 =
let
- 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
+ val (Q, P) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th1))
+ val rl = \<^instantiate>\<open>(no_beta) P and Q in lemma \<open>Q = P \<Longrightarrow> Q \<Longrightarrow> P\<close> by (fact iffD1)\<close>
in
- meta_mp i2 th2
- end
-
-fun comb th1 th2 =
- let
- 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
+ Thm.implies_elim (Thm.implies_elim rl th1) th2
end
-fun trans th1 th2 =
+fun deduct_antisym_rule th1 th2 =
let
- 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
+ val Q = Thm.cprop_of th1
+ val P = Thm.cprop_of th2
+ val th1' = Thm.implies_intr P th1
+ val th2' = Thm.implies_intr Q th2
+ val rl =
+ \<^instantiate>\<open>(no_beta)
+ P = \<open>HOLogic.dest_judgment P\<close> and
+ Q = \<open>HOLogic.dest_judgment Q\<close>
+ in lemma \<open>(P \<Longrightarrow> Q) \<Longrightarrow> (Q \<Longrightarrow> P) \<Longrightarrow> Q = P\<close> by (rule iffI)\<close>
in
- meta_mp i2 th2
- end
-
-fun deduct th1 th2 =
- let
- 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 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
- val i4 = Thm.implies_elim i3 th2b
- in
- implies_intr_hyps i4
+ Thm.implies_elim (Thm.implies_elim rl th1') th2'
end
fun conj1 th =
let
- val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th))
- val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct1}
+ val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th))
+ val rl = \<^instantiate>\<open>(no_beta) P and Q in lemma \<open>P \<and> Q \<Longrightarrow> P\<close> by (fact conjunct1)\<close>
in
- meta_mp i th
+ Thm.implies_elim rl th
end
fun conj2 th =
let
- val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th))
- val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct2}
+ val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th))
+ val rl = \<^instantiate>\<open>(no_beta) P and Q in lemma \<open>P \<and> Q \<Longrightarrow> Q\<close> by (fact conjunct2)\<close>
in
- meta_mp i th
+ Thm.implies_elim rl th
end
-fun refl t =
- let val A = Thm.ctyp_of_cterm t
- in Thm.instantiate' [SOME A] [SOME t] @{thm refl} end
-fun abs x th =
- let
- val th1 = implies_elim_all th
- 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
- |> 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 th2
- end
+(* instantiation *)
fun freezeT thy th =
let
@@ -156,7 +127,7 @@
Thm.instantiate (tyinst, Vars.empty) th
end
-fun freeze thy = freezeT thy #> (fn th =>
+fun freeze' th =
let
val vars = Vars.build (th |> Thm.add_vars)
val inst = vars |> Vars.map (fn _ => fn v =>
@@ -166,18 +137,42 @@
in Thm.free (x, ty) end)
in
Thm.instantiate (TVars.empty, inst) th
- end)
+ end
+
+fun freeze thy = freezeT thy #> freeze';
+
+fun inst_type theta =
+ let
+ val tyinst =
+ TFrees.build (theta |> fold (fn (a, b) =>
+ TFrees.add (Term.dest_TFree (Thm.typ_of a), b)))
+ in
+ Thm.instantiate_frees (tyinst, Frees.empty)
+ end
-fun def' c rhs thy =
+fun inst theta th =
let
+ val inst =
+ Frees.build (theta |> fold (fn (a, b) =>
+ Frees.add (Term.dest_Free (Thm.term_of a), b)))
+ in
+ Thm.instantiate_frees (TFrees.empty, inst) th
+ end
+
+
+(* constant definitions *)
+
+fun def' (name as {isabelle = c, ...}) rhs thy =
+ let
+ val _ = tracing_item thy "const" name;
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
+ val def_thm = freezeT thy1 th |> to_obj_eq
in
- (meta_eq_to_obj_eq def_thm, thy2)
+ (def_thm, thy2)
end
fun mdef thy name =
@@ -185,21 +180,24 @@
SOME th => th
| NONE => error ("Constant mapped, but no definition: " ^ quote name))
-fun def c rhs thy =
+fun def (name as {isabelle = 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
+ (warning ("Const mapped, but def provided: " ^ quote c); (freeze thy (mdef thy c), thy))
+ else def' name (Thm.term_of rhs) thy
+
+
+(* type definitions *)
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)"
+ \<^instantiate>\<open>(no_beta) 'a = A and 'b = B and Rep = rep and Abs = abs and P = pred and a and r
+ in 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)}
+ type_definition.Rep mem_Collect_eq)\<close>
fun typedef_hollight th =
let
val ((rep, abs), P) =
- Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
+ Thm.dest_comb (HOLogic.dest_judgment (Thm.cprop_of th))
|>> (Thm.dest_comb #>> Thm.dest_arg)
||> Thm.dest_arg
val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep)
@@ -207,145 +205,148 @@
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 =
+fun tydef' (name as {isabelle = tycname, ...}) abs_name rep_name P t witness thy =
let
- val ctT = Thm.ctyp_of_cterm ct
- 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_>\<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 _ = tracing_item thy "type" name;
+
+ val T = Thm.ctyp_of_cterm t
+ val nonempty =
+ \<^instantiate>\<open>(no_beta) 'a = T and P and t
+ in lemma "P t \<Longrightarrow> \<exists>x. x \<in> Collect P" by auto\<close>
+ |> Thm.elim_implies witness
+ val \<^Const_>\<open>Trueprop for \<^Const_>\<open>Ex _ for \<open>Abs (_, _, \<^Const_>\<open>Set.member _ for _ set\<close>)\<close>\<close>\<close> =
+ Thm.concl_of nonempty
+
+ val tfrees = Term.add_tfrees set []
val tnames = sort_strings (map fst tfrees)
val typedef_bindings =
{Rep_name = Binding.name rep_name,
Abs_name = Binding.name abs_name,
type_definition_name = Binding.name ("type_definition_" ^ tycname)}
val ((_, typedef_info), thy') =
- Named_Target.theory_map_result (apsnd o Typedef.transform_info)
- (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
+ Typedef.add_typedef_global {overloaded = false}
+ (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) set
+ (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [nonempty] 1) thy
val aty = Thm.global_ctyp_of thy' (#abs_type (#1 typedef_info))
val th = freezeT thy' (#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 (rep, abs) = Thm.dest_binop (Thm.dest_fun (HOLogic.dest_judgment (Thm.cprop_of th)))
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))
+ val typedef_th = typedef_hol2hollight A B rep abs P (Thm.free ("a", aty)) (Thm.free ("r", T))
in
(typedef_th OF [#type_definition (#2 typedef_info)], thy')
end
fun mtydef thy name =
(case Import_Data.get_typ_def thy name of
- SOME th => meta_mp (typedef_hollight th) th
+ SOME th => Thm.implies_elim (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 =
+fun tydef (name as {hol = 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
+ else tydef' name abs_name rep_name P t td_th thy
+
+
-fun inst_type lambda =
- let
- val tyinst =
- TFrees.build (lambda |> fold (fn (a, b) =>
- TFrees.add (Term.dest_TFree (Thm.typ_of a), b)))
- in
- Thm.instantiate_frees (tyinst, Frees.empty)
- end
+(** importer **)
+
+(* basic entities *)
+
+fun make_name hol =
+ {hol = hol, isabelle = String.translate (fn #"." => "dot" | c => Char.toString c) hol}
-fun inst sigma th =
- let
- val (dom, rng) = ListPair.unzip (rev sigma)
- in
- th |> forall_intr_list dom
- |> forall_elim_list rng
- end
+fun make_bound a =
+ (case try (unprefix "_") a of
+ SOME b => if forall_string Symbol.is_ascii_digit b then "u" else b
+ | NONE => a);
-val make_name = String.translate (fn #"." => "dot" | c => Char.toString c)
-
-fun make_free (x, ty) = Free (make_name x, ty)
+fun make_free x ty = Thm.free (#isabelle (make_name x), ty);
-fun make_tfree a =
+fun make_tfree thy a =
let val b = "'" ^ String.translate (fn #"?" => "t" | c => Char.toString c) a
- in TFree (b, \<^sort>\<open>type\<close>) end
+ in Thm.global_ctyp_of thy (TFree (b, \<^sort>\<open>type\<close>)) end
-fun make_type thy (c, args) =
+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
+ | NONE => Sign.full_bname thy (#isabelle (make_name c)))
+ val T = Thm.global_ctyp_of thy (Type (d, replicate (length args) dummyT))
+ in Thm.make_ctyp T args end
-fun make_const thy (c, ty) =
+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
+ | NONE => Sign.full_bname thy (#isabelle (make_name c)))
+ in Thm.global_cterm_of thy (Const (d, Thm.typ_of ty)) end
+
+val make_thm = Skip_Proof.make_thm_cterm o HOLogic.mk_judgment
+(* import file *)
+
+local
+
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 (tab, no) s =
+fun get (tab, reg) 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))))
+ | SOME res => (res, (if i < 0 then Inttab.delete (Int.abs i) tab else tab, reg))))
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;
+val theory = `get_theory;
+fun theory_op f (State (thy, a, b, c)) = let val (y, thy') = f thy in (y, State (thy', a, b, c)) end;
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 set (tab, no) v = (Inttab.update_new (no + 1, v) tab, no + 1)
+val typs = fold_map typ
+val terms = fold_map term
+
+fun set (tab, reg) res = (Inttab.update_new (reg + 1, res) tab, reg + 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 stored_thm name (State (thy, a, b, c)) =
+ let val th = freeze thy (Global_Theory.get_thm thy name)
+ in State (thy, a, b, set c th) end
+
+fun store_thm name (State (thy, a, b, c as (tab, reg))) =
+ let
+ val _ = tracing_item thy "thm" name;
-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"
+ val th =
+ (case Inttab.lookup tab reg of
+ NONE => raise Fail "store_thm: lookup failed"
+ | SOME th0 => Drule.export_without_context_open th0)
+
+ val tvars = TVars.build (Thm.fold_terms {hyps = false} TVars.add_tvars th);
+ val names = Name.invent_global_types (TVars.size tvars)
+ val tyinst =
+ TVars.build (fold2
+ (fn v as ((_, i), S) => fn b => TVars.add (v, Thm.global_ctyp_of thy (TVar ((b, i), S))))
+ (TVars.list_set tvars) names)
+
+ val th' = Thm.instantiate (tyinst, Vars.empty) th
+ val thy' = #2 (Global_Theory.add_thm ((Binding.name (#isabelle name), th'), []) thy)
+ in State (thy', a, b, c) end
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 th0 thy =
- let
- val ctxt = Proof_Context.init_global thy
- 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 th' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) th
- in
- snd (Global_Theory.add_thm ((binding, th'), []) thy)
- end
-
fun parse_line s =
(case String.tokens (fn x => x = #"\n" orelse x = #" ") s of
[] => raise Fail "parse_line: empty"
@@ -354,81 +355,43 @@
[] => raise Fail "parse_line: empty command"
| c :: cs => (c, String.implode cs :: args)))
-fun process_line str =
- let
- 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 thy = get_theory state
- val th = Global_Theory.get_thm thy s
- in
- set_thm (freeze thy th) state
- end)
- | process (#"Q", l) = (fn state =>
- let
- val (tys, th) = list_last l
- val (th, state1) = thm th state
- val (tys, state2) = fold_map typ tys state1
- in
- set_thm (inst_type (pair_list tys) th) state2
- end)
- | process (#"S", l) = (fn state =>
- let
- val (tms, th) = list_last l
- val (th, state1) = thm th state
- val (tms, state2) = fold_map term tms state1
- in
- set_thm (inst (pair_list tms) th) state2
- end)
- | process (#"F", [name, t]) = (fn state =>
- let
- val (tm, state1) = term t state
- in
- 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 (parse_line str)
- end
+fun command (#"R", [t]) = term t #>> refl #-> set_thm
+ | command (#"B", [t]) = term t #>> beta #-> set_thm
+ | command (#"1", [th]) = thm th #>> conj1 #-> set_thm
+ | command (#"2", [th]) = thm th #>> conj2 #-> set_thm
+ | command (#"H", [t]) = term t #>> assume #-> set_thm
+ | command (#"A", [_, t]) = term t #>> make_thm #-> set_thm
+ | command (#"C", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry mk_comb #-> set_thm
+ | command (#"T", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry trans #-> set_thm
+ | command (#"E", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry eq_mp #-> set_thm
+ | command (#"D", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry deduct_antisym_rule #-> set_thm
+ | command (#"L", [t, th]) = term t ##>> thm th #>> uncurry abs #-> set_thm
+ | command (#"M", [name]) = stored_thm name
+ | command (#"Q", args) =
+ split_last args |> (fn (tys, th) => thm th #-> (fn th => typs tys #-> (fn tys =>
+ set_thm (inst_type (pair_list tys) th))))
+ | command (#"S", args) =
+ split_last args |> (fn (ts, th) => thm th #-> (fn th => terms ts #-> (fn ts =>
+ set_thm (inst (pair_list ts) th))))
+ | command (#"F", [name, t]) =
+ term t #-> (fn t => theory_op (def (make_name name) t) #-> set_thm)
+ | command (#"F", [name]) = theory #-> (fn thy => set_thm (mdef thy name))
+ | command (#"Y", [name, abs, rep, t1, t2, th]) =
+ thm th #-> (fn th => term t1 #-> (fn t1 => term t2 #-> (fn t2 =>
+ theory_op (tydef (make_name name) abs rep t1 t2 th) #-> set_thm)))
+ | command (#"Y", [name, _, _]) = theory #-> (fn thy => set_thm (mtydef thy name))
+ | command (#"t", [a]) = theory #-> (fn thy => set_typ (make_tfree thy a))
+ | command (#"a", c :: tys) = theory #-> (fn thy => typs tys #>> make_type thy c #-> set_typ)
+ | command (#"v", [x, ty]) = typ ty #>> make_free x #-> set_term
+ | command (#"c", [c, ty]) = theory #-> (fn thy => typ ty #>> make_const thy c #-> set_term)
+ | command (#"f", [t, u]) = term t #-> (fn t => term u #-> (fn u => set_term (Thm.apply t u)))
+ | command (#"l", [x, t]) =
+ term x #-> (fn x => term t #-> (fn t =>
+ set_term (Thm.lambda_name (make_bound (#1 (dest_Free (Thm.term_of x))), x) t)))
+ | command (#"+", [name]) = store_thm (make_name name)
+ | command (c, _) = raise Fail ("process: unknown command: " ^ String.str c)
+
+in
fun import_file path0 thy =
let
@@ -436,10 +399,12 @@
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
+ in init_state thy |> fold (parse_line #> command) lines |> get_theory end
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
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/offline/maps.lst Fri Jan 24 10:22:17 2025 +0100
@@ -0,0 +1,197 @@
+T_DEF
+AND_DEF
+IMP_DEF
+FORALL_DEF
+EXISTS_DEF
+OR_DEF
+F_DEF
+NOT_DEF
+EXISTS_UNIQUE_DEF
+_FALSITY_
+ETA_AX hl_ax1
+SELECT_AX hl_ax2
+COND_DEF
+DEF_o
+I_DEF
+TYDEF_1
+one_DEF
+DEF_mk_pair
+TYDEF_prod
+DEF_,
+DEF_FST
+DEF_SND
+DEF_CURRY -
+CURRY_DEF CURRY_DEF
+DEF_ONE_ONE
+DEF_ONTO
+INFINITY_AX hl_ax3
+TYDEF_num -
+ZERO_DEF -
+DEF_SUC -
+SUC_DEF -
+NOT_SUC NOT_SUC
+SUC_INJ SUC_INJ
+num_INDUCTION num_INDUCTION
+DEF_NUMERAL
+num_Axiom num_Axiom
+DEF_BIT0
+DEF_BIT1
+DEF_WF -
+WF WF
+DEF_PRE -
+PRE PRE
+DEF_+ -
+ADD ADD
+DEF_* -
+MULT MULT
+DEF_EXP -
+EXP EXP
+DEF_<= -
+LE LE
+DEF_< -
+LT LT
+DEF_>=
+DEF_>
+DEF_MAX
+DEF_MIN
+DEF_EVEN -
+EVEN EVEN
+DEF_- -
+SUB SUB
+DEF_FACT -
+FACT FACT
+DEF_DIV -
+DEF_MOD -
+DIVISION_0 DIVISION_0
+TYDEF_sum -
+DEF_INL -
+DEF_INR -
+sum_RECURSION sum_RECURSION
+sum_INDUCT sum_INDUCT
+DEF_OUTL -
+OUTL OUTL
+DEF_OUTR -
+OUTR OUTR
+TYDEF_list -
+DEF_NIL -
+DEF_CONS -
+list_RECURSION list_RECURSION
+list_INDUCT list_INDUCT
+DEF_HD -
+HD HD
+DEF_TL -
+TL TL
+DEF_APPEND -
+APPEND APPEND
+DEF_LENGTH -
+LENGTH LENGTH
+DEF_MAP -
+MAP MAP
+DEF_LAST -
+LAST LAST
+TYDEF_real -
+DEF_real_of_num -
+real_of_num -
+real_of_num_th -
+DEF_real_neg -
+real_neg -
+real_neg_th -
+DEF_real_add -
+real_add -
+real_add_th -
+DEF_real_mul -
+real_mul -
+real_mul_th -
+DEF_real_le -
+real_le -
+real_le_th -
+DEF_real_inv -
+real_inv -
+real_inv_th -
+REAL_ADD_SYM REAL_ADD_SYM
+REAL_ADD_ASSOC REAL_ADD_ASSOC
+REAL_ADD_LID REAL_ADD_LID
+REAL_ADD_LINV REAL_ADD_LINV
+REAL_MUL_SYM REAL_MUL_SYM
+REAL_MUL_ASSOC REAL_MUL_ASSOC
+REAL_MUL_LID REAL_MUL_LID
+REAL_ADD_LDISTRIB REAL_ADD_LDISTRIB
+REAL_LE_REFL REAL_LE_REFL
+REAL_LE_ANTISYM REAL_LE_ANTISYM
+REAL_LE_TRANS REAL_LE_TRANS
+REAL_LE_TOTAL REAL_LE_TOTAL
+REAL_LE_LADD_IMP REAL_LE_LADD_IMP
+REAL_LE_MUL REAL_LE_MUL
+REAL_OF_NUM_LE REAL_OF_NUM_LE
+DEF_real_sub -
+real_sub real_sub
+DEF_real_lt -
+real_lt real_lt
+DEF_real_ge -
+real_ge real_ge
+DEF_real_gt -
+real_gt real_gt
+DEF_real_abs -
+real_abs real_abs
+DEF_real_pow -
+DEF_real_div -
+real_div real_div
+DEF_real_max -
+real_max real_max
+DEF_real_min -
+real_min real_min
+DEF_real_sgn -
+real_sgn real_sgn
+REAL_HREAL_LEMMA1 -
+REAL_HREAL_LEMMA2 -
+REAL_COMPLETE_SOMEPOS REAL_COMPLETE_SOMEPOS
+REAL_OF_NUM_MUL REAL_OF_NUM_MUL
+REAL_OF_NUM_ADD REAL_OF_NUM_ADD
+REAL_OF_NUM_EQ REAL_OF_NUM_EQ
+REAL_INV_0 REAL_INV_0
+REAL_MUL_LINV REAL_MUL_LINV
+TYDEF_int -
+DEF_integer -
+integer integer
+int_rep int_rep
+int_abstr int_abstr
+dest_int_rep dest_int_rep
+int_eq int_eq
+DEF_int_le -
+int_le int_le
+DEF_int_ge -
+int_ge int_ge
+DEF_int_lt -
+int_lt int_lt
+DEF_int_gt -
+int_gt int_gt
+DEF_int_of_num -
+int_of_num int_of_num
+int_of_num_th int_of_num_th
+int_neg -
+int_neg_th int_neg_th
+DEF_int_add -
+int_add -
+int_add_th int_add_th
+DEF_int_sub -
+int_sub -
+int_sub_th int_sub_th
+DEF_int_mul -
+int_mul -
+int_mul_th int_mul_th
+DEF_int_abs -
+int_abs -
+int_abs_th int_abs_th
+DEF_int_sgn -
+int_sgn -
+int_sgn_th int_sgn_th
+DEF_int_max -
+int_max -
+int_max_th int_max_th
+DEF_int_min -
+int_min -
+int_min_th int_min_th
+DEF_int_pow -
+int_pow -
+int_pow_th int_pow_th
+INT_IMAGE INT_IMAGE
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/offline/offline.ml Fri Jan 24 10:22:17 2025 +0100
@@ -0,0 +1,324 @@
+(* Title: HOL/Import/offline/offline.ml
+ Author: Cezary Kaliszyk, University of Innsbruck
+ Author: Alexander Krauss, QAware GmbH
+
+Stand-alone OCaml program for post-processing of HOL Light export:
+
+ - input files: facts.lst, maps.lst, proofs
+ - output files: facts.lstN, proofsN
+
+Compile and run "offline/offline.ml" like this:
+
+ ocamlopt offline.ml -o offline
+ > maps.lst
+ ./offline # this uses a lot of memory
+
+Format of maps.lst:
+
+ THM1 THM2
+ map HOL Light THM1 to Isabelle/HOL THM2 and forget its deps
+ THM -
+ do not record THM and make sure it is not used (its deps must be mapped)
+ THM
+ the definition of constant/type is mapped in Isabelle/HOL, so forget
+ its deps and look its map up when defining (may fail at import time)
+*)
+
+let output_int oc i = output_string oc (string_of_int i);;
+let string_list_of_string str sep =
+ let rec slos_aux str ans =
+ if str = "" then ans else
+ try
+ let first_space = String.index str sep in
+ if first_space = 0 then
+ slos_aux (String.sub str 1 (String.length str - 1)) ans
+ else
+ slos_aux
+ (String.sub str (first_space + 1)(String.length str - 1 - first_space))
+ ((String.sub str 0 (first_space)) :: ans)
+ with
+ Not_found ->
+ List.rev (str :: ans)
+ in slos_aux str []
+;;
+
+module SM = Map.Make(struct type t = string let compare = compare end);;
+module IM = Map.Make(struct type t = int let compare = compare end);;
+let facts = ref SM.empty;;
+let maps = ref IM.empty;;
+let facts_rev = ref IM.empty;;
+
+let rec addfact s n =
+ if SM.mem s (!facts) then failwith ("addfact:" ^ s) else
+ if IM.mem n (!facts_rev) then () else (
+ facts := SM.add s n (!facts);
+ facts_rev := IM.add n s (!facts_rev));;
+
+let read_facts () =
+ let inc = open_in "facts.lst" in
+ (try
+ while true do
+ let l = (string_list_of_string (input_line inc) ' ') in
+ let no = int_of_string (List.nth l 1) in
+ addfact (List.hd l) no
+ done
+ with End_of_file -> close_in inc);
+ (let inc = open_in "maps.lst" in
+ try
+ while true do
+ let (hl_name :: t) = (string_list_of_string (input_line inc) ' ') in
+ let no = try SM.find hl_name (!facts) with Not_found -> failwith ("read facts: " ^ hl_name) in
+ facts := SM.remove hl_name (!facts);
+ let isa_name = if t = [] then "" else List.hd t in
+ maps := IM.add no isa_name (!maps);
+ done
+ with End_of_file -> close_in inc);;
+
+let tyno = ref 0;;
+let tmno = ref 0;;
+let thno = ref 0;;
+let ios s = abs(int_of_string s);;
+
+let process thth thtm tmtm thty tmty tyty = function
+ ('R', [t]) -> incr thno; thtm (ios t)
+| ('B', [t]) -> incr thno; thtm (ios t)
+| ('T', [p; q]) -> incr thno; thth (ios p); thth (ios q)
+| ('C', [p; q]) -> incr thno; thth (ios p); thth (ios q)
+| ('L', [t; p]) -> incr thno; thth (ios p); thtm (ios t)
+| ('H', [t]) -> incr thno; thtm (ios t)
+| ('E', [p; q]) -> incr thno; thth (ios p); thth (ios q)
+| ('D', [p; q]) -> incr thno; thth (ios p); thth (ios q)
+| ('Q', ((h :: t) as l)) -> incr thno; thth (ios (List.hd (List.rev l)));
+ List.iter thty (List.map ios (List.tl (List.rev l)))
+| ('S', ((h :: t) as l)) -> incr thno; thth (ios (List.hd (List.rev l)));
+ List.iter thtm (List.map ios (List.tl (List.rev l)))
+| ('A', [_; t]) -> incr thno; thtm (ios t)
+| ('F', [_; t]) -> incr thno; thtm (ios t)
+| ('Y', [_; _; _; t; s; p]) -> incr thno; thth (ios p); thtm (ios t); thtm (ios s)
+| ('1', [p]) -> incr thno; thth (ios p)
+| ('2', [p]) -> incr thno; thth (ios p)
+| ('t', [_]) -> incr tyno
+| ('a', (h :: t)) -> incr tyno; List.iter tyty (List.map ios t)
+| ('v', [_; ty]) -> incr tmno; tmty (ios ty)
+| ('c', [_; ty]) -> incr tmno; tmty (ios ty)
+| ('f', [t; s]) -> incr tmno; tmtm (ios t); tmtm (ios s)
+| ('l', [t; s]) -> incr tmno; tmtm (ios t); tmtm (ios s)
+| (c, l) -> failwith ((String.make 1 c) ^ (String.concat " " l))
+;;
+
+let thth = Array.make 155097624 [];;
+let tmth = Array.make 55000000 [];;
+let tmtm = Array.make 55000000 [];;
+let tyth = Array.make 200000 [];;
+let tytm = Array.make 200000 [];;
+let tyty = Array.make 200000 [];;
+
+let needth no = not (IM.mem no !maps);;
+
+let addthth s = if needth !thno then thth.(s) <- !thno :: thth.(s);;
+let addtmth s = if needth !thno then tmth.(s) <- !thno :: tmth.(s);;
+let addtyth s = if needth !thno then tyth.(s) <- !thno :: tyth.(s);;
+let addtmtm s = tmtm.(s) <- !tmno :: tmtm.(s);;
+let addtytm s = tytm.(s) <- !tmno :: tytm.(s);;
+let addtyty s = tyty.(s) <- !tyno :: tyty.(s);;
+
+let add_facts_deps () =
+ thth.(0) <- 0 :: thth.(0);
+ SM.iter (fun _ n -> thth.(n) <- 0 :: thth.(n)) !facts
+;;
+
+let process_all thth thtm tmtm thty tmty tyty =
+ tyno := 0; tmno := 0; thno := 0;
+ let inc = open_in "proofs" in
+ try while true do
+ let c = input_char inc in
+ let s = input_line inc in
+ process thth thtm tmtm thty tmty tyty (c, (string_list_of_string s ' '))
+ done
+ with End_of_file -> close_in inc;;
+
+let count_nonnil l =
+ Array.fold_left (fun n l -> if l = [] then n else n + 1) 0 l;;
+
+let clean tab filter =
+ for i = Array.length tab - 1 downto 1 do
+ tab.(i) <- List.filter filter tab.(i)
+ done;;
+
+let clean_all () =
+ clean thth (fun j -> not (thth.(j) = []));
+ clean tmth (fun j -> not (thth.(j) = []));
+ clean tmtm (fun j -> not (tmth.(j) = [] && tmtm.(j) = []));
+ clean tyth (fun j -> not (thth.(j) = []));
+ clean tytm (fun j -> not (tmth.(j) = [] && tmtm.(j) = []));
+ clean tyty (fun j -> not (tyth.(j) = [] && tytm.(j) = [] && tyty.(j) = []))
+;;
+
+read_facts ();;
+let facts_rev = !facts_rev;;
+add_facts_deps ();;
+process_all addthth addtmth addtmtm addtyth addtytm addtyty;;
+
+print_string "thms: "; print_int !thno;
+print_string " tms: "; print_int !tmno;
+print_string " tys: "; print_int !tyno; print_newline (); flush stdout;;
+print_string "Direct uses: th->th th->tm tm->tm th->ty tm->ty ty->ty: \n";
+print_int (count_nonnil thth); print_char ' ';
+print_int (count_nonnil tmth); print_char ' ';
+print_int (count_nonnil tmtm); print_char ' ';
+print_int (count_nonnil tyth); print_char ' ';
+print_int (count_nonnil tytm); print_char ' ';
+print_int (count_nonnil tyty); print_newline (); flush stdout;;
+clean_all ();;
+
+print_string "After removing:\n";
+print_string "Depends: th->th th->tm tm->tm th->ty tm->ty ty->ty: \n";
+print_int (count_nonnil thth); print_char ' ';
+print_int (count_nonnil tmth); print_char ' ';
+print_int (count_nonnil tmtm); print_char ' ';
+print_int (count_nonnil tyth); print_char ' ';
+print_int (count_nonnil tytm); print_char ' ';
+print_int (count_nonnil tyty); print_newline (); flush stdout;;
+
+let rev_tables () =
+ let rev_tab t =
+ for i = 0 to Array.length t - 1 do
+ t.(i) <- List.rev (t.(i));
+ done
+ in
+ rev_tab thth; rev_tab tmth; rev_tab tyth;
+ rev_tab tmtm; rev_tab tytm; rev_tab tyty
+;;
+print_char 'c'; flush stdout;;
+rev_tables ();;
+print_char 'C'; flush stdout;;
+
+let othnth = Array.make 155300000 0;;
+let otmntm = Array.make 55000000 0;;
+let otynty = Array.make 200000 0;;
+
+let outl oc tag ss is =
+ let ss = ss @ (List.map string_of_int is) in
+ output_char oc tag; output_string oc (String.concat " " ss); output_char oc '\n'
+;;
+let ntyno = ref 0;; let ntmno = ref 0;; let nthno = ref 0;;
+let ty t i = (*!ntyno -*)
+ t.(i) <- List.tl t.(i);
+ if tyth.(i) = [] && tytm.(i) = [] && tyty.(i) = [] then (- otynty.(i)) else otynty.(i);;
+let tm t i = (*!ntmno -*)
+ t.(i) <- List.tl t.(i);
+ if tmth.(i) = [] && tmtm.(i) = [] then (- otmntm.(i)) else otmntm.(i);;
+let th i = (*!nthno -*)
+(* (if List.hd thth.(i) = 0 then (print_int !thno));*)
+ thth.(i) <- List.tl thth.(i);
+ if thth.(i) = [] then (- othnth.(i)) else othnth.(i);;
+
+let rec itlist f l b =
+ match l with
+ [] -> b
+ | (h::t) -> f h (itlist f t b);;
+
+let insert x l =
+ if List.mem x l then l else x::l;;
+
+let union l1 l2 = itlist insert l1 l2;;
+
+let rec neededby l acc =
+ match l with [] -> acc
+ | h :: t ->
+ try if List.length acc > 10 then acc else
+ neededby t (insert (IM.find h facts_rev) acc)
+ with Not_found -> neededby (union thth.(h) t) acc
+;;
+let neededby l = String.concat " " (neededby l [])
+
+let outt oc tag ss tys tms ths =
+ if thth.(!thno) = [] then () else
+ begin
+ incr nthno;
+ othnth.(!thno) <- !nthno;
+ begin
+ try
+ let s = IM.find (!thno) (!maps) in
+ if s = "-" then failwith ("removed thm:" ^ IM.find !thno facts_rev ^ " around:" ^ neededby (thth.(!thno)))
+ else if s = "" then outl oc tag ss []
+ else outl oc 'M' [s] []
+ with Not_found ->
+ outl oc tag ss
+ (List.map (fun i -> ty tyth (ios i)) tys @ List.map
+ (fun i -> tm tmth (ios i)) tms @ List.map (fun i -> th (ios i)) ths)
+ end;
+ try outl oc '+' [IM.find (!thno) facts_rev] []
+ with Not_found -> ()
+ end
+;;
+
+let outtm oc tag ss tys tms =
+ if tmth.(!tmno) = [] && tmtm.(!tmno) = [] then () else
+ (incr ntmno; otmntm.(!tmno) <- !ntmno; outl oc tag ss (List.map (fun i -> ty tytm (ios i)) tys @ List.map (fun i -> tm tmtm (ios i)) tms))
+;;
+
+let outty oc tag ss tys =
+ if tyth.(!tyno) = [] && tytm.(!tyno) = [] && tyty.(!tyno) = [] then () else
+ (incr ntyno; otynty.(!tyno) <- !ntyno; outl oc tag ss (List.map (fun i -> ty tyty (ios i)) tys))
+;;
+
+let printer oc = function
+ ('R', [t]) -> incr thno; outt oc 'R' [] [] [t] []
+| ('B', [t]) -> incr thno; outt oc 'B' [] [] [t] []
+| ('T', [p; q]) -> incr thno; outt oc 'T' [] [] [] [p; q]
+| ('C', [p; q]) -> incr thno; outt oc 'C' [] [] [] [p; q]
+| ('L', [t; p]) -> incr thno; outt oc 'L' [] [] [t] [p]
+| ('H', [t]) -> incr thno; outt oc 'H' [] [] [t] []
+| ('E', [p; q]) -> incr thno; outt oc 'E' [] [] [] [p; q]
+| ('D', [p; q]) -> incr thno; outt oc 'D' [] [] [] [p; q]
+| ('Q', ((h :: t) as l)) -> incr thno;
+ let (th, tys) = (List.hd (List.rev l), List.rev (List.tl (List.rev l))) in
+ outt oc 'Q' [] tys [] [th]
+| ('S', ((h :: t) as l)) -> incr thno;
+ let (th, tms) = (List.hd (List.rev l), List.rev (List.tl (List.rev l))) in
+ outt oc 'S' [] [] tms [th]
+| ('A', [n; t]) -> incr thno; outt oc 'A' [n] [] [t] []
+| ('F', [n; t]) -> incr thno; outt oc 'F' [n] [] [t] []
+| ('Y', [n1; n2; n3; t; s; p]) -> incr thno; outt oc 'Y' [n1; n2; n3] [] [t; s] [p]
+| ('1', [p]) -> incr thno; outt oc '1' [] [] [] [p]
+| ('2', [p]) -> incr thno; outt oc '2' [] [] [] [p]
+| ('t', [n]) -> incr tyno; outty oc 't' [n] []
+| ('a', (h :: t)) -> incr tyno; outty oc 'a' [h] t
+| ('v', [n; ty]) -> incr tmno; outtm oc 'v' [n] [ty] []
+| ('c', [n; ty]) -> incr tmno; outtm oc 'c' [n] [ty] []
+| ('f', [t; s]) -> incr tmno; outtm oc 'f' [] [] [t; s]
+| ('l', [t; s]) -> incr tmno; outtm oc 'l' [] [] [t; s]
+| (c, l) -> failwith ((String.make 1 c) ^ (String.concat " " l))
+;;
+
+let print_all () =
+ tyno := 0; tmno := 0; thno := 0;
+ let inc = open_in "proofs" in
+ let oc = open_out "proofsN" in
+ try while true do
+ let c = input_char inc in
+ let s = input_line inc in
+ printer oc (c, string_list_of_string s ' ')
+ done
+ with End_of_file -> (close_in inc; close_out oc);;
+
+print_all ();;
+
+print_string "thms: "; print_int !nthno;
+print_string " tms: "; print_int !ntmno;
+print_string " tys: "; print_int !ntyno; print_newline (); flush stdout;;
+
+let inc = open_in "facts.lst" in
+let oc = open_out "facts.lstN" in
+try
+ while true do
+ let [name; no] = string_list_of_string (input_line inc) ' ' in
+ let no = int_of_string no in
+ try if IM.find no facts_rev = name then (
+ output_string oc name; output_char oc ' ';
+ output_int oc othnth.(no); output_char oc '\n'
+ ) else ()
+ with Not_found -> ()
+ done
+ with End_of_file -> (close_in inc; close_out oc);;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/patches/patch1 Fri Jan 24 10:22:17 2025 +0100
@@ -0,0 +1,24 @@
+--- hol-light/statements.ml 1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/statements.ml 2025-01-18 11:12:11.185279392 +0100
+@@ -0,0 +1,6 @@
++let dump_theorems () =
++ let oc = open_out "theorems" in
++ output_value oc (map (fun (a,b) -> (a, dest_thm b)) !theorems);
++ close_out oc
++;;
++dump_theorems ();;
+--- hol-light/stage1.ml 1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/stage1.ml 2025-01-18 11:12:11.185279392 +0100
+@@ -0,0 +1,5 @@
++#use "hol.ml";;
++(*LOAD MORE*)
++#use "update_database.ml";;
++#use "statements.ml";;
++exit 0;;
+--- hol-light/stage2.ml 1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/stage2.ml 2025-01-18 11:12:11.384276293 +0100
+@@ -0,0 +1,4 @@
++#use "hol.ml";;
++(*LOAD MORE*)
++stop_recording ();;
++exit 0;;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/patches/patch2 Fri Jan 24 10:22:17 2025 +0100
@@ -0,0 +1,361 @@
+--- hol-light/fusion.ml 2025-01-18 11:11:28.417955236 +0100
++++ hol-light-patched/fusion.ml 2025-01-18 11:12:11.384276293 +0100
+@@ -9,6 +9,18 @@
+
+ needs "lib.ml";;
+
++#load "unix.cma";;
++let poutc = open_out "proofs";;
++let foutc = open_out "facts.lst";;
++let stop_recording () = close_out poutc; close_out foutc;;
++
++let rec outl = function
++ [] -> ()
++| (h :: t) -> try
++ output_string poutc h; List.fold_left
++ (fun () e -> output_char poutc ' '; output_string poutc e) () t
++ with Sys_error _ -> ();;
++
+ module type Hol_kernel =
+ sig
+ type hol_type = private
+@@ -101,7 +113,165 @@
+ | Comb of term * term
+ | Abs of term * term
+
+- type thm = Sequent of (term list * term)
++ type thm = Sequent of (term list * term * int)
++(* PROOFRECORDING BEGIN *)
++let thms = Hashtbl.create 20000;;
++
++let inc = open_in "theorems";;
++let l = ((input_value inc) : ((string * (term list * term)) list));;
++close_in inc;;
++List.iter (fun (n,t) -> Hashtbl.replace thms t (n, 0)) l;;
++print_endline ("Read in: " ^ string_of_int (Hashtbl.length thms));;
++
++module Fm = Map.Make(struct type t = float let compare = compare end);;
++module Tys = Map.Make(struct type t = hol_type let compare = compare end);;
++module Tms = Map.Make(struct type t = term let compare = compare end);;
++module Ps = Map.Make(struct type t = (term list * term) let compare = compare end);;
++
++let ty_no = ref 0;;
++let tys = ref Tys.empty;;
++
++let rec out_type ty =
++ try
++ Tys.find ty !tys
++ with Not_found ->
++ match ty with
++ Tyvar t ->
++ incr ty_no; tys := Tys.add ty !ty_no !tys;
++ output_char poutc 't'; output_string poutc t; output_char poutc '\n';
++ !ty_no
++ | Tyapp (id, tl) ->
++ let tln = map out_type tl in
++ incr ty_no; tys := Tys.add ty !ty_no !tys;
++ output_char poutc 'a'; output_string poutc id; output_char poutc ' ';
++ outl (map string_of_int tln); output_char poutc '\n';
++ !ty_no;;
++
++let tm_no = ref 0;;
++let tms = ref Tms.empty;;
++let tms_prio = ref Fm.empty;;
++let tms_size = ref 0;;
++let tms_maxsize = ref (int_of_string (Sys.getenv "MAXTMS"));;
++let tm_lookup tm =
++ let (ret, oldtime) = Tms.find tm !tms in
++ let newtime = Unix.gettimeofday () in
++ tms := Tms.add tm (ret, newtime) !tms;
++ tms_prio := Fm.add newtime tm (Fm.remove oldtime !tms_prio);
++ ret;;
++
++let tm_delete () =
++ let (time, tm) = Fm.min_binding !tms_prio in
++ tms := Tms.remove tm !tms;
++ tms_prio := Fm.remove time !tms_prio;
++ decr tms_size; ();;
++
++let tm_add tm no =
++ while (!tms_size > !tms_maxsize) do tm_delete (); done;
++ let newtime = Unix.gettimeofday () in
++ tms := Tms.add tm (no, newtime) (!tms);
++ tms_prio := Fm.add newtime tm (!tms_prio);
++ incr tms_size; ();;
++
++let rec out_term tm =
++ try
++ tm_lookup tm
++ with Not_found ->
++ let outc = output_char poutc and out = output_string poutc in
++ match tm with
++ Var (name, ty) ->
++ let ty = out_type ty in
++ incr tm_no; tm_add tm !tm_no;
++ outc 'v'; out name; outc ' '; out (string_of_int ty); outc '\n';
++ !tm_no
++ | Const (name, ty) ->
++ let ty = out_type ty in
++ incr tm_no; tm_add tm !tm_no;
++ outc 'c'; out name; outc ' '; out (string_of_int ty); outc '\n';
++ !tm_no
++ | Comb (f, a) ->
++ let f = out_term f and a = out_term a in
++ incr tm_no; tm_add tm !tm_no;
++ outc 'f'; out (string_of_int f); outc ' '; out (string_of_int a); outc '\n';
++ !tm_no
++ | Abs (x, a) ->
++ let x = out_term x and a = out_term a in
++ incr tm_no; tm_add tm !tm_no;
++ outc 'l'; out (string_of_int x); outc ' '; out (string_of_int a); outc '\n';
++ !tm_no
++;;
++
++let prf_no = ref 0;;
++let outt tag ss tys tms pfs =
++ let tys = map out_type tys and
++ tms = map out_term tms in
++ try
++ output_char poutc tag;
++ outl (ss @ (map string_of_int tys)
++ @ (map string_of_int tms)
++ @ (map string_of_int pfs));
++ output_char poutc '\n'
++ with Sys_error _ -> ()
++;;
++
++let ps = ref Ps.empty;;
++
++let p_lookup p = Ps.find p !ps;;
++let p_add p no = ps := Ps.singleton p no;;
++
++let mk_prff f = incr prf_no; f (); !prf_no;;
++
++let chk_mk_prff f th =
++ try p_lookup th
++ with Not_found ->
++ try
++ let (name, i) = Hashtbl.find thms th in
++ if i > 0 then i else
++ let i = mk_prff f in
++ (ps := Ps.empty;
++ Hashtbl.replace thms th (name, i);
++ (try output_string foutc (name ^ " " ^ string_of_int i ^ "\n"); flush foutc with Sys_error _ -> ());
++ i)
++ with Not_found ->
++ mk_prff (fun () -> f (); p_add th !prf_no);;
++
++
++let mk_prf t l1 l2 l3 l4 _ = mk_prff (fun () -> outt t l1 l2 l3 l4);;
++let chk_mk_prf t l1 l2 l3 l4 th = chk_mk_prff (fun () -> outt t l1 l2 l3 l4) th;;
++let proof_REFL t th = chk_mk_prf 'R' [] [] [t] [] th;;
++let proof_TRANS (p, q) th = chk_mk_prf 'T' [] [] [] [p; q] th;;
++let proof_MK_COMB (p, q) th = chk_mk_prf 'C' [] [] [] [p; q] th;;
++let proof_ABS x p th = chk_mk_prf 'L' [] [] [x] [p] th;;
++let proof_BETA t th = chk_mk_prf 'B' [] [] [t] [] th;;
++let proof_ASSUME t th = chk_mk_prf 'H' [] [] [t] [] th;;
++let proof_EQ_MP p q th = chk_mk_prf 'E' [] [] [] [p; q] th;;
++let proof_DEDUCT_ANTISYM_RULE (p1,t1) (p2,t2) th =
++ chk_mk_prf 'D' [] [] [] [p1; p2] th;;
++let rec explode_subst = function
++ [] -> []
++| ((y,x)::rest) -> x::y::(explode_subst rest);;
++let proof_INST_TYPE s p th = chk_mk_prf 'Q' [] (explode_subst s) [] [p] th;;
++let proof_INST s p th = chk_mk_prf 'S' [] [] (explode_subst s) [p] th;;
++
++let global_ax_counter = ref 0;;
++let new_axiom_name n = incr global_ax_counter; ("ax_" ^ n ^ "_" ^ string_of_int(!global_ax_counter));;
++let proof_new_axiom axname t th = chk_mk_prf 'A' [axname] [] [t] [] th;;
++let proof_new_definition cname t th =
++ chk_mk_prf 'F' [cname] [] [t] [] th;;
++let proof_new_basic_type_definition tyname (absname, repname) (pt,tt) p th =
++ chk_mk_prf 'Y' [tyname; absname; repname] [] [pt; tt] [p] th;;
++let proof_CONJUNCT1 p th = chk_mk_prf '1' [] [] [] [p] th;;
++let proof_CONJUNCT2 p th = chk_mk_prf '2' [] [] [] [p] th;;
++
++let clean_ts_at_saved = ((try Sys.getenv "CLEANTMS" with _ -> "") = "YES");;
++
++let save_proof name p th =
++ Hashtbl.replace thms th (name, p);
++ ps := Ps.empty;
++ if clean_ts_at_saved then (
++ tms := Tms.empty; tms_prio := Fm.empty; tms_size := 0;
++ );
++ (try output_string foutc (name ^ " " ^ string_of_int p ^ "\n"); flush foutc with Sys_error _ -> ());;
++(* PROOFRECORDING END *)
+
+ (* ------------------------------------------------------------------------- *)
+ (* List of current type constants with their arities. *)
+@@ -485,43 +655,48 @@
+ (* Basic theorem destructors. *)
+ (* ------------------------------------------------------------------------- *)
+
+- let dest_thm (Sequent(asl,c)) = (asl,c)
++ let dest_thm (Sequent(asl,c,_)) = (asl,c)
+
+- let hyp (Sequent(asl,c)) = asl
++ let hyp (Sequent(asl,c,_)) = asl
+
+- let concl (Sequent(asl,c)) = c
++ let concl (Sequent(asl,c,_)) = c
+
+ (* ------------------------------------------------------------------------- *)
+ (* Basic equality properties; TRANS is derivable but included for efficiency *)
+ (* ------------------------------------------------------------------------- *)
+
+ let REFL tm =
+- Sequent([],safe_mk_eq tm tm)
++ let eq = safe_mk_eq tm tm in
++ Sequent([],eq,proof_REFL tm ([], eq))
+
+- let TRANS (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
++ let TRANS (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
+ match (c1,c2) with
+ Comb((Comb(Const("=",_),_) as eql),m1),Comb(Comb(Const("=",_),m2),r)
+- when alphaorder m1 m2 = 0 -> Sequent(term_union asl1 asl2,Comb(eql,r))
++ when alphaorder m1 m2 = 0 ->
++ let (a, g) = (term_union asl1 asl2,Comb(eql,r)) in
++ Sequent (a, g, proof_TRANS (p1, p2) (a, g))
+ | _ -> failwith "TRANS"
+
+ (* ------------------------------------------------------------------------- *)
+ (* Congruence properties of equality. *)
+ (* ------------------------------------------------------------------------- *)
+
+- let MK_COMB(Sequent(asl1,c1),Sequent(asl2,c2)) =
++ let MK_COMB(Sequent(asl1,c1,p1),Sequent(asl2,c2,p2)) =
+ match (c1,c2) with
+ Comb(Comb(Const("=",_),l1),r1),Comb(Comb(Const("=",_),l2),r2) ->
+ (match type_of r1 with
+ Tyapp("fun",[ty;_]) when compare ty (type_of r2) = 0
+- -> Sequent(term_union asl1 asl2,
+- safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2)))
++ -> let (a, g) = (term_union asl1 asl2,
++ safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2))) in
++ Sequent (a, g, proof_MK_COMB (p1, p2) (a,g))
+ | _ -> failwith "MK_COMB: types do not agree")
+ | _ -> failwith "MK_COMB: not both equations"
+
+- let ABS v (Sequent(asl,c)) =
++ let ABS v (Sequent(asl,c,p)) =
+ match (v,c) with
+ Var(_,_),Comb(Comb(Const("=",_),l),r) when not(exists (vfree_in v) asl)
+- -> Sequent(asl,safe_mk_eq (Abs(v,l)) (Abs(v,r)))
++ -> let eq = safe_mk_eq (Abs(v,l)) (Abs(v,r)) in
++ Sequent (asl,eq,proof_ABS v p (asl,eq))
+ | _ -> failwith "ABS";;
+
+ (* ------------------------------------------------------------------------- *)
+@@ -531,7 +706,8 @@
+ let BETA tm =
+ match tm with
+ Comb(Abs(v,bod),arg) when compare arg v = 0
+- -> Sequent([],safe_mk_eq tm bod)
++ -> let eq = safe_mk_eq tm bod in
++ Sequent([],eq,proof_BETA tm ([], eq))
+ | _ -> failwith "BETA: not a trivial beta-redex"
+
+ (* ------------------------------------------------------------------------- *)
+@@ -539,30 +715,35 @@
+ (* ------------------------------------------------------------------------- *)
+
+ let ASSUME tm =
+- if compare (type_of tm) bool_ty = 0 then Sequent([tm],tm)
++ if compare (type_of tm) bool_ty = 0 then
++ Sequent([tm],tm,proof_ASSUME tm ([tm], tm))
+ else failwith "ASSUME: not a proposition"
+
+- let EQ_MP (Sequent(asl1,eq)) (Sequent(asl2,c)) =
++ let EQ_MP (Sequent(asl1,eq,p1)) (Sequent(asl2,c,p2)) =
+ match eq with
+ Comb(Comb(Const("=",_),l),r) when alphaorder l c = 0
+- -> Sequent(term_union asl1 asl2,r)
++ -> let t = term_union asl1 asl2 in
++ Sequent(t,r,proof_EQ_MP p1 p2 (t,r))
+ | _ -> failwith "EQ_MP"
+
+- let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
++ let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
+ let asl1' = term_remove c2 asl1 and asl2' = term_remove c1 asl2 in
+- Sequent(term_union asl1' asl2',safe_mk_eq c1 c2)
++ let (a,g) = (term_union asl1' asl2',safe_mk_eq c1 c2) in
++ Sequent (a, g, proof_DEDUCT_ANTISYM_RULE (p1,c1) (p2,c2) (a, g))
+
+ (* ------------------------------------------------------------------------- *)
+ (* Type and term instantiation. *)
+ (* ------------------------------------------------------------------------- *)
+
+- let INST_TYPE theta (Sequent(asl,c)) =
++ let INST_TYPE theta (Sequent(asl,c,p)) =
+ let inst_fn = inst theta in
+- Sequent(term_image inst_fn asl,inst_fn c)
++ let (a, g) = (term_image inst_fn asl,inst_fn c) in
++ Sequent(a,g, proof_INST_TYPE theta p (a,g))
+
+- let INST theta (Sequent(asl,c)) =
++ let INST theta (Sequent(asl,c,p)) =
+ let inst_fun = vsubst theta in
+- Sequent(term_image inst_fun asl,inst_fun c)
++ let (a, g) = (term_image inst_fun asl,inst_fun c) in
++ Sequent(a, g, proof_INST theta p (a,g))
+
+ (* ------------------------------------------------------------------------- *)
+ (* Handling of axioms. *)
+@@ -574,8 +755,11 @@
+
+ let new_axiom tm =
+ if compare (type_of tm) bool_ty = 0 then
+- let th = Sequent([],tm) in
+- (the_axioms := th::(!the_axioms); th)
++ let axname = new_axiom_name "" in
++ let p = proof_new_axiom axname tm ([], tm) in
++ let th = Sequent([],tm,p) in
++ (the_axioms := th::(!the_axioms);
++ save_proof axname p ([], tm); th)
+ else failwith "new_axiom: Not a proposition"
+
+ (* ------------------------------------------------------------------------- *)
+@@ -595,7 +779,10 @@
+ else if not (subset (type_vars_in_term r) (tyvars ty))
+ then failwith "new_definition: Type variables not reflected in constant"
+ else let c = new_constant(cname,ty); Const(cname,ty) in
+- let dth = Sequent([],safe_mk_eq c r) in
++ let concl = safe_mk_eq c r in
++ let p = proof_new_definition cname r ([], concl) in
++ let dth = Sequent([],concl, p) in
++ save_proof ("DEF_"^cname) p ([], concl);
+ the_definitions := dth::(!the_definitions); dth
+ | Comb(Comb(Const("=",_),Const(cname,ty)),r) ->
+ failwith ("new_basic_definition: '" ^ cname ^ "' is already defined")
+@@ -614,7 +801,7 @@
+ (* Where "abs" and "rep" are new constants with the nominated names. *)
+ (* ------------------------------------------------------------------------- *)
+
+- let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c)) =
++ let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c,p)) =
+ if exists (can get_const_type) [absname; repname] then
+ failwith "new_basic_type_definition: Constant(s) already in use" else
+ if not (asl = []) then
+@@ -634,9 +821,19 @@
+ let abs = (new_constant(absname,absty); Const(absname,absty))
+ and rep = (new_constant(repname,repty); Const(repname,repty)) in
+ let a = Var("a",aty) and r = Var("r",rty) in
+- Sequent([],safe_mk_eq (Comb(abs,mk_comb(rep,a))) a),
+- Sequent([],safe_mk_eq (Comb(P,r))
+- (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r))
++ let ax1 = safe_mk_eq (Comb(abs,mk_comb(rep,a))) a
++ and ax2 = safe_mk_eq (Comb(P,r)) (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r) in
++ let mk_binary s =
++ let c = mk_const(s,[]) in
++ fun (l,r) -> try mk_comb(mk_comb(c,l),r)
++ with Failure _ -> failwith "tydef_mk_binary"
++ in
++ let axc = mk_binary "/\\" (ax1, ax2) in
++ let tp = proof_new_basic_type_definition tyname (absname, repname) (P,x) p ([], axc) in
++ let p1 = proof_CONJUNCT1 tp ([], ax1) in
++ let p2 = proof_CONJUNCT2 tp ([], ax2) in
++ save_proof ("TYDEF_" ^ tyname) tp ([], axc);
++ (Sequent([],ax1,p1), Sequent([],ax2,p2));;
+
+ end;;
+
--- a/src/HOL/Library/Code_Abstract_Nat.thy Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Fri Jan 24 10:22:17 2025 +0100
@@ -59,8 +59,8 @@
val vname = singleton (Name.variant_list (map fst
(fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
val cv = Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT));
- val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of;
- val rhs_of = snd o Thm.dest_comb o Thm.cprop_of;
+ val lhs_of = Thm.dest_arg1 o Thm.cprop_of;
+ val rhs_of = Thm.dest_arg o Thm.cprop_of;
fun find_vars ct = (case Thm.term_of ct of
(Const (\<^const_name>\<open>Suc\<close>, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
| _ $ _ =>
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Fri Jan 24 10:22:17 2025 +0100
@@ -461,10 +461,10 @@
let
val (th1, cert1) =
overall (Left::cert_choice) dun
- (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.dest_arg1 ct))::oths)
+ (Thm.assume (HOLogic.mk_judgment (Thm.dest_arg1 ct))::oths)
val (th2, cert2) =
overall (Right::cert_choice) dun
- (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.dest_arg ct))::oths)
+ (Thm.assume (HOLogic.mk_judgment (Thm.dest_arg ct))::oths)
in (disj_cases th th1 th2, Branch (cert1, cert2)) end
else overall cert_choice (th::dun) oths
end
@@ -572,7 +572,7 @@
val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
val th3 =
fold simple_choose evs
- (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> bod))) th2)
+ (prove_hyp (Thm.equal_elim th1 (Thm.assume (HOLogic.mk_judgment bod))) th2)
in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume not_A)) th3), certs)
end
in
--- a/src/HOL/Library/cconv.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Library/cconv.ML Fri Jan 24 10:22:17 2025 +0100
@@ -131,7 +131,7 @@
|> Thm.cterm_of ctxt
end
val rule = abstract_rule_thm x
- val inst = Thm.match (hd (Drule.cprems_of rule), mk_concl eq)
+ val inst = Thm.match (hd (Thm.take_cprems_of 1 rule), mk_concl eq)
val gen = (Names.empty, Names.make1_set (#1 (dest_Free v)))
in
(Drule.instantiate_normalize inst rule OF [Drule.generalize gen eq])
--- a/src/HOL/Library/old_recdef.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Library/old_recdef.ML Fri Jan 24 10:22:17 2025 +0100
@@ -896,13 +896,8 @@
* Going into and out of prop
*---------------------------------------------------------------------------*)
-fun is_Trueprop ct =
- (case Thm.term_of ct of
- Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => true
- | _ => false);
-
-fun mk_prop ct = if is_Trueprop ct then ct else Thm.apply \<^cterm>\<open>Trueprop\<close> ct;
-fun drop_prop ct = if is_Trueprop ct then Thm.dest_arg ct else ct;
+fun mk_prop ct = if HOLogic.is_judgment ct then ct else HOLogic.mk_judgment ct;
+fun drop_prop ct = if HOLogic.is_judgment ct then Thm.dest_arg ct else ct;
end;
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Fri Jan 24 10:22:17 2025 +0100
@@ -12,7 +12,7 @@
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st =
let
- val cgoal = nth (cprems_of st) (i - 1);
+ val cgoal = nth (Thm.cprems_of st) (i - 1);
val maxidx = Thm.maxidx_of_cterm cgoal;
val j = maxidx + 1;
val tyinst' = map (apfst (Logic.incr_tvar j)) tyinst;
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Jan 24 10:22:17 2025 +0100
@@ -33,8 +33,8 @@
val perm_bool = mk_meta_eq @{thm perm_bool_def};
val perm_boolI = @{thm perm_boolI};
-val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
- (Drule.strip_imp_concl (Thm.cprop_of perm_boolI))));
+val (_, [perm_boolI_pi, _]) = Drule.strip_comb (Thm.dest_arg
+ (Drule.strip_imp_concl (Thm.cprop_of perm_boolI)));
fun mk_perm_bool ctxt pi th =
th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
@@ -147,7 +147,7 @@
eta_contract_cterm (Conjunction.mk_conjunction_balanced objs));
fun first_order_mrs ths th = ths MRS
- Thm.instantiate (first_order_matchs (cprems_of th) (map Thm.cprop_of ths)) th;
+ Thm.instantiate (first_order_matchs (Thm.cprems_of th) (map Thm.cprop_of ths)) th;
fun prove_strong_ind s avoids lthy =
let
@@ -531,7 +531,7 @@
| NONE => fold_rev (NominalDatatype.mk_perm []) pis x)
| x => x) o HOLogic.dest_Trueprop o Thm.prop_of) case_hyps));
val inst = Thm.first_order_match (Thm.dest_arg
- (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj);
+ (Drule.strip_imp_concl (hd (Thm.cprems_of case_hyp))), obj);
val th = Goal.prove ctxt3 [] [] (Thm.term_of concl)
(fn {context = ctxt4, ...} =>
resolve_tac ctxt4 [Thm.instantiate inst case_hyp] 1 THEN
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Jan 24 10:22:17 2025 +0100
@@ -37,8 +37,8 @@
val perm_bool = mk_meta_eq @{thm perm_bool_def};
val perm_boolI = @{thm perm_boolI};
-val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
- (Drule.strip_imp_concl (Thm.cprop_of perm_boolI))));
+val (_, [perm_boolI_pi, _]) = Drule.strip_comb (Thm.dest_arg
+ (Drule.strip_imp_concl (Thm.cprop_of perm_boolI)));
fun mk_perm_bool ctxt pi th =
th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
--- a/src/HOL/Nominal/nominal_permeq.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Fri Jan 24 10:22:17 2025 +0100
@@ -289,7 +289,7 @@
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
fun finite_guess_tac_i tactical ctxt i st =
- let val goal = nth (cprems_of st) (i - 1)
+ let val goal = nth (Thm.cprems_of st) (i - 1)
in
case Envir.eta_contract (Logic.strip_assums_concl (Thm.term_of goal)) of
_ $ (Const (\<^const_name>\<open>finite\<close>, _) $ (Const (\<^const_name>\<open>Nominal.supp\<close>, T) $ x)) =>
@@ -329,7 +329,7 @@
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
fun fresh_guess_tac_i tactical ctxt i st =
let
- val goal = nth (cprems_of st) (i - 1)
+ val goal = nth (Thm.cprems_of st) (i - 1)
val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm"
val ctxt1 = ctxt addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
--- a/src/HOL/Real_Asymp/exp_log_expression.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML Fri Jan 24 10:22:17 2025 +0100
@@ -192,9 +192,9 @@
fun rewrite ctxt thms ct =
let
val thm1 = Thm.eta_long_conversion ct
- val rhs = thm1 |> Thm.cprop_of |> Thm.dest_comb |> snd
+ val rhs = thm1 |> Thm.cprop_of |> Thm.dest_arg
val (thm2, prems) = rewrite' ctxt [] [] thms rhs
- val rhs = thm2 |> Thm.cprop_of |> Thm.dest_comb |> snd
+ val rhs = thm2 |> Thm.cprop_of |> Thm.dest_arg
val thm3 = Thm.eta_conversion rhs
val thm = Thm.transitive thm1 (Thm.transitive thm2 thm3)
in
--- a/src/HOL/Statespace/state_space.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Statespace/state_space.ML Fri Jan 24 10:22:17 2025 +0100
@@ -239,7 +239,7 @@
fun get_paths dist_thm =
let
- val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
+ val ctree = Thm.cprop_of dist_thm |> Thm.dest_arg |> Thm.dest_arg;
val tree = Thm.term_of ctree;
val x_path = the (DistinctTreeProver.find_tree x tree);
val y_path = the (DistinctTreeProver.find_tree y tree);
@@ -349,7 +349,7 @@
val assume =
((Binding.name dist_thm_name, [attr]),
- [(HOLogic.Trueprop $
+ [(HOLogic.mk_Trueprop
(Const (\<^const_name>\<open>all_distinct\<close>, Type (\<^type_name>\<open>tree\<close>, [nameT]) --> HOLogic.boolT) $
DistinctTreeProver.mk_tree (fn n => Free (n, nameT)) nameT
(sort fast_string_ord all_comps)), [])]);
--- a/src/HOL/Tools/Argo/argo_tactic.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Fri Jan 24 10:22:17 2025 +0100
@@ -286,10 +286,8 @@
SOME t => t
| NONE => raise Fail "bad expression")
-fun as_prop ct = Thm.apply \<^cterm>\<open>Trueprop\<close> ct
-
fun cterm_of ctxt cons e = Thm.cterm_of ctxt (term_of (ctxt, cons) e)
-fun cprop_of ctxt cons e = as_prop (cterm_of ctxt cons e)
+fun cprop_of ctxt cons e = HOLogic.mk_judgment (cterm_of ctxt cons e)
(* generic proof tools *)
@@ -299,7 +297,7 @@
fun discharges thm rules = [thm] RL rules
fun under_assumption f ct =
- let val cprop = as_prop ct
+ let val cprop = HOLogic.mk_judgment ct
in Thm.implies_intr cprop (f (Thm.assume cprop)) end
@@ -537,7 +535,7 @@
fun replay_hyp i ct =
if i < 0 then (Thm.assume ct, [(~i, ct)])
else
- let val cu = as_prop (Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply \<^cterm>\<open>Not\<close> (Thm.dest_arg ct)))
+ let val cu = HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply \<^cterm>\<open>Not\<close> (Thm.dest_arg ct)))
in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Jan 24 10:22:17 2025 +0100
@@ -545,7 +545,7 @@
val assms_tac =
let val assms' = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms in
fold (curry (op ORELSE')) (map (fn thm =>
- funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt)
+ funpow (Thm.nprems_of thm) (fn tac => tac THEN' assume_tac ctxt)
(rtac ctxt thm)) assms')
(etac ctxt FalseE)
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Fri Jan 24 10:22:17 2025 +0100
@@ -176,7 +176,7 @@
Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
inj_map_strongs')
- |> HOLogic.conj_elims ctxt
+ |> HOLogic.conj_elims
|> Proof_Context.export names_ctxt ctxt
|> map (Thm.close_derivation \<^here>)
end;
--- a/src/HOL/Tools/Function/induction_schema.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Fri Jan 24 10:22:17 2025 +0100
@@ -141,7 +141,7 @@
end
fun mk_wf R (IndScheme {T, ...}) =
- HOLogic.Trueprop $ (Const (\<^const_abbrev>\<open>wf\<close>, mk_relT T --> HOLogic.boolT) $ R)
+ HOLogic.mk_Trueprop (Const (\<^const_abbrev>\<open>wf\<close>, mk_relT T --> HOLogic.boolT) $ R)
fun mk_ineqs R thesisn (IndScheme {T, cases, branches}) =
let
--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri Jan 24 10:22:17 2025 +0100
@@ -76,7 +76,7 @@
(case try_proof ctxt (goals \<^const_name>\<open>Orderings.less_eq\<close>) solve_tac of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
- if Thm.prems_of thm2 = [HOLogic.Trueprop $ \<^term>\<open>False\<close>] then False thm2
+ if Thm.prems_of thm2 = [\<^prop>\<open>False\<close>] then False thm2
else None (thm2, thm)
| _ => raise Match) (* FIXME *)
| _ => raise Match)
--- a/src/HOL/Tools/Function/mutual.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Fri Jan 24 10:22:17 2025 +0100
@@ -176,7 +176,7 @@
val psimp = import sum_psimp_eq
val (simp, restore_cond) =
- case cprems_of psimp of
+ case Thm.cprems_of psimp of
[] => (psimp, I)
| [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
| _ => raise General.Fail "Too many conditions"
@@ -184,7 +184,7 @@
val simp_ctxt = fold Thm.declare_hyps (Thm.chyps_of simp) ctxt
in
Goal.prove simp_ctxt [] []
- (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (f, args), rhs)))
(fn _ =>
Local_Defs.unfold0_tac ctxt all_orig_fdefs
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
--- a/src/HOL/Tools/Function/partial_function.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Fri Jan 24 10:22:17 2025 +0100
@@ -129,7 +129,7 @@
end;
fun head_conv cv ct =
- if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct;
+ if can Thm.dest_fun ct then Conv.fun_conv (head_conv cv) ct else cv ct;
(*** currying transformation ***)
--- a/src/HOL/Tools/Function/termination.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Function/termination.ML Fri Jan 24 10:22:17 2025 +0100
@@ -179,7 +179,7 @@
(case try \<^const_name>\<open>Orderings.less_eq\<close> of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
- if Thm.prems_of thm2 = [HOLogic.Trueprop $ \<^term>\<open>False\<close>]
+ if Thm.prems_of thm2 = [\<^prop>\<open>False\<close>]
then False thm2 else None (thm2, thm)
| _ => raise Match) (* FIXME *)
| _ => raise Match)
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Jan 24 10:22:17 2025 +0100
@@ -156,7 +156,7 @@
val concl_pat = Drule.strip_imp_concl (Thm.cprop_of rule)
val insts = Thm.first_order_match (concl_pat, cprop)
val rule = Drule.instantiate_normalize insts rule
- val prop = hd (Thm.prems_of rule)
+ val prop = hd (Thm.take_prems_of 1 rule)
in
case mono_eq_prover ctxt prop of
SOME thm => SOME (thm RS rule)
@@ -222,8 +222,7 @@
val typ = Thm.typ_of_cterm rel
val POS_const = Thm.cterm_of ctxt (mk_POS typ)
val var = Thm.cterm_of ctxt (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
- val goal =
- Thm.apply (Thm.cterm_of ctxt HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
+ val goal = HOLogic.mk_judgment (Thm.apply (Thm.apply POS_const rel) var)
in
[Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
end
@@ -234,7 +233,7 @@
val preprocessed_thm = preprocess ctxt0 thm
val (fixed_thm, ctxt1) = ctxt0
|> yield_singleton (apfst snd oo Variable.import true) preprocessed_thm
- val assms = cprems_of fixed_thm
+ val assms = Thm.cprems_of fixed_thm
val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
val (prems, ctxt2) = ctxt1 |> fold_map Thm.assume_hyps assms
val ctxt3 = ctxt2 |> Context.proof_map (fold add_transfer_rule prems)
@@ -387,7 +386,7 @@
val rel_fun = prove_rel ctxt rsp_thm (rty, qty)
val rep_abs_thm = [quot_thm, rel_fun] MRSL @{thm Quotient_rep_abs_eq}
in
- case mono_eq_prover ctxt (hd (Thm.prems_of rep_abs_thm)) of
+ case mono_eq_prover ctxt (hd (Thm.take_prems_of 1 rep_abs_thm)) of
SOME mono_eq_thm =>
let
val rep_abs_eq = mono_eq_thm RS rep_abs_thm
@@ -418,7 +417,7 @@
val ctm = Thm.dest_equals_lhs (Thm.cprop_of rep_id)
val unfolded_maps_eq = unfold_fun_maps ctm
val t1 = [quot_thm, def_thm, rsp_thm] MRSL @{thm Quotient_rep_abs_fold_unmap}
- val prems_pat = (hd o Drule.cprems_of) t1
+ val prems_pat = Thm.cprem_of t1 1
val insts = Thm.first_order_match (prems_pat, Thm.cprop_of unfolded_maps_eq)
in
unfolded_maps_eq RS (Drule.instantiate_normalize insts t1)
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Jan 24 10:22:17 2025 +0100
@@ -637,7 +637,7 @@
let
fun prove_extra_assms thm =
let
- val assms = cprems_of thm
+ val assms = Thm.cprems_of thm
fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
in
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Jan 24 10:22:17 2025 +0100
@@ -427,7 +427,7 @@
fun reduce_Domainp ctxt rules thm =
let
- val goal = thm |> Thm.prems_of |> hd
+ val goal = hd (Thm.take_prems_of 1 thm)
val var = goal |> HOLogic.dest_Trueprop |> dest_comb |> snd |> dest_Var
val reduced_assm =
reduce_goal [var] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt
@@ -439,7 +439,7 @@
let
fun reduce_first_assm ctxt rules thm =
let
- val goal = thm |> Thm.prems_of |> hd
+ val goal = hd (Thm.take_prems_of 1 thm)
val reduced_assm =
reduce_goal [] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt
in
--- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Fri Jan 24 10:22:17 2025 +0100
@@ -463,7 +463,7 @@
| _ => false
val inst_distr_rule = rewr_imp distr_rule ctm
- val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule)
+ val extra_assms = filter_out is_POS_or_NEG (Thm.cprems_of inst_distr_rule)
val proved_assms = map_interrupt prove_assm extra_assms
in
Option.map (curry op OF inst_distr_rule) proved_assms
@@ -491,7 +491,7 @@
case distr_rule of
NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ())
| SOME distr_rule =>
- map (gen_merge_transfer_relations quotients ctxt0) (cprems_of distr_rule)
+ map (gen_merge_transfer_relations quotients ctxt0) (Thm.cprems_of distr_rule)
MRSL distr_rule
end
else
@@ -504,7 +504,7 @@
val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
val result = (map (gen_merge_transfer_relations quotients ctxt0)
- (cprems_of distr_rule)) MRSL distr_rule
+ (Thm.cprems_of distr_rule)) MRSL distr_rule
val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def)
in
Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv
--- a/src/HOL/Tools/Meson/meson.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Fri Jan 24 10:22:17 2025 +0100
@@ -558,7 +558,7 @@
#> let_simps ? rewrite_rule ctxt @{thms Let_def [abs_def]}
fun make_nnf simp_options ctxt th =
- (case Thm.prems_of th of
+ (case Thm.take_prems_of 1 th of
[] => th |> presimplify simp_options ctxt |> make_nnf1 ctxt
| _ => raise THM ("make_nnf: premises in argument", 0, [th]));
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Jan 24 10:22:17 2025 +0100
@@ -184,9 +184,6 @@
(* A type variable of sort "{}" will make "abstraction" fail. *)
TrueI)
-(*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop;
-
(*Given an abstraction over n variables, replace the bound variables by free
ones. Return the body, along with the list of free variables.*)
fun c_variant_abs_multi (ct0, vars) =
@@ -200,7 +197,7 @@
fun old_skolem_theorem_of_def ctxt rhs0 =
let
val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt
- val rhs' = rhs |> Thm.dest_comb |> snd
+ val rhs' = rhs |> Thm.dest_arg
val (ch, frees) = c_variant_abs_multi (rhs', [])
val (hilbert, cabs) = ch |> Thm.dest_comb |>> Thm.term_of
val T =
@@ -208,10 +205,10 @@
Const (_, Type (\<^type_name>\<open>fun\<close>, [_, T])) => T
| _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
val cex = Thm.cterm_of ctxt (HOLogic.exists_const T)
- val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
+ val ex_tm = HOLogic.mk_judgment (Thm.apply cex cabs)
val conc =
Drule.list_comb (rhs, frees)
- |> Drule.beta_conv cabs |> Thm.apply cTrueprop
+ |> Drule.beta_conv cabs |> HOLogic.mk_judgment
fun tacf [prem] =
rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
THEN resolve_tac ctxt
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Fri Jan 24 10:22:17 2025 +0100
@@ -154,7 +154,7 @@
val params = Logic.strip_params goal;
val tname = dest_Type_name (#2 (hd (rev params)));
val exhaustion = Thm.lift_rule cgoal (exh_thm_of tname);
- val prem' = hd (Thm.prems_of exhaustion);
+ val prem' = hd (Thm.take_prems_of 1 exhaustion);
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
val exhaustion' =
infer_instantiate ctxt
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Jan 24 10:22:17 2025 +0100
@@ -385,7 +385,7 @@
fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
let
- val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion)));
+ val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.take_prems_of 1 exhaustion)));
val ctxt = Proof_Context.init_global thy;
val exhaustion' = exhaustion
|> infer_instantiate ctxt [(#1 (dest_Var lhs), Thm.cterm_of ctxt (Free ("x", T)))];
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Jan 24 10:22:17 2025 +0100
@@ -237,7 +237,7 @@
val prems2 = maps (dest_conjunct_prem o rewrite_rule ctxt2 tuple_rew_rules) prems1
val pats =
map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop)
- (take nargs (Thm.prems_of case_th))
+ (Thm.take_prems_of nargs case_th)
val case_th' =
Thm.instantiate (TVars.empty, Vars.make (inst_of_matches pats)) case_th
OF replicate nargs @{thm refl}
@@ -325,7 +325,7 @@
fun set_elim thm =
let
- val name = dest_Const_name (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))))
+ val name = dest_Const_name (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.take_prems_of 1 thm)))))
in
PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm))))))))
end
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Jan 24 10:22:17 2025 +0100
@@ -376,7 +376,7 @@
let
val th =
Simplifier.rewrite (put_simpset lin_ss ctxt)
- (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close>
+ (HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>Not\<close>
(Thm.apply (Thm.apply \<^cterm>\<open>(=) :: int => _\<close> (Numeral.mk_cnumber \<^ctyp>\<open>int\<close> x))
\<^cterm>\<open>0::int\<close>)))
in Thm.equal_elim (Thm.symmetric th) TrueI end;
@@ -469,7 +469,7 @@
let
val th =
Simplifier.rewrite (put_simpset lin_ss ctxt)
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber \<^ctyp>\<open>int\<close> x)) cd))
in Thm.equal_elim (Thm.symmetric th) TrueI end;
val dvd =
@@ -481,7 +481,7 @@
end
val dp =
let val th = Simplifier.rewrite (put_simpset lin_ss ctxt)
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(Thm.apply (Thm.apply \<^cterm>\<open>(<) :: int => _\<close> \<^cterm>\<open>0::int\<close>) cd))
in Thm.equal_elim (Thm.symmetric th) TrueI end;
(* A and B set *)
@@ -736,7 +736,7 @@
val q = if P c then c else \<^cterm>\<open>False\<close>
val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs
(fold_rev (fn p => fn q => Thm.apply (Thm.apply \<^cterm>\<open>HOL.implies\<close> p) q) qs q)
- val g = Thm.apply (Thm.apply \<^cterm>\<open>(==>)\<close> (Thm.apply \<^cterm>\<open>Trueprop\<close> ng)) p'
+ val g = Thm.apply (Thm.apply \<^cterm>\<open>(==>)\<close> (HOLogic.mk_judgment ng)) p'
val ntac = (case qs of [] => q aconvc \<^cterm>\<open>False\<close>
| _ => false)
in
--- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Jan 24 10:22:17 2025 +0100
@@ -31,7 +31,7 @@
(** instantiate elimination rules **)
local
- val (cpfalse, cfalse) = `SMT_Util.mk_cprop \<^cterm>\<open>False\<close>
+ val (cpfalse, cfalse) = `HOLogic.mk_judgment \<^cterm>\<open>False\<close>
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
--- a/src/HOL/Tools/SMT/smt_replay.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_replay.ML Fri Jan 24 10:22:17 2025 +0100
@@ -80,7 +80,7 @@
(* proof combinators *)
fun under_assumption f ct =
- let val ct' = SMT_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
+ let val ct' = HOLogic.mk_judgment ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
fun discharge p pq = Thm.implies_elim pq p
--- a/src/HOL/Tools/SMT/smt_util.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Fri Jan 24 10:22:17 2025 +0100
@@ -51,8 +51,6 @@
val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context
- val mk_cprop: cterm -> cterm
- val dest_cprop: cterm -> cterm
val mk_cequals: cterm -> cterm -> cterm
val term_of: cterm -> term
val prop_of: thm -> term
@@ -201,13 +199,6 @@
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
-val mk_cprop = Thm.apply \<^cterm>\<open>Trueprop\<close>
-
-fun dest_cprop ct =
- (case Thm.term_of ct of
- \<^Const_>\<open>Trueprop for _\<close> => Thm.dest_arg ct
- | _ => raise CTERM ("not a property", [ct]))
-
val equals = mk_const_pat \<^theory> \<^const_name>\<open>Pure.eq\<close> Thm.dest_ctyp0
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
--- a/src/HOL/Tools/cnf.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/cnf.ML Fri Jan 24 10:22:17 2025 +0100
@@ -104,9 +104,6 @@
(Seq.hd (REPEAT_DETERM (resolve_tac ctxt @{thms cnf.clause2raw_not_disj} i) thm))
(* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
(* becomes "[..., A1, ..., An] |- B" *)
- fun prems_to_hyps thm =
- fold (fn cprem => fn thm' =>
- Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
in
(* [...] |- ~(x1 | ... | xn) ==> False *)
(@{thm cnf.clause2raw_notE} OF [clause])
@@ -115,7 +112,7 @@
(* [...] |- x1' ==> ... ==> xn' ==> False *)
|> Seq.hd o TRYALL (resolve_tac ctxt @{thms cnf.clause2raw_not_not})
(* [..., x1', ..., xn'] |- False *)
- |> prems_to_hyps
+ |> Thm.assume_prems ~1
end;
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/coinduction.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/coinduction.ML Fri Jan 24 10:22:17 2025 +0100
@@ -71,7 +71,7 @@
val (instT, inst) = Thm.match (thm_concl, concl);
val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) (TVars.dest instT);
val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) (Vars.dest inst);
- val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
+ val xs = hd (Thm.take_prems_of 1 raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
|> map (subst_atomic_types rhoTs);
val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
@@ -106,7 +106,7 @@
[] => all_tac
| inv :: case_prems =>
let
- val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
+ val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
val inv_thms = init @ [last];
val eqs = take e inv_thms;
fun is_local_var t =
--- a/src/HOL/Tools/datatype_simprocs.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/datatype_simprocs.ML Fri Jan 24 10:22:17 2025 +0100
@@ -88,7 +88,7 @@
*)
fun no_proper_subterm_proc ctxt ct =
let
- val (clhs, crhs) = ct |> Thm.dest_comb |> apfst (Thm.dest_comb #> snd)
+ val (clhs, crhs) = Thm.dest_binop ct
val (lhs, rhs) = apply2 Thm.term_of (clhs, crhs)
val cT = Thm.ctyp_of_cterm clhs
val T = Thm.typ_of cT
--- a/src/HOL/Tools/groebner.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/groebner.ML Fri Jan 24 10:22:17 2025 +0100
@@ -455,8 +455,8 @@
fun conj_ac_rule eq =
let
val (l,r) = Thm.dest_equals eq
- val ctabl = mk_conj_tab (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> l))
- val ctabr = mk_conj_tab (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> r))
+ val ctabl = mk_conj_tab (Thm.assume (HOLogic.mk_judgment l))
+ val ctabr = mk_conj_tab (Thm.assume (HOLogic.mk_judgment r))
fun tabl c = the (Termtab.lookup ctabl (Thm.term_of c))
fun tabr c = the (Termtab.lookup ctabr (Thm.term_of c))
val thl = prove_conj tabl (conjuncts r) |> implies_intr_hyps
@@ -485,7 +485,7 @@
| _ => error "" (* FIXME ? *)
fun simple_choose ctxt v th =
- choose v (Thm.assume ((Thm.apply \<^cterm>\<open>Trueprop\<close> o mk_ex ctxt v)
+ choose v (Thm.assume ((HOLogic.mk_judgment o mk_ex ctxt v)
(Thm.dest_arg (hd (Thm.chyps_of th))))) th
@@ -502,7 +502,7 @@
val (p0,q0) = Thm.dest_binop t
val (vs',P) = strip_exists p0
val (vs,_) = strip_exists q0
- val th = Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> P)
+ val th = Thm.assume (HOLogic.mk_judgment P)
val th1 = implies_intr_hyps (fold (simple_choose ctxt) vs' (fold mkexi vs th))
val th2 = implies_intr_hyps (fold (simple_choose ctxt) vs (fold mkexi vs' th))
val p = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) th1
@@ -662,23 +662,23 @@
fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1);
fun refute ctxt tm =
- if Thm.term_of tm aconv \<^Const>\<open>False\<close> then Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> tm) else
+ if Thm.term_of tm aconv \<^Const>\<open>False\<close> then Thm.assume (HOLogic.mk_judgment tm) else
((let
val (nths0,eths0) =
List.partition (is_neg o concl)
- (HOLogic.conj_elims ctxt (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> tm)))
+ (HOLogic.conj_elims (Thm.assume (HOLogic.mk_judgment tm)))
val nths = filter (is_eq o Thm.dest_arg o concl) nths0
val eths = filter (is_eq o concl) eths0
in
if null eths then
let
- val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
+ val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
val th2 =
Conv.fconv_rule
((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
val conc = th2 |> concl |> Thm.dest_arg
val (l,_) = conc |> dest_eq
- in Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> tm)
+ in Thm.implies_intr (HOLogic.mk_judgment tm)
(Thm.equal_elim (Drule.arg_cong_rule \<^cterm>\<open>Trueprop\<close> (eqF_intr th2))
(HOLogic.mk_obj_eq (Thm.reflexive l)))
end
@@ -692,13 +692,13 @@
end
else
let
- val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
+ val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
val (vars,pol::pols) =
grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
val (deg,l,cert) = grobner_strong vars pols pol
val th1 =
Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) nth
- val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
+ val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr th1) neq_01
in (vars,l,cert,th2)
end)
val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert
@@ -713,12 +713,12 @@
(nth eths i |> mk_meta_eq)) pols)
val th1 = thm_fn herts_pos
val th2 = thm_fn herts_neg
- val th3 = HOLogic.conj_intr ctxt (HOLogic.mk_obj_eq (mk_add (Thm.symmetric th1) th2)) noteqth
+ val th3 = HOLogic.conj_intr (HOLogic.mk_obj_eq (mk_add (Thm.symmetric th1) th2)) noteqth
val th4 =
Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
(neq_rule l th3)
val (l, _) = dest_eq(Thm.dest_arg(concl th4))
- in Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> tm)
+ in Thm.implies_intr (HOLogic.mk_judgment tm)
(Thm.equal_elim (Drule.arg_cong_rule \<^cterm>\<open>Trueprop\<close> (eqF_intr th4))
(HOLogic.mk_obj_eq (Thm.reflexive l)))
end
--- a/src/HOL/Tools/hologic.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/hologic.ML Fri Jan 24 10:22:17 2025 +0100
@@ -14,7 +14,11 @@
val Trueprop: term
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
+ val is_Trueprop: term -> bool
val Trueprop_conv: conv -> conv
+ val mk_judgment: cterm -> cterm
+ val is_judgment: cterm -> bool
+ val dest_judgment: cterm -> cterm
val mk_induct_forall: typ -> term
val mk_setT: typ -> typ
val dest_setT: typ -> typ
@@ -25,9 +29,9 @@
val mk_set: typ -> term list -> term
val dest_set: term -> term list
val mk_UNIV: typ -> term
- val conj_intr: Proof.context -> thm -> thm -> thm
- val conj_elim: Proof.context -> thm -> thm * thm
- val conj_elims: Proof.context -> thm -> thm list
+ val conj_intr: thm -> thm -> thm
+ val conj_elim: thm -> thm * thm
+ val conj_elims: thm -> thm list
val conj: term
val disj: term
val imp: term
@@ -149,8 +153,8 @@
(* bool and set *)
-val boolN = "HOL.bool";
-val boolT = Type (boolN, []);
+val boolT = \<^Type>\<open>bool\<close>;
+val boolN = dest_Type_name boolT;
fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
@@ -188,29 +192,38 @@
fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq};
-val Trueprop = Const (\<^const_name>\<open>Trueprop\<close>, boolT --> propT);
+val Trueprop = \<^Const>\<open>Trueprop\<close>;
fun mk_Trueprop P = Trueprop $ P;
-fun dest_Trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ P) = P
+fun dest_Trueprop \<^Const_>\<open>Trueprop for P\<close> = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
+fun is_Trueprop \<^Const_>\<open>Trueprop for _\<close> = true
+ | is_Trueprop _ = false;
+
+val is_judgment = is_Trueprop o Thm.term_of;
+
fun Trueprop_conv cv ct =
- (case Thm.term_of ct of
- Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => Conv.arg_conv cv ct
- | _ => raise CTERM ("Trueprop_conv", [ct]))
+ if is_judgment ct then Conv.arg_conv cv ct
+ else raise CTERM ("Trueprop_conv", [ct]);
+
+val mk_judgment = Thm.apply \<^cterm>\<open>Trueprop\<close>;
+fun dest_judgment ct =
+ if is_judgment ct then Thm.dest_arg ct
+ else raise CTERM ("dest_judgment", [ct]);
-fun conj_intr ctxt thP thQ =
+fun conj_intr thP thQ =
let
- val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
+ val (P, Q) = apply2 (dest_judgment o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
val rule = \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q\<close> by (rule conjI)\<close>
in Drule.implies_elim_list rule [thP, thQ] end;
-fun conj_elim ctxt thPQ =
+fun conj_elim thPQ =
let
- val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
+ val (P, Q) = Thm.dest_binop (dest_judgment (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
val thP =
Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> P\<close> by (rule conjunct1)\<close> thPQ;
@@ -218,62 +231,62 @@
Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> Q\<close> by (rule conjunct2)\<close> thPQ;
in (thP, thQ) end;
-fun conj_elims ctxt th =
- let val (th1, th2) = conj_elim ctxt th
- in conj_elims ctxt th1 @ conj_elims ctxt th2 end handle THM _ => [th];
+fun conj_elims th =
+ let val (th1, th2) = conj_elim th
+ in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
-val conj = \<^term>\<open>HOL.conj\<close>
-and disj = \<^term>\<open>HOL.disj\<close>
-and imp = \<^term>\<open>implies\<close>
-and Not = \<^term>\<open>Not\<close>;
+val conj = \<^Const>\<open>conj\<close>;
+val disj = \<^Const>\<open>disj\<close>;
+val imp = \<^Const>\<open>implies\<close>;
+val Not = \<^Const>\<open>Not\<close>;
-fun mk_conj (t1, t2) = conj $ t1 $ t2
-and mk_disj (t1, t2) = disj $ t1 $ t2
-and mk_imp (t1, t2) = imp $ t1 $ t2
-and mk_not t = Not $ t;
+fun mk_conj (t1, t2) = \<^Const>\<open>conj for t1 t2\<close>;
+fun mk_disj (t1, t2) = \<^Const>\<open>disj for t1 t2\<close>;
+fun mk_imp (t1, t2) = \<^Const>\<open>implies for t1 t2\<close>;
+fun mk_not t = \<^Const>\<open>Not for t\<close>;
-fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
+fun dest_conj \<^Const_>\<open>conj for t t'\<close> = t :: dest_conj t'
| dest_conj t = [t];
(*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const ("HOL.conj", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+fun conjuncts_aux \<^Const_>\<open>conj for t t'\<close> conjs = conjuncts_aux t (conjuncts_aux t' conjs)
| conjuncts_aux t conjs = t::conjs;
fun conjuncts t = conjuncts_aux t [];
-fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
+fun dest_disj \<^Const_>\<open>disj for t t'\<close> = t :: dest_disj t'
| dest_disj t = [t];
(*Like dest_disj, but flattens disjunctions however nested*)
-fun disjuncts_aux (Const ("HOL.disj", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
+fun disjuncts_aux \<^Const_>\<open>disj for t t'\<close> disjs = disjuncts_aux t (disjuncts_aux t' disjs)
| disjuncts_aux t disjs = t::disjs;
fun disjuncts t = disjuncts_aux t [];
-fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B)
+fun dest_imp \<^Const_>\<open>implies for A B\<close> = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
-fun dest_not (Const ("HOL.Not", _) $ t) = t
+fun dest_not \<^Const_>\<open>Not for t\<close> = t
| dest_not t = raise TERM ("dest_not", [t]);
fun conj_conv cv1 cv2 ct =
(case Thm.term_of ct of
- Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ =>
+ \<^Const_>\<open>conj for _ _\<close> =>
Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
| _ => raise CTERM ("conj_conv", [ct]));
-fun eq_const T = Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> boolT);
+fun eq_const T = \<^Const>\<open>HOL.eq T\<close>;
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq \<^Const_>\<open>HOL.eq _ for lhs rhs\<close> = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
fun eq_conv cv1 cv2 ct =
(case Thm.term_of ct of
- Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
+ \<^Const_>\<open>HOL.eq _ for _ _\<close> => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
| _ => raise CTERM ("eq_conv", [ct]));
@@ -301,8 +314,8 @@
(*destruct the application of a binary operator. The dummyT case is a crude
way of handling polymorphic operators.*)
-fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
- if c = c' andalso (T=T' orelse T=dummyT) then (t, u)
+fun dest_bin c T (tm as Const (c', \<^Type>\<open>fun T' _\<close>) $ t $ u) =
+ if c = c' andalso (T = T' orelse T = dummyT) then (t, u)
else raise TERM ("dest_bin " ^ c, [tm])
| dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
@@ -352,7 +365,7 @@
fun mk_case_prod t =
(case Term.fastype_of t of
- T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
+ T as \<^Type>\<open>fun A \<^Type>\<open>fun B C\<close>\<close> =>
Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t
| _ => raise TERM ("mk_case_prod: bad body type", [t]));
@@ -549,9 +562,8 @@
fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
| dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
- | dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
- (T, dest_numeral t)
- | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", _)) $ t) =
+ | dest_number (Const ("Num.numeral_class.numeral", \<^Type>\<open>fun _ T\<close>) $ t) = (T, dest_numeral t)
+ | dest_number (Const ("Groups.uminus_class.uminus", \<^Type>\<open>fun _ _\<close>) $ t) =
apsnd (op ~) (dest_number t)
| dest_number t = raise TERM ("dest_number", [t]);
@@ -592,14 +604,15 @@
(* booleans as bits *)
-fun mk_bit b = if b = 0 then \<^term>\<open>False\<close>
- else if b = 1 then \<^term>\<open>True\<close>
+fun mk_bit b =
+ if b = 0 then \<^Const>\<open>False\<close>
+ else if b = 1 then \<^Const>\<open>True\<close>
else raise TERM ("mk_bit", []);
fun mk_bits len = map mk_bit o Integer.radicify 2 len;
-fun dest_bit \<^term>\<open>False\<close> = 0
- | dest_bit \<^term>\<open>True\<close> = 1
+fun dest_bit \<^Const>\<open>False\<close> = 0
+ | dest_bit \<^Const>\<open>True\<close> = 1
| dest_bit _ = raise TERM ("dest_bit", []);
val dest_bits = Integer.eval_radix 2 o map dest_bit;
--- a/src/HOL/Tools/inductive_realizer.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Jan 24 10:22:17 2025 +0100
@@ -372,7 +372,7 @@
let
val vs' = rename (map (apply2 (fst o fst o dest_Var))
(params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
- (hd (Thm.prems_of (hd inducts))))), nparms))) vs;
+ (hd (Thm.take_prems_of 1 (hd inducts))))), nparms))) vs;
val rs = indrule_realizer thy induct raw_induct rsets params'
(vs' @ Ps) rec_names rss' intrs dummies;
val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
@@ -505,7 +505,7 @@
fun err () = error "ind_realizer: bad rule";
val sets =
(case HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of thm)) of
- [_] => [pred_of (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))]
+ [_] => [pred_of (HOLogic.dest_Trueprop (hd (Thm.take_prems_of 1 thm)))]
| xs => map (pred_of o fst o HOLogic.dest_imp) xs)
handle TERM _ => err () | List.Empty => err ();
in
--- a/src/HOL/Tools/numeral_simprocs.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Fri Jan 24 10:22:17 2025 +0100
@@ -471,7 +471,7 @@
simplify_one ctxt (([th, cancel_th]) MRS trans);
local
- val Tp_Eq = Thm.reflexive (Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop)
+ val Tp_Eq = Thm.reflexive \<^cterm>\<open>Trueprop\<close>
fun Eq_True_elim Eq =
Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
in
@@ -593,7 +593,7 @@
val eq = Thm.instantiate_cterm (TVars.make1 (type_tvar, T), Vars.empty) geq
val th =
Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
- (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close>
+ (HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>Not\<close>
(Thm.apply (Thm.apply eq t) z)))
in Thm.equal_elim (Thm.symmetric th) TrueI end
--- a/src/HOL/Tools/record.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/record.ML Fri Jan 24 10:22:17 2025 +0100
@@ -1504,7 +1504,7 @@
val (x, ca) =
(case rev (drop (length params) ys) of
[] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
- (hd (rev (Logic.strip_assums_hyp (hd (Thm.prems_of rule')))))))), true)
+ (hd (rev (Logic.strip_assums_hyp (hd (Thm.take_prems_of 1 rule')))))))), true)
| [x] => (head_of x, false));
val rule'' =
infer_instantiate ctxt
--- a/src/HOL/Tools/sat.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/sat.ML Fri Jan 24 10:22:17 2025 +0100
@@ -165,8 +165,7 @@
val res_thm =
let
- val P =
- snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *)
+ val P = HOLogic.dest_judgment (if hyp1_is_neg then hyp2 else hyp1)
in
\<^instantiate>\<open>P in
lemma \<open>(P \<Longrightarrow> False) \<Longrightarrow> (\<not> P \<Longrightarrow> False) \<Longrightarrow> False\<close> by (rule case_split)\<close>
--- a/src/HOL/Tools/typedef.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/HOL/Tools/typedef.ML Fri Jan 24 10:22:17 2025 +0100
@@ -302,7 +302,7 @@
fun add_typedef_global overloaded typ set opt_bindings tac =
Named_Target.theory_map_result (apsnd o transform_info)
- (add_typedef overloaded typ set opt_bindings tac)
+ (add_typedef overloaded typ set opt_bindings tac);
(* typedef: proof interface *)
--- a/src/Provers/hypsubst.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Provers/hypsubst.ML Fri Jan 24 10:22:17 2025 +0100
@@ -169,7 +169,7 @@
val (ixn, T) = dest_Var (Term.head_of (Data.dest_Trueprop
(Logic.strip_assums_concl (Thm.prop_of rl'))));
val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
- (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
+ (Logic.strip_assums_concl (hd (Thm.take_prems_of 1 rl'))));
val (Ts, V) = split_last (Term.binder_types T);
val u =
fold_rev Term.abs (ps @ [("x", U)])
--- a/src/Pure/Admin/component_hol_light.scala Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala Fri Jan 24 10:22:17 2025 +0100
@@ -11,57 +11,40 @@
object Component_HOL_Light {
/* resources */
+ val hol_import_dir: Path = Path.explode("~~/src/HOL/Import")
+ def default_maps: Path = hol_import_dir + Path.explode("offline/maps.lst")
+
+ def bundle_contents(preserve_raw: Boolean = false): List[String] =
+ List("facts.lstN", "maps.lst", "proofsN.zst") :::
+ (if (preserve_raw) List("facts.lst", "proofs") else Nil)
+
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,
+ load_more: List[Path] = Nil,
+ maps: Option[Path] = Some(default_maps),
+ preserve_raw: Boolean = false,
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
+ hol_light_rev: String = default_hol_light_rev
): Unit = {
/* system */
if (!only_offline) {
Linux.check_system()
- Isabelle_System.require_command("buffer", test = "-i /dev/null")
Isabelle_System.require_command("patch")
+ Isabelle_System.require_command("zstd")
}
/* 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 component_dir =
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
val platform = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform))
@@ -71,7 +54,7 @@
component_dir.write_settings("""
HOL_LIGHT_IMPORT="$COMPONENT"
-HOL_LIGTH_BUNDLE="$HOL_LIGHT_IMPORT/bundle/proofs"
+HOL_LIGHT_BUNDLE="$HOL_LIGHT_IMPORT/bundle/proofsN.zst"
HOL_LIGHT_OFFLINE="$HOL_LIGHT_IMPORT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}/offline"
""")
@@ -83,6 +66,7 @@
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
@@ -90,20 +74,24 @@
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:
+has been patched in 2 phases. The overall export process works like this:
+ isabelle ocaml_setup
+ isabelle ocaml_opam install -y camlp5
+ eval $(isabelle ocaml_opam env)
+
+ cd hol-light
make
- patch -p1 < patches/stage1.patch
+ patch -p1 < "$HOL_LIGHT_IMPORT/patches/patch1"
./ocaml-hol -I +compiler-libs stage1.ml
- patch -p1 < patches/stage2.patch
+ patch -p1 < "$HOL_LIGHT_IMPORT/patches/patch2"
export MAXTMS=10000
./ocaml-hol -I +compiler-libs stage2.ml
- gzip -d proofs.gz
- > maps.lst
- x86_64-linux/offline
+ cp "$HOL_LIGHT_IMPORT/bundle/maps.lst" .
+ "$HOL_LIGHT_IMPORT/x86_64-linux/offline"
Makarius
@@ -115,7 +103,6 @@
/* 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",
@@ -124,80 +111,86 @@
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
+ val offline_dir = Isabelle_System.make_directory(tmp_dir + offline_path)
+
+ Isabelle_System.copy_dir(hol_import_dir + offline_path, offline_dir, direct = true)
- 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)
+ progress.bash("ocamlopt offline.ml -o offline",
+ cwd = offline_dir, echo = progress.verbose).check
+ Isabelle_System.copy_file(offline_dir + offline_exe, platform_dir + offline_exe)
File.set_executable(platform_dir + offline_exe)
if (!only_offline) {
+ /* clone repository */
+
+ val hol_light_dir = tmp_dir + Path.basic("hol-light")
+
+ Isabelle_System.git_clone(hol_light_url, hol_light_dir, checkout = hol_light_rev,
+ progress = progress)
+
/* patches */
- progress.echo("Preparing patches ...")
+ Isabelle_System.make_directory(component_dir.path + Path.basic("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")
+ def patch(n: Int, source: Boolean = false): Path =
+ (if (source) hol_import_dir else component_dir.path) + Path.explode("patches/patch" + n)
- Isabelle_System.bash("git reset --hard origin/stdlib/isabelle-export-base",
- cwd = hol_light_patched_dir).check
+ for (n <- List(1, 2)) Isabelle_System.copy_file(patch(n, source = true), patch(n))
- File.write(patch1, make_patch(tmp_dir))
-
- Isabelle_System.bash("patch -p1 < " + File.bash_path(patch1), cwd = hol_light_dir).check
+ if (load_more.nonEmpty) {
+ val bad = load_more.filter(path => !(hol_light_dir + path).is_file)
+ if (bad.nonEmpty) error("Bad HOL Light files: " + bad.mkString(", "))
- Isabelle_System.bash("git reset --hard origin/stdlib/isabelle-export",
- cwd = hol_light_patched_dir).check
-
- File.write(patch2, make_patch(tmp_dir))
+ val more = load_more.map(path => "needs " + path + ";; ").mkString("+", "", "")
+ File.change_lines(patch(1), strict = true)(_.map(line =>
+ if (line == "+(*LOAD MORE*)") more else line))
+ }
- /* export */
+ /* export stages */
+
+ def run(n: Int, lines: String*): Unit = {
+ val title = "stage " + n
+ if (n > 0) progress.echo("Running " + title + " ...")
+
+ val start = Time.now()
+ progress.bash(cat_lines("set -e" :: opam_env :: lines.toList),
+ cwd = hol_light_dir, echo = progress.verbose).check.timing
+ val elapsed = Time.now() - start
+
+ if (n > 0) {
+ progress.echo("Finished " + title + " (" + elapsed.message_hms + " elapsed time)")
+ }
+ }
- 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
+ run(0, "make")
+ run(1,
+ "patch -p1 < " + File.bash_path(patch(1)),
+ "./ocaml-hol -I +compiler-libs stage1.ml")
+ run(2,
+ "patch -p1 < " + File.bash_path(patch(2)),
+ "export MAXTMS=10000",
+ "./ocaml-hol -I +compiler-libs stage2.ml")
+
+ Bytes.write(hol_light_dir + Path.explode("maps.lst"),
+ if (maps.isEmpty) Bytes.empty else Bytes.read(maps.get))
+
+ run(3,
+ File.bash_path(platform_dir + offline_exe),
+ "zstd -8 proofsN")
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)
+ for (name <- bundle_contents(preserve_raw = preserve_raw)) {
+ Isabelle_System.copy_file(hol_light_dir + Path.explode(name), bundle_dir)
+ }
}
}
}
@@ -210,13 +203,12 @@
Scala_Project.here,
{ args =>
var target_dir = Path.current
+ var load_more = List.empty[Path]
+ var maps: Option[Path] = Some(default_maps)
var only_offline = false
+ var preserve_raw = 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("""
@@ -224,31 +216,29 @@
Options are:
-D DIR target directory (default ".")
+ -L PATH load additional HOL Light files, after "hol.ml"
+ -M PATH alternative maps.lst for offline alignment of facts
+ ("." means empty, default: """ + default_maps + """)
-O only build the "offline" tool
+ -P preserve raw proofs, before offline alignment of facts
-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.
+ Build Isabelle component for HOL Light import. For example:
+
+ isabelle component_hol_light_import -L Logic/make.ml
+ isabelle component_hol_light_import -L 100/thales.ml -L 100/ceva.ml
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
+ "L:" -> (arg => load_more = load_more ::: List(Path.explode(arg))),
+ "M:" -> (arg => maps = if (arg == ".") None else Some(Path.explode(arg))),
"O" -> (_ => only_offline = true),
+ "P" -> (_ => preserve_raw = 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)
@@ -258,11 +248,7 @@
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)
+ load_more = load_more, maps = maps, preserve_raw = preserve_raw,
+ hol_light_url = hol_light_url, hol_light_rev = hol_light_rev)
})
}
--- a/src/Pure/Admin/component_polyml.scala Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/Admin/component_polyml.scala Fri Jan 24 10:22:17 2025 +0100
@@ -195,8 +195,8 @@
/* component */
val component_name1 = if (component_name.isEmpty) "polyml-" + polyml_version else component_name
- val component_dir = Components.Directory(target_dir + Path.basic(component_name1)).create()
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory(target_dir + Path.basic(component_name1)).create(progress = progress)
/* download and build */
--- a/src/Pure/Isar/rule_cases.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/Isar/rule_cases.ML Fri Jan 24 10:22:17 2025 +0100
@@ -423,7 +423,7 @@
fun prep_rule n th =
let
val th' = Thm.permute_prems 0 n th;
- val prems = take (Thm.nprems_of th' - n) (Drule.cprems_of th');
+ val prems = Thm.take_cprems_of (Thm.nprems_of th' - n) th';
val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
in (prems, (n, th'')) end;
--- a/src/Pure/Isar/runtime.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/Isar/runtime.ML Fri Jan 24 10:22:17 2025 +0100
@@ -106,6 +106,9 @@
EXCURSION_FAIL (exn, loc) =>
map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
(sorted_msgs context exn)
+ | Morphism.MORPHISM (name, exn) =>
+ map (fn ((i, msg), id) => ((i, "MORPHISM " ^ quote name ^ "\n" ^ msg), id))
+ (sorted_msgs context exn)
| _ =>
let
val msg =
--- a/src/Pure/ML/ml_instantiate.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/ML/ml_instantiate.ML Fri Jan 24 10:22:17 2025 +0100
@@ -12,10 +12,10 @@
type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
val instantiate_typ: insts -> typ -> typ
val instantiate_ctyp: Position.T -> cinsts -> ctyp -> ctyp
- val instantiate_term: insts -> term -> term
- val instantiate_cterm: Position.T -> cinsts -> cterm -> cterm
- val instantiate_thm: Position.T -> cinsts -> thm -> thm
- val instantiate_thms: Position.T -> cinsts -> thm list -> thm list
+ val instantiate_term: bool -> insts -> term -> term
+ val instantiate_cterm: Position.T -> bool -> cinsts -> cterm -> cterm
+ val instantiate_thm: Position.T -> bool -> cinsts -> thm -> thm
+ val instantiate_thms: Position.T -> bool -> cinsts -> thm list -> thm list
val get_thms: Proof.context -> int -> thm list
val get_thm: Proof.context -> int -> thm
end;
@@ -38,12 +38,12 @@
Thm.instantiate_ctyp (TVars.make (#1 cinsts)) cT
handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args));
-fun instantiate_term (insts: insts) =
+fun instantiate_term beta (insts: insts) =
let
val instT = TVars.make (#1 insts);
val instantiateT = Term_Subst.instantiateT instT;
val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts));
- in Term_Subst.instantiate_beta (instT, inst) end;
+ in (if beta then Term_Subst.instantiate_beta else Term_Subst.instantiate) (instT, inst) end;
fun make_cinsts (cinsts: cinsts) =
let
@@ -52,15 +52,15 @@
val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts));
in (cinstT, cinst) end;
-fun instantiate_cterm pos cinsts ct =
- Thm.instantiate_beta_cterm (make_cinsts cinsts) ct
+fun instantiate_cterm pos beta cinsts ct =
+ (if beta then Thm.instantiate_beta_cterm else Thm.instantiate_cterm) (make_cinsts cinsts) ct
handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args));
-fun instantiate_thm pos cinsts th =
- Thm.instantiate_beta (make_cinsts cinsts) th
+fun instantiate_thm pos beta cinsts th =
+ (if beta then Thm.instantiate_beta else Thm.instantiate) (make_cinsts cinsts) th
handle THM (msg, i, args) => Exn.reraise (THM (msg ^ Position.here pos, i, args));
-fun instantiate_thms pos cinsts = map (instantiate_thm pos cinsts);
+fun instantiate_thms pos beta cinsts = map (instantiate_thm pos beta cinsts);
(* context data *)
@@ -180,6 +180,8 @@
ml_range range (ML_Context.struct_name ctxt ^ "." ^ ml_name));
in ((ml_env, ml_body), ctxt') end;
+fun prepare_beta {beta} = " " ^ Value.print_bool beta;
+
fun prepare_type range ((((kind, pos), ml1, ml2), schematic), s) insts ctxt =
let
val T = Syntax.read_typ ctxt s;
@@ -189,23 +191,24 @@
prepare_insts pos schematic ctxt1 ctxt insts [t] ||> (the_single #> Logic.dest_type);
in prepare_ml range kind ml1 ml2 (ML_Syntax.print_typ T') ml_insts ctxt end;
-fun prepare_term read range ((((kind, pos), ml1, ml2), schematic), (s, fixes)) insts ctxt =
+fun prepare_term read range ((((kind, pos), ml1, ml2), schematic), (s, fixes)) beta insts ctxt =
let
val ctxt' = #2 (Proof_Context.add_fixes_cmd fixes ctxt);
val t = read ctxt' s;
val ctxt1 = Proof_Context.augment t ctxt';
val (ml_insts, t') = prepare_insts pos schematic ctxt1 ctxt insts [t] ||> the_single;
- in prepare_ml range kind ml1 ml2 (ML_Syntax.print_term t') ml_insts ctxt end;
+ in prepare_ml range kind ml1 (ml2 ^ prepare_beta beta) (ML_Syntax.print_term t') ml_insts ctxt end;
-fun prepare_lemma range ((pos, schematic), make_lemma) insts ctxt =
+fun prepare_lemma range ((pos, schematic), make_lemma) beta insts ctxt =
let
val (ths, (props, ctxt1)) = make_lemma ctxt
val (i, thms_ctxt) = put_thms ths ctxt;
val ml_insts = #1 (prepare_insts pos schematic ctxt1 ctxt insts props);
+ val args = ml_here pos ^ prepare_beta beta;
val (ml1, ml2) =
if length ths = 1
- then ("ML_Instantiate.get_thm ML_context", "ML_Instantiate.instantiate_thm " ^ ml_here pos)
- else ("ML_Instantiate.get_thms ML_context", "ML_Instantiate.instantiate_thms " ^ ml_here pos);
+ then ("ML_Instantiate.get_thm ML_context", "ML_Instantiate.instantiate_thm " ^ args)
+ else ("ML_Instantiate.get_thms ML_context", "ML_Instantiate.instantiate_thms " ^ args);
in prepare_ml range "lemma" ml1 ml2 (ML_Syntax.print_int i) ml_insts thms_ctxt end;
fun typ_ml (kind, pos: Position.T) = ((kind, pos), "", "ML_Instantiate.instantiate_typ ");
@@ -219,11 +222,12 @@
val command_name = Parse.position o Parse.command_name;
+val parse_beta = Args.mode "no_beta" >> (fn b => {beta = not b});
val parse_schematic = Args.mode "schematic" >> (fn b => {schematic = b});
fun parse_body range =
(command_name "typ" >> typ_ml || command_name "ctyp" >> ctyp_ml) -- parse_schematic --
- Parse.!!! Parse.typ >> prepare_type range ||
+ Parse.!!! Parse.typ >> (K o prepare_type range) ||
(command_name "term" >> term_ml || command_name "cterm" >> cterm_ml) -- parse_schematic --
Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range ||
(command_name "prop" >> term_ml || command_name "cprop" >> cterm_ml) -- parse_schematic --
@@ -234,12 +238,12 @@
(ML_Context.add_antiquotation_embedded \<^binding>\<open>instantiate\<close>
(fn range => fn input => fn ctxt =>
let
- val (insts, prepare_val) = input
+ val ((beta, insts), prepare_val) = input
|> Parse.read_embedded ctxt (make_keywords ctxt)
- ((parse_insts --| Parse.$$$ "in") -- parse_body range);
+ (parse_beta -- (parse_insts --| Parse.$$$ "in") -- parse_body range);
val (((ml_env, ml_body), decls), ctxt1) = ctxt
- |> prepare_val (apply2 (map #1) insts)
+ |> prepare_val beta (apply2 (map #1) insts)
||>> ML_Context.expand_antiquotes_list (op @ (apply2 (map #2) insts));
fun decl' ctxt' =
--- a/src/Pure/cterm_items.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/cterm_items.ML Fri Jan 24 10:22:17 2025 +0100
@@ -37,8 +37,8 @@
);
open Term_Items;
-val add_vars = Thm.fold_atomic_cterms {hyps = false} Term.is_Var add_set;
-val add_frees = Thm.fold_atomic_cterms {hyps = true} Term.is_Free add_set;
+val add_vars = Thm.fold_atomic_cterms {hyps = false} (K Term.is_Var) add_set;
+val add_frees = Thm.fold_atomic_cterms {hyps = true} (K Term.is_Free) add_set;
end;
--- a/src/Pure/drule.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/drule.ML Fri Jan 24 10:22:17 2025 +0100
@@ -12,7 +12,6 @@
val list_implies: cterm list * cterm -> cterm
val strip_imp_prems: cterm -> cterm list
val strip_imp_concl: cterm -> cterm
- val cprems_of: thm -> cterm list
val forall_intr_list: cterm list -> thm -> thm
val forall_elim_list: cterm list -> thm -> thm
val lift_all: Proof.context -> cterm -> thm -> thm
@@ -127,9 +126,6 @@
Const ("Pure.imp", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
| _ => ct);
-(*The premises of a theorem, as a cterm list*)
-val cprems_of = strip_imp_prems o Thm.cprop_of;
-
fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
val implies = certify Logic.implies;
--- a/src/Pure/logic.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/logic.ML Fri Jan 24 10:22:17 2025 +0100
@@ -23,6 +23,7 @@
val list_implies: term list * term -> term
val strip_imp_prems: term -> term list
val strip_imp_concl: term -> term
+ val take_imp_prems: int -> term -> term list
val strip_prems: int * term list * term -> term list * term
val count_prems: term -> int
val no_prems: term -> bool
@@ -200,6 +201,11 @@
fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B
| strip_imp_concl A = A : term;
+(* take at most n prems, where n < 0 means infinity *)
+fun take_imp_prems 0 _ = []
+ | take_imp_prems n (Const ("Pure.imp", _) $ A $ B) = A :: take_imp_prems (n - 1) B
+ | take_imp_prems _ _ = [];
+
(*Strip and return premises: (i, [], A1\<Longrightarrow>...Ai\<Longrightarrow>B)
goes to ([Ai, A(i-1),...,A1] , B) (REVERSED)
if i<0 or else i too big then raises TERM*)
--- a/src/Pure/more_thm.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/more_thm.ML Fri Jan 24 10:22:17 2025 +0100
@@ -63,6 +63,7 @@
val check_shyps: Proof.context -> thm -> thm
val weaken_sorts': Proof.context -> cterm -> cterm
val elim_implies: thm -> thm -> thm
+ val assume_prems: int -> thm -> thm
val forall_intr_name: string * cterm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
@@ -133,14 +134,14 @@
val op aconvc = op aconv o apply2 Thm.term_of;
val add_tvars =
- Thm.fold_atomic_ctyps {hyps = false} Term.is_TVar (fn cT => fn tab =>
- let val v = Term.dest_TVar (Thm.typ_of cT)
- in tab |> not (TVars.defined tab v) ? TVars.add (v, cT) end);
+ Thm.fold_atomic_ctyps {hyps = false}
+ (fn tab => fn T => Term.is_TVar T andalso not (TVars.defined tab (Term.dest_TVar T)))
+ (fn cT => TVars.add (Term.dest_TVar (Thm.typ_of cT), cT));
val add_vars =
- Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab =>
- let val v = Term.dest_Var (Thm.term_of ct)
- in tab |> not (Vars.defined tab v) ? Vars.add (v, ct) end);
+ Thm.fold_atomic_cterms {hyps = false}
+ (fn tab => fn t => Term.is_Var t andalso not (Vars.defined tab (Term.dest_Var t)))
+ (fn ct => Vars.add (Term.dest_Var (Thm.term_of ct), ct));
(* ctyp operations *)
@@ -334,6 +335,12 @@
fun elim_implies thA thAB = Thm.implies_elim thAB thA;
+(* assume_prems: shift at most n premises into hyps, where n < 0 means infinity *)
+
+fun assume_prems n th =
+ fold (elim_implies o Thm.assume) (Thm.take_cprems_of n th) th;
+
+
(* forall_intr_name *)
fun forall_intr_name (a, x) th =
@@ -401,24 +408,53 @@
if TFrees.is_empty instT andalso Frees.is_empty inst then th
else
let
- val idx = Thm.maxidx_of th + 1;
+ val namesT = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT);
+ val names = Names.build (Frees.fold (Names.add_set o #1 o #1) inst);
+
+ val idx =
+ (Thm.maxidx_of th
+ |> TFrees.fold (Integer.max o Thm.maxidx_of_ctyp o #2) instT
+ |> Frees.fold (Integer.max o Thm.maxidx_of_cterm o #2) inst) + 1;
fun index ((a, A), b) = (((a, idx), A), b);
- val insts =
- (TVars.build (TFrees.fold (TVars.add o index) instT),
- Vars.build (Frees.fold (Vars.add o index) inst));
- val tfrees = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT);
- val frees = Names.build (Frees.fold (Names.add_set o #1 o #1) inst);
+
+ val instT' =
+ TVars.build (TFrees.fold (TVars.add o index) instT)
+ |> not (Names.is_empty namesT) ? Thm.fold_atomic_ctyps {hyps = true}
+ (fn tab => fn T => Term.is_TFree T andalso
+ let val (a, S) = Term.dest_TFree T in
+ Names.defined namesT a andalso
+ not (TFrees.defined instT (a, S)) andalso
+ not (TVars.defined tab ((a, idx), S))
+ end)
+ (fn cT =>
+ let val (a, S) = Term.dest_TFree (Thm.typ_of cT)
+ in TVars.add (((a, idx), S), cT) end) th;
+
+ val inst_typ = Term_Subst.instantiateT_frees (TFrees.map (K Thm.typ_of) instT);
+ val inst_ctyp =
+ Thm.generalize_cterm (namesT, Names.empty) idx #>
+ Thm.instantiate_cterm (instT', Vars.empty);
+
+ val inst' =
+ Vars.build (Frees.fold (Vars.add o index) inst)
+ |> not (Names.is_empty names) ? Thm.fold_atomic_cterms {hyps = true}
+ (fn tab => fn t => Term.is_Free t andalso
+ let val (x, T) = Term.dest_Free t in
+ Names.defined names x andalso
+ let val U = inst_typ T
+ in not (Frees.defined inst (x, U)) andalso not (Vars.defined tab ((x, idx), U)) end
+ end)
+ (fn ct =>
+ let val (x, T) = Term.dest_Free (Thm.term_of ct)
+ in Vars.add (((x, idx), inst_typ T), inst_ctyp ct) end) th;
val hyps = Thm.chyps_of th;
- val inst_cterm =
- Thm.generalize_cterm (tfrees, frees) idx #>
- Thm.instantiate_cterm insts;
in
th
|> fold_rev Thm.implies_intr hyps
- |> Thm.generalize (tfrees, frees) idx
- |> Thm.instantiate insts
- |> fold (elim_implies o Thm.assume o inst_cterm) hyps
+ |> Thm.generalize (namesT, names) idx
+ |> Thm.instantiate (instT', inst')
+ |> assume_prems (length hyps)
end;
@@ -453,10 +489,8 @@
Frees.build
(fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
fold Frees.add_frees (Thm.hyps_of th));
- val is_fixed = Frees.defined fixed o Term.dest_Free o Thm.term_of;
- val frees =
- Cterms.build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
- (fn ct => not (is_fixed ct) ? Cterms.add_set ct));
+ fun guard t = Term.is_Free t andalso not (Frees.defined fixed (Term.dest_Free t));
+ val frees = Cterms.build (th |> Thm.fold_atomic_cterms {hyps = false} (K guard) Cterms.add_set);
in fold_rev Thm.forall_intr (Cterms.list_set frees) th end;
--- a/src/Pure/search.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/search.ML Fri Jan 24 10:22:17 2025 +0100
@@ -129,7 +129,7 @@
let
val np' = Thm.nprems_of st;
(*rgd' calculation assumes tactic operates on subgoal 1*)
- val rgd' = not (has_vars (hd (Thm.prems_of st)));
+ val rgd' = not (has_vars (hd (Thm.take_prems_of 1 st)));
val k' = k + np' - np + 1; (*difference in # of subgoals, +1*)
in
if k' + np' >= bnd then depth (bnd, Int.min (inc, k' + np' + 1 - bnd)) qs
--- a/src/Pure/thm.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Pure/thm.ML Fri Jan 24 10:22:17 2025 +0100
@@ -31,6 +31,7 @@
val dest_ctyp: ctyp -> ctyp list
val dest_ctypN: int -> ctyp -> ctyp
val make_ctyp: ctyp -> ctyp list -> ctyp
+ val maxidx_of_ctyp: ctyp -> int
(*certified terms*)
val term_of: cterm -> term
val typ_of_cterm: cterm -> typ
@@ -60,8 +61,10 @@
val first_order_match: cterm * cterm -> ctyp TVars.table * cterm Vars.table
(*theorems*)
val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a
- val fold_atomic_ctyps: {hyps: bool} -> (typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
- val fold_atomic_cterms: {hyps: bool} -> (term -> bool) -> (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
+ val fold_atomic_ctyps: {hyps: bool} ->
+ ('a -> typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
+ val fold_atomic_cterms: {hyps: bool} ->
+ ('a -> term -> bool) -> (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
val terms_of_tpairs: (term * term) list -> term list
val full_prop_of: thm -> term
val theory_id: thm -> Context.theory_id
@@ -76,13 +79,16 @@
val tpairs_of: thm -> (term * term) list
val concl_of: thm -> term
val prems_of: thm -> term list
+ val take_prems_of: int -> thm -> term list
val nprems_of: thm -> int
val no_prems: thm -> bool
+ val prem_of: thm -> int -> term
val major_prem_of: thm -> term
val cprop_of: thm -> cterm
val cprem_of: thm -> int -> cterm
val cconcl_of: thm -> cterm
val cprems_of: thm -> cterm list
+ val take_cprems_of: int -> thm -> cterm list
val chyps_of: thm -> cterm list
val thm_ord: thm ord
exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
@@ -142,7 +148,8 @@
val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list
val check_oracle: Proof.context -> xstring * Position.T -> string
(*inference rules*)
- val assume: cterm -> thm
+ val assume: cterm -> thm (*exception THM*)
+ val assume_cterm: cterm -> thm (*exception CTERM*)
val implies_intr: cterm -> thm -> thm
val implies_elim: thm -> thm -> thm
val forall_intr: cterm -> thm -> thm
@@ -203,6 +210,8 @@
fun typ_of (Ctyp {T, ...}) = T;
+fun maxidx_of_ctyp (Ctyp {maxidx, ...}) = maxidx;
+
fun global_ctyp_of thy raw_T =
let
val T = Sign.certify_typ thy raw_T;
@@ -461,13 +470,15 @@
fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps;
fun fold_atomic_ctyps h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
- let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps}
- in (fold_terms h o fold_types o fold_atyps) (fn T => if g T then f (ctyp T) else I) th end;
+ let
+ fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps};
+ fun apply T a = if g a T then f (ctyp T) a else a;
+ in (fold_terms h o fold_types o fold_atyps) apply th end;
fun fold_atomic_cterms h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
let
fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps};
- fun apply t T = if g t then f (cterm t T) else I;
+ fun apply t T a = if g a t then f (cterm t T) a else a;
in
(fold_terms h o fold_aterms)
(fn t as Const (_, T) => apply t T
@@ -518,11 +529,15 @@
val concl_of = Logic.strip_imp_concl o prop_of;
val prems_of = Logic.strip_imp_prems o prop_of;
+fun take_prems_of n = Logic.take_imp_prems n o prop_of;
val nprems_of = Logic.count_prems o prop_of;
val no_prems = Logic.no_prems o prop_of;
+fun prem_of th i =
+ Logic.nth_prem (i, prop_of th) handle TERM _ => raise THM ("prem_of", i, [th]);
+
fun major_prem_of th =
- (case prems_of th of
+ (case take_prems_of 1 th of
prem :: _ => Logic.strip_assums_concl prem
| [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));
@@ -540,6 +555,10 @@
map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
(prems_of th);
+fun take_cprems_of n (th as Thm (_, {cert, maxidx, shyps, ...})) =
+ map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
+ (take_prems_of n th);
+
fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) =
map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;
@@ -1262,6 +1281,10 @@
end
end;
+fun assume_cterm A = assume A
+ handle THM (msg, _, _) => raise CTERM (msg, [A]);
+
+
(*Implication introduction
[A]
:
--- a/src/Tools/IsaPlanner/isand.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Tools/IsaPlanner/isand.ML Fri Jan 24 10:22:17 2025 +0100
@@ -102,7 +102,7 @@
fun hide_other_goals th =
let
(* tl beacuse fst sg is the goal we are interested in *)
- val cprems = tl (Drule.cprems_of th);
+ val cprems = tl (Thm.cprems_of th);
val aprems = map Thm.assume cprems;
in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end;
--- a/src/Tools/induct.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/Tools/induct.ML Fri Jan 24 10:22:17 2025 +0100
@@ -120,7 +120,7 @@
in
-fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty =>
+fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.take_prems_of 1 thm)))) handle List.Empty =>
raise THM ("No variables in major premise of rule", 0, [thm]);
val left_var_concl = concl_var hd;
--- a/src/ZF/Tools/induct_tacs.ML Thu Jan 23 13:42:58 2025 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Fri Jan 24 10:22:17 2025 +0100
@@ -97,7 +97,7 @@
|> (if exh then #exhaustion else #induct)
|> Thm.transfer thy;
val \<^Const_>\<open>mem for \<open>Var(ixn,_)\<close> _\<close> =
- (case Thm.prems_of rule of
+ (case Thm.take_prems_of 1 rule of
[] => error "induction is not available for this datatype"
| major::_ => \<^dest_judgment> major)
in
@@ -124,7 +124,7 @@
val constructors =
map (head_of o const_of o \<^dest_judgment> o Thm.prop_of) case_eqns;
- val \<^Const_>\<open>mem for _ data\<close> = \<^dest_judgment> (hd (Thm.prems_of elim));
+ val \<^Const_>\<open>mem for _ data\<close> = \<^dest_judgment> (hd (Thm.take_prems_of 1 elim));
val Const(big_rec_name, _) = head_of data;