author paulson Thu, 04 Oct 2007 12:32:58 +0200 changeset 24827 646bdc51eb7d parent 24826 78e6a3cea367 child 24828 137c242e7277
combinator translation
 src/HOL/ATP_Linkup.thy file | annotate | diff | comparison | revisions src/HOL/MetisExamples/Abstraction.thy file | annotate | diff | comparison | revisions src/HOL/MetisExamples/Tarski.thy file | annotate | diff | comparison | revisions src/HOL/Tools/meson.ML file | annotate | diff | comparison | revisions src/HOL/Tools/metis_tools.ML file | annotate | diff | comparison | revisions src/HOL/Tools/res_atp.ML file | annotate | diff | comparison | revisions src/HOL/Tools/res_axioms.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/ATP_Linkup.thy	Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/ATP_Linkup.thy	Thu Oct 04 12:32:58 2007 +0200
@@ -56,24 +56,6 @@
lemma equal_imp_fequal: "X=Y ==> fequal X Y"

-lemma K_simp: "COMBK P == (%Q. P)"
-apply (rule eq_reflection)
-apply (rule ext)
-done
-
-lemma I_simp: "COMBI == (%P. P)"
-apply (rule eq_reflection)
-apply (rule ext)
-done
-
-lemma B_simp: "COMBB P Q == %R. P (Q R)"
-apply (rule eq_reflection)
-apply (rule ext)
-done
-
text{*These two represent the equivalence between Boolean equality and iff.
They can't be converted to clauses automatically, as the iff would be
expanded...*}
@@ -84,8 +66,41 @@
lemma iff_negative: "~P | ~Q | P=Q"
by blast

+text{*Theorems for translation to combinators*}
+
+lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+lemma abs_I: "(%x. x) == COMBI"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+lemma abs_K: "(%x. y) == COMBK y"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+lemma abs_B: "(%x. a (g x)) == COMBB a g"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+lemma abs_C: "(%x. (f x) b) == COMBC f b"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+
use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
-use "Tools/res_hol_clause.ML"  --{*requires the combinators*}
+use "Tools/res_hol_clause.ML"
use "Tools/res_reconstruct.ML"
use "Tools/watcher.ML"
use "Tools/res_atp.ML"
@@ -102,17 +117,14 @@
oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}

use "Tools/res_atp_methods.ML"
-setup ResAtpMethods.setup
-
+setup ResAtpMethods.setup      --{*Oracle ATP methods: still useful?*}
+setup ResAxioms.setup          --{*Sledgehammer*}

subsection {* The Metis prover *}

use "Tools/metis_tools.ML"
setup MetisTools.setup

-(*Sledgehammer*)
-setup ResAxioms.setup
-
setup {*
Theory.at_end ResAxioms.clause_cache_endtheory
*}```
```--- a/src/HOL/MetisExamples/Abstraction.thy	Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/MetisExamples/Abstraction.thy	Thu Oct 04 12:32:58 2007 +0200
@@ -67,74 +67,107 @@

+(*single-step*)
+lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"

-(*single-step*)
+
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
proof (neg_clausify)
-assume 0: "(a, b) \<in> Sigma A (llabs_subgoal_1 f)"
-assume 1: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)"
-assume 2: "a \<notin> A \<or> a \<noteq> f b"
-have 3: "a \<in> A"
-have 4: "f b \<noteq> a"
-  by (metis 3 2)
-have 5: "f b = a"
-  by (metis Domain_Id Compl_UNIV_eq singleton_conv2 vimage_Collect_eq 1 vimage_singleton_eq SigmaD2 0)
+assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type)
+\<in> Sigma (A\<Colon>'a\<Colon>type set)
+   (COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)))"
+assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> a \<noteq> (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type)"
+have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
+have 3: "(b\<Colon>'b\<Colon>type)
+\<in> COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)) (a\<Colon>'a\<Colon>type)"
+have 4: "(b\<Colon>'b\<Colon>type) \<in> Collect (COMBB (op = (a\<Colon>'a\<Colon>type)) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type))"
+  by (metis 3)
+have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)"
+  by (metis 1 2)
+have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)"
+  by (metis 4 vimage_singleton_eq insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def)
show "False"
-  by (metis 5 4)
-qed finish_clausify
+  by (metis 5 6)
+qed
+
+(*Alternative structured proof, untyped*)
+lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
+proof (neg_clausify)
+assume 0: "(a, b) \<in> Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))"
+have 1: "b \<in> Collect (COMBB (op = a) f)"
+have 2: "f b = a"
+  by (metis 1 vimage_Collect_eq singleton_conv2 insert_def union_empty2 vimage_singleton_eq vimage_def)
+assume 3: "a \<notin> A \<or> a \<noteq> f b"
+have 4: "a \<in> A"
+have 5: "f b \<noteq> a"
+  by (metis 4 3)
+show "False"
+  by (metis 5 2)
+qed

ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*}
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
-done

lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
proof (neg_clausify)
-assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
-   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set) cl =
-   Collect (llabs_Set_XCollect_ex_eq_3 op \<in> (pset cl))"
-assume 1: "(f\<Colon>'a\<Colon>type) \<notin> pset (cl\<Colon>'a\<Colon>type set)"
-assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type) \<in> (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)"
-have 3: "llabs_Predicate_Xsup_Un_eq2_1 (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
- (cl\<Colon>'a\<Colon>type set) (f\<Colon>'a\<Colon>type)"
-  by (metis acc_def 2)
-assume 4: "(CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set) =
-Sigma (CL\<Colon>'a\<Colon>type set set) (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set)"
+assume 0: "(cl, f) \<in> CLF"
+assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \<in>) pset))"
+assume 2: "f \<notin> pset cl"
+have 3: "\<And>X1 X2. X2 \<in> COMBB Collect (COMBB (COMBC op \<in>) pset) X1 \<or> (X1, X2) \<notin> CLF"
+have 4: "\<And>X1 X2. X2 \<in> pset X1 \<or> (X1, X2) \<notin> CLF"
+  by (metis 3 Collect_mem_eq)
+have 5: "(cl, f) \<notin> CLF"
+  by (metis 2 4)
show "False"
-  by (metis 1 Collect_mem_eq 0 3 4 acc_def SigmaD2)
-qed finish_clausify (*ugly hack: combinators??*)
+  by (metis 5 0)
+qed

ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}
lemma
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
f \<in> pset cl \<rightarrow> pset cl"
-done
+proof (neg_clausify)
+assume 0: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
+assume 1: "(cl, f)
+\<in> Sigma CL
+   (COMBB Collect
+     (COMBB (COMBC op \<in>) (COMBS (COMBB Pi pset) (COMBB COMBK pset))))"
+show "False"
+(*  by (metis 0 Collect_mem_eq SigmaD2 1) ??doesn't terminate*)
+  by (insert 0 1, simp add: COMBB_def COMBS_def COMBC_def)
+qed

-lemma
-    "(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
-    f \<in> pset cl \<rightarrow> pset cl"
-proof (neg_clausify)
-assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
-   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set) cl =
-   Collect
-    (llabs_Set_XCollect_ex_eq_3 op \<in> (Pi (pset cl) (COMBK (pset cl))))"
-assume 1: "(f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type) \<notin> Pi (pset (cl\<Colon>'a\<Colon>type set)) (COMBK (pset cl))"
-assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type)
-\<in> Sigma (CL\<Colon>'a\<Colon>type set set)
-   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set)"
-show "False"
-  by (metis 1 Collect_mem_eq 0 SigmaD2 2)
-qed finish_clausify
-    (*Hack to prevent the "Additional hypotheses" error*)

ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*}
lemma
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
f \<in> pset cl \<inter> cl"
+proof (neg_clausify)
+assume 0: "(cl, f)
+\<in> Sigma CL
+   (COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)))"
+assume 1: "f \<notin> pset cl \<inter> cl"
+have 2: "f \<in> COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)) cl"
+  by (insert 0, simp add: COMBB_def)
+(*  by (metis SigmaD2 0)  ??doesn't terminate*)
+have 3: "f \<in> COMBS (COMBB op \<inter> pset) COMBI cl"
+  by (metis 2 Collect_mem_eq)
+have 4: "f \<notin> cl \<inter> pset cl"
+  by (metis 1 Int_commute)
+have 5: "f \<in> cl \<inter> pset cl"
+  by (metis 3 Int_commute)
+show "False"
+  by (metis 5 4)
+qed
+

ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}
lemma
@@ -146,28 +179,40 @@
lemma "(cl,f) \<in> CLF ==>
CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
f \<in> pset cl \<inter> cl"
+by auto
+(*??no longer terminates, with combinators
by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
--{*@{text Int_def} is redundant}
+*)

ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
lemma "(cl,f) \<in> CLF ==>
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
f \<in> pset cl \<inter> cl"
+by auto
+(*??no longer terminates, with combinators
+*)

ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}
lemma
"(cl,f) \<in> CLF ==>
CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==>
f \<in> pset cl \<rightarrow> pset cl"
+by auto
+(*??no longer terminates, with combinators
+*)

ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}
lemma
"(cl,f) \<in> CLF ==>
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
f \<in> pset cl \<rightarrow> pset cl"
+by auto
+(*??no longer terminates, with combinators
by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
+*)

ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}
lemma ```
```--- a/src/HOL/MetisExamples/Tarski.thy	Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/MetisExamples/Tarski.thy	Thu Oct 04 12:32:58 2007 +0200
@@ -515,8 +515,11 @@
apply (rule_tac t = "H" in ssubst, assumption)
apply (rule CollectI)
apply (rule conjI)
-ML{*ResAtp.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*}
-apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE monotone_f reflD1 reflD2)
+ML{*ResAtp.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*}
+(*??no longer terminates, with combinators
+apply (metis CO_refl lubH_le_flubH monotone_def monotone_f reflD1 reflD2)
+*)
+apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE [OF monotone_f] reflD1 reflD2)
apply (metis CO_refl lubH_le_flubH reflD2)
done
declare CLF.f_in_funcset[rule del] funcset_mem[rule del]
@@ -529,51 +532,73 @@
ML{*ResAtp.problem_name:="Tarski__CLF_lubH_is_fixp"*}
(*Single-step version fails. The conjecture clauses refer to local abstraction
functions (Frees), which prevents expand_defs_tac from removing those
-"definitions" at the end of the proof.
+"definitions" at the end of the proof. *)
lemma (in CLF) lubH_is_fixp:
"H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
apply (rule conjI)
- proof (neg_clausify)
-assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)"
-assume 1: "lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl \<notin> A"
-have 2: "glb H (dual cl) \<notin> A"
-  by (metis 0 1 lub_dual_glb)
-have 3: "(glb H (dual cl), f (glb H (dual cl))) \<in> r"
-  by (metis 0 lubH_le_flubH lub_dual_glb)
-have 4: "(f (glb H (dual cl)), glb H (dual cl)) \<in> r"
-  by (metis 0 flubH_le_lubH lub_dual_glb)
-have 5: "glb H (dual cl) = f (glb H (dual cl)) \<or>
-(glb H (dual cl), f (glb H (dual cl))) \<notin> r"
-  by (metis 4 antisymE)
-have 6: "glb H (dual cl) = f (glb H (dual cl))"
-  by (metis 3 5)
-have 7: "(glb H (dual cl), glb H (dual cl)) \<in> r"
-  by (metis 4 6)
-have 8: "\<And>X1. glb H (dual cl) \<in> X1 \<or> \<not> refl X1 r"
-  by (metis reflD2 7)
+proof (neg_clausify)
+assume 0: "H =
+Collect
+ (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
+assume 1: "lub (Collect
+      (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
+        (COMBC op \<in> A)))
+ cl
+\<notin> A"
+have 2: "lub H cl \<notin> A"
+  by (metis 1 0)
+have 3: "(lub H cl, f (lub H cl)) \<in> r"
+  by (metis lubH_le_flubH 0)
+have 4: "(f (lub H cl), lub H cl) \<in> r"
+  by (metis flubH_le_lubH 0)
+have 5: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
+  by (metis antisymE 4)
+have 6: "lub H cl = f (lub H cl)"
+  by (metis 5 3)
+have 7: "(lub H cl, lub H cl) \<in> r"
+  by (metis 6 4)
+have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl X1 r"
+  by (metis 7 reflD2)
have 9: "\<not> refl A r"
-  by (metis 2 8)
+  by (metis 8 2)
show "False"
-  by (metis 9 CO_refl)
-proof (neg_clausify)
-assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)"
-assume 1: "f (lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl) \<noteq>
-lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl"
-have 2: "(glb H (dual cl), f (glb H (dual cl))) \<in> r"
-  by (metis 0 lubH_le_flubH lub_dual_glb lub_dual_glb)
-have 3: "f (glb H (dual cl)) \<noteq> glb H (dual cl)"
-  by (metis 0 1 lub_dual_glb)
-have 4: "(f (glb H (dual cl)), glb H (dual cl)) \<in> r"
-  by (metis lub_dual_glb flubH_le_lubH 0)
-have 5: "f (glb H (dual cl)) = glb H (dual cl) \<or>
-(f (glb H (dual cl)), glb H (dual cl)) \<notin> r"
-  by (metis antisymE 2)
-have 6: "f (glb H (dual cl)) = glb H (dual cl)"
-  by (metis 5 4)
-show "False"
-  by (metis 3 6)
-*)
+  by (metis CO_refl 9);
+next --{*apparently the way to insert a second structured proof*}
+  show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow>
+  f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) = lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
+  proof (neg_clausify)
+  assume 0: "H =
+  Collect
+   (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
+  assume 1: "f (lub (Collect
+	   (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
+	     (COMBC op \<in> A)))
+      cl) \<noteq>
+  lub (Collect
+	(COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
+	  (COMBC op \<in> A)))
+   cl"
+  have 2: "f (lub H cl) \<noteq>
+  lub (Collect
+	(COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
+	  (COMBC op \<in> A)))
+   cl"
+    by (metis 1 0)
+  have 3: "f (lub H cl) \<noteq> lub H cl"
+    by (metis 2 0)
+  have 4: "(lub H cl, f (lub H cl)) \<in> r"
+    by (metis lubH_le_flubH 0)
+  have 5: "(f (lub H cl), lub H cl) \<in> r"
+    by (metis flubH_le_lubH 0)
+  have 6: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
+    by (metis antisymE 5)
+  have 7: "lub H cl = f (lub H cl)"
+    by (metis 6 4)
+  show "False"
+    by (metis 3 7)
+  qed
+qed

