--- a/src/HOL/MetisExamples/Abstraction.thy Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/MetisExamples/Abstraction.thy Thu Oct 04 12:32:58 2007 +0200
@@ -67,74 +67,107 @@
by (meson CollectD SigmaD1 SigmaD2)
+(*single-step*)
+lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
+by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def vimage_singleton_eq)
-(*single-step*)
+
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
proof (neg_clausify)
-assume 0: "(a, b) \<in> Sigma A (llabs_subgoal_1 f)"
-assume 1: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)"
-assume 2: "a \<notin> A \<or> a \<noteq> f b"
-have 3: "a \<in> A"
- by (metis SigmaD1 0)
-have 4: "f b \<noteq> a"
- by (metis 3 2)
-have 5: "f b = a"
- by (metis Domain_Id Compl_UNIV_eq singleton_conv2 vimage_Collect_eq 1 vimage_singleton_eq SigmaD2 0)
+assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type)
+\<in> Sigma (A\<Colon>'a\<Colon>type set)
+ (COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)))"
+assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> a \<noteq> (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type)"
+have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
+ by (metis 0 SigmaD1)
+have 3: "(b\<Colon>'b\<Colon>type)
+\<in> COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)) (a\<Colon>'a\<Colon>type)"
+ by (metis 0 SigmaD2)
+have 4: "(b\<Colon>'b\<Colon>type) \<in> Collect (COMBB (op = (a\<Colon>'a\<Colon>type)) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type))"
+ by (metis 3)
+have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)"
+ by (metis 1 2)
+have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)"
+ by (metis 4 vimage_singleton_eq insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def)
show "False"
- by (metis 5 4)
-qed finish_clausify
+ by (metis 5 6)
+qed
+
+(*Alternative structured proof, untyped*)
+lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
+proof (neg_clausify)
+assume 0: "(a, b) \<in> Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))"
+have 1: "b \<in> Collect (COMBB (op = a) f)"
+ by (metis 0 SigmaD2)
+have 2: "f b = a"
+ by (metis 1 vimage_Collect_eq singleton_conv2 insert_def union_empty2 vimage_singleton_eq vimage_def)
+assume 3: "a \<notin> A \<or> a \<noteq> f b"
+have 4: "a \<in> A"
+ by (metis 0 SigmaD1)
+have 5: "f b \<noteq> a"
+ by (metis 4 3)
+show "False"
+ by (metis 5 2)
+qed
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*}
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
-apply (metis Collect_mem_eq SigmaD2);
-done
+by (metis Collect_mem_eq SigmaD2)
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
proof (neg_clausify)
-assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
- (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set) cl =
- Collect (llabs_Set_XCollect_ex_eq_3 op \<in> (pset cl))"
-assume 1: "(f\<Colon>'a\<Colon>type) \<notin> pset (cl\<Colon>'a\<Colon>type set)"
-assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type) \<in> (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)"
-have 3: "llabs_Predicate_Xsup_Un_eq2_1 (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
- (cl\<Colon>'a\<Colon>type set) (f\<Colon>'a\<Colon>type)"
- by (metis acc_def 2)
-assume 4: "(CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set) =
-Sigma (CL\<Colon>'a\<Colon>type set set) (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set)"
+assume 0: "(cl, f) \<in> CLF"
+assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \<in>) pset))"
+assume 2: "f \<notin> pset cl"
+have 3: "\<And>X1 X2. X2 \<in> COMBB Collect (COMBB (COMBC op \<in>) pset) X1 \<or> (X1, X2) \<notin> CLF"
+ by (metis SigmaD2 1)
+have 4: "\<And>X1 X2. X2 \<in> pset X1 \<or> (X1, X2) \<notin> CLF"
+ by (metis 3 Collect_mem_eq)
+have 5: "(cl, f) \<notin> CLF"
+ by (metis 2 4)
show "False"
- by (metis 1 Collect_mem_eq 0 3 4 acc_def SigmaD2)
-qed finish_clausify (*ugly hack: combinators??*)
+ by (metis 5 0)
+qed
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}
lemma
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
f \<in> pset cl \<rightarrow> pset cl"
-apply (metis Collect_mem_eq SigmaD2);
-done
+proof (neg_clausify)
+assume 0: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
+assume 1: "(cl, f)
+\<in> Sigma CL
+ (COMBB Collect
+ (COMBB (COMBC op \<in>) (COMBS (COMBB Pi pset) (COMBB COMBK pset))))"
+show "False"
+(* by (metis 0 Collect_mem_eq SigmaD2 1) ??doesn't terminate*)
+ by (insert 0 1, simp add: COMBB_def COMBS_def COMBC_def)
+qed
-lemma
- "(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
- f \<in> pset cl \<rightarrow> pset cl"
-proof (neg_clausify)
-assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
- (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set) cl =
- Collect
- (llabs_Set_XCollect_ex_eq_3 op \<in> (Pi (pset cl) (COMBK (pset cl))))"
-assume 1: "(f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type) \<notin> Pi (pset (cl\<Colon>'a\<Colon>type set)) (COMBK (pset cl))"
-assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type)
-\<in> Sigma (CL\<Colon>'a\<Colon>type set set)
- (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set)"
-show "False"
- by (metis 1 Collect_mem_eq 0 SigmaD2 2)
-qed finish_clausify
- (*Hack to prevent the "Additional hypotheses" error*)
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*}
lemma
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
f \<in> pset cl \<inter> cl"
-by (metis Collect_mem_eq SigmaD2)
+proof (neg_clausify)
+assume 0: "(cl, f)
+\<in> Sigma CL
+ (COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)))"
+assume 1: "f \<notin> pset cl \<inter> cl"
+have 2: "f \<in> COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)) cl"
+ by (insert 0, simp add: COMBB_def)
+(* by (metis SigmaD2 0) ??doesn't terminate*)
+have 3: "f \<in> COMBS (COMBB op \<inter> pset) COMBI cl"
+ by (metis 2 Collect_mem_eq)
+have 4: "f \<notin> cl \<inter> pset cl"
+ by (metis 1 Int_commute)
+have 5: "f \<in> cl \<inter> pset cl"
+ by (metis 3 Int_commute)
+show "False"
+ by (metis 5 4)
+qed
+
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}
lemma
@@ -146,28 +179,40 @@
lemma "(cl,f) \<in> CLF ==>
CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
f \<in> pset cl \<inter> cl"
+by auto
+(*??no longer terminates, with combinators
by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
--{*@{text Int_def} is redundant}
+*)
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
lemma "(cl,f) \<in> CLF ==>
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
f \<in> pset cl \<inter> cl"
+by auto
+(*??no longer terminates, with combinators
by (metis Collect_mem_eq Int_commute SigmaD2)
+*)
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}
lemma
"(cl,f) \<in> CLF ==>
CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==>
f \<in> pset cl \<rightarrow> pset cl"
+by auto
+(*??no longer terminates, with combinators
by (metis Collect_mem_eq SigmaD2 subsetD)
+*)
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}
lemma
"(cl,f) \<in> CLF ==>
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
f \<in> pset cl \<rightarrow> pset cl"
+by auto
+(*??no longer terminates, with combinators
by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
+*)
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}
lemma
--- a/src/HOL/MetisExamples/Tarski.thy Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/MetisExamples/Tarski.thy Thu Oct 04 12:32:58 2007 +0200
@@ -515,8 +515,11 @@
apply (rule_tac t = "H" in ssubst, assumption)
apply (rule CollectI)
apply (rule conjI)
-ML{*ResAtp.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*}
-apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE monotone_f reflD1 reflD2)
+ML{*ResAtp.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*}
+(*??no longer terminates, with combinators
+apply (metis CO_refl lubH_le_flubH monotone_def monotone_f reflD1 reflD2)
+*)
+apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE [OF monotone_f] reflD1 reflD2)
apply (metis CO_refl lubH_le_flubH reflD2)
done
declare CLF.f_in_funcset[rule del] funcset_mem[rule del]
@@ -529,51 +532,73 @@
ML{*ResAtp.problem_name:="Tarski__CLF_lubH_is_fixp"*}
(*Single-step version fails. The conjecture clauses refer to local abstraction
functions (Frees), which prevents expand_defs_tac from removing those
-"definitions" at the end of the proof.
+"definitions" at the end of the proof. *)
lemma (in CLF) lubH_is_fixp:
"H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
apply (simp add: fix_def)
apply (rule conjI)
- proof (neg_clausify)
-assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)"
-assume 1: "lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl \<notin> A"
-have 2: "glb H (dual cl) \<notin> A"
- by (metis 0 1 lub_dual_glb)
-have 3: "(glb H (dual cl), f (glb H (dual cl))) \<in> r"
- by (metis 0 lubH_le_flubH lub_dual_glb)
-have 4: "(f (glb H (dual cl)), glb H (dual cl)) \<in> r"
- by (metis 0 flubH_le_lubH lub_dual_glb)
-have 5: "glb H (dual cl) = f (glb H (dual cl)) \<or>
-(glb H (dual cl), f (glb H (dual cl))) \<notin> r"
- by (metis 4 antisymE)
-have 6: "glb H (dual cl) = f (glb H (dual cl))"
- by (metis 3 5)
-have 7: "(glb H (dual cl), glb H (dual cl)) \<in> r"
- by (metis 4 6)
-have 8: "\<And>X1. glb H (dual cl) \<in> X1 \<or> \<not> refl X1 r"
- by (metis reflD2 7)
+proof (neg_clausify)
+assume 0: "H =
+Collect
+ (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
+assume 1: "lub (Collect
+ (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
+ (COMBC op \<in> A)))
+ cl
+\<notin> A"
+have 2: "lub H cl \<notin> A"
+ by (metis 1 0)
+have 3: "(lub H cl, f (lub H cl)) \<in> r"
+ by (metis lubH_le_flubH 0)
+have 4: "(f (lub H cl), lub H cl) \<in> r"
+ by (metis flubH_le_lubH 0)
+have 5: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
+ by (metis antisymE 4)
+have 6: "lub H cl = f (lub H cl)"
+ by (metis 5 3)
+have 7: "(lub H cl, lub H cl) \<in> r"
+ by (metis 6 4)
+have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl X1 r"
+ by (metis 7 reflD2)
have 9: "\<not> refl A r"
- by (metis 2 8)
+ by (metis 8 2)
show "False"
- by (metis 9 CO_refl)
-proof (neg_clausify)
-assume 0: "H = Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)"
-assume 1: "f (lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl) \<noteq>
-lub (Collect (llabs_local_Xcl_A_r_f_P_XlubH_le_flubH_1 A f r)) cl"
-have 2: "(glb H (dual cl), f (glb H (dual cl))) \<in> r"
- by (metis 0 lubH_le_flubH lub_dual_glb lub_dual_glb)
-have 3: "f (glb H (dual cl)) \<noteq> glb H (dual cl)"
- by (metis 0 1 lub_dual_glb)
-have 4: "(f (glb H (dual cl)), glb H (dual cl)) \<in> r"
- by (metis lub_dual_glb flubH_le_lubH 0)
-have 5: "f (glb H (dual cl)) = glb H (dual cl) \<or>
-(f (glb H (dual cl)), glb H (dual cl)) \<notin> r"
- by (metis antisymE 2)
-have 6: "f (glb H (dual cl)) = glb H (dual cl)"
- by (metis 5 4)
-show "False"
- by (metis 3 6)
-*)
+ by (metis CO_refl 9);
+next --{*apparently the way to insert a second structured proof*}
+ show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow>
+ f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) = lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
+ proof (neg_clausify)
+ assume 0: "H =
+ Collect
+ (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
+ assume 1: "f (lub (Collect
+ (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
+ (COMBC op \<in> A)))
+ cl) \<noteq>
+ lub (Collect
+ (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
+ (COMBC op \<in> A)))
+ cl"
+ have 2: "f (lub H cl) \<noteq>
+ lub (Collect
+ (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
+ (COMBC op \<in> A)))
+ cl"
+ by (metis 1 0)
+ have 3: "f (lub H cl) \<noteq> lub H cl"
+ by (metis 2 0)
+ have 4: "(lub H cl, f (lub H cl)) \<in> r"
+ by (metis lubH_le_flubH 0)
+ have 5: "(f (lub H cl), lub H cl) \<in> r"
+ by (metis flubH_le_lubH 0)
+ have 6: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
+ by (metis antisymE 5)
+ have 7: "lub H cl = f (lub H cl)"
+ by (metis 6 4)
+ show "False"
+ by (metis 3 7)
+ qed
+qed
lemma (in CLF) lubH_is_fixp:
"H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
@@ -616,9 +641,13 @@
apply (rule lubI)
ML{*ResAtp.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*}
apply (metis P_def equalityE fix_subset subset_trans)
-apply (metis P_def fix_subset lubH_is_fixp set_mp subset_refl subset_trans)
-apply (metis P_def fixf_le_lubH)
-apply (metis P_def lubH_is_fixp)
+apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def)
+(*??no longer terminates, with combinators
+apply (metis P_def fix_def fixf_le_lubH)
+apply (metis P_def fix_def lubH_least_fixf)
+*)
+apply (simp add: fixf_le_lubH)
+apply (simp add: lubH_least_fixf)
done
declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del]
CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del]
@@ -662,21 +691,18 @@
ML{*ResAtp.problem_name:="Tarski__rel_imp_elem"*}
declare (in CLF) CO_refl[simp] refl_def [simp]
lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
-apply (metis CO_refl reflD1)
-done
+by (metis CO_refl reflD1)
declare (in CLF) CO_refl[simp del] refl_def [simp del]
ML{*ResAtp.problem_name:="Tarski__interval_subset"*}
declare (in CLF) rel_imp_elem[intro]
declare interval_def [simp]
lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
-apply (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
-done
+by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
declare (in CLF) rel_imp_elem[rule del]
declare interval_def [simp del]
-
lemma (in CLF) intervalI:
"[| (a, x) \<in> r; (x, b) \<in> r |] ==> x \<in> interval r a b"
by (simp add: interval_def)
@@ -966,8 +992,7 @@
ML{*ResAtp.problem_name:="Tarski__intY1_func"*} (*ALL THEOREMS*)
lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
-apply (metis intY1_f_closed restrict_in_funcset)
-done
+by (metis intY1_f_closed restrict_in_funcset)
ML{*ResAtp.problem_name:="Tarski__intY1_mono"*} (*ALL THEOREMS*)
lemma (in Tarski) intY1_mono [skolem]:
--- a/src/HOL/Tools/res_axioms.ML Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Thu Oct 04 12:32:58 2007 +0200
@@ -15,7 +15,7 @@
val cnf_rules_of_ths: thm list -> thm list
val neg_clausify: thm list -> thm list
val expand_defs_tac: thm -> tactic
- val assume_abstract_list: string -> thm list -> thm list
+ val combinators: thm -> thm
val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
@@ -31,26 +31,6 @@
(* FIXME legacy *)
fun freeze_thm th = #1 (Drule.freeze_thaw th);
-val lhs_of = #1 o Logic.dest_equals o Thm.prop_of;
-val rhs_of = #2 o Logic.dest_equals o Thm.prop_of;
-
-
-(*Store definitions of abstraction functions, ensuring that identical right-hand
- sides are denoted by the same functions and thereby reducing the need for
- extensionality in proofs.
- FIXME! Store in theory data!!*)
-
-(*Populate the abstraction cache with common combinators.*)
-fun seed th net =
- let val (_,ct) = Thm.dest_abs NONE (Thm.rhs_of th)
- val t = Logic.legacy_varify (term_of ct)
- in Net.insert_term Thm.eq_thm (t, th) net end;
-
-val abstraction_cache = ref
- (seed (thm"ATP_Linkup.I_simp")
- (seed (thm"ATP_Linkup.B_simp")
- (seed (thm"ATP_Linkup.K_simp") Net.empty)));
-
(**** Transformation of Elimination Rules into First-Order Formulas****)
@@ -149,7 +129,7 @@
in dec_sko (prop_of th) [] end;
-(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****)
+(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
(*Returns the vars of a theorem*)
fun vars_of_thm th =
@@ -175,201 +155,98 @@
strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
| _ => th;
-(*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
- where some types have the empty sort.*)
-val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
-fun mk_object_eq th = th RS meta_eq_to_obj_eq
- handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
-
-(*Apply a function definition to an argument, beta-reducing the result.*)
-fun beta_comb cf x =
- let val th1 = combination cf (reflexive x)
- val th2 = beta_conversion false (Thm.rhs_of th1)
- in transitive th1 th2 end;
-
-(*Apply a function definition to arguments, beta-reducing along the way.*)
-fun list_combination cf [] = cf
- | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs;
-
-fun list_cabs ([] , t) = t
- | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
-
fun assert_eta_free ct =
let val t = term_of ct
in if (t aconv Envir.eta_contract t) then ()
else error ("Eta redex in term: " ^ string_of_cterm ct)
end;
-fun eq_absdef (th1, th2) =
- Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso
- rhs_of th1 aconv rhs_of th2;
-
val lambda_free = not o Term.has_abs;
val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
-fun dest_abs_list ct =
- let val (cv,ct') = Thm.dest_abs NONE ct
- val (cvs,cu) = dest_abs_list ct'
- in (cv::cvs, cu) end
- handle CTERM _ => ([],ct);
+val abs_S = @{thm"abs_S"};
+val abs_K = @{thm"abs_K"};
+val abs_I = @{thm"abs_I"};
+val abs_B = @{thm"abs_B"};
+val abs_C = @{thm"abs_C"};
-fun abstract_rule_list [] [] th = th
- | abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th)
- | abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]);
-
-
-val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
+val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B));
+val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C));
+val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S));
-(*Does an existing abstraction definition have an RHS that matches the one we need now?
- thy is the current theory, which must extend that of theorem th.*)
-fun match_rhs thy t th =
- let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
- " against\n" ^ string_of_thm th);
- val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
- val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
- val ct_pairs = if subthy (theory_of_thm th, thy) andalso
- forall lambda_free (map #2 term_insts)
- then map (pairself (cterm_of thy)) term_insts
- else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*)
- fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
- val th' = cterm_instantiate ct_pairs th
- in SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th') end
- handle _ => NONE;
+(*FIXME: requires more use of cterm constructors*)
+fun abstract ct =
+ let val Abs(x,_,body) = term_of ct
+ val thy = theory_of_cterm ct
+ val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
+ val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
+ fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K
+ in
+ case body of
+ Const _ => makeK()
+ | Free _ => makeK()
+ | Var _ => makeK() (*though Var isn't expected*)
+ | Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*)
+ | rator$rand =>
+ if loose_bvar1 (rator,0) then (*C or S*)
+ if loose_bvar1 (rand,0) then (*S*)
+ let val crator = cterm_of thy (Abs(x,xT,rator))
+ val crand = cterm_of thy (Abs(x,xT,rand))
+ val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
+ in
+ Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
+ end
+ else (*C*)
+ let val crator = cterm_of thy (Abs(x,xT,rator))
+ val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
+ in
+ Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
+ end
+ else if loose_bvar1 (rand,0) then (*B or eta*)
+ if rand = Bound 0 then eta_conversion ct
+ else (*B*)
+ let val crand = cterm_of thy (Abs(x,xT,rand))
+ val abs_B' = cterm_instantiate [(f_B, cterm_of thy rator),(g_B,crand)] abs_B
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
+ in
+ Thm.transitive abs_B' (Conv.arg_conv abstract rhs)
+ end
+ else makeK()
+ | _ => error "abstract: Bad term"
+ end;
(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
prefix for the constants. Resulting theory is returned in the first theorem. *)
-fun declare_absfuns s th =
- let val nref = ref 0
- fun abstract thy ct =
- if lambda_free (term_of ct) then (transfer thy (reflexive ct), [])
- else
- case term_of ct of
- Abs _ =>
- let val cname = "llabs_" ^ s ^ "_" ^ Int.toString (inc nref)
- val _ = assert_eta_free ct;
- val (cvs,cta) = dest_abs_list ct
- val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
- val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta);
- val (u'_th,defs) = abstract thy cta
- val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th);
- val cu' = Thm.rhs_of u'_th
- val u' = term_of cu'
- val abs_v_u = fold_rev (lambda o term_of) cvs u'
- (*get the formal parameters: ALL variables free in the term*)
- val args = term_frees abs_v_u
- val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments");
- val rhs = list_abs_free (map dest_Free args, abs_v_u)
- (*Forms a lambda-abstraction over the formal parameters*)
- val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu');
- val thy = theory_of_thm u'_th
- val (ax,ax',thy) =
- case List.mapPartial (match_rhs thy abs_v_u)
- (Net.match_term (!abstraction_cache) u') of
- (ax,ax')::_ =>
- (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
- (ax,ax',thy))
- | [] =>
- let val _ = Output.debug (fn()=>"Lookup was empty");
- val Ts = map type_of args
- val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
- val c = Const (Sign.full_name thy cname, cT)
- val thy =
- Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy
- (*Theory is augmented with the constant,
- then its definition*)
- val cdef = cname ^ "_def"
- val thy = Theory.add_defs_i true false
- [(cdef, equals cT $ c $ rhs)] thy
- handle ERROR _ => raise Clausify_failure thy
- val ax = Thm.get_axiom_i thy (Sign.full_name thy cdef)
- |> Drule.unvarify
- |> mk_object_eq |> strip_lambdas (length args)
- |> mk_meta_eq |> Meson.generalize
- val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
- val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^
- "Instance: " ^ string_of_thm ax');
- val _ = abstraction_cache := Net.insert_term eq_absdef
- ((Logic.varify u'), ax) (!abstraction_cache)
- handle Net.INSERT =>
- raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
- in (ax,ax',thy) end
- in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
- (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
- | (t1$t2) =>
- let val (ct1,ct2) = Thm.dest_comb ct
- val (th1,defs1) = abstract thy ct1
- val (th2,defs2) = abstract (theory_of_thm th1) ct2
- in (combination th1 th2, defs1@defs2) end
- val _ = Output.debug (fn()=>"declare_absfuns, Abstracting: " ^ string_of_thm th);
- val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
- val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
- val _ = Output.debug (fn()=>"declare_absfuns, Result: " ^ string_of_thm (hd ths));
- in (theory_of_thm eqth, map Drule.eta_contraction_rule ths) end;
-
-fun name_of def = try (#1 o dest_Free o lhs_of) def;
-
-(*A name is valid provided it isn't the name of a defined abstraction.*)
-fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
- | valid_name defs _ = false;
-
-(*s is the theorem name (hint) or the word "subgoal"*)
-fun assume_absfuns s th =
- let val thy = theory_of_thm th
- val cterm = cterm_of thy
- val abs_count = ref 0
- fun abstract ct =
- if lambda_free (term_of ct) then (reflexive ct, [])
- else
- case term_of ct of
- Abs (_,T,u) =>
- let val _ = assert_eta_free ct;
- val (cvs,cta) = dest_abs_list ct
- val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
- val (u'_th,defs) = abstract cta
- val cu' = Thm.rhs_of u'_th
- val u' = term_of cu'
- (*Could use Thm.cabs instead of lambda to work at level of cterms*)
- val abs_v_u = fold_rev (lambda o term_of) cvs (term_of cu')
- (*get the formal parameters: free variables not present in the defs
- (to avoid taking abstraction function names as parameters) *)
- val args = filter (valid_name defs) (term_frees abs_v_u)
- val crhs = list_cabs (map cterm args, cterm abs_v_u)
- (*Forms a lambda-abstraction over the formal parameters*)
- val rhs = term_of crhs
- val (ax,ax') =
- case List.mapPartial (match_rhs thy abs_v_u)
- (Net.match_term (!abstraction_cache) u') of
- (ax,ax')::_ =>
- (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
- (ax,ax'))
- | [] =>
- let val Ts = map type_of args
- val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
- val id = "llabs_" ^ s ^ "_" ^ Int.toString (inc abs_count)
- val c = Free (id, const_ty)
- val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
- |> mk_object_eq |> strip_lambdas (length args)
- |> mk_meta_eq |> Meson.generalize
- val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
- val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax)
- (!abstraction_cache)
- handle Net.INSERT =>
- raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
- in (ax,ax') end
- in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
- (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
- | (t1$t2) =>
- let val (ct1,ct2) = Thm.dest_comb ct
- val (t1',defs1) = abstract ct1
- val (t2',defs2) = abstract ct2
- in (combination t1' t2', defs1@defs2) end
- val _ = Output.debug (fn()=>"assume_absfuns, Abstracting: " ^ string_of_thm th);
- val (eqth,defs) = abstract (cprop_of th)
- val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
- val _ = Output.debug (fn()=>"assume_absfuns, Result: " ^ string_of_thm (hd ths));
- in map Drule.eta_contraction_rule ths end;
-
+fun combinators_aux ct =
+ if lambda_free (term_of ct) then reflexive ct
+ else
+ case term_of ct of
+ Abs _ =>
+ let val _ = assert_eta_free ct;
+ val (cv,cta) = Thm.dest_abs NONE ct
+ val (v,Tv) = (dest_Free o term_of) cv
+ val _ = Output.debug (fn()=>" recursion: " ^ string_of_cterm cta);
+ val u_th = combinators_aux cta
+ val _ = Output.debug (fn()=>" returned " ^ string_of_thm u_th);
+ val cu = Thm.rhs_of u_th
+ val comb_eq = abstract (Thm.cabs cv cu)
+ in Output.debug (fn()=>" abstraction result: " ^ string_of_thm comb_eq);
+ (transitive (abstract_rule v cv u_th) comb_eq) end
+ | t1 $ t2 =>
+ let val (ct1,ct2) = Thm.dest_comb ct
+ in combination (combinators_aux ct1) (combinators_aux ct2) end;
+
+fun combinators th =
+ if lambda_free (prop_of th) then th
+ else
+ let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ string_of_thm th);
+ val th = Drule.eta_contraction_rule th
+ val eqth = combinators_aux (cprop_of th)
+ val _ = Output.debug (fn()=>"Conversion result: " ^ string_of_thm eqth);
+ in equal_elim eqth th end;
(*cterms are used throughout for efficiency*)
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
@@ -430,27 +307,6 @@
[] => ()
| ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths'));
-fun assume_abstract s th =
- if lambda_free (prop_of th) then [th]
- else th |> Drule.eta_contraction_rule |> assume_absfuns s
- |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
-
-(*Replace lambdas by assumed function definitions in the theorems*)
-fun assume_abstract_list s ths = List.concat (map (assume_abstract s) ths);
-
-(*Replace lambdas by declared function definitions in the theorems*)
-fun declare_abstract s (thy, []) = (thy, [])
- | declare_abstract s (thy, th::ths) =
- let val (thy', th_defs) =
- if lambda_free (prop_of th) then (thy, [th])
- else
- th |> zero_var_indexes |> freeze_thm
- |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns s
- handle Clausify_failure thy_e => (thy_e,[])
- val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
- val (thy'', ths') = declare_abstract (s^"'") (thy', ths)
- in (thy'', th_defs @ ths') end;
-
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (NameSpace.explode s);
@@ -465,7 +321,7 @@
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
fun skolem_thm th =
let val nnfth = to_nnf th and s = fake_name th
- in Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |> assume_abstract_list s |> Meson.finish_cnf
+ in Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |> map combinators |> Meson.finish_cnf
end
handle THM _ => [];
@@ -480,8 +336,8 @@
val (thy',defs) = declare_skofuns s nnfth thy
val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
- val (thy'',cnfs') = declare_abstract s (thy',cnfs)
- in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') end
+ val cnfs' = map combinators cnfs
+ in (map Goal.close_result (Meson.finish_cnf cnfs'), thy') end
handle Clausify_failure thy_e => ([],thy_e)
)
(try to_nnf th);
@@ -575,8 +431,26 @@
val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
+val max_lambda_nesting = 3;
+
+fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k)
+ | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1)
+ | excessive_lambdas _ = false;
+
+fun is_formula_type T = (T = HOLogic.boolT orelse T = propT);
+
+(*Don't count nested lambdas at the level of formulas, as they are quantifiers*)
+fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t
+ | excessive_lambdas_fm Ts t =
+ if is_formula_type (fastype_of1 (Ts, t))
+ then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t))
+ else excessive_lambdas (t, max_lambda_nesting);
+
+fun too_complex t =
+ Meson.too_many_clauses t orelse excessive_lambdas_fm [] t;
+
fun skolem_cache th thy =
- if PureThy.is_internal th then thy
+ if PureThy.is_internal th orelse too_complex (prop_of th) then thy
else #2 (skolem_cache_thm th thy);
val skolem_cache_theorems_of = Symtab.fold (fold skolem_cache o snd) o #2 o PureThy.theorems_of;
@@ -598,7 +472,7 @@
fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);
(*Expand all new*definitions of abstraction or Skolem functions in a proof state.*)
-fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
+fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a
| is_absko _ = false;
fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*)
@@ -607,7 +481,7 @@
(*This function tries to cope with open locales, which introduce hypotheses of the form
Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
- of llabs_ and sko_ functions. *)
+ of sko_ functions. *)
fun expand_defs_tac st0 st =
let val hyps0 = #hyps (rep_thm st0)
val hyps = #hyps (crep_thm st)
@@ -652,7 +526,7 @@
val no_tvars = null o term_tvars o prop_of;
val neg_clausify =
- filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o Meson.make_clauses;
+ filter no_tvars o Meson.finish_cnf o map combinators o Meson.make_clauses;
fun neg_conjecture_clauses st0 n =
let val st = Seq.hd (neg_skolemize_tac n st0)