combinator translation
authorpaulson
Thu Oct 04 12:32:58 2007 +0200 (2007-10-04)
changeset 24827646bdc51eb7d
parent 24826 78e6a3cea367
child 24828 137c242e7277
combinator translation
src/HOL/ATP_Linkup.thy
src/HOL/MetisExamples/Abstraction.thy
src/HOL/MetisExamples/Tarski.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Wed Oct 03 22:33:17 2007 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Thu Oct 04 12:32:58 2007 +0200
     1.3 @@ -56,24 +56,6 @@
     1.4  lemma equal_imp_fequal: "X=Y ==> fequal X Y"
     1.5    by (simp add: fequal_def)
     1.6  
     1.7 -lemma K_simp: "COMBK P == (%Q. P)"
     1.8 -apply (rule eq_reflection)
     1.9 -apply (rule ext)
    1.10 -apply (simp add: COMBK_def)
    1.11 -done
    1.12 -
    1.13 -lemma I_simp: "COMBI == (%P. P)"
    1.14 -apply (rule eq_reflection)
    1.15 -apply (rule ext)
    1.16 -apply (simp add: COMBI_def)
    1.17 -done
    1.18 -
    1.19 -lemma B_simp: "COMBB P Q == %R. P (Q R)"
    1.20 -apply (rule eq_reflection)
    1.21 -apply (rule ext)
    1.22 -apply (simp add: COMBB_def)
    1.23 -done
    1.24 -
    1.25  text{*These two represent the equivalence between Boolean equality and iff.
    1.26  They can't be converted to clauses automatically, as the iff would be
    1.27  expanded...*}
    1.28 @@ -84,8 +66,41 @@
    1.29  lemma iff_negative: "~P | ~Q | P=Q"
    1.30  by blast
    1.31  
    1.32 +text{*Theorems for translation to combinators*}
    1.33 +
    1.34 +lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
    1.35 +apply (rule eq_reflection)
    1.36 +apply (rule ext) 
    1.37 +apply (simp add: COMBS_def) 
    1.38 +done
    1.39 +
    1.40 +lemma abs_I: "(%x. x) == COMBI"
    1.41 +apply (rule eq_reflection)
    1.42 +apply (rule ext) 
    1.43 +apply (simp add: COMBI_def) 
    1.44 +done
    1.45 +
    1.46 +lemma abs_K: "(%x. y) == COMBK y"
    1.47 +apply (rule eq_reflection)
    1.48 +apply (rule ext) 
    1.49 +apply (simp add: COMBK_def) 
    1.50 +done
    1.51 +
    1.52 +lemma abs_B: "(%x. a (g x)) == COMBB a g"
    1.53 +apply (rule eq_reflection)
    1.54 +apply (rule ext) 
    1.55 +apply (simp add: COMBB_def) 
    1.56 +done
    1.57 +
    1.58 +lemma abs_C: "(%x. (f x) b) == COMBC f b"
    1.59 +apply (rule eq_reflection)
    1.60 +apply (rule ext) 
    1.61 +apply (simp add: COMBC_def) 
    1.62 +done
    1.63 +
    1.64 +
    1.65  use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
    1.66 -use "Tools/res_hol_clause.ML"  --{*requires the combinators*}
    1.67 +use "Tools/res_hol_clause.ML"
    1.68  use "Tools/res_reconstruct.ML"
    1.69  use "Tools/watcher.ML"
    1.70  use "Tools/res_atp.ML"
    1.71 @@ -102,17 +117,14 @@
    1.72  oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
    1.73  
    1.74  use "Tools/res_atp_methods.ML"
    1.75 -setup ResAtpMethods.setup
    1.76 -
    1.77 +setup ResAtpMethods.setup      --{*Oracle ATP methods: still useful?*}
    1.78 +setup ResAxioms.setup          --{*Sledgehammer*}
    1.79  
    1.80  subsection {* The Metis prover *}
    1.81  
    1.82  use "Tools/metis_tools.ML"
    1.83  setup MetisTools.setup
    1.84  
    1.85 -(*Sledgehammer*)
    1.86 -setup ResAxioms.setup
    1.87 -
    1.88  setup {*
    1.89    Theory.at_end ResAxioms.clause_cache_endtheory
    1.90  *}
     2.1 --- a/src/HOL/MetisExamples/Abstraction.thy	Wed Oct 03 22:33:17 2007 +0200
     2.2 +++ b/src/HOL/MetisExamples/Abstraction.thy	Thu Oct 04 12:32:58 2007 +0200
     2.3 @@ -67,74 +67,107 @@
     2.4  by (meson CollectD SigmaD1 SigmaD2)
     2.5  
     2.6  
     2.7 +(*single-step*)
     2.8 +lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
     2.9 +by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def vimage_singleton_eq)
    2.10  
    2.11 -(*single-step*)
    2.12 +
    2.13  lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
    2.14  proof (neg_clausify)
    2.15 -assume 0: "(a, b) \<in> Sigma A (llabs_subgoal_1 f)"
    2.16 -assume 1: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)"
    2.17 -assume 2: "a \<notin> A \<or> a \<noteq> f b"
    2.18 -have 3: "a \<in> A"
    2.19 -  by (metis SigmaD1 0)
    2.20 -have 4: "f b \<noteq> a"
    2.21 -  by (metis 3 2)
    2.22 -have 5: "f b = a"
    2.23 -  by (metis Domain_Id Compl_UNIV_eq singleton_conv2 vimage_Collect_eq 1 vimage_singleton_eq SigmaD2 0)
    2.24 +assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type)
    2.25 +\<in> Sigma (A\<Colon>'a\<Colon>type set)
    2.26 +   (COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)))"
    2.27 +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)"
    2.28 +have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
    2.29 +  by (metis 0 SigmaD1)
    2.30 +have 3: "(b\<Colon>'b\<Colon>type)
    2.31 +\<in> COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)) (a\<Colon>'a\<Colon>type)"
    2.32 +  by (metis 0 SigmaD2) 
    2.33 +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))"
    2.34 +  by (metis 3)
    2.35 +have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)"
    2.36 +  by (metis 1 2)
    2.37 +have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)"
    2.38 +  by (metis 4 vimage_singleton_eq insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def)
    2.39  show "False"
    2.40 -  by (metis 5 4)
    2.41 -qed finish_clausify
    2.42 +  by (metis 5 6)
    2.43 +qed
    2.44 +
    2.45 +(*Alternative structured proof, untyped*)
    2.46 +lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
    2.47 +proof (neg_clausify)
    2.48 +assume 0: "(a, b) \<in> Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))"
    2.49 +have 1: "b \<in> Collect (COMBB (op = a) f)"
    2.50 +  by (metis 0 SigmaD2)
    2.51 +have 2: "f b = a"
    2.52 +  by (metis 1 vimage_Collect_eq singleton_conv2 insert_def union_empty2 vimage_singleton_eq vimage_def)
    2.53 +assume 3: "a \<notin> A \<or> a \<noteq> f b"
    2.54 +have 4: "a \<in> A"
    2.55 +  by (metis 0 SigmaD1)
    2.56 +have 5: "f b \<noteq> a"
    2.57 +  by (metis 4 3)
    2.58 +show "False"
    2.59 +  by (metis 5 2)
    2.60 +qed
    2.61  
    2.62  
    2.63  ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*}
    2.64  lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
    2.65 -apply (metis Collect_mem_eq SigmaD2);
    2.66 -done
    2.67 +by (metis Collect_mem_eq SigmaD2)
    2.68  
    2.69  lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
    2.70  proof (neg_clausify)
    2.71 -assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
    2.72 -   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set) cl =
    2.73 -   Collect (llabs_Set_XCollect_ex_eq_3 op \<in> (pset cl))"
    2.74 -assume 1: "(f\<Colon>'a\<Colon>type) \<notin> pset (cl\<Colon>'a\<Colon>type set)"
    2.75 -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)"
    2.76 -have 3: "llabs_Predicate_Xsup_Un_eq2_1 (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
    2.77 - (cl\<Colon>'a\<Colon>type set) (f\<Colon>'a\<Colon>type)"
    2.78 -  by (metis acc_def 2)
    2.79 -assume 4: "(CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set) =
    2.80 -Sigma (CL\<Colon>'a\<Colon>type set set) (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set)"
    2.81 +assume 0: "(cl, f) \<in> CLF"
    2.82 +assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \<in>) pset))"
    2.83 +assume 2: "f \<notin> pset cl"
    2.84 +have 3: "\<And>X1 X2. X2 \<in> COMBB Collect (COMBB (COMBC op \<in>) pset) X1 \<or> (X1, X2) \<notin> CLF"
    2.85 +  by (metis SigmaD2 1)
    2.86 +have 4: "\<And>X1 X2. X2 \<in> pset X1 \<or> (X1, X2) \<notin> CLF"
    2.87 +  by (metis 3 Collect_mem_eq)
    2.88 +have 5: "(cl, f) \<notin> CLF"
    2.89 +  by (metis 2 4)
    2.90  show "False"
    2.91 -  by (metis 1 Collect_mem_eq 0 3 4 acc_def SigmaD2)
    2.92 -qed finish_clausify (*ugly hack: combinators??*)
    2.93 +  by (metis 5 0)
    2.94 +qed
    2.95  
    2.96  ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}
    2.97  lemma
    2.98      "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
    2.99      f \<in> pset cl \<rightarrow> pset cl"
   2.100 -apply (metis Collect_mem_eq SigmaD2);
   2.101 -done
   2.102 +proof (neg_clausify)
   2.103 +assume 0: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
   2.104 +assume 1: "(cl, f)
   2.105 +\<in> Sigma CL
   2.106 +   (COMBB Collect
   2.107 +     (COMBB (COMBC op \<in>) (COMBS (COMBB Pi pset) (COMBB COMBK pset))))"
   2.108 +show "False"
   2.109 +(*  by (metis 0 Collect_mem_eq SigmaD2 1) ??doesn't terminate*)
   2.110 +  by (insert 0 1, simp add: COMBB_def COMBS_def COMBC_def)
   2.111 +qed
   2.112  
   2.113 -lemma
   2.114 -    "(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
   2.115 -    f \<in> pset cl \<rightarrow> pset cl"
   2.116 -proof (neg_clausify)
   2.117 -assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
   2.118 -   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set) cl =
   2.119 -   Collect
   2.120 -    (llabs_Set_XCollect_ex_eq_3 op \<in> (Pi (pset cl) (COMBK (pset cl))))"
   2.121 -assume 1: "(f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type) \<notin> Pi (pset (cl\<Colon>'a\<Colon>type set)) (COMBK (pset cl))"
   2.122 -assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type)
   2.123 -\<in> Sigma (CL\<Colon>'a\<Colon>type set set)
   2.124 -   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set)"
   2.125 -show "False"
   2.126 -  by (metis 1 Collect_mem_eq 0 SigmaD2 2)
   2.127 -qed finish_clausify
   2.128 -    (*Hack to prevent the "Additional hypotheses" error*)
   2.129  
   2.130  ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*}
   2.131  lemma
   2.132      "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   2.133     f \<in> pset cl \<inter> cl"
   2.134 -by (metis Collect_mem_eq SigmaD2)
   2.135 +proof (neg_clausify)
   2.136 +assume 0: "(cl, f)
   2.137 +\<in> Sigma CL
   2.138 +   (COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)))"
   2.139 +assume 1: "f \<notin> pset cl \<inter> cl"
   2.140 +have 2: "f \<in> COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)) cl" 
   2.141 +  by (insert 0, simp add: COMBB_def) 
   2.142 +(*  by (metis SigmaD2 0)  ??doesn't terminate*)
   2.143 +have 3: "f \<in> COMBS (COMBB op \<inter> pset) COMBI cl"
   2.144 +  by (metis 2 Collect_mem_eq)
   2.145 +have 4: "f \<notin> cl \<inter> pset cl"
   2.146 +  by (metis 1 Int_commute)
   2.147 +have 5: "f \<in> cl \<inter> pset cl"
   2.148 +  by (metis 3 Int_commute)
   2.149 +show "False"
   2.150 +  by (metis 5 4)
   2.151 +qed
   2.152 +
   2.153  
   2.154  ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}
   2.155  lemma
   2.156 @@ -146,28 +179,40 @@
   2.157  lemma "(cl,f) \<in> CLF ==> 
   2.158     CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   2.159     f \<in> pset cl \<inter> cl"
   2.160 +by auto
   2.161 +(*??no longer terminates, with combinators
   2.162  by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
   2.163    --{*@{text Int_def} is redundant}
   2.164 +*)
   2.165  
   2.166  ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
   2.167  lemma "(cl,f) \<in> CLF ==> 
   2.168     CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   2.169     f \<in> pset cl \<inter> cl"
   2.170 +by auto
   2.171 +(*??no longer terminates, with combinators
   2.172  by (metis Collect_mem_eq Int_commute SigmaD2)
   2.173 +*)
   2.174  
   2.175  ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}
   2.176  lemma 
   2.177     "(cl,f) \<in> CLF ==> 
   2.178      CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
   2.179      f \<in> pset cl \<rightarrow> pset cl"
   2.180 +by auto
   2.181 +(*??no longer terminates, with combinators
   2.182  by (metis Collect_mem_eq SigmaD2 subsetD)
   2.183 +*)
   2.184  
   2.185  ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}
   2.186  lemma 
   2.187    "(cl,f) \<in> CLF ==> 
   2.188     CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
   2.189     f \<in> pset cl \<rightarrow> pset cl"
   2.190 +by auto
   2.191 +(*??no longer terminates, with combinators
   2.192  by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
   2.193 +*)
   2.194  
   2.195  ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}
   2.196  lemma 
     3.1 --- a/src/HOL/MetisExamples/Tarski.thy	Wed Oct 03 22:33:17 2007 +0200
     3.2 +++ b/src/HOL/MetisExamples/Tarski.thy	Thu Oct 04 12:32:58 2007 +0200
     3.3 @@ -515,8 +515,11 @@
     3.4  apply (rule_tac t = "H" in ssubst, assumption)
     3.5  apply (rule CollectI)
     3.6  apply (rule conjI)
     3.7 -ML{*ResAtp.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*} 
     3.8 -apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE monotone_f reflD1 reflD2)
     3.9 +ML{*ResAtp.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*}
    3.10 +(*??no longer terminates, with combinators
    3.11 +apply (metis CO_refl lubH_le_flubH monotone_def monotone_f reflD1 reflD2) 
    3.12 +*)
    3.13 +apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE [OF monotone_f] reflD1 reflD2)
    3.14  apply (metis CO_refl lubH_le_flubH reflD2)
    3.15  done
    3.16    declare CLF.f_in_funcset[rule del] funcset_mem[rule del] 
    3.17 @@ -529,51 +532,73 @@
    3.18  ML{*ResAtp.problem_name:="Tarski__CLF_lubH_is_fixp"*}
    3.19  (*Single-step version fails. The conjecture clauses refer to local abstraction
    3.20  functions (Frees), which prevents expand_defs_tac from removing those 
    3.21 -"definitions" at the end of the proof. 
    3.22 +"definitions" at the end of the proof. *)
    3.23  lemma (in CLF) lubH_is_fixp:
    3.24       "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
    3.25  apply (simp add: fix_def)
    3.26  apply (rule conjI)
    3.27 - proof (neg_clausify)
    3.28 -assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)"
    3.29 -assume 1: "lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl \<notin> A"
    3.30 -have 2: "glb H (dual cl) \<notin> A"
    3.31 -  by (metis 0 1 lub_dual_glb)
    3.32 -have 3: "(glb H (dual cl), f (glb H (dual cl))) \<in> r"
    3.33 -  by (metis 0 lubH_le_flubH lub_dual_glb)
    3.34 -have 4: "(f (glb H (dual cl)), glb H (dual cl)) \<in> r"
    3.35 -  by (metis 0 flubH_le_lubH lub_dual_glb)
    3.36 -have 5: "glb H (dual cl) = f (glb H (dual cl)) \<or>
    3.37 -(glb H (dual cl), f (glb H (dual cl))) \<notin> r"
    3.38 -  by (metis 4 antisymE)
    3.39 -have 6: "glb H (dual cl) = f (glb H (dual cl))"
    3.40 -  by (metis 3 5)
    3.41 -have 7: "(glb H (dual cl), glb H (dual cl)) \<in> r"
    3.42 -  by (metis 4 6)
    3.43 -have 8: "\<And>X1. glb H (dual cl) \<in> X1 \<or> \<not> refl X1 r"
    3.44 -  by (metis reflD2 7)
    3.45 +proof (neg_clausify)
    3.46 +assume 0: "H =
    3.47 +Collect
    3.48 + (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
    3.49 +assume 1: "lub (Collect
    3.50 +      (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
    3.51 +        (COMBC op \<in> A)))
    3.52 + cl
    3.53 +\<notin> A"
    3.54 +have 2: "lub H cl \<notin> A"
    3.55 +  by (metis 1 0)
    3.56 +have 3: "(lub H cl, f (lub H cl)) \<in> r"
    3.57 +  by (metis lubH_le_flubH 0)
    3.58 +have 4: "(f (lub H cl), lub H cl) \<in> r"
    3.59 +  by (metis flubH_le_lubH 0)
    3.60 +have 5: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
    3.61 +  by (metis antisymE 4)
    3.62 +have 6: "lub H cl = f (lub H cl)"
    3.63 +  by (metis 5 3)
    3.64 +have 7: "(lub H cl, lub H cl) \<in> r"
    3.65 +  by (metis 6 4)
    3.66 +have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl X1 r"
    3.67 +  by (metis 7 reflD2)
    3.68  have 9: "\<not> refl A r"
    3.69 -  by (metis 2 8)
    3.70 +  by (metis 8 2)
    3.71  show "False"
    3.72 -  by (metis 9 CO_refl)
    3.73 -proof (neg_clausify)
    3.74 -assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)"
    3.75 -assume 1: "f (lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl) \<noteq>
    3.76 -lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl"
    3.77 -have 2: "(glb H (dual cl), f (glb H (dual cl))) \<in> r"
    3.78 -  by (metis 0 lubH_le_flubH lub_dual_glb lub_dual_glb)
    3.79 -have 3: "f (glb H (dual cl)) \<noteq> glb H (dual cl)"
    3.80 -  by (metis 0 1 lub_dual_glb)
    3.81 -have 4: "(f (glb H (dual cl)), glb H (dual cl)) \<in> r"
    3.82 -  by (metis lub_dual_glb flubH_le_lubH 0)
    3.83 -have 5: "f (glb H (dual cl)) = glb H (dual cl) \<or>
    3.84 -(f (glb H (dual cl)), glb H (dual cl)) \<notin> r"
    3.85 -  by (metis antisymE 2)
    3.86 -have 6: "f (glb H (dual cl)) = glb H (dual cl)"
    3.87 -  by (metis 5 4)
    3.88 -show "False"
    3.89 -  by (metis 3 6)
    3.90 -*)
    3.91 +  by (metis CO_refl 9);
    3.92 +next --{*apparently the way to insert a second structured proof*}
    3.93 +  show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow>
    3.94 +  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"
    3.95 +  proof (neg_clausify)
    3.96 +  assume 0: "H =
    3.97 +  Collect
    3.98 +   (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
    3.99 +  assume 1: "f (lub (Collect
   3.100 +	   (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
   3.101 +	     (COMBC op \<in> A)))
   3.102 +      cl) \<noteq>
   3.103 +  lub (Collect
   3.104 +	(COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
   3.105 +	  (COMBC op \<in> A)))
   3.106 +   cl"
   3.107 +  have 2: "f (lub H cl) \<noteq>
   3.108 +  lub (Collect
   3.109 +	(COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
   3.110 +	  (COMBC op \<in> A)))
   3.111 +   cl"
   3.112 +    by (metis 1 0)
   3.113 +  have 3: "f (lub H cl) \<noteq> lub H cl"
   3.114 +    by (metis 2 0)
   3.115 +  have 4: "(lub H cl, f (lub H cl)) \<in> r"
   3.116 +    by (metis lubH_le_flubH 0)
   3.117 +  have 5: "(f (lub H cl), lub H cl) \<in> r"
   3.118 +    by (metis flubH_le_lubH 0)
   3.119 +  have 6: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
   3.120 +    by (metis antisymE 5)
   3.121 +  have 7: "lub H cl = f (lub H cl)"
   3.122 +    by (metis 6 4)
   3.123 +  show "False"
   3.124 +    by (metis 3 7)
   3.125 +  qed
   3.126 +qed
   3.127  
   3.128  lemma (in CLF) lubH_is_fixp:
   3.129       "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
   3.130 @@ -616,9 +641,13 @@
   3.131  apply (rule lubI)
   3.132  ML{*ResAtp.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*}
   3.133  apply (metis P_def equalityE fix_subset subset_trans) 
   3.134 -apply (metis P_def fix_subset lubH_is_fixp set_mp subset_refl subset_trans)
   3.135 -apply (metis P_def fixf_le_lubH)
   3.136 -apply (metis P_def lubH_is_fixp)
   3.137 +apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def)
   3.138 +(*??no longer terminates, with combinators
   3.139 +apply (metis P_def fix_def fixf_le_lubH)
   3.140 +apply (metis P_def fix_def lubH_least_fixf)
   3.141 +*)
   3.142 +apply (simp add: fixf_le_lubH)
   3.143 +apply (simp add: lubH_least_fixf)
   3.144  done
   3.145    declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] 
   3.146            CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del]
   3.147 @@ -662,21 +691,18 @@
   3.148  ML{*ResAtp.problem_name:="Tarski__rel_imp_elem"*}
   3.149    declare (in CLF) CO_refl[simp] refl_def [simp]
   3.150  lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
   3.151 -apply (metis CO_refl reflD1)
   3.152 -done
   3.153 +by (metis CO_refl reflD1)
   3.154    declare (in CLF) CO_refl[simp del]  refl_def [simp del]
   3.155  
   3.156  ML{*ResAtp.problem_name:="Tarski__interval_subset"*}
   3.157    declare (in CLF) rel_imp_elem[intro] 
   3.158    declare interval_def [simp]
   3.159  lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
   3.160 -apply (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
   3.161 -done
   3.162 +by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
   3.163    declare (in CLF) rel_imp_elem[rule del] 
   3.164    declare interval_def [simp del]
   3.165  
   3.166  
   3.167 -
   3.168  lemma (in CLF) intervalI:
   3.169       "[| (a, x) \<in> r; (x, b) \<in> r |] ==> x \<in> interval r a b"
   3.170  by (simp add: interval_def)
   3.171 @@ -966,8 +992,7 @@
   3.172  
   3.173  ML{*ResAtp.problem_name:="Tarski__intY1_func"*}  (*ALL THEOREMS*)
   3.174  lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1" 
   3.175 -apply (metis intY1_f_closed restrict_in_funcset)
   3.176 -done
   3.177 +by (metis intY1_f_closed restrict_in_funcset)
   3.178  
   3.179  ML{*ResAtp.problem_name:="Tarski__intY1_mono"*}  (*ALL THEOREMS*)
   3.180  lemma (in Tarski) intY1_mono [skolem]:
     4.1 --- a/src/HOL/Tools/meson.ML	Wed Oct 03 22:33:17 2007 +0200
     4.2 +++ b/src/HOL/Tools/meson.ML	Thu Oct 04 12:32:58 2007 +0200
     4.3 @@ -17,6 +17,7 @@
     4.4    val first_order_resolve: thm -> thm -> thm
     4.5    val flexflex_first_order: thm -> thm
     4.6    val size_of_subgoals: thm -> int
     4.7 +  val too_many_clauses: term -> bool
     4.8    val make_cnf: thm list -> thm -> thm list
     4.9    val finish_cnf: thm list -> thm list
    4.10    val generalize: thm -> thm
     5.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Oct 03 22:33:17 2007 +0200
     5.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 04 12:32:58 2007 +0200
     5.3 @@ -290,7 +290,10 @@
     5.4                let val v = find_var x
     5.5                    val t = fol_term_to_hol_RAW ctxt y
     5.6                in  SOME (cterm_of thy v, t)  end
     5.7 -              handle Option => NONE (*List.find failed for the variable.*)
     5.8 +              handle Option => 
     5.9 +                  (Output.debug (fn() => "List.find failed for the variable " ^ x ^ 
    5.10 +                                         " in " ^ string_of_thm i_th); 
    5.11 +                   NONE) 
    5.12          fun remove_typeinst (a, t) =
    5.13                case Recon.strip_prefix ResClause.schematic_var_prefix a of
    5.14                    SOME b => SOME (b, t)
    5.15 @@ -446,11 +449,11 @@
    5.16    val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal");
    5.17    val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal");
    5.18  
    5.19 -  val comb_I  = ResHolClause.comb_I  RS meta_eq_to_obj_eq;
    5.20 -  val comb_K  = ResHolClause.comb_K  RS meta_eq_to_obj_eq;
    5.21 -  val comb_B  = ResHolClause.comb_B  RS meta_eq_to_obj_eq;
    5.22 -
    5.23 -  val ext_thm = cnf_th ResHolClause.ext;
    5.24 +  val comb_I = cnf_th ResHolClause.comb_I;
    5.25 +  val comb_K = cnf_th ResHolClause.comb_K;
    5.26 +  val comb_B = cnf_th ResHolClause.comb_B;
    5.27 +  val comb_C = cnf_th ResHolClause.comb_C;
    5.28 +  val comb_S = cnf_th ResHolClause.comb_S;
    5.29  
    5.30    fun dest_Arity (ResClause.ArityClause{premLits,...}) =
    5.31          map ResClause.class_of_arityLit premLits;
    5.32 @@ -509,10 +512,14 @@
    5.33          val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
    5.34          fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
    5.35          (*Now check for the existence of certain combinators*)
    5.36 -        val IK    = if used "c_COMBI" orelse used "c_COMBK" then [comb_I,comb_K] else []
    5.37 -        val BC    = if used "c_COMBB" then [comb_B] else []
    5.38 -        val EQ    = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
    5.39 -        val lmap' = if isFO then lmap else foldl (add_thm ctxt) lmap ([ext_thm] @ EQ @ IK @ BC)
    5.40 +        val thI  = if used "c_COMBI" then [comb_I] else []
    5.41 +        val thK  = if used "c_COMBK" then [comb_K] else []
    5.42 +        val thB   = if used "c_COMBB" then [comb_B] else []
    5.43 +        val thC   = if used "c_COMBC" then [comb_C] else []
    5.44 +        val thS   = if used "c_COMBS" then [comb_S] else []
    5.45 +        val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
    5.46 +        val lmap' = if isFO then lmap 
    5.47 +                    else foldl (add_thm ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
    5.48      in
    5.49          add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
    5.50      end;
     6.1 --- a/src/HOL/Tools/res_atp.ML	Wed Oct 03 22:33:17 2007 +0200
     6.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Oct 04 12:32:58 2007 +0200
     6.3 @@ -769,7 +769,7 @@
     6.4  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
     6.5  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
     6.6      let val conj_cls = Meson.make_clauses conjectures
     6.7 -                         |> ResAxioms.assume_abstract_list "subgoal" |> Meson.finish_cnf
     6.8 +                         |> map ResAxioms.combinators |> Meson.finish_cnf
     6.9          val hyp_cls = cnf_hyps_thms ctxt
    6.10          val goal_cls = conj_cls@hyp_cls
    6.11          val goal_tms = map prop_of goal_cls
     7.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Oct 03 22:33:17 2007 +0200
     7.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 04 12:32:58 2007 +0200
     7.3 @@ -15,7 +15,7 @@
     7.4    val cnf_rules_of_ths: thm list -> thm list
     7.5    val neg_clausify: thm list -> thm list
     7.6    val expand_defs_tac: thm -> tactic
     7.7 -  val assume_abstract_list: string -> thm list -> thm list
     7.8 +  val combinators: thm -> thm
     7.9    val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
    7.10    val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
    7.11    val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
    7.12 @@ -31,26 +31,6 @@
    7.13  (* FIXME legacy *)
    7.14  fun freeze_thm th = #1 (Drule.freeze_thaw th);
    7.15  
    7.16 -val lhs_of = #1 o Logic.dest_equals o Thm.prop_of;
    7.17 -val rhs_of = #2 o Logic.dest_equals o Thm.prop_of;
    7.18 -
    7.19 -
    7.20 -(*Store definitions of abstraction functions, ensuring that identical right-hand
    7.21 -  sides are denoted by the same functions and thereby reducing the need for
    7.22 -  extensionality in proofs.
    7.23 -  FIXME!  Store in theory data!!*)
    7.24 -
    7.25 -(*Populate the abstraction cache with common combinators.*)
    7.26 -fun seed th net =
    7.27 -  let val (_,ct) = Thm.dest_abs NONE (Thm.rhs_of th)
    7.28 -      val t = Logic.legacy_varify (term_of ct)
    7.29 -  in  Net.insert_term Thm.eq_thm (t, th) net end;
    7.30 -
    7.31 -val abstraction_cache = ref
    7.32 -      (seed (thm"ATP_Linkup.I_simp")
    7.33 -       (seed (thm"ATP_Linkup.B_simp")
    7.34 -        (seed (thm"ATP_Linkup.K_simp") Net.empty)));
    7.35 -
    7.36  
    7.37  (**** Transformation of Elimination Rules into First-Order Formulas****)
    7.38  
    7.39 @@ -149,7 +129,7 @@
    7.40    in  dec_sko (prop_of th) []  end;
    7.41  
    7.42  
    7.43 -(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****)
    7.44 +(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    7.45  
    7.46  (*Returns the vars of a theorem*)
    7.47  fun vars_of_thm th =
    7.48 @@ -175,201 +155,98 @@
    7.49                strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
    7.50          | _ => th;
    7.51  
    7.52 -(*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
    7.53 -  where some types have the empty sort.*)
    7.54 -val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
    7.55 -fun mk_object_eq th = th RS meta_eq_to_obj_eq
    7.56 -    handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
    7.57 -
    7.58 -(*Apply a function definition to an argument, beta-reducing the result.*)
    7.59 -fun beta_comb cf x =
    7.60 -  let val th1 = combination cf (reflexive x)
    7.61 -      val th2 = beta_conversion false (Thm.rhs_of th1)
    7.62 -  in  transitive th1 th2  end;
    7.63 -
    7.64 -(*Apply a function definition to arguments, beta-reducing along the way.*)
    7.65 -fun list_combination cf [] = cf
    7.66 -  | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs;
    7.67 -
    7.68 -fun list_cabs ([] ,     t) = t
    7.69 -  | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
    7.70 -
    7.71  fun assert_eta_free ct =
    7.72    let val t = term_of ct
    7.73    in if (t aconv Envir.eta_contract t) then ()
    7.74       else error ("Eta redex in term: " ^ string_of_cterm ct)
    7.75    end;
    7.76  
    7.77 -fun eq_absdef (th1, th2) =
    7.78 -    Context.joinable (theory_of_thm th1, theory_of_thm th2)  andalso
    7.79 -    rhs_of th1 aconv rhs_of th2;
    7.80 -
    7.81  val lambda_free = not o Term.has_abs;
    7.82  
    7.83  val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
    7.84  
    7.85 -fun dest_abs_list ct =
    7.86 -  let val (cv,ct') = Thm.dest_abs NONE ct
    7.87 -      val (cvs,cu) = dest_abs_list ct'
    7.88 -  in (cv::cvs, cu) end
    7.89 -  handle CTERM _ => ([],ct);
    7.90 +val abs_S = @{thm"abs_S"};
    7.91 +val abs_K = @{thm"abs_K"};
    7.92 +val abs_I = @{thm"abs_I"};
    7.93 +val abs_B = @{thm"abs_B"};
    7.94 +val abs_C = @{thm"abs_C"};
    7.95  
    7.96 -fun abstract_rule_list [] [] th = th
    7.97 -  | abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th)
    7.98 -  | abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]);
    7.99 -
   7.100 -
   7.101 -val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
   7.102 +val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B));
   7.103 +val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C));
   7.104 +val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S));
   7.105  
   7.106 -(*Does an existing abstraction definition have an RHS that matches the one we need now?
   7.107 -  thy is the current theory, which must extend that of theorem th.*)
   7.108 -fun match_rhs thy t th =
   7.109 -  let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
   7.110 -                                   " against\n" ^ string_of_thm th);
   7.111 -      val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
   7.112 -      val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
   7.113 -      val ct_pairs = if subthy (theory_of_thm th, thy) andalso
   7.114 -                        forall lambda_free (map #2 term_insts)
   7.115 -                     then map (pairself (cterm_of thy)) term_insts
   7.116 -                     else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*)
   7.117 -      fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
   7.118 -      val th' = cterm_instantiate ct_pairs th
   7.119 -  in  SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th')  end
   7.120 -  handle _ => NONE;
   7.121 +(*FIXME: requires more use of cterm constructors*)
   7.122 +fun abstract ct =
   7.123 +  let val Abs(x,_,body) = term_of ct
   7.124 +      val thy = theory_of_cterm ct
   7.125 +      val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
   7.126 +      val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
   7.127 +      fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K
   7.128 +  in
   7.129 +      case body of
   7.130 +          Const _ => makeK()
   7.131 +        | Free _ => makeK()
   7.132 +        | Var _ => makeK()  (*though Var isn't expected*)
   7.133 +        | Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*)
   7.134 +        | rator$rand =>
   7.135 +	    if loose_bvar1 (rator,0) then (*C or S*) 
   7.136 +	       if loose_bvar1 (rand,0) then (*S*)
   7.137 +	         let val crator = cterm_of thy (Abs(x,xT,rator))
   7.138 +	             val crand = cterm_of thy (Abs(x,xT,rand))
   7.139 +	             val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S
   7.140 +	             val (_,rhs) = Thm.dest_equals (cprop_of abs_S') 
   7.141 +	         in
   7.142 +	           Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
   7.143 +	         end
   7.144 +	       else (*C*)
   7.145 +	         let val crator = cterm_of thy (Abs(x,xT,rator))
   7.146 +	             val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C
   7.147 +	             val (_,rhs) = Thm.dest_equals (cprop_of abs_C') 
   7.148 +	         in
   7.149 +	           Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
   7.150 +	         end
   7.151 +	    else if loose_bvar1 (rand,0) then (*B or eta*) 
   7.152 +	       if rand = Bound 0 then eta_conversion ct
   7.153 +	       else (*B*)
   7.154 +	         let val crand = cterm_of thy (Abs(x,xT,rand))
   7.155 +	             val abs_B' = cterm_instantiate [(f_B, cterm_of thy rator),(g_B,crand)] abs_B
   7.156 +	             val (_,rhs) = Thm.dest_equals (cprop_of abs_B') 
   7.157 +	         in
   7.158 +	           Thm.transitive abs_B' (Conv.arg_conv abstract rhs)
   7.159 +	         end
   7.160 +	    else makeK()
   7.161 +        | _ => error "abstract: Bad term"
   7.162 +  end;
   7.163  
   7.164  (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
   7.165    prefix for the constants. Resulting theory is returned in the first theorem. *)
   7.166 -fun declare_absfuns s th =
   7.167 -  let val nref = ref 0
   7.168 -      fun abstract thy ct =
   7.169 -        if lambda_free (term_of ct) then (transfer thy (reflexive ct), [])
   7.170 -        else
   7.171 -        case term_of ct of
   7.172 -          Abs _ =>
   7.173 -            let val cname = "llabs_" ^ s ^ "_" ^ Int.toString (inc nref)
   7.174 -                val _ = assert_eta_free ct;
   7.175 -                val (cvs,cta) = dest_abs_list ct
   7.176 -                val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
   7.177 -                val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta);
   7.178 -                val (u'_th,defs) = abstract thy cta
   7.179 -                val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th);
   7.180 -                val cu' = Thm.rhs_of u'_th
   7.181 -                val u' = term_of cu'
   7.182 -                val abs_v_u = fold_rev (lambda o term_of) cvs u'
   7.183 -                (*get the formal parameters: ALL variables free in the term*)
   7.184 -                val args = term_frees abs_v_u
   7.185 -                val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments");
   7.186 -                val rhs = list_abs_free (map dest_Free args, abs_v_u)
   7.187 -                      (*Forms a lambda-abstraction over the formal parameters*)
   7.188 -                val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu');
   7.189 -                val thy = theory_of_thm u'_th
   7.190 -                val (ax,ax',thy) =
   7.191 -                 case List.mapPartial (match_rhs thy abs_v_u)
   7.192 -                         (Net.match_term (!abstraction_cache) u') of
   7.193 -                     (ax,ax')::_ =>
   7.194 -                       (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
   7.195 -                        (ax,ax',thy))
   7.196 -                   | [] =>
   7.197 -                      let val _ = Output.debug (fn()=>"Lookup was empty");
   7.198 -                          val Ts = map type_of args
   7.199 -                          val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
   7.200 -                          val c = Const (Sign.full_name thy cname, cT)
   7.201 -                          val thy =
   7.202 -                            Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy
   7.203 -                                     (*Theory is augmented with the constant,
   7.204 -                                       then its definition*)
   7.205 -                          val cdef = cname ^ "_def"
   7.206 -                          val thy = Theory.add_defs_i true false
   7.207 -                                       [(cdef, equals cT $ c $ rhs)] thy
   7.208 -                                    handle ERROR _ => raise Clausify_failure thy
   7.209 -                          val ax = Thm.get_axiom_i thy (Sign.full_name thy cdef)
   7.210 -                                     |> Drule.unvarify
   7.211 -                                     |> mk_object_eq |> strip_lambdas (length args)
   7.212 -                                     |> mk_meta_eq |> Meson.generalize
   7.213 -                          val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
   7.214 -                          val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^
   7.215 -                                                       "Instance: " ^ string_of_thm ax');
   7.216 -                          val _ = abstraction_cache := Net.insert_term eq_absdef
   7.217 -                                            ((Logic.varify u'), ax) (!abstraction_cache)
   7.218 -                            handle Net.INSERT =>
   7.219 -                              raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
   7.220 -                       in  (ax,ax',thy)  end
   7.221 -            in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
   7.222 -               (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
   7.223 -        | (t1$t2) =>
   7.224 -            let val (ct1,ct2) = Thm.dest_comb ct
   7.225 -                val (th1,defs1) = abstract thy ct1
   7.226 -                val (th2,defs2) = abstract (theory_of_thm th1) ct2
   7.227 -            in  (combination th1 th2, defs1@defs2)  end
   7.228 -      val _ = Output.debug (fn()=>"declare_absfuns, Abstracting: " ^ string_of_thm th);
   7.229 -      val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
   7.230 -      val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   7.231 -      val _ = Output.debug (fn()=>"declare_absfuns, Result: " ^ string_of_thm (hd ths));
   7.232 -  in  (theory_of_thm eqth, map Drule.eta_contraction_rule ths)  end;
   7.233 -
   7.234 -fun name_of def = try (#1 o dest_Free o lhs_of) def;
   7.235 -
   7.236 -(*A name is valid provided it isn't the name of a defined abstraction.*)
   7.237 -fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
   7.238 -  | valid_name defs _ = false;
   7.239 -
   7.240 -(*s is the theorem name (hint) or the word "subgoal"*)
   7.241 -fun assume_absfuns s th =
   7.242 -  let val thy = theory_of_thm th
   7.243 -      val cterm = cterm_of thy
   7.244 -      val abs_count = ref 0
   7.245 -      fun abstract ct =
   7.246 -        if lambda_free (term_of ct) then (reflexive ct, [])
   7.247 -        else
   7.248 -        case term_of ct of
   7.249 -          Abs (_,T,u) =>
   7.250 -            let val _ = assert_eta_free ct;
   7.251 -                val (cvs,cta) = dest_abs_list ct
   7.252 -                val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
   7.253 -                val (u'_th,defs) = abstract cta
   7.254 -                val cu' = Thm.rhs_of u'_th
   7.255 -                val u' = term_of cu'
   7.256 -                (*Could use Thm.cabs instead of lambda to work at level of cterms*)
   7.257 -                val abs_v_u = fold_rev (lambda o term_of) cvs (term_of cu')
   7.258 -                (*get the formal parameters: free variables not present in the defs
   7.259 -                  (to avoid taking abstraction function names as parameters) *)
   7.260 -                val args = filter (valid_name defs) (term_frees abs_v_u)
   7.261 -                val crhs = list_cabs (map cterm args, cterm abs_v_u)
   7.262 -                      (*Forms a lambda-abstraction over the formal parameters*)
   7.263 -                val rhs = term_of crhs
   7.264 -                val (ax,ax') =
   7.265 -                 case List.mapPartial (match_rhs thy abs_v_u)
   7.266 -                        (Net.match_term (!abstraction_cache) u') of
   7.267 -                     (ax,ax')::_ =>
   7.268 -                       (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
   7.269 -                        (ax,ax'))
   7.270 -                   | [] =>
   7.271 -                      let val Ts = map type_of args
   7.272 -                          val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
   7.273 -                          val id = "llabs_" ^ s ^ "_" ^ Int.toString (inc abs_count)
   7.274 -                          val c = Free (id, const_ty)
   7.275 -                          val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
   7.276 -                                     |> mk_object_eq |> strip_lambdas (length args)
   7.277 -                                     |> mk_meta_eq |> Meson.generalize
   7.278 -                          val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
   7.279 -                          val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax)
   7.280 -                                    (!abstraction_cache)
   7.281 -                            handle Net.INSERT =>
   7.282 -                              raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
   7.283 -                      in (ax,ax') end
   7.284 -            in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
   7.285 -               (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
   7.286 -        | (t1$t2) =>
   7.287 -            let val (ct1,ct2) = Thm.dest_comb ct
   7.288 -                val (t1',defs1) = abstract ct1
   7.289 -                val (t2',defs2) = abstract ct2
   7.290 -            in  (combination t1' t2', defs1@defs2)  end
   7.291 -      val _ = Output.debug (fn()=>"assume_absfuns, Abstracting: " ^ string_of_thm th);
   7.292 -      val (eqth,defs) = abstract (cprop_of th)
   7.293 -      val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   7.294 -      val _ = Output.debug (fn()=>"assume_absfuns, Result: " ^ string_of_thm (hd ths));
   7.295 -  in  map Drule.eta_contraction_rule ths  end;
   7.296 -
   7.297 +fun combinators_aux ct =
   7.298 +  if lambda_free (term_of ct) then reflexive ct
   7.299 +  else
   7.300 +  case term_of ct of
   7.301 +      Abs _ =>
   7.302 +	let val _ = assert_eta_free ct;
   7.303 +	    val (cv,cta) = Thm.dest_abs NONE ct
   7.304 +	    val (v,Tv) = (dest_Free o term_of) cv
   7.305 +	    val _ = Output.debug (fn()=>"  recursion: " ^ string_of_cterm cta);
   7.306 +	    val u_th = combinators_aux cta
   7.307 +	    val _ = Output.debug (fn()=>"  returned " ^ string_of_thm u_th);
   7.308 +	    val cu = Thm.rhs_of u_th
   7.309 +	    val comb_eq = abstract (Thm.cabs cv cu)
   7.310 +	in Output.debug (fn()=>"  abstraction result: " ^ string_of_thm comb_eq);
   7.311 +	   (transitive (abstract_rule v cv u_th) comb_eq) end
   7.312 +    | t1 $ t2 =>
   7.313 +	let val (ct1,ct2) = Thm.dest_comb ct
   7.314 +	in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
   7.315 +            
   7.316 +fun combinators th =
   7.317 +  if lambda_free (prop_of th) then th 
   7.318 +  else
   7.319 +    let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ string_of_thm th);
   7.320 +	val th = Drule.eta_contraction_rule th
   7.321 +	val eqth = combinators_aux (cprop_of th)
   7.322 +	val _ = Output.debug (fn()=>"Conversion result: " ^ string_of_thm eqth);
   7.323 +    in  equal_elim eqth th   end;
   7.324  
   7.325  (*cterms are used throughout for efficiency*)
   7.326  val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
   7.327 @@ -430,27 +307,6 @@
   7.328        [] => ()
   7.329      | ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths'));
   7.330  
   7.331 -fun assume_abstract s th =
   7.332 -  if lambda_free (prop_of th) then [th]
   7.333 -  else th |> Drule.eta_contraction_rule |> assume_absfuns s
   7.334 -          |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
   7.335 -
   7.336 -(*Replace lambdas by assumed function definitions in the theorems*)
   7.337 -fun assume_abstract_list s ths = List.concat (map (assume_abstract s) ths);
   7.338 -
   7.339 -(*Replace lambdas by declared function definitions in the theorems*)
   7.340 -fun declare_abstract s (thy, []) = (thy, [])
   7.341 -  | declare_abstract s (thy, th::ths) =
   7.342 -      let val (thy', th_defs) =
   7.343 -            if lambda_free (prop_of th) then (thy, [th])
   7.344 -            else
   7.345 -                th |> zero_var_indexes |> freeze_thm
   7.346 -                   |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns s
   7.347 -                handle Clausify_failure thy_e => (thy_e,[])
   7.348 -          val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
   7.349 -          val (thy'', ths') = declare_abstract (s^"'") (thy', ths)
   7.350 -      in  (thy'', th_defs @ ths')  end;
   7.351 -
   7.352  (*Keep the full complexity of the original name*)
   7.353  fun flatten_name s = space_implode "_X" (NameSpace.explode s);
   7.354  
   7.355 @@ -465,7 +321,7 @@
   7.356  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   7.357  fun skolem_thm th =
   7.358    let val nnfth = to_nnf th and s = fake_name th
   7.359 -  in  Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |> assume_abstract_list s |> Meson.finish_cnf
   7.360 +  in  Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |>  map combinators |> Meson.finish_cnf
   7.361    end
   7.362    handle THM _ => [];
   7.363  
   7.364 @@ -480,8 +336,8 @@
   7.365                val (thy',defs) = declare_skofuns s nnfth thy
   7.366                val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
   7.367                val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
   7.368 -              val (thy'',cnfs') = declare_abstract s (thy',cnfs)
   7.369 -          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') end
   7.370 +              val cnfs' = map combinators cnfs
   7.371 +          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy') end
   7.372            handle Clausify_failure thy_e => ([],thy_e)
   7.373          )
   7.374        (try to_nnf th);
   7.375 @@ -575,8 +431,26 @@
   7.376  
   7.377  val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
   7.378  
   7.379 +val max_lambda_nesting = 3;
   7.380 +     
   7.381 +fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k)
   7.382 +  | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1)
   7.383 +  | excessive_lambdas _ = false;
   7.384 +
   7.385 +fun is_formula_type T = (T = HOLogic.boolT orelse T = propT);
   7.386 +
   7.387 +(*Don't count nested lambdas at the level of formulas, as they are quantifiers*)
   7.388 +fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t
   7.389 +  | excessive_lambdas_fm Ts t =
   7.390 +      if is_formula_type (fastype_of1 (Ts, t))
   7.391 +      then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t))
   7.392 +      else excessive_lambdas (t, max_lambda_nesting);
   7.393 +
   7.394 +fun too_complex t = 
   7.395 +  Meson.too_many_clauses t orelse excessive_lambdas_fm [] t;
   7.396 +  
   7.397  fun skolem_cache th thy =
   7.398 -  if PureThy.is_internal th then thy
   7.399 +  if PureThy.is_internal th orelse too_complex (prop_of th) then thy
   7.400    else #2 (skolem_cache_thm th thy);
   7.401  
   7.402  val skolem_cache_theorems_of = Symtab.fold (fold skolem_cache o snd) o #2 o PureThy.theorems_of;
   7.403 @@ -598,7 +472,7 @@
   7.404  fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);
   7.405  
   7.406  (*Expand all new*definitions of abstraction or Skolem functions in a proof state.*)
   7.407 -fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
   7.408 +fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a
   7.409    | is_absko _ = false;
   7.410  
   7.411  fun is_okdef xs (Const ("==", _) $ t $ u) =   (*Definition of Free, not in certain terms*)
   7.412 @@ -607,7 +481,7 @@
   7.413  
   7.414  (*This function tries to cope with open locales, which introduce hypotheses of the form
   7.415    Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
   7.416 -  of llabs_ and sko_ functions. *)
   7.417 +  of sko_ functions. *)
   7.418  fun expand_defs_tac st0 st =
   7.419    let val hyps0 = #hyps (rep_thm st0)
   7.420        val hyps = #hyps (crep_thm st)
   7.421 @@ -652,7 +526,7 @@
   7.422  val no_tvars = null o term_tvars o prop_of;
   7.423  
   7.424  val neg_clausify =
   7.425 -  filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o Meson.make_clauses;
   7.426 +  filter no_tvars o Meson.finish_cnf o map combinators o Meson.make_clauses;
   7.427  
   7.428  fun neg_conjecture_clauses st0 n =
   7.429    let val st = Seq.hd (neg_skolemize_tac n st0)