lemma (in CLF) lubH_is_fixp:
"H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
@@ -616,9 +641,13 @@
apply (rule lubI)
ML{*ResAtp.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*}
apply (metis P_def equalityE fix_subset subset_trans)
-apply (metis P_def fix_subset lubH_is_fixp set_mp subset_refl subset_trans)
-apply (metis P_def fixf_le_lubH)
-apply (metis P_def lubH_is_fixp)
+apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def)
+(*??no longer terminates, with combinators
+apply (metis P_def fix_def fixf_le_lubH)
+apply (metis P_def fix_def lubH_least_fixf)
+*)
done
declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del]
CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del]
@@ -662,21 +691,18 @@
ML{*ResAtp.problem_name:="Tarski__rel_imp_elem"*}
declare (in CLF) CO_refl[simp] refl_def [simp]
lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
-apply (metis CO_refl reflD1)
-done
+by (metis CO_refl reflD1)
declare (in CLF) CO_refl[simp del]  refl_def [simp del]

ML{*ResAtp.problem_name:="Tarski__interval_subset"*}
declare (in CLF) rel_imp_elem[intro]
declare interval_def [simp]
lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
-apply (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
-done
+by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
declare (in CLF) rel_imp_elem[rule del]
declare interval_def [simp del]

-
lemma (in CLF) intervalI:
"[| (a, x) \<in> r; (x, b) \<in> r |] ==> x \<in> interval r a b"
@@ -966,8 +992,7 @@

ML{*ResAtp.problem_name:="Tarski__intY1_func"*}  (*ALL THEOREMS*)
lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
-apply (metis intY1_f_closed restrict_in_funcset)
-done
+by (metis intY1_f_closed restrict_in_funcset)

ML{*ResAtp.problem_name:="Tarski__intY1_mono"*}  (*ALL THEOREMS*)
lemma (in Tarski) intY1_mono [skolem]:```
```--- a/src/HOL/Tools/meson.ML	Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Oct 04 12:32:58 2007 +0200
@@ -17,6 +17,7 @@
val first_order_resolve: thm -> thm -> thm
val flexflex_first_order: thm -> thm
val size_of_subgoals: thm -> int
+  val too_many_clauses: term -> bool
val make_cnf: thm list -> thm -> thm list
val finish_cnf: thm list -> thm list
val generalize: thm -> thm```
```--- a/src/HOL/Tools/metis_tools.ML	Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 04 12:32:58 2007 +0200
@@ -290,7 +290,10 @@
let val v = find_var x
val t = fol_term_to_hol_RAW ctxt y
in  SOME (cterm_of thy v, t)  end
-              handle Option => NONE (*List.find failed for the variable.*)
+              handle Option =>
+                  (Output.debug (fn() => "List.find failed for the variable " ^ x ^
+                                         " in " ^ string_of_thm i_th);
+                   NONE)
fun remove_typeinst (a, t) =
case Recon.strip_prefix ResClause.schematic_var_prefix a of
SOME b => SOME (b, t)
@@ -446,11 +449,11 @@
val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal");
val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal");

-  val comb_I  = ResHolClause.comb_I  RS meta_eq_to_obj_eq;
-  val comb_K  = ResHolClause.comb_K  RS meta_eq_to_obj_eq;
-  val comb_B  = ResHolClause.comb_B  RS meta_eq_to_obj_eq;
-
-  val ext_thm = cnf_th ResHolClause.ext;
+  val comb_I = cnf_th ResHolClause.comb_I;
+  val comb_K = cnf_th ResHolClause.comb_K;
+  val comb_B = cnf_th ResHolClause.comb_B;
+  val comb_C = cnf_th ResHolClause.comb_C;
+  val comb_S = cnf_th ResHolClause.comb_S;

fun dest_Arity (ResClause.ArityClause{premLits,...}) =
map ResClause.class_of_arityLit premLits;
@@ -509,10 +512,14 @@
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
(*Now check for the existence of certain combinators*)
-        val IK    = if used "c_COMBI" orelse used "c_COMBK" then [comb_I,comb_K] else []
-        val BC    = if used "c_COMBB" then [comb_B] else []
-        val EQ    = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
-        val lmap' = if isFO then lmap else foldl (add_thm ctxt) lmap ([ext_thm] @ EQ @ IK @ BC)
+        val thI  = if used "c_COMBI" then [comb_I] else []
+        val thK  = if used "c_COMBK" then [comb_K] else []
+        val thB   = if used "c_COMBB" then [comb_B] else []
+        val thC   = if used "c_COMBC" then [comb_C] else []
+        val thS   = if used "c_COMBS" then [comb_S] else []
+        val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
+        val lmap' = if isFO then lmap
+                    else foldl (add_thm ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
in
add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
end;```
```--- a/src/HOL/Tools/res_atp.ML	Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Oct 04 12:32:58 2007 +0200
@@ -769,7 +769,7 @@
(*Called by the oracle-based methods declared in res_atp_methods.ML*)
fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
let val conj_cls = Meson.make_clauses conjectures
-                         |> ResAxioms.assume_abstract_list "subgoal" |> Meson.finish_cnf
+                         |> map ResAxioms.combinators |> Meson.finish_cnf
val hyp_cls = cnf_hyps_thms ctxt
val goal_cls = conj_cls@hyp_cls
val goal_tms = map prop_of goal_cls```
```--- a/src/HOL/Tools/res_axioms.ML	Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 04 12:32:58 2007 +0200
@@ -15,7 +15,7 @@
val cnf_rules_of_ths: thm list -> thm list
val neg_clausify: thm list -> thm list
val expand_defs_tac: thm -> tactic
-  val assume_abstract_list: string -> thm list -> thm list
+  val combinators: thm -> thm
val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
@@ -31,26 +31,6 @@
(* FIXME legacy *)
fun freeze_thm th = #1 (Drule.freeze_thaw th);

-val lhs_of = #1 o Logic.dest_equals o Thm.prop_of;
-val rhs_of = #2 o Logic.dest_equals o Thm.prop_of;
-
-
-(*Store definitions of abstraction functions, ensuring that identical right-hand
-  sides are denoted by the same functions and thereby reducing the need for
-  extensionality in proofs.
-  FIXME!  Store in theory data!!*)
-
-(*Populate the abstraction cache with common combinators.*)
-fun seed th net =
-  let val (_,ct) = Thm.dest_abs NONE (Thm.rhs_of th)
-      val t = Logic.legacy_varify (term_of ct)
-  in  Net.insert_term Thm.eq_thm (t, th) net end;
-
-val abstraction_cache = ref
-

(**** Transformation of Elimination Rules into First-Order Formulas****)

@@ -149,7 +129,7 @@
in  dec_sko (prop_of th) []  end;

-(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****)
+(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)

(*Returns the vars of a theorem*)
fun vars_of_thm th =
@@ -175,201 +155,98 @@
strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
| _ => th;

-(*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
-  where some types have the empty sort.*)
-val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
-fun mk_object_eq th = th RS meta_eq_to_obj_eq
-    handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
-
-(*Apply a function definition to an argument, beta-reducing the result.*)
-fun beta_comb cf x =
-  let val th1 = combination cf (reflexive x)
-      val th2 = beta_conversion false (Thm.rhs_of th1)
-  in  transitive th1 th2  end;
-
-(*Apply a function definition to arguments, beta-reducing along the way.*)
-fun list_combination cf [] = cf
-  | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs;
-
-fun list_cabs ([] ,     t) = t
-  | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
-
fun assert_eta_free ct =
let val t = term_of ct
in if (t aconv Envir.eta_contract t) then ()
else error ("Eta redex in term: " ^ string_of_cterm ct)
end;

-fun eq_absdef (th1, th2) =
-    Context.joinable (theory_of_thm th1, theory_of_thm th2)  andalso
-    rhs_of th1 aconv rhs_of th2;
-
val lambda_free = not o Term.has_abs;

val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);

-fun dest_abs_list ct =
-  let val (cv,ct') = Thm.dest_abs NONE ct
-      val (cvs,cu) = dest_abs_list ct'
-  in (cv::cvs, cu) end
-  handle CTERM _ => ([],ct);
+val abs_S = @{thm"abs_S"};
+val abs_K = @{thm"abs_K"};
+val abs_I = @{thm"abs_I"};
+val abs_B = @{thm"abs_B"};
+val abs_C = @{thm"abs_C"};

-fun abstract_rule_list [] [] th = th
-  | abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th)
-  | abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]);
-
-
-val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
+val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B));
+val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C));
+val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S));

