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 -
2.8 (*single-step*)
2.9 lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
2.10 +by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def vimage_singleton_eq)
2.11 +
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 +val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B));
7.100 +val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C));
7.101 +val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S));
7.102
7.103 -
7.104 -val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
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)