-(*Does an existing abstraction definition have an RHS that matches the one we need now?
-  thy is the current theory, which must extend that of theorem th.*)
-fun match_rhs thy t th =
-  let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
-                                   " against\n" ^ string_of_thm th);
-      val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
-      val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
-      val ct_pairs = if subthy (theory_of_thm th, thy) andalso
-                        forall lambda_free (map #2 term_insts)
-                     then map (pairself (cterm_of thy)) term_insts
-                     else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*)
-      fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
-      val th' = cterm_instantiate ct_pairs th
-  in  SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th')  end
-  handle _ => NONE;
+(*FIXME: requires more use of cterm constructors*)
+fun abstract ct =
+  let val Abs(x,_,body) = term_of ct
+      val thy = theory_of_cterm ct
+      val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
+      val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
+      fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K
+  in
+      case body of
+          Const _ => makeK()
+        | Free _ => makeK()
+        | Var _ => makeK()  (*though Var isn't expected*)
+        | Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*)
+        | rator\$rand =>
+	    if loose_bvar1 (rator,0) then (*C or S*)
+	       if loose_bvar1 (rand,0) then (*S*)
+	         let val crator = cterm_of thy (Abs(x,xT,rator))
+	             val crand = cterm_of thy (Abs(x,xT,rand))
+	             val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S
+	             val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
+	         in
+	           Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
+	         end
+	       else (*C*)
+	         let val crator = cterm_of thy (Abs(x,xT,rator))
+	             val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C
+	             val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
+	         in
+	           Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
+	         end
+	    else if loose_bvar1 (rand,0) then (*B or eta*)
+	       if rand = Bound 0 then eta_conversion ct
+	       else (*B*)
+	         let val crand = cterm_of thy (Abs(x,xT,rand))
+	             val abs_B' = cterm_instantiate [(f_B, cterm_of thy rator),(g_B,crand)] abs_B
+	             val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
+	         in
+	           Thm.transitive abs_B' (Conv.arg_conv abstract rhs)
+	         end
+	    else makeK()
+        | _ => error "abstract: Bad term"
+  end;

(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
prefix for the constants. Resulting theory is returned in the first theorem. *)
-fun declare_absfuns s th =
-  let val nref = ref 0
-      fun abstract thy ct =
-        if lambda_free (term_of ct) then (transfer thy (reflexive ct), [])
-        else
-        case term_of ct of
-          Abs _ =>
-            let val cname = "llabs_" ^ s ^ "_" ^ Int.toString (inc nref)
-                val _ = assert_eta_free ct;
-                val (cvs,cta) = dest_abs_list ct
-                val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
-                val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta);
-                val (u'_th,defs) = abstract thy cta
-                val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th);
-                val cu' = Thm.rhs_of u'_th
-                val u' = term_of cu'
-                val abs_v_u = fold_rev (lambda o term_of) cvs u'
-                (*get the formal parameters: ALL variables free in the term*)
-                val args = term_frees abs_v_u
-                val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments");
-                val rhs = list_abs_free (map dest_Free args, abs_v_u)
-                      (*Forms a lambda-abstraction over the formal parameters*)
-                val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu');
-                val thy = theory_of_thm u'_th
-                val (ax,ax',thy) =
-                 case List.mapPartial (match_rhs thy abs_v_u)
-                         (Net.match_term (!abstraction_cache) u') of
-                     (ax,ax')::_ =>
-                       (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
-                        (ax,ax',thy))
-                   | [] =>
-                      let val _ = Output.debug (fn()=>"Lookup was empty");
-                          val Ts = map type_of args
-                          val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
-                          val c = Const (Sign.full_name thy cname, cT)
-                          val thy =
-                            Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy
-                                     (*Theory is augmented with the constant,
-                                       then its definition*)
-                          val cdef = cname ^ "_def"
-                          val thy = Theory.add_defs_i true false
-                                       [(cdef, equals cT \$ c \$ rhs)] thy
-                                    handle ERROR _ => raise Clausify_failure thy
-                          val ax = Thm.get_axiom_i thy (Sign.full_name thy cdef)
-                                     |> Drule.unvarify
-                                     |> mk_object_eq |> strip_lambdas (length args)
-                                     |> mk_meta_eq |> Meson.generalize
-                          val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
-                          val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^
-                                                       "Instance: " ^ string_of_thm ax');
-                          val _ = abstraction_cache := Net.insert_term eq_absdef
-                                            ((Logic.varify u'), ax) (!abstraction_cache)
-                            handle Net.INSERT =>
-                              raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
-                       in  (ax,ax',thy)  end
-            in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
-               (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
-        | (t1\$t2) =>
-            let val (ct1,ct2) = Thm.dest_comb ct
-                val (th1,defs1) = abstract thy ct1
-                val (th2,defs2) = abstract (theory_of_thm th1) ct2
-            in  (combination th1 th2, defs1@defs2)  end
-      val _ = Output.debug (fn()=>"declare_absfuns, Abstracting: " ^ string_of_thm th);
-      val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
-      val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
-      val _ = Output.debug (fn()=>"declare_absfuns, Result: " ^ string_of_thm (hd ths));
-  in  (theory_of_thm eqth, map Drule.eta_contraction_rule ths)  end;
-
-fun name_of def = try (#1 o dest_Free o lhs_of) def;
-
-(*A name is valid provided it isn't the name of a defined abstraction.*)
-fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
-  | valid_name defs _ = false;
-
-(*s is the theorem name (hint) or the word "subgoal"*)
-fun assume_absfuns s th =
-  let val thy = theory_of_thm th
-      val cterm = cterm_of thy
-      val abs_count = ref 0
-      fun abstract ct =
-        if lambda_free (term_of ct) then (reflexive ct, [])
-        else
-        case term_of ct of
-          Abs (_,T,u) =>
-            let val _ = assert_eta_free ct;
-                val (cvs,cta) = dest_abs_list ct
-                val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
-                val (u'_th,defs) = abstract cta
-                val cu' = Thm.rhs_of u'_th
-                val u' = term_of cu'
-                (*Could use Thm.cabs instead of lambda to work at level of cterms*)
-                val abs_v_u = fold_rev (lambda o term_of) cvs (term_of cu')
-                (*get the formal parameters: free variables not present in the defs
-                  (to avoid taking abstraction function names as parameters) *)
-                val args = filter (valid_name defs) (term_frees abs_v_u)
-                val crhs = list_cabs (map cterm args, cterm abs_v_u)
-                      (*Forms a lambda-abstraction over the formal parameters*)
-                val rhs = term_of crhs
-                val (ax,ax') =
-                 case List.mapPartial (match_rhs thy abs_v_u)
-                        (Net.match_term (!abstraction_cache) u') of
-                     (ax,ax')::_ =>
-                       (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
-                        (ax,ax'))
-                   | [] =>
-                      let val Ts = map type_of args
-                          val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
-                          val id = "llabs_" ^ s ^ "_" ^ Int.toString (inc abs_count)
-                          val c = Free (id, const_ty)
-                          val ax = assume (Thm.capply (cterm (equals const_ty \$ c)) crhs)
-                                     |> mk_object_eq |> strip_lambdas (length args)
-                                     |> mk_meta_eq |> Meson.generalize
-                          val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
-                          val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax)
-                                    (!abstraction_cache)
-                            handle Net.INSERT =>
-                              raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
-                      in (ax,ax') end
-            in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
-               (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
-        | (t1\$t2) =>
-            let val (ct1,ct2) = Thm.dest_comb ct
-                val (t1',defs1) = abstract ct1
-                val (t2',defs2) = abstract ct2
-            in  (combination t1' t2', defs1@defs2)  end
-      val _ = Output.debug (fn()=>"assume_absfuns, Abstracting: " ^ string_of_thm th);
-      val (eqth,defs) = abstract (cprop_of th)
-      val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
-      val _ = Output.debug (fn()=>"assume_absfuns, Result: " ^ string_of_thm (hd ths));
-  in  map Drule.eta_contraction_rule ths  end;
-
+fun combinators_aux ct =
+  if lambda_free (term_of ct) then reflexive ct
+  else
+  case term_of ct of
+      Abs _ =>
+	let val _ = assert_eta_free ct;
+	    val (cv,cta) = Thm.dest_abs NONE ct
+	    val (v,Tv) = (dest_Free o term_of) cv
+	    val _ = Output.debug (fn()=>"  recursion: " ^ string_of_cterm cta);
+	    val u_th = combinators_aux cta
+	    val _ = Output.debug (fn()=>"  returned " ^ string_of_thm u_th);
+	    val cu = Thm.rhs_of u_th
+	    val comb_eq = abstract (Thm.cabs cv cu)
+	in Output.debug (fn()=>"  abstraction result: " ^ string_of_thm comb_eq);
+	   (transitive (abstract_rule v cv u_th) comb_eq) end
+    | t1 \$ t2 =>
+	let val (ct1,ct2) = Thm.dest_comb ct
+	in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
+
+fun combinators th =
+  if lambda_free (prop_of th) then th
+  else
+    let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ string_of_thm th);
+	val th = Drule.eta_contraction_rule th
+	val eqth = combinators_aux (cprop_of th)
+	val _ = Output.debug (fn()=>"Conversion result: " ^ string_of_thm eqth);
+    in  equal_elim eqth th   end;

(*cterms are used throughout for efficiency*)
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
@@ -430,27 +307,6 @@
[] => ()
| ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths'));

-fun assume_abstract s th =
-  if lambda_free (prop_of th) then [th]
-  else th |> Drule.eta_contraction_rule |> assume_absfuns s
-          |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
-
-(*Replace lambdas by assumed function definitions in the theorems*)
-fun assume_abstract_list s ths = List.concat (map (assume_abstract s) ths);
-
-(*Replace lambdas by declared function definitions in the theorems*)
-fun declare_abstract s (thy, []) = (thy, [])
-  | declare_abstract s (thy, th::ths) =
-      let val (thy', th_defs) =
-            if lambda_free (prop_of th) then (thy, [th])
-            else
-                th |> zero_var_indexes |> freeze_thm
-                   |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns s
-                handle Clausify_failure thy_e => (thy_e,[])
-          val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
-          val (thy'', ths') = declare_abstract (s^"'") (thy', ths)
-      in  (thy'', th_defs @ ths')  end;
-
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (NameSpace.explode s);

@@ -465,7 +321,7 @@
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
fun skolem_thm th =
let val nnfth = to_nnf th and s = fake_name th
-  in  Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |> assume_abstract_list s |> Meson.finish_cnf
+  in  Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |>  map combinators |> Meson.finish_cnf
end
handle THM _ => [];

@@ -480,8 +336,8 @@
val (thy',defs) = declare_skofuns s nnfth thy
val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
-              val (thy'',cnfs') = declare_abstract s (thy',cnfs)
-          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') end
+              val cnfs' = map combinators cnfs
+          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy') end
handle Clausify_failure thy_e => ([],thy_e)
)
(try to_nnf th);
@@ -575,8 +431,26 @@

val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];

+val max_lambda_nesting = 3;
+
+fun excessive_lambdas (f\$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k)
+  | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1)
+  | excessive_lambdas _ = false;
+
+fun is_formula_type T = (T = HOLogic.boolT orelse T = propT);
+
+(*Don't count nested lambdas at the level of formulas, as they are quantifiers*)
+fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t
+  | excessive_lambdas_fm Ts t =
+      if is_formula_type (fastype_of1 (Ts, t))
+      then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t))
+      else excessive_lambdas (t, max_lambda_nesting);
+
+fun too_complex t =
+  Meson.too_many_clauses t orelse excessive_lambdas_fm [] t;
+
fun skolem_cache th thy =
-  if PureThy.is_internal th then thy
+  if PureThy.is_internal th orelse too_complex (prop_of th) then thy
else #2 (skolem_cache_thm th thy);

val skolem_cache_theorems_of = Symtab.fold (fold skolem_cache o snd) o #2 o PureThy.theorems_of;
@@ -598,7 +472,7 @@
fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);

(*Expand all new*definitions of abstraction or Skolem functions in a proof state.*)
-fun is_absko (Const ("==", _) \$ Free (a,_) \$ u) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
+fun is_absko (Const ("==", _) \$ Free (a,_) \$ u) = String.isPrefix "sko_" a
| is_absko _ = false;

fun is_okdef xs (Const ("==", _) \$ t \$ u) =   (*Definition of Free, not in certain terms*)
@@ -607,7 +481,7 @@

(*This function tries to cope with open locales, which introduce hypotheses of the form
Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
-  of llabs_ and sko_ functions. *)
+  of sko_ functions. *)
fun expand_defs_tac st0 st =
let val hyps0 = #hyps (rep_thm st0)
val hyps = #hyps (crep_thm st)
@@ -652,7 +526,7 @@
val no_tvars = null o term_tvars o prop_of;

val neg_clausify =
-  filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o Meson.make_clauses;
+  filter no_tvars o Meson.finish_cnf o map combinators o Meson.make_clauses;

fun neg_conjecture_clauses st0 n =
let val st = Seq.hd (neg_skolemize_tac n st0)```