--- a/NEWS Wed Apr 28 16:56:51 2010 +0200
+++ b/NEWS Wed Apr 28 17:29:58 2010 +0200
@@ -84,6 +84,8 @@
*** Pure ***
+* Empty class specifications observe default sort. INCOMPATIBILITY.
+
* Old 'axclass' has been discontinued. Use 'class' instead. INCOMPATIBILITY.
* Code generator: simple concept for abstract datatypes obeying invariants.
--- a/etc/isar-keywords.el Wed Apr 28 16:56:51 2010 +0200
+++ b/etc/isar-keywords.el Wed Apr 28 17:29:58 2010 +0200
@@ -61,6 +61,7 @@
"code_modulename"
"code_monad"
"code_pred"
+ "code_reflect"
"code_reserved"
"code_thms"
"code_type"
@@ -288,10 +289,12 @@
"congs"
"constrains"
"contains"
+ "datatypes"
"defines"
"file"
"fixes"
"for"
+ "functions"
"hide_action"
"hints"
"identifier"
@@ -466,6 +469,7 @@
"code_module"
"code_modulename"
"code_monad"
+ "code_reflect"
"code_reserved"
"code_type"
"coinductive"
--- a/src/HOL/Metis_Examples/BT.thy Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy Wed Apr 28 17:29:58 2010 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/MetisTest/BT.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
Testing the metis method
*)
@@ -10,7 +11,6 @@
imports Main
begin
-
datatype 'a bt =
Lf
| Br 'a "'a bt" "'a bt"
@@ -66,178 +66,223 @@
text {* \medskip BT simplification *}
declare [[ atp_problem_prefix = "BT__n_leaves_reflect" ]]
+
lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
- apply (induct t)
- apply (metis add_right_cancel n_leaves.simps(1) reflect.simps(1))
- apply (metis add_commute n_leaves.simps(2) reflect.simps(2))
- done
+proof (induct t)
+ case Lf thus ?case
+ proof -
+ let "?p\<^isub>1 x\<^isub>1" = "x\<^isub>1 \<noteq> n_leaves (reflect (Lf::'a bt))"
+ have "\<not> ?p\<^isub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1))
+ hence "\<not> ?p\<^isub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1))
+ thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis
+ qed
+next
+ case (Br a t1 t2) thus ?case
+ by (metis n_leaves.simps(2) nat_add_commute reflect.simps(2))
+qed
declare [[ atp_problem_prefix = "BT__n_nodes_reflect" ]]
+
lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
- apply (induct t)
- apply (metis reflect.simps(1))
- apply (metis n_nodes.simps(2) nat_add_commute reflect.simps(2))
- done
+proof (induct t)
+ case Lf thus ?case by (metis reflect.simps(1))
+next
+ case (Br a t1 t2) thus ?case
+ by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
+qed
declare [[ atp_problem_prefix = "BT__depth_reflect" ]]
+
lemma depth_reflect: "depth (reflect t) = depth t"
- apply (induct t)
- apply (metis depth.simps(1) reflect.simps(1))
- apply (metis depth.simps(2) min_max.sup_commute reflect.simps(2))
- done
+apply (induct t)
+ apply (metis depth.simps(1) reflect.simps(1))
+by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2))
text {*
- The famous relationship between the numbers of leaves and nodes.
+The famous relationship between the numbers of leaves and nodes.
*}
declare [[ atp_problem_prefix = "BT__n_leaves_nodes" ]]
+
lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
- apply (induct t)
- apply (metis n_leaves.simps(1) n_nodes.simps(1))
- apply auto
- done
+apply (induct t)
+ apply (metis n_leaves.simps(1) n_nodes.simps(1))
+by auto
declare [[ atp_problem_prefix = "BT__reflect_reflect_ident" ]]
+
lemma reflect_reflect_ident: "reflect (reflect t) = t"
- apply (induct t)
- apply (metis add_right_cancel reflect.simps(1));
- apply (metis reflect.simps(2))
- done
+apply (induct t)
+ apply (metis reflect.simps(1))
+proof -
+ fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt"
+ assume A1: "reflect (reflect t1) = t1"
+ assume A2: "reflect (reflect t2) = t2"
+ have "\<And>V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)"
+ using A1 by (metis reflect.simps(2))
+ hence "\<And>V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))"
+ by (metis reflect.simps(2))
+ hence "\<And>U. reflect (reflect (Br U t1 t2)) = Br U t1 t2"
+ using A2 by metis
+ thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast
+qed
declare [[ atp_problem_prefix = "BT__bt_map_ident" ]]
+
lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
apply (rule ext)
apply (induct_tac y)
- apply (metis bt_map.simps(1))
-txt{*BUG involving flex-flex pairs*}
-(* apply (metis bt_map.simps(2)) *)
-apply auto
-done
-
+ apply (metis bt_map.simps(1))
+by (metis COMBI_def bt_map.simps(2))
declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]]
+
lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)"
apply (induct t)
- apply (metis appnd.simps(1) bt_map.simps(1))
- apply (metis appnd.simps(2) bt_map.simps(2)) (*slow!!*)
-done
-
+ apply (metis appnd.simps(1) bt_map.simps(1))
+by (metis appnd.simps(2) bt_map.simps(2))
declare [[ atp_problem_prefix = "BT__bt_map_compose" ]]
+
lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
-apply (induct t)
- apply (metis bt_map.simps(1))
-txt{*Metis runs forever*}
-(* apply (metis bt_map.simps(2) o_apply)*)
-apply auto
-done
-
+apply (induct t)
+ apply (metis bt_map.simps(1))
+by (metis bt_map.simps(2) o_eq_dest_lhs)
declare [[ atp_problem_prefix = "BT__bt_map_reflect" ]]
+
lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
- apply (induct t)
- apply (metis add_right_cancel bt_map.simps(1) reflect.simps(1))
- apply (metis add_right_cancel bt_map.simps(2) reflect.simps(2))
- done
+apply (induct t)
+ apply (metis bt_map.simps(1) reflect.simps(1))
+by (metis bt_map.simps(2) reflect.simps(2))
declare [[ atp_problem_prefix = "BT__preorder_bt_map" ]]
+
lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
- apply (induct t)
- apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
- apply simp
- done
+apply (induct t)
+ apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
+by simp
declare [[ atp_problem_prefix = "BT__inorder_bt_map" ]]
+
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
- apply (induct t)
- apply (metis bt_map.simps(1) inorder.simps(1) map.simps(1))
- apply simp
- done
+proof (induct t)
+ case Lf thus ?case
+ proof -
+ have "map f [] = []" by (metis map.simps(1))
+ hence "map f [] = inorder Lf" by (metis inorder.simps(1))
+ hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1))
+ thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1))
+ qed
+next
+ case (Br a t1 t2) thus ?case by simp
+qed
declare [[ atp_problem_prefix = "BT__postorder_bt_map" ]]
+
lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
- apply (induct t)
- apply (metis bt_map.simps(1) map.simps(1) postorder.simps(1))
- apply simp
- done
+apply (induct t)
+ apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1))
+by simp
declare [[ atp_problem_prefix = "BT__depth_bt_map" ]]
+
lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
- apply (induct t)
- apply (metis bt_map.simps(1) depth.simps(1))
- apply simp
- done
+apply (induct t)
+ apply (metis bt_map.simps(1) depth.simps(1))
+by simp
declare [[ atp_problem_prefix = "BT__n_leaves_bt_map" ]]
+
lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
- apply (induct t)
- apply (metis One_nat_def Suc_eq_plus1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
- apply (metis bt_map.simps(2) n_leaves.simps(2))
- done
-
+apply (induct t)
+ apply (metis bt_map.simps(1) n_leaves.simps(1))
+proof -
+ fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt"
+ assume A1: "n_leaves (bt_map f t1) = n_leaves t1"
+ assume A2: "n_leaves (bt_map f t2) = n_leaves t2"
+ have "\<And>V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V"
+ using A1 by (metis n_leaves.simps(2))
+ hence "\<And>V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)"
+ by (metis bt_map.simps(2))
+ hence F1: "\<And>U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2"
+ using A2 by metis
+ have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)"
+ by (metis n_leaves.simps(2))
+ thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)"
+ using F1 by metis
+qed
declare [[ atp_problem_prefix = "BT__preorder_reflect" ]]
+
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
- apply (induct t)
- apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
- apply (metis append_Nil Cons_eq_append_conv postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident)
- done
+apply (induct t)
+ apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
+ reflect.simps(1))
+by (metis append.simps(1) append.simps(2) postorder.simps(2) preorder.simps(2)
+ reflect.simps(2) rev.simps(2) rev_append rev_swap)
declare [[ atp_problem_prefix = "BT__inorder_reflect" ]]
+
lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
- apply (induct t)
- apply (metis inorder.simps(1) reflect.simps(1) rev.simps(1))
- apply simp
- done
+apply (induct t)
+ apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1))
+by simp
+(* Slow:
+by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2)
+ reflect.simps(2) rev.simps(2) rev_append)
+*)
declare [[ atp_problem_prefix = "BT__postorder_reflect" ]]
+
lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
- apply (induct t)
- apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1))
- apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append self_append_conv2)
- done
+apply (induct t)
+ apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
+ reflect.simps(1))
+by (metis preorder_reflect reflect_reflect_ident rev_swap)
text {*
- Analogues of the standard properties of the append function for lists.
+Analogues of the standard properties of the append function for lists.
*}
declare [[ atp_problem_prefix = "BT__appnd_assoc" ]]
-lemma appnd_assoc [simp]:
- "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
- apply (induct t1)
- apply (metis appnd.simps(1))
- apply (metis appnd.simps(2))
- done
+
+lemma appnd_assoc [simp]: "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
+apply (induct t1)
+ apply (metis appnd.simps(1))
+by (metis appnd.simps(2))
declare [[ atp_problem_prefix = "BT__appnd_Lf2" ]]
+
lemma appnd_Lf2 [simp]: "appnd t Lf = t"
- apply (induct t)
- apply (metis appnd.simps(1))
- apply (metis appnd.simps(2))
- done
+apply (induct t)
+ apply (metis appnd.simps(1))
+by (metis appnd.simps(2))
+
+declare max_add_distrib_left [simp]
declare [[ atp_problem_prefix = "BT__depth_appnd" ]]
- declare max_add_distrib_left [simp]
+
lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
- apply (induct t1)
- apply (metis add_0 appnd.simps(1) depth.simps(1))
-apply (simp add: );
- done
+apply (induct t1)
+ apply (metis appnd.simps(1) depth.simps(1) plus_nat.simps(1))
+by simp
declare [[ atp_problem_prefix = "BT__n_leaves_appnd" ]]
+
lemma n_leaves_appnd [simp]:
"n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
- apply (induct t1)
- apply (metis One_nat_def appnd.simps(1) less_irrefl less_linear n_leaves.simps(1) nat_mult_1)
- apply (simp add: left_distrib)
- done
+apply (induct t1)
+ apply (metis appnd.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
+ semiring_norm(111))
+by (simp add: left_distrib)
declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]]
+
lemma (*bt_map_appnd:*)
"bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
- apply (induct t1)
- apply (metis appnd.simps(1) bt_map_appnd)
- apply (metis bt_map_appnd)
- done
+apply (induct t1)
+ apply (metis appnd.simps(1) bt_map.simps(1))
+by (metis bt_map_appnd)
end
--- a/src/HOL/Metis_Examples/BigO.thy Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Wed Apr 28 17:29:58 2010 +0200
@@ -206,8 +206,6 @@
qed
-sledgehammer_params [sorts]
-
lemma bigo_alt_def: "O(f) =
{h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
by (auto simp add: bigo_def bigo_pos_const)
--- a/src/HOL/Metis_Examples/TransClosure.thy Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Metis_Examples/TransClosure.thy Wed Apr 28 17:29:58 2010 +0200
@@ -17,45 +17,45 @@
| Intg int -- "integer value"
| Addr addr -- "addresses of objects in the heap"
-consts R::"(addr \<times> addr) set"
-
-consts f:: "addr \<Rightarrow> val"
+consts R :: "(addr \<times> addr) set"
-declare [[ atp_problem_prefix = "TransClosure__test" ]]
-lemma "\<lbrakk> f c = Intg x; \<forall> y. f b = Intg y \<longrightarrow> y \<noteq> x; (a,b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>* \<rbrakk>
- \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
-by (metis Transitive_Closure.rtrancl_into_rtrancl converse_rtranclE trancl_reflcl)
+consts f :: "addr \<Rightarrow> val"
-lemma "\<lbrakk> f c = Intg x; \<forall> y. f b = Intg y \<longrightarrow> y \<noteq> x; (a,b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>* \<rbrakk>
- \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
-proof (neg_clausify)
-assume 0: "f c = Intg x"
-assume 1: "(a, b) \<in> R\<^sup>*"
-assume 2: "(b, c) \<in> R\<^sup>*"
-assume 3: "f b \<noteq> Intg x"
-assume 4: "\<And>A. (b, A) \<notin> R \<or> (a, A) \<notin> R\<^sup>*"
-have 5: "b = c \<or> b \<in> Domain R"
- by (metis Not_Domain_rtrancl 2)
-have 6: "\<And>X1. (a, X1) \<in> R\<^sup>* \<or> (b, X1) \<notin> R"
- by (metis Transitive_Closure.rtrancl_into_rtrancl 1)
-have 7: "\<And>X1. (b, X1) \<notin> R"
- by (metis 6 4)
-have 8: "b \<notin> Domain R"
- by (metis 7 DomainE)
-have 9: "c = b"
- by (metis 5 8)
-have 10: "f b = Intg x"
- by (metis 0 9)
-show "False"
- by (metis 10 3)
+lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
+ \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
+sledgehammer
+proof -
+ assume A1: "f c = Intg x"
+ assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
+ assume A3: "(a, b) \<in> R\<^sup>*"
+ assume A4: "(b, c) \<in> R\<^sup>*"
+ have F1: "f c \<noteq> f b" using A2 A1 by metis
+ have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
+ have F3: "\<exists>x. (b, x R b c) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
+ have "c \<noteq> b" using F1 by metis
+ hence "\<exists>u. (b, u) \<in> R" using F3 by metis
+ thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
qed
-declare [[ atp_problem_prefix = "TransClosure__test_simpler" ]]
-lemma "\<lbrakk> f c = Intg x; \<forall> y. f b = Intg y \<longrightarrow> y \<noteq> x; (a,b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>* \<rbrakk>
- \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
-apply (erule_tac x="b" in converse_rtranclE)
-apply (metis rel_pow_0_E rel_pow_0_I)
-apply (metis DomainE Domain_iff Transitive_Closure.rtrancl_into_rtrancl)
-done
+lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
+ \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
+(* sledgehammer [isar_proof, shrink_factor = 2] *)
+proof -
+ assume A1: "f c = Intg x"
+ assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
+ assume A3: "(a, b) \<in> R\<^sup>*"
+ assume A4: "(b, c) \<in> R\<^sup>*"
+ have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
+ hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
+ have "b \<noteq> c" using A1 A2 by metis
+ hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
+ thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
+qed
+
+lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
+ \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
+apply (erule_tac x = b in converse_rtranclE)
+ apply metis
+by (metis transitive_closure_trans(6))
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Apr 28 17:29:58 2010 +0200
@@ -377,6 +377,8 @@
end
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
open Sledgehammer_Fact_Minimizer
@@ -390,7 +392,7 @@
|> the_default 5
val params = default_params thy
[("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
- val minimize = minimize_theorems params 1
+ val minimize = minimize_theorems params 1 (subgoal_count st)
val _ = log separator
in
case minimize st (these (!named_thms)) of
--- a/src/HOL/Quotient_Examples/FSet.thy Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Wed Apr 28 17:29:58 2010 +0200
@@ -1,11 +1,12 @@
-(* Title: Quotient.thy
- Author: Cezary Kaliszyk
- Author: Christian Urban
+(* Title: HOL/Quotient_Examples/Quotient.thy
+ Author: Cezary Kaliszyk, TU Munich
+ Author: Christian Urban, TU Munich
- provides a reasoning infrastructure for the type of finite sets
+A reasoning infrastructure for the type of finite sets.
*)
+
theory FSet
-imports Quotient Quotient_List List
+imports Quotient_List
begin
text {* Definiton of List relation and the quotient type *}
@@ -80,9 +81,9 @@
lemma compose_list_refl:
shows "(list_rel op \<approx> OOO op \<approx>) r r"
proof
- show c: "list_rel op \<approx> r r" by (rule list_rel_refl)
- have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
- show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
+ have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
+ show "list_rel op \<approx> r r" by (rule list_rel_refl)
+ with * show "(op \<approx> OO list_rel op \<approx>) r r" ..
qed
lemma Quotient_fset_list:
@@ -117,7 +118,8 @@
show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
next
assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
- then have b: "map abs_fset r \<approx> map abs_fset s" proof (elim pred_compE)
+ then have b: "map abs_fset r \<approx> map abs_fset s"
+ proof (elim pred_compE)
fix b ba
assume c: "list_rel op \<approx> r b"
assume d: "b \<approx> ba"
@@ -221,20 +223,43 @@
assumes a: "xs \<approx> ys"
shows "fcard_raw xs = fcard_raw ys"
using a
- apply (induct xs arbitrary: ys)
- apply (auto simp add: memb_def)
- apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
- apply (auto)
- apply (drule_tac x="x" in spec)
- apply (blast)
- apply (drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
- apply (simp add: fcard_raw_delete_one memb_def)
- apply (case_tac "a \<in> set ys")
- apply (simp only: if_True)
- apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
- apply (drule Suc_pred'[OF fcard_raw_gt_0])
- apply (auto)
- done
+ proof (induct xs arbitrary: ys)
+ case Nil
+ show ?case using Nil.prems by simp
+ next
+ case (Cons a xs)
+ have a: "a # xs \<approx> ys" by fact
+ have b: "\<And>ys. xs \<approx> ys \<Longrightarrow> fcard_raw xs = fcard_raw ys" by fact
+ show ?case proof (cases "a \<in> set xs")
+ assume c: "a \<in> set xs"
+ have "\<forall>x. (x \<in> set xs) = (x \<in> set ys)"
+ proof (intro allI iffI)
+ fix x
+ assume "x \<in> set xs"
+ then show "x \<in> set ys" using a by auto
+ next
+ fix x
+ assume d: "x \<in> set ys"
+ have e: "(x \<in> set (a # xs)) = (x \<in> set ys)" using a by simp
+ show "x \<in> set xs" using c d e unfolding list_eq.simps by simp blast
+ qed
+ then show ?thesis using b c by (simp add: memb_def)
+ next
+ assume c: "a \<notin> set xs"
+ have d: "xs \<approx> [x\<leftarrow>ys . x \<noteq> a] \<Longrightarrow> fcard_raw xs = fcard_raw [x\<leftarrow>ys . x \<noteq> a]" using b by simp
+ have "Suc (fcard_raw xs) = fcard_raw ys"
+ proof (cases "a \<in> set ys")
+ assume e: "a \<in> set ys"
+ have f: "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)" using a c
+ by (auto simp add: fcard_raw_delete_one)
+ have "fcard_raw ys = Suc (fcard_raw ys - 1)" by (rule Suc_pred'[OF fcard_raw_gt_0]) (rule e)
+ then show ?thesis using d e f by (simp_all add: fcard_raw_delete_one memb_def)
+ next
+ case False then show ?thesis using a c d by auto
+ qed
+ then show ?thesis using a c d by (simp add: memb_def)
+ qed
+qed
lemma fcard_raw_rsp[quot_respect]:
shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
@@ -306,8 +331,8 @@
obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a])
then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
- have j: "ya \<in> set y'" using b h by simp
- have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" by (rule list_rel_find_element[OF j c])
+ have "ya \<in> set y'" using b h by simp
+ then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_rel_find_element)
then show ?thesis using f i by auto
qed
@@ -385,7 +410,8 @@
apply (induct x)
apply (simp_all add: memb_def)
apply (simp add: memb_def[symmetric] memb_finter_raw)
- by (auto simp add: memb_def)
+ apply (auto simp add: memb_def)
+ done
instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice}"
begin
@@ -496,10 +522,10 @@
where
"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
-section {* Other constants on the Quotient Type *}
+section {* Other constants on the Quotient Type *}
quotient_definition
- "fcard :: 'a fset \<Rightarrow> nat"
+ "fcard :: 'a fset \<Rightarrow> nat"
is
"fcard_raw"
@@ -509,11 +535,11 @@
"map"
quotient_definition
- "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
+ "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
is "delete_raw"
quotient_definition
- "fset_to_set :: 'a fset \<Rightarrow> 'a set"
+ "fset_to_set :: 'a fset \<Rightarrow> 'a set"
is "set"
quotient_definition
@@ -701,23 +727,37 @@
by auto
lemma fset_raw_strong_cases:
- "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
- apply (induct xs)
- apply (simp)
- apply (rule disjI2)
- apply (erule disjE)
- apply (rule_tac x="a" in exI)
- apply (rule_tac x="[]" in exI)
- apply (simp add: memb_def)
- apply (erule exE)+
- apply (case_tac "x = a")
- apply (rule_tac x="a" in exI)
- apply (rule_tac x="ys" in exI)
- apply (simp)
- apply (rule_tac x="x" in exI)
- apply (rule_tac x="a # ys" in exI)
- apply (auto simp add: memb_def)
- done
+ obtains "xs = []"
+ | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
+proof (induct xs arbitrary: x ys)
+ case Nil
+ then show thesis by simp
+next
+ case (Cons a xs)
+ have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
+ have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
+ have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
+ have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
+ proof -
+ fix x :: 'a
+ fix ys :: "'a list"
+ assume d:"\<not> memb x ys"
+ assume e:"xs \<approx> x # ys"
+ show thesis
+ proof (cases "x = a")
+ assume h: "x = a"
+ then have f: "\<not> memb a ys" using d by simp
+ have g: "a # xs \<approx> a # ys" using e h by auto
+ show thesis using b f g by simp
+ next
+ assume h: "x \<noteq> a"
+ then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
+ have g: "a # xs \<approx> x # (a # ys)" using e h by auto
+ show thesis using b f g by simp
+ qed
+ qed
+ then show thesis using a c by blast
+qed
section {* deletion *}
@@ -741,7 +781,7 @@
"finter_raw l [] = []"
by (induct l) (simp_all add: not_memb_nil)
-lemma set_cong:
+lemma set_cong:
shows "(set x = set y) = (x \<approx> y)"
by auto
@@ -812,13 +852,13 @@
case (Suc m)
have b: "l \<approx> r" by fact
have d: "fcard_raw l = Suc m" by fact
- have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
+ then have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb)
then obtain a where e: "memb a l" by auto
then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
- have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
- have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
+ have "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+ then have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5))
have i: "list_eq2 l (a # delete_raw l a)"
by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
@@ -899,11 +939,11 @@
shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
by (lifting fcard_raw_1)
-lemma fcard_gt_0:
+lemma fcard_gt_0:
shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
by (lifting fcard_raw_gt_0)
-lemma fcard_not_fin:
+lemma fcard_not_fin:
shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
by (lifting fcard_raw_not_memb)
@@ -923,8 +963,8 @@
text {* funion *}
lemmas [simp] =
- sup_bot_left[where 'a="'a fset"]
- sup_bot_right[where 'a="'a fset"]
+ sup_bot_left[where 'a="'a fset", standard]
+ sup_bot_right[where 'a="'a fset", standard]
lemma funion_finsert[simp]:
shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
@@ -941,7 +981,8 @@
section {* Induction and Cases rules for finite sets *}
lemma fset_strong_cases:
- "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
+ obtains "xs = {||}"
+ | x ys where "x |\<notin>| ys" and "xs = finsert x ys"
by (lifting fset_raw_strong_cases)
lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
@@ -953,7 +994,7 @@
by (lifting list.induct)
lemma fset_induct[case_names fempty finsert, induct type: fset]:
- assumes prem1: "P {||}"
+ assumes prem1: "P {||}"
and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
shows "P S"
proof(induct S rule: fset_induct_weak)
@@ -1016,15 +1057,15 @@
text {* fdelete *}
-lemma fin_fdelete:
+lemma fin_fdelete:
shows "x |\<in>| fdelete S y \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
by (lifting memb_delete_raw)
-lemma fin_fdelete_ident:
+lemma fin_fdelete_ident:
shows "x |\<notin>| fdelete S x"
by (lifting memb_delete_raw_ident)
-lemma not_memb_fdelete_ident:
+lemma not_memb_fdelete_ident:
shows "x |\<notin>| S \<Longrightarrow> fdelete S x = S"
by (lifting not_memb_delete_raw_ident)
@@ -1102,7 +1143,7 @@
by (lifting concat_append)
ML {*
-fun dest_fsetT (Type ("FSet.fset", [T])) = T
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
*}
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 28 17:29:58 2010 +0200
@@ -22,11 +22,9 @@
relevance_threshold: real,
convergence: real,
theory_relevant: bool option,
- higher_order: bool option,
follow_defs: bool,
isar_proof: bool,
shrink_factor: int,
- sorts: bool,
timeout: Time.time,
minimize_timeout: Time.time}
type problem =
@@ -59,7 +57,7 @@
val get_prover: theory -> string -> prover
val available_atps: theory -> unit
val start_prover_thread:
- params -> Time.time -> Time.time -> int -> relevance_override
+ params -> Time.time -> Time.time -> int -> int -> relevance_override
-> (string -> minimize_command) -> Proof.state -> string -> unit
end;
@@ -83,11 +81,9 @@
relevance_threshold: real,
convergence: real,
theory_relevant: bool option,
- higher_order: bool option,
follow_defs: bool,
isar_proof: bool,
shrink_factor: int,
- sorts: bool,
timeout: Time.time,
minimize_timeout: Time.time}
@@ -268,6 +264,8 @@
let
val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
val state' = make_state manager timeout_heap [] (killing @ cancelling) messages store;
+ val _ = if null active then ()
+ else priority "Killed active Sledgehammer threads."
in state' end);
@@ -338,12 +336,11 @@
(* start prover thread *)
-fun start_prover_thread (params as {timeout, ...}) birth_time death_time i
+fun start_prover_thread (params as {timeout, ...}) birth_time death_time i n
relevance_override minimize_command proof_state name =
let
val prover = get_prover (Proof.theory_of proof_state) name
val {context = ctxt, facts, goal} = Proof.goal proof_state;
- val n = Logic.count_prems (prop_of goal)
val desc =
"ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Apr 28 17:29:58 2010 +0200
@@ -110,8 +110,8 @@
fun generic_prover overlord get_facts prepare write_file home executable args
proof_delims known_failures name
- ({debug, full_types, explicit_apply, isar_proof, shrink_factor, sorts,
- ...} : params) minimize_command
+ ({debug, full_types, explicit_apply, isar_proof, shrink_factor, ...}
+ : params) minimize_command
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
let
@@ -161,8 +161,7 @@
File.shell_path probfile, "2>&1"]) ^
(if overlord then
" | sed 's/,/, /g' \
- \| sed 's/\\([^!=]\\)\\([=|]\\)\\([^=]\\)/\\1 \\2 \\3/g' \
- \| sed 's/! =/ !=/g' \
+ \| sed 's/\\([^!=<]\\)\\([=|]\\)\\([^=>]\\)/\\1 \\2 \\3/g' \
\| sed 's/ / /g' | sed 's/| |/||/g' \
\| sed 's/ = = =/===/g' \
\| sed 's/= = /== /g'"
@@ -214,7 +213,7 @@
case outcome of
NONE =>
proof_text isar_proof
- (pool, debug, shrink_factor, sorts, ctxt, conjecture_shape)
+ (pool, debug, shrink_factor, ctxt, conjecture_shape)
(minimize_command, proof, internal_thm_names, th, subgoal)
| SOME failure => (string_for_failure failure ^ "\n", [])
in
@@ -233,14 +232,13 @@
(name, {home, executable, arguments, proof_delims, known_failures,
max_axiom_clauses, prefers_theory_relevant})
(params as {debug, overlord, respect_no_atp, relevance_threshold,
- convergence, theory_relevant, higher_order, follow_defs,
- isar_proof, ...})
+ convergence, theory_relevant, follow_defs, isar_proof, ...})
minimize_command timeout =
generic_prover overlord
(get_relevant_facts respect_no_atp relevance_threshold convergence
- higher_order follow_defs max_axiom_clauses
+ follow_defs max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant))
- (prepare_clauses higher_order false)
+ (prepare_clauses false)
(write_tptp_file (debug andalso overlord)) home
executable (arguments timeout) proof_delims known_failures name params
minimize_command
@@ -305,13 +303,13 @@
(name, {home, executable, arguments, proof_delims, known_failures,
max_axiom_clauses, prefers_theory_relevant})
(params as {overlord, respect_no_atp, relevance_threshold, convergence,
- theory_relevant, higher_order, follow_defs, ...})
+ theory_relevant, follow_defs, ...})
minimize_command timeout =
generic_prover overlord
(get_relevant_facts respect_no_atp relevance_threshold convergence
- higher_order follow_defs max_axiom_clauses
+ follow_defs max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant))
- (prepare_clauses higher_order true) write_dfg_file home executable
+ (prepare_clauses true) write_dfg_file home executable
(arguments timeout) proof_delims known_failures name params
minimize_command
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Apr 28 17:29:58 2010 +0200
@@ -248,20 +248,11 @@
val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
-fun plain_string_from_xml_tree t =
- Buffer.empty |> XML.add_content t |> Buffer.content
-val unyxml = plain_string_from_xml_tree o YXML.parse
-
-val is_long_identifier = forall Syntax.is_identifier o space_explode "."
-fun maybe_quote y =
- let val s = unyxml y in
- y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
- not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
- OuterKeyword.is_keyword s) ? quote
- end
+val unyxml = Sledgehammer_Util.unyxml
+val maybe_quote = Sledgehammer_Util.maybe_quote
(* This hash function is recommended in Compilers: Principles, Techniques, and
- Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
+ Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they
particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Apr 28 17:29:58 2010 +0200
@@ -10,6 +10,7 @@
type axiom_name = Sledgehammer_HOL_Clause.axiom_name
type hol_clause = Sledgehammer_HOL_Clause.hol_clause
type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
+
type relevance_override =
{add: Facts.ref list,
del: Facts.ref list,
@@ -19,15 +20,15 @@
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
val get_relevant_facts :
- bool -> real -> real -> bool option -> bool -> int -> bool
- -> relevance_override -> Proof.context * (thm list * 'a) -> thm list
+ bool -> real -> real -> bool -> int -> bool -> relevance_override
+ -> Proof.context * (thm list * 'a) -> thm list
-> (thm * (string * int)) list
- val prepare_clauses : bool option -> bool -> thm list -> thm list ->
- (thm * (axiom_name * hol_clause_id)) list ->
- (thm * (axiom_name * hol_clause_id)) list -> theory ->
- axiom_name vector *
- (hol_clause list * hol_clause list * hol_clause list *
- hol_clause list * classrel_clause list * arity_clause list)
+ val prepare_clauses :
+ bool -> thm list -> thm list -> (thm * (axiom_name * hol_clause_id)) list
+ -> (thm * (axiom_name * hol_clause_id)) list -> theory
+ -> axiom_name vector
+ * (hol_clause list * hol_clause list * hol_clause list *
+ hol_clause list * classrel_clause list * arity_clause list)
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -500,13 +501,10 @@
likely to lead to unsound proofs.*)
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
-fun is_first_order thy higher_order goal_cls =
- case higher_order of
- NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
- | SOME b => not b
+fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
fun get_relevant_facts respect_no_atp relevance_threshold convergence
- higher_order follow_defs max_new theory_relevant
+ follow_defs max_new theory_relevant
(relevance_override as {add, only, ...})
(ctxt, (chain_ths, th)) goal_cls =
if (only andalso null add) orelse relevance_threshold > 1.0 then
@@ -514,7 +512,7 @@
else
let
val thy = ProofContext.theory_of ctxt
- val is_FO = is_first_order thy higher_order goal_cls
+ val is_FO = is_first_order thy goal_cls
val included_cls = get_all_lemmas respect_no_atp ctxt
|> cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy is_FO
@@ -527,7 +525,7 @@
(* prepare for passing to writer,
create additional clauses based on the information from extra_cls *)
-fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy =
+fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
let
(* add chain thms *)
val chain_cls =
@@ -535,7 +533,7 @@
(map (`Thm.get_name_hint) chain_ths))
val axcls = chain_cls @ axcls
val extra_cls = chain_cls @ extra_cls
- val is_FO = is_first_order thy higher_order goal_cls
+ val is_FO = is_first_order thy goal_cls
val ccls = subtract_cls extra_cls goal_cls
val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Apr 28 17:29:58 2010 +0200
@@ -11,7 +11,7 @@
type prover_result = ATP_Manager.prover_result
val minimize_theorems :
- params -> int -> Proof.state -> (string * thm list) list
+ params -> int -> int -> Proof.state -> (string * thm list) list
-> (string * thm list) list option * string
end;
@@ -68,15 +68,14 @@
(* minimalization of thms *)
fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
- shrink_factor, sorts, ...})
- i state name_thms_pairs =
+ shrink_factor, ...})
+ i n state name_thms_pairs =
let
val thy = Proof.theory_of state
val prover = case atps of
[atp_name] => get_prover thy atp_name
| _ => error "Expected a single ATP."
val msecs = Time.toMilliseconds minimize_timeout
- val n = length name_thms_pairs
val _ =
priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
" with a time limit of " ^ string_of_int msecs ^ " ms.")
@@ -88,7 +87,6 @@
| _ => NONE
val {context = ctxt, facts, goal} = Proof.goal state;
- val n = Logic.count_prems (prop_of goal)
in
(* try prove first to check result and get used theorems *)
(case test_thms_fun NONE name_thms_pairs of
@@ -105,14 +103,13 @@
val (min_thms, {proof, internal_thm_names, ...}) =
linear_minimize (test_thms (SOME filtered_clauses)) to_use
([], result)
- val n = length min_thms
+ val m = length min_thms
val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
+ ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
in
(SOME min_thms,
proof_text isar_proof
- (pool, debug, shrink_factor, sorts, ctxt,
- conjecture_shape)
+ (pool, debug, shrink_factor, ctxt, conjecture_shape)
(K "", proof, internal_thm_names, goal, i) |> fst)
end
| {outcome = SOME TimedOut, ...} =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Apr 28 17:29:58 2010 +0200
@@ -10,6 +10,7 @@
val trace: bool Unsynchronized.ref
val trace_msg: (unit -> string) -> unit
val skolem_prefix: string
+ val skolem_infix: string
val cnf_axiom: theory -> thm -> thm list
val multi_base_blacklist: string list
val bad_for_atp: thm -> bool
@@ -17,7 +18,7 @@
val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
val suppress_endtheory: bool Unsynchronized.ref
(*for emergency use where endtheory causes problems*)
- val strip_subgoal : thm -> int -> term list * term list * term
+ val strip_subgoal : thm -> int -> (string * typ) list * term list * term
val neg_clausify: thm -> thm list
val neg_conjecture_clauses:
Proof.context -> thm -> int -> thm list list * (string * typ) list
@@ -34,6 +35,7 @@
fun trace_msg msg = if !trace then tracing (msg ()) else ();
val skolem_prefix = "sko_"
+val skolem_infix = "$"
fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
@@ -65,6 +67,13 @@
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
+(*Keep the full complexity of the original name*)
+fun flatten_name s = space_implode "_X" (Long_Name.explode s);
+
+fun skolem_name thm_name nref var_name =
+ skolem_prefix ^ thm_name ^ "_" ^ Int.toString (Unsynchronized.inc nref) ^
+ skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
+
fun rhs_extra_types lhsT rhs =
let val lhs_vars = Term.add_tfreesT lhsT []
fun add_new_TFrees (TFree v) =
@@ -78,10 +87,10 @@
fun declare_skofuns s th =
let
val nref = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (_, T, p))) (axs, thy) =
+ fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) (axs, thy) =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
- val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
+ val cname = skolem_name s nref s'
val args0 = OldTerm.term_frees xtp (*get the formal parameter list*)
val Ts = map type_of args0
val extraTs = rhs_extra_types (Ts ---> T) xtp
@@ -110,13 +119,13 @@
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skofuns s th =
let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs(_,T,p))) defs =
+ fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
val Ts = map type_of args
val cT = Ts ---> T
- val id = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
+ val id = skolem_name s sko_count s'
val c = Free (id, cT)
val rhs = list_abs_free (map dest_Free args,
HOLogic.choice_const T $ xtp)
@@ -337,9 +346,6 @@
["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
"split_asm", "cases", "ext_cases"];
-(*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (Long_Name.explode s);
-
fun fake_name th =
if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
else gensym "unknown_thm_";
@@ -463,7 +469,7 @@
val (t, frees) = Logic.goal_params (prop_of goal) i
val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
- in (rev frees, hyp_ts, concl_t) end
+ in (rev (map dest_Free frees), hyp_ts, concl_t) end
(*** Converting a subgoal into negated conjecture clauses. ***)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Apr 28 17:29:58 2010 +0200
@@ -107,10 +107,10 @@
fun union_all xss = fold (union (op =)) xss []
-(* Provide readable names for the more common symbolic functions *)
+(* Readable names for the more common symbolic functions. Do not mess with the
+ last six entries of the table unless you know what you are doing. *)
val const_trans_table =
Symtab.make [(@{const_name "op ="}, "equal"),
- (@{const_name Orderings.less_eq}, "lessequals"),
(@{const_name "op &"}, "and"),
(@{const_name "op |"}, "or"),
(@{const_name "op -->"}, "implies"),
@@ -120,10 +120,11 @@
(@{const_name COMBK}, "COMBK"),
(@{const_name COMBB}, "COMBB"),
(@{const_name COMBC}, "COMBC"),
- (@{const_name COMBS}, "COMBS")];
+ (@{const_name COMBS}, "COMBS")]
val type_const_trans_table =
- Symtab.make [("*", "prod"), ("+", "sum"), ("~=>", "map")];
+ Symtab.make [(@{type_name "*"}, "prod"),
+ (@{type_name "+"}, "sum")]
(*Escaping of special characters.
Alphanumeric characters are left unchanged.
@@ -191,7 +192,8 @@
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
-val max_dfg_symbol_length = 63
+val max_dfg_symbol_length =
+ if is_new_spass_version then 1000000 (* arbitrary large number *) else 63
(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
fun controlled_length dfg s =
@@ -263,7 +265,9 @@
val s' =
if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
else s'
- val s' = if s' = "op" then full_name else s'
+ (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
+ ("op &", "op |", etc.). *)
+ val s' = if s' = "equal" orelse s' = "op" then full_name else s'
in
case (Char.isLower (String.sub (full_name, 0)),
Char.isLower (String.sub (s', 0))) of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Apr 28 17:29:58 2010 +0200
@@ -487,8 +487,8 @@
fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
|> fold count_constants_clause extra_clauses
|> fold count_constants_clause helper_clauses
- val _ = List.app (display_arity explicit_apply const_needs_hBOOL)
- (Symtab.dest (const_min_arity))
+ val _ = app (display_arity explicit_apply const_needs_hBOOL)
+ (Symtab.dest (const_min_arity))
in (const_min_arity, const_needs_hBOOL) end
else (Symtab.empty, Symtab.empty);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 28 17:29:58 2010 +0200
@@ -96,11 +96,9 @@
("relevance_threshold", "50"),
("convergence", "320"),
("theory_relevant", "smart"),
- ("higher_order", "smart"),
("follow_defs", "false"),
("isar_proof", "false"),
("shrink_factor", "1"),
- ("sorts", "false"),
("minimize_timeout", "5 s")]
val alias_params =
@@ -113,14 +111,12 @@
("implicit_apply", "explicit_apply"),
("ignore_no_atp", "respect_no_atp"),
("theory_irrelevant", "theory_relevant"),
- ("first_order", "higher_order"),
("dont_follow_defs", "follow_defs"),
- ("metis_proof", "isar_proof"),
- ("no_sorts", "sorts")]
+ ("metis_proof", "isar_proof")]
val params_for_minimize =
["debug", "verbose", "overlord", "full_types", "explicit_apply",
- "higher_order", "isar_proof", "shrink_factor", "sorts", "minimize_timeout"]
+ "isar_proof", "shrink_factor", "minimize_timeout"]
val property_dependent_params = ["atps", "full_types", "timeout"]
@@ -200,11 +196,9 @@
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
val theory_relevant = lookup_bool_option "theory_relevant"
- val higher_order = lookup_bool_option "higher_order"
val follow_defs = lookup_bool "follow_defs"
val isar_proof = lookup_bool "isar_proof"
val shrink_factor = Int.max (1, lookup_int "shrink_factor")
- val sorts = lookup_bool "sorts"
val timeout = lookup_time "timeout"
val minimize_timeout = lookup_time "minimize_timeout"
in
@@ -212,28 +206,33 @@
full_types = full_types, explicit_apply = explicit_apply,
respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
convergence = convergence, theory_relevant = theory_relevant,
- higher_order = higher_order, follow_defs = follow_defs,
- isar_proof = isar_proof, shrink_factor = shrink_factor, sorts = sorts,
- timeout = timeout, minimize_timeout = minimize_timeout}
+ follow_defs = follow_defs, isar_proof = isar_proof,
+ shrink_factor = shrink_factor, timeout = timeout,
+ minimize_timeout = minimize_timeout}
end
fun get_params thy = extract_params thy (default_raw_params thy)
fun default_params thy = get_params thy o map (apsnd single)
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
(* Sledgehammer the given subgoal *)
fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
| run (params as {atps, timeout, ...}) i relevance_override minimize_command
- proof_state =
- let
- val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, timeout)
- val _ = kill_atps () (* race w.r.t. other invocations of Sledgehammer *)
- val _ = priority "Sledgehammering..."
- val _ = List.app (start_prover_thread params birth_time death_time i
- relevance_override minimize_command
- proof_state) atps
- in () end
+ state =
+ case subgoal_count state of
+ 0 => priority "No subgoal!"
+ | n =>
+ let
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, timeout)
+ val _ = kill_atps () (* race w.r.t. other Sledgehammer invocations *)
+ val _ = priority "Sledgehammering..."
+ val _ = app (start_prover_thread params birth_time death_time i n
+ relevance_override minimize_command
+ state) atps
+ in () end
fun minimize override_params i fact_refs state =
let
@@ -243,8 +242,10 @@
map o pairf Facts.string_of_ref o ProofContext.get_fact
val name_thms_pairs = theorems_from_refs ctxt fact_refs
in
- priority (#2 (minimize_theorems (get_params thy override_params) i state
- name_thms_pairs))
+ case subgoal_count state of
+ 0 => priority "No subgoal!"
+ | n => priority (#2 (minimize_theorems (get_params thy override_params) i n
+ state name_thms_pairs))
end
val sledgehammerN = "sledgehammer"
@@ -265,9 +266,7 @@
val is_raw_param_relevant_for_minimize =
member (op =) params_for_minimize o fst o unalias_raw_param
fun string_for_raw_param (key, values) =
- key ^ (case space_implode " " values of
- "" => ""
- | value => " = " ^ value)
+ key ^ (case space_implode " " values of "" => "" | value => " = " ^ value)
fun minimize_command override_params i atp_name facts =
sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
@@ -279,7 +278,7 @@
fun hammer_away override_params subcommand opt_i relevance_override state =
let
val thy = Proof.theory_of state
- val _ = List.app check_raw_param override_params
+ val _ = app check_raw_param override_params
in
if subcommand = runN then
let val i = the_default 1 opt_i in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Apr 28 17:29:58 2010 +0200
@@ -21,11 +21,11 @@
minimize_command * string * string vector * thm * int
-> string * string list
val isar_proof_text:
- name_pool option * bool * int * bool * Proof.context * int list list
+ name_pool option * bool * int * Proof.context * int list list
-> minimize_command * string * string vector * thm * int
-> string * string list
val proof_text:
- bool -> name_pool option * bool * int * bool * Proof.context * int list list
+ bool -> name_pool option * bool * int * Proof.context * int list list
-> minimize_command * string * string vector * thm * int
-> string * string list
end;
@@ -33,6 +33,7 @@
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
struct
+open Sledgehammer_Util
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
@@ -49,14 +50,29 @@
SOME s' => s'
| NONE => s
+fun smart_lambda v t =
+ Abs (case v of
+ Const (s, _) =>
+ List.last (space_explode skolem_infix (Long_Name.base_name s))
+ | Var ((s, _), _) => s
+ | Free (s, _) => s
+ | _ => "", fastype_of v, abstract_over (v, t))
+
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
+fun exists_of v t = HOLogic.exists_const (fastype_of v) $ smart_lambda v t
+
+datatype ('a, 'b, 'c, 'd, 'e) raw_step =
+ Definition of 'a * 'b * 'c |
+ Inference of 'a * 'd * 'e list
+
(**** PARSING OF TSTP FORMAT ****)
(* Syntax trees, either term list or formulae *)
-datatype stree = SInt of int | SBranch of string * stree list;
+datatype node = IntLeaf of int | StrNode of string * node list
-fun atom x = SBranch (x, [])
+fun atom x = StrNode (x, [])
-fun scons (x, y) = SBranch ("cons", [x, y])
+fun scons (x, y) = StrNode ("cons", [x, y])
val slist_of = List.foldl scons (atom "nil")
(*Strings enclosed in single quotes, e.g. filenames*)
@@ -74,54 +90,63 @@
(* The "x" argument is not strictly necessary, but without it Poly/ML loops
forever at compile time. *)
fun parse_term pool x =
- (parse_quoted >> atom
- || parse_integer >> SInt
+ (parse_quoted >> atom
+ || parse_integer >> IntLeaf
|| $$ "$" |-- Symbol.scan_id >> (atom o repair_bool_literal)
|| (Symbol.scan_id >> repair_name pool)
- -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> SBranch
+ -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
|| $$ "(" |-- parse_term pool --| $$ ")"
|| $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
and parse_terms pool x =
(parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
-fun negate_stree t = SBranch ("c_Not", [t])
-fun equate_strees t1 t2 = SBranch ("c_equal", [t1, t2]);
+fun negate_node u = StrNode ("c_Not", [u])
+fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
(* Apply equal or not-equal to a term. *)
-fun repair_predicate_term (t, NONE) = t
- | repair_predicate_term (t1, SOME (NONE, t2)) = equate_strees t1 t2
- | repair_predicate_term (t1, SOME (SOME _, t2)) =
- negate_stree (equate_strees t1 t2)
+fun repair_predicate_term (u, NONE) = u
+ | repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2
+ | repair_predicate_term (u1, SOME (SOME _, u2)) =
+ negate_node (equate_nodes u1 u2)
fun parse_predicate_term pool =
parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
-- parse_term pool)
>> repair_predicate_term
-(*Literals can involve negation, = and !=.*)
+(* Literals can involve "~", "=", and "!=". *)
fun parse_literal pool x =
- ($$ "~" |-- parse_literal pool >> negate_stree || parse_predicate_term pool) x
+ ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
fun parse_literals pool =
parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
-(* Clause: a list of literals separated by the disjunction sign. *)
+(* Clause: a list of literals separated by disjunction operators ("|"). *)
fun parse_clause pool =
$$ "(" |-- parse_literals pool --| $$ ")" || Scan.single (parse_literal pool)
-fun ints_of_stree (SInt n) = cons n
- | ints_of_stree (SBranch (_, ts)) = fold ints_of_stree ts
+fun ints_of_node (IntLeaf n) = cons n
+ | ints_of_node (StrNode (_, us)) = fold ints_of_node us
val parse_tstp_annotations =
Scan.optional ($$ "," |-- parse_term NONE
--| Scan.option ($$ "," |-- parse_terms NONE)
- >> (fn source => ints_of_stree source [])) []
+ >> (fn source => ints_of_node source [])) []
+
+fun parse_definition pool =
+ $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
+ -- parse_clause pool --| $$ ")"
-(* <cnf_annotated> ::= cnf(<name>, <formula_role>, <cnf_formula> <annotations>).
- The <name> could be an identifier, but we assume integers. *)
-fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps)
+(* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
+ The <num> could be an identifier, but we assume integers. *)
+fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
+fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
fun parse_tstp_line pool =
- (Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
- --| Symbol.scan_id --| $$ "," -- parse_clause pool -- parse_tstp_annotations
- --| $$ ")" --| $$ "."
- >> retuple_tstp_line
+ ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
+ --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
+ --| parse_tstp_annotations --| $$ ")" --| $$ "."
+ >> finish_tstp_definition_line)
+ || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
+ --| Symbol.scan_id --| $$ "," -- parse_clause pool
+ -- parse_tstp_annotations --| $$ ")" --| $$ "."
+ >> finish_tstp_inference_line)
(**** PARSING OF SPASS OUTPUT ****)
@@ -142,22 +167,22 @@
Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
-- Scan.repeat (parse_starred_predicate_term pool)
>> (fn ([], []) => [atom "c_False"]
- | (clauses1, clauses2) => map negate_stree clauses1 @ clauses2)
+ | (clauses1, clauses2) => map negate_node clauses1 @ clauses2)
-(* Syntax: <name>[0:<inference><annotations>] ||
+(* Syntax: <num>[0:<inference><annotations>] ||
<cnf_formulas> -> <cnf_formulas>. *)
-fun retuple_spass_line ((name, deps), ts) = (name, ts, deps)
+fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
fun parse_spass_line pool =
parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
-- parse_horn_clause pool --| $$ "."
- >> retuple_spass_line
+ >> finish_spass_line
fun parse_line pool = fst o (parse_tstp_line pool || parse_spass_line pool)
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
-exception STREE of stree;
+exception NODE of node
(*If string s has the prefix s1, return the result of deleting it.*)
fun strip_prefix s1 s =
@@ -180,24 +205,21 @@
(*Type variables are given the basic sort, HOL.type. Some will later be constrained
by information from type literals, or by type inference.*)
-fun type_of_stree t =
- case t of
- SInt _ => raise STREE t
- | SBranch (a,ts) =>
- let val Ts = map type_of_stree ts
- in
- case strip_prefix tconst_prefix a of
- SOME b => Type(invert_type_const b, Ts)
- | NONE =>
- if not (null ts) then raise STREE t (*only tconsts have type arguments*)
- else
- case strip_prefix tfree_prefix a of
- SOME b => TFree("'" ^ b, HOLogic.typeS)
- | NONE =>
- case strip_prefix tvar_prefix a of
- SOME b => make_tvar b
- | NONE => make_tparam a (* Variable from the ATP, say "X1" *)
- end;
+fun type_of_node (u as IntLeaf _) = raise NODE u
+ | type_of_node (u as StrNode (a, us)) =
+ let val Ts = map type_of_node us in
+ case strip_prefix tconst_prefix a of
+ SOME b => Type (invert_type_const b, Ts)
+ | NONE =>
+ if not (null us) then
+ raise NODE u (*only tconsts have type arguments*)
+ else case strip_prefix tfree_prefix a of
+ SOME b => TFree ("'" ^ b, HOLogic.typeS)
+ | NONE =>
+ case strip_prefix tvar_prefix a of
+ SOME b => make_tvar b
+ | NONE => make_tparam a (* Variable from the ATP, say "X1" *)
+ end
(*Invert the table of translations between Isabelle and ATPs*)
val const_trans_table_inv =
@@ -212,62 +234,81 @@
(*Generates a constant, given its type arguments*)
fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts));
+fun fix_atp_variable_name s =
+ let
+ fun subscript_name s n = s ^ nat_subscript n
+ val s = String.map Char.toLower s
+ in
+ case space_explode "_" s of
+ [_] => (case take_suffix Char.isDigit (String.explode s) of
+ (cs1 as _ :: _, cs2 as _ :: _) =>
+ subscript_name (String.implode cs1)
+ (the (Int.fromString (String.implode cs2)))
+ | (_, _) => s)
+ | [s1, s2] => (case Int.fromString s2 of
+ SOME n => subscript_name s1 n
+ | NONE => s)
+ | _ => s
+ end
+
(*First-order translation. No types are known for variables. HOLogic.typeT should allow
them to be inferred.*)
-fun term_of_stree args thy t =
- case t of
- SInt _ => raise STREE t
- | SBranch ("hBOOL", [t]) => term_of_stree [] thy t (*ignore hBOOL*)
- | SBranch ("hAPP", [t, u]) => term_of_stree (u::args) thy t
- | SBranch (a, ts) =>
- case strip_prefix const_prefix a of
- SOME "equal" =>
- list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts)
- | SOME b =>
- let val c = invert_const b
- val nterms = length ts - num_typargs thy c
- val us = List.map (term_of_stree [] thy) (List.take(ts,nterms) @ args)
- (*Extra args from hAPP come AFTER any arguments given directly to the
- constant.*)
- val Ts = List.map type_of_stree (List.drop(ts,nterms))
- in list_comb(const_of thy (c, Ts), us) end
- | NONE => (*a variable, not a constant*)
- let val T = HOLogic.typeT
- val opr = (*a Free variable is typically a Skolem function*)
- case strip_prefix fixed_var_prefix a of
- SOME b => Free(b,T)
- | NONE =>
- case strip_prefix schematic_var_prefix a of
- SOME b => make_var (b,T)
- | NONE => make_var (a,T) (* Variable from the ATP, say "X1" *)
- in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end;
+fun term_of_node args thy u =
+ case u of
+ IntLeaf _ => raise NODE u
+ | StrNode ("hBOOL", [u]) => term_of_node [] thy u (* ignore hBOOL *)
+ | StrNode ("hAPP", [u1, u2]) => term_of_node (u2 :: args) thy u1
+ | StrNode (a, us) =>
+ case strip_prefix const_prefix a of
+ SOME "equal" =>
+ list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
+ map (term_of_node [] thy) us)
+ | SOME b =>
+ let
+ val c = invert_const b
+ val nterms = length us - num_typargs thy c
+ val ts = map (term_of_node [] thy) (take nterms us @ args)
+ (*Extra args from hAPP come AFTER any arguments given directly to the
+ constant.*)
+ val Ts = map type_of_node (drop nterms us)
+ in list_comb(const_of thy (c, Ts), ts) end
+ | NONE => (*a variable, not a constant*)
+ let
+ val opr =
+ (* a Free variable is typically a Skolem function *)
+ case strip_prefix fixed_var_prefix a of
+ SOME b => Free (b, HOLogic.typeT)
+ | NONE =>
+ case strip_prefix schematic_var_prefix a of
+ SOME b => make_var (b, HOLogic.typeT)
+ | NONE =>
+ (* Variable from the ATP, say "X1" *)
+ make_var (fix_atp_variable_name a, HOLogic.typeT)
+ in list_comb (opr, map (term_of_node [] thy) (us @ args)) end
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
-fun constraint_of_stree pol (SBranch ("c_Not", [t])) =
- constraint_of_stree (not pol) t
- | constraint_of_stree pol t = case t of
- SInt _ => raise STREE t
- | SBranch (a, ts) =>
- (case (strip_prefix class_prefix a, map type_of_stree ts) of
- (SOME b, [T]) => (pol, b, T)
- | _ => raise STREE t);
+fun constraint_of_node pos (StrNode ("c_Not", [u])) =
+ constraint_of_node (not pos) u
+ | constraint_of_node pos u = case u of
+ IntLeaf _ => raise NODE u
+ | StrNode (a, us) =>
+ (case (strip_prefix class_prefix a, map type_of_node us) of
+ (SOME b, [T]) => (pos, b, T)
+ | _ => raise NODE u)
(** Accumulate type constraints in a clause: negative type literals **)
-fun addix (key,z) = Vartab.map_default (key,[]) (cons z);
+fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
-fun add_constraint ((false, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt
- | add_constraint ((false, cl, TVar(ix,_)), vt) = addix (ix,cl) vt
+fun add_constraint ((false, cl, TFree(a,_)), vt) = add_var ((a,~1),cl) vt
+ | add_constraint ((false, cl, TVar(ix,_)), vt) = add_var (ix,cl) vt
| add_constraint (_, vt) = vt;
-fun is_positive_literal (@{const Trueprop} $ t) = is_positive_literal t
- | is_positive_literal (@{const Not} $ _) = false
+fun is_positive_literal (@{const Not} $ _) = false
| is_positive_literal t = true
-fun negate_term thy (@{const Trueprop} $ t) =
- @{const Trueprop} $ negate_term thy t
- | negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
+fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
| negate_term thy (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
Const (@{const_name All}, T) $ Abs (s, T', negate_term thy t')
@@ -277,12 +318,8 @@
@{const "op |"} $ negate_term thy t1 $ negate_term thy t2
| negate_term thy (@{const "op |"} $ t1 $ t2) =
@{const "op &"} $ negate_term thy t1 $ negate_term thy t2
- | negate_term thy (@{const Not} $ t) = t
- | negate_term thy t =
- if fastype_of t = @{typ prop} then
- HOLogic.mk_Trueprop (negate_term thy (Object_Logic.atomize_term thy t))
- else
- @{const Not} $ t
+ | negate_term _ (@{const Not} $ t) = t
+ | negate_term _ t = @{const Not} $ t
fun clause_for_literals _ [] = HOLogic.false_const
| clause_for_literals _ [lit] = lit
@@ -302,11 +339,10 @@
|> clause_for_literals thy
(*Accumulate sort constraints in vt, with "real" literals in lits.*)
-fun lits_of_strees thy (vt, lits) [] = (vt, finish_clause thy lits)
- | lits_of_strees thy (vt, lits) (t :: ts) =
- lits_of_strees thy (add_constraint (constraint_of_stree true t, vt), lits)
- ts
- handle STREE _ => lits_of_strees thy (vt, term_of_stree [] thy t :: lits) ts
+fun lits_of_nodes thy (vt, lits) [] = (vt, finish_clause thy lits)
+ | lits_of_nodes thy (vt, lits) (u :: us) =
+ lits_of_nodes thy (add_constraint (constraint_of_node true u, vt), lits) us
+ handle NODE _ => lits_of_nodes thy (vt, term_of_node [] thy u :: lits) us
(*Update TVars/TFrees with detected sort constraints.*)
fun repair_sorts vt =
@@ -318,122 +354,133 @@
| tmsubst (Var (xi, T)) = Var (xi, tysubst T)
| tmsubst (t as Bound _) = t
| tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
- | tmsubst (t $ u) = tmsubst t $ tmsubst u;
+ | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2
in not (Vartab.is_empty vt) ? tmsubst end;
-(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
- vt0 holds the initial sort constraints, from the conjecture clauses.*)
-fun clause_of_strees ctxt vt ts =
- let val (vt, dt) = lits_of_strees (ProofContext.theory_of ctxt) (vt, []) ts in
- dt |> repair_sorts vt |> TypeInfer.constrain HOLogic.boolT
- |> Syntax.check_term ctxt
+(* Interpret a list of syntax trees as a clause, given by "real" literals and
+ sort constraints. "vt" holds the initial sort constraints, from the
+ conjecture clauses. *)
+fun clause_of_nodes ctxt vt us =
+ let val (vt, dt) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
+ dt |> repair_sorts vt
end
-
-fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
+fun check_clause ctxt =
+ TypeInfer.constrain HOLogic.boolT
+ #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
+fun checked_clause_of_nodes ctxt = check_clause ctxt oo clause_of_nodes ctxt
-fun decode_line vt0 (name, ts, deps) ctxt =
- let val cl = clause_of_strees ctxt vt0 ts in
- ((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
- end
-
-(** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **)
+(** Global sort constraints on TFrees (from tfree_tcs) are positive unit
+ clauses. **)
-fun add_tfree_constraint ((true, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt
- | add_tfree_constraint (_, vt) = vt;
-
+fun add_tfree_constraint (true, cl, TFree (a, _)) = add_var ((a, ~1), cl)
+ | add_tfree_constraint _ = I
fun tfree_constraints_of_clauses vt [] = vt
- | tfree_constraints_of_clauses vt ([lit]::tss) =
- (tfree_constraints_of_clauses (add_tfree_constraint (constraint_of_stree true lit, vt)) tss
- handle STREE _ => (*not a positive type constraint: ignore*)
- tfree_constraints_of_clauses vt tss)
- | tfree_constraints_of_clauses vt (_::tss) = tfree_constraints_of_clauses vt tss;
+ | tfree_constraints_of_clauses vt ([lit] :: uss) =
+ (tfree_constraints_of_clauses (add_tfree_constraint
+ (constraint_of_node true lit) vt) uss
+ handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
+ tfree_constraints_of_clauses vt uss)
+ | tfree_constraints_of_clauses vt (_ :: uss) =
+ tfree_constraints_of_clauses vt uss
(**** Translation of TSTP files to Isar Proofs ****)
-fun decode_lines ctxt tuples =
- let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #2 tuples) in
- #1 (fold_map (decode_line vt0) tuples ctxt)
- end
+fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
+ | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-fun unequal t (_, t', _) = not (t aconv t');
+fun clauses_in_lines (Definition (_, u, us)) = u :: us
+ | clauses_in_lines (Inference (_, us, _)) = us
-(*No "real" literals means only type information*)
-fun eq_types t = t aconv HOLogic.true_const;
+fun decode_line vt (Definition (num, u, us)) ctxt =
+ let
+ val cl1 = clause_of_nodes ctxt vt [u]
+ val vars = snd (strip_comb cl1)
+ val frees = map unvarify_term vars
+ val unvarify_args = subst_atomic (vars ~~ frees)
+ val cl2 = clause_of_nodes ctxt vt us
+ val (cl1, cl2) =
+ HOLogic.eq_const HOLogic.typeT $ cl1 $ cl2
+ |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq
+ in
+ (Definition (num, cl1, cl2),
+ fold Variable.declare_term (maps OldTerm.term_frees [cl1, cl2]) ctxt)
+ end
+ | decode_line vt (Inference (num, us, deps)) ctxt =
+ let val cl = us |> clause_of_nodes ctxt vt |> check_clause ctxt in
+ (Inference (num, cl, deps),
+ fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
+ end
+fun decode_lines ctxt lines =
+ let
+ val vt = tfree_constraints_of_clauses Vartab.empty
+ (map clauses_in_lines lines)
+ in #1 (fold_map (decode_line vt) lines ctxt) end
-fun replace_dep (old, new) dep = if dep = old then new else [dep]
-fun replace_deps p (num, t, deps) =
- (num, t, fold (union (op =) o replace_dep p) deps [])
+fun aint_inference _ (Definition _) = true
+ | aint_inference t (Inference (_, t', _)) = not (t aconv t')
+
+(* No "real" literals means only type information (tfree_tcs, clsrel, or
+ clsarity). *)
+val is_only_type_information = curry (op aconv) HOLogic.true_const
+
+fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
+fun replace_deps_in_line _ (line as Definition _) = line
+ | replace_deps_in_line p (Inference (num, t, deps)) =
+ Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
only in type information.*)
-fun add_line thm_names (num, t, []) lines =
- (* No dependencies: axiom or conjecture clause *)
- if is_axiom_clause_number thm_names num then
- (* Axioms are not proof lines *)
- if eq_types t then
- (* Must be clsrel/clsarity: type information, so delete refs to it *)
- map (replace_deps (num, [])) lines
- else
- (case take_prefix (unequal t) lines of
- (_,[]) => lines (*no repetition of proof line*)
- | (pre, (num', _, _) :: post) => (*repetition: replace later line by earlier one*)
- pre @ map (replace_deps (num', [num])) post)
- else
- (num, t, []) :: lines
- | add_line _ (num, t, deps) lines =
- if eq_types t then (num, t, deps) :: lines
- (*Type information will be deleted later; skip repetition test.*)
- else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
- case take_prefix (unequal t) lines of
- (_,[]) => (num, t, deps) :: lines (*no repetition of proof line*)
- | (pre, (num', t', _) :: post) =>
- (num, t', deps) :: (*repetition: replace later line by earlier one*)
- (pre @ map (replace_deps (num', [num])) post);
+fun add_line _ (line as Definition _) lines = line :: lines
+ | add_line thm_names (Inference (num, t, [])) lines =
+ (* No dependencies: axiom or conjecture clause *)
+ if is_axiom_clause_number thm_names num then
+ (* Axioms are not proof lines. *)
+ if is_only_type_information t then
+ map (replace_deps_in_line (num, [])) lines
+ (* Is there a repetition? If so, replace later line by earlier one. *)
+ else case take_prefix (aint_inference t) lines of
+ (_, []) => lines (*no repetition of proof line*)
+ | (pre, Inference (num', _, _) :: post) =>
+ pre @ map (replace_deps_in_line (num', [num])) post
+ else
+ Inference (num, t, []) :: lines
+ | add_line _ (Inference (num, t, deps)) lines =
+ (* Type information will be deleted later; skip repetition test. *)
+ if is_only_type_information t then
+ Inference (num, t, deps) :: lines
+ (* Is there a repetition? If so, replace later line by earlier one. *)
+ else case take_prefix (aint_inference t) lines of
+ (* FIXME: Doesn't this code risk conflating proofs involving different
+ types?? *)
+ (_, []) => Inference (num, t, deps) :: lines
+ | (pre, Inference (num', t', _) :: post) =>
+ Inference (num, t', deps) ::
+ pre @ map (replace_deps_in_line (num', [num])) post
-(*Recursively delete empty lines (type information) from the proof.*)
-fun add_nonnull_line (num, t, []) lines = (*no dependencies, so a conjecture clause*)
- if eq_types t then
- (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*)
- delete_dep num lines
- else
- (num, t, []) :: lines
- | add_nonnull_line (num, t, deps) lines = (num, t, deps) :: lines
+(* Recursively delete empty lines (type information) from the proof. *)
+fun add_nontrivial_line (Inference (num, t, [])) lines =
+ if is_only_type_information t then delete_dep num lines
+ else Inference (num, t, []) :: lines
+ | add_nontrivial_line line lines = line :: lines
and delete_dep num lines =
- fold_rev add_nonnull_line (map (replace_deps (num, [])) lines) []
-
-fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
- | bad_free _ = false;
+ fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
-fun add_desired_line ctxt (num, t, []) (j, lines) =
- (j, (num, t, []) :: lines) (* conjecture clauses must be kept *)
- | add_desired_line ctxt (num, t, deps) (j, lines) =
- (j + 1,
- if eq_types t orelse not (null (Term.add_tvars t [])) orelse
- exists_subterm bad_free t orelse length deps < 2 then
- map (replace_deps (num, deps)) lines (* delete line *)
- else
- (num, t, deps) :: lines)
+fun is_bad_free (Free (a, _)) = String.isPrefix skolem_prefix a
+ | is_bad_free _ = false
-(* ### *)
-(*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*)
-fun stringify_deps thm_names deps_map [] = []
- | stringify_deps thm_names deps_map ((num, t, deps) :: lines) =
- if is_axiom_clause_number thm_names num then
- (Vector.sub (thm_names, num - 1), t, []) ::
- stringify_deps thm_names deps_map lines
- else
- let
- val label = Int.toString (length deps_map)
- fun string_for_num num =
- if is_axiom_clause_number thm_names num then
- SOME (Vector.sub (thm_names, num - 1))
- else
- AList.lookup (op =) deps_map num
- in
- (label, t, map_filter string_for_num (distinct (op=) deps)) ::
- stringify_deps thm_names ((num, label) :: deps_map) lines
- end
+fun add_desired_line _ _ (line as Definition _) (j, lines) = (j, line :: lines)
+ | add_desired_line ctxt _ (Inference (num, t, [])) (j, lines) =
+ (j, Inference (num, t, []) :: lines) (* conjecture clauses must be kept *)
+ | add_desired_line ctxt shrink_factor (Inference (num, t, deps)) (j, lines) =
+ (j + 1,
+ if is_only_type_information t orelse
+ not (null (Term.add_tvars t [])) orelse
+ exists_subterm is_bad_free t orelse
+ (length deps < 2 orelse j mod shrink_factor <> 0) then
+ map (replace_deps_in_line (num, deps)) lines (* delete line *)
+ else
+ Inference (num, t, deps) :: lines)
(** EXTRACTING LEMMAS **)
@@ -485,20 +532,22 @@
val n = Logic.count_prems (prop_of goal)
in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end
-val is_valid_line = String.isPrefix "cnf(" orf String.isSubstring "||"
+val is_valid_line =
+ String.isPrefix "fof(" orf String.isPrefix "cnf(" orf String.isSubstring "||"
-(** NEW PROOF RECONSTRUCTION CODE **)
+(** Isar proof construction and manipulation **)
+
+fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
+ (union (op =) ls1 ls2, union (op =) ss1 ss2)
type label = string * int
type facts = label list * string list
-fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
- (union (op =) ls1 ls2, union (op =) ss1 ss2)
-
datatype qualifier = Show | Then | Moreover | Ultimately
datatype step =
- Fix of term list |
+ Fix of (string * typ) list |
+ Let of term * term |
Assume of label * term |
Have of qualifier list * label * term * byline
and byline =
@@ -509,19 +558,20 @@
val assum_prefix = "A"
val fact_prefix = "F"
-(* ###
-fun add_fact_from_dep s =
- case Int.fromString s of
- SOME n => apfst (cons (raw_prefix, n))
- | NONE => apsnd (cons s)
-*)
+fun add_fact_from_dep thm_names num =
+ if is_axiom_clause_number thm_names num then
+ apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
+ else
+ apfst (insert (op =) (raw_prefix, num))
-val add_fact_from_dep = apfst o cons o pair raw_prefix
+fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
-fun step_for_tuple _ (label, t, []) = Assume ((raw_prefix, label), t)
- | step_for_tuple j (label, t, deps) =
- Have (if j = 1 then [Show] else [], (raw_prefix, label), t,
- Facts (fold add_fact_from_dep deps ([], [])))
+fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
+ | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
+ | step_for_line thm_names j (Inference (num, t, deps)) =
+ Have (if j = 1 then [Show] else [], (raw_prefix, num),
+ forall_vars t,
+ Facts (fold (add_fact_from_dep thm_names) deps ([], [])))
fun strip_spaces_in_list [] = ""
| strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
@@ -540,19 +590,20 @@
str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
val strip_spaces = strip_spaces_in_list o String.explode
-fun proof_from_atp_proof pool ctxt atp_proof thm_names frees =
+fun proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names frees =
let
- val tuples =
- atp_proof |> split_lines |> map strip_spaces
- |> filter is_valid_line
- |> map (parse_line pool o explode)
- |> decode_lines ctxt
- val tuples = fold_rev (add_line thm_names) tuples []
- val tuples = fold_rev add_nonnull_line tuples []
- val tuples = fold_rev (add_desired_line ctxt) tuples (0, []) |> snd
+ val lines =
+ atp_proof
+ |> split_lines |> map strip_spaces |> filter is_valid_line
+ |> map (parse_line pool o explode)
+ |> decode_lines ctxt
+ |> rpair [] |-> fold_rev (add_line thm_names)
+ |> rpair [] |-> fold_rev add_nontrivial_line
+ |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor)
+ |> snd
in
(if null frees then [] else [Fix frees]) @
- map2 step_for_tuple (length tuples downto 1) tuples
+ map2 (step_for_line thm_names) (length lines downto 1) lines
end
val indent_size = 2
@@ -575,6 +626,7 @@
and using_of proof = fold (union (op =) o using_of_step) proof []
fun new_labels_of_step (Fix _) = []
+ | new_labels_of_step (Let _) = []
| new_labels_of_step (Assume (l, _)) = [l]
| new_labels_of_step (Have (_, l, _, _)) = [l]
val new_labels_of = maps new_labels_of_step
@@ -607,23 +659,26 @@
val index_in_shape = find_index o exists o curry (op =)
-fun direct_proof thy conjecture_shape hyp_ts concl_t proof =
+fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
let
val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
fun find_hyp (_, j) = nth hyp_ts (index_in_shape j conjecture_shape)
fun first_pass ([], contra) = ([], contra)
- | first_pass ((ps as Fix _) :: proof, contra) =
- first_pass (proof, contra) |>> cons ps
- | first_pass ((ps as Assume (l, t)) :: proof, contra) =
+ | first_pass ((step as Fix _) :: proof, contra) =
+ first_pass (proof, contra) |>> cons step
+ | first_pass ((step as Let _) :: proof, contra) =
+ first_pass (proof, contra) |>> cons step
+ | first_pass ((step as Assume (l, t)) :: proof, contra) =
if member (op =) concl_ls l then
- first_pass (proof, contra ||> cons ps)
+ first_pass (proof, contra ||> cons step)
else
first_pass (proof, contra) |>> cons (Assume (l, find_hyp l))
- | first_pass ((ps as Have (qs, l, t, Facts (ls, ss))) :: proof, contra) =
+ | first_pass ((step as Have (qs, l, t, Facts (ls, ss))) :: proof,
+ contra) =
if exists (member (op =) (fst contra)) ls then
- first_pass (proof, contra |>> cons l ||> cons ps)
+ first_pass (proof, contra |>> cons l ||> cons step)
else
- first_pass (proof, contra) |>> cons ps
+ first_pass (proof, contra) |>> cons step
| first_pass _ = raise Fail "malformed proof"
val (proof_top, (contra_ls, contra_proof)) =
first_pass (proof, (concl_ls, []))
@@ -690,20 +745,18 @@
end
| _ => raise Fail "malformed proof")
| second_pass _ _ = raise Fail "malformed proof"
- val (proof_bottom, _) =
- second_pass [Show] (contra_proof, [], ([], ([], [])))
+ val proof_bottom =
+ second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
in proof_top @ proof_bottom end
val kill_duplicate_assumptions_in_proof =
let
fun relabel_facts subst =
apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
- fun do_step (ps as Fix _) (proof, subst, assums) =
- (ps :: proof, subst, assums)
- | do_step (ps as Assume (l, t)) (proof, subst, assums) =
+ fun do_step (step as Assume (l, t)) (proof, subst, assums) =
(case AList.lookup (op aconv) assums t of
SOME l' => (proof, (l', l) :: subst, assums)
- | NONE => (ps :: proof, subst, (t, l) :: assums))
+ | NONE => (step :: proof, subst, (t, l) :: assums))
| do_step (Have (qs, l, t, by)) (proof, subst, assums) =
(Have (qs, l, t,
case by of
@@ -711,17 +764,29 @@
| CaseSplit (proofs, facts) =>
CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
proof, subst, assums)
+ | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
in do_proof end
-(* FIXME: implement *)
-fun shrink_proof shrink_factor proof = proof
+
+(* Hack: Could return false positives (e.g., a user happens to declare a
+ constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+ Long_Name.base_name
+ #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
+fun unskolemize_term t =
+ fold exists_of (Term.add_consts t []
+ |> filter (is_skolem_const_name o fst) |> map Const) t
+
+fun unskolemize_step (Have (qs, l, t, by)) =
+ Have (qs, l, unskolemize_term t, by)
+ | unskolemize_step step = step
val then_chain_proof =
let
fun aux _ [] = []
- | aux _ ((ps as Fix _) :: proof) = ps :: aux no_label proof
- | aux _ ((ps as Assume (l, _)) :: proof) = ps :: aux l proof
+ | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
| aux l' (Have (qs, l, t, by) :: proof) =
(case by of
Facts (ls, ss) =>
@@ -733,20 +798,21 @@
| CaseSplit (proofs, facts) =>
Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
aux l proof
+ | aux _ (step :: proof) = step :: aux no_label proof
in aux no_label end
fun kill_useless_labels_in_proof proof =
let
val used_ls = using_of proof
fun do_label l = if member (op =) used_ls l then l else no_label
- fun kill (Fix ts) = Fix ts
- | kill (Assume (l, t)) = Assume (do_label l, t)
+ fun kill (Assume (l, t)) = Assume (do_label l, t)
| kill (Have (qs, l, t, by)) =
Have (qs, do_label l, t,
case by of
CaseSplit (proofs, facts) =>
CaseSplit (map (map kill) proofs, facts)
| _ => by)
+ | kill step = step
in map kill proof end
fun prefix_for_depth n = replicate_string (n + 1)
@@ -754,8 +820,6 @@
val relabel_proof =
let
fun aux _ _ _ [] = []
- | aux subst depth nextp ((ps as Fix _) :: proof) =
- ps :: aux subst depth nextp proof
| aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
if l = no_label then
Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
@@ -773,7 +837,7 @@
let
val l' = (prefix_for_depth depth fact_prefix, next_fact)
in (l', (l, l') :: subst, next_fact + 1) end
- val relabel_facts = apfst (map (the o AList.lookup (op =) subst))
+ val relabel_facts = apfst (map_filter (AList.lookup (op =) subst))
val by =
case by of
Facts facts => Facts (relabel_facts facts)
@@ -784,11 +848,19 @@
Have (qs, l', t, by) ::
aux subst depth (next_assum, next_fact) proof
end
+ | aux subst depth nextp (step :: proof) =
+ step :: aux subst depth nextp proof
in aux [] 0 (1, 1) end
-fun string_for_proof ctxt sorts i n =
+fun string_for_proof ctxt i n =
let
+ fun fix_print_mode f =
+ PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) f
fun do_indent ind = replicate_string (ind * indent_size) " "
+ fun do_free (s, T) =
+ maybe_quote s ^ " :: " ^
+ maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
fun do_raw_label (s, j) = s ^ string_of_int j
fun do_label l = if l = no_label then "" else do_raw_label l ^ ": "
fun do_have qs =
@@ -798,29 +870,26 @@
if member (op =) qs Show then "thus" else "hence"
else
if member (op =) qs Show then "show" else "have")
- val do_term =
- quote o PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ()))
- (Syntax.string_of_term ctxt)
+ val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
fun do_using [] = ""
| do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
- fun do_by_facts [] [] = "by blast"
- | do_by_facts _ [] = "by metis"
- | do_by_facts _ ss = "by (metis " ^ space_implode " " ss ^ ")"
- fun do_facts ind (ls, ss) =
- do_indent (ind + 1) ^ do_using ls ^ do_by_facts ls ss
- and do_step ind (Fix ts) =
- do_indent ind ^ "fix " ^ space_implode " and " (map do_term ts) ^ "\n"
+ fun do_by_facts [] = "by metis"
+ | do_by_facts ss = "by (metis " ^ space_implode " " ss ^ ")"
+ fun do_facts (ls, ss) = do_using ls ^ do_by_facts ss
+ and do_step ind (Fix xs) =
+ do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
+ | do_step ind (Let (t1, t2)) =
+ do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
| do_step ind (Assume (l, t)) =
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
| do_step ind (Have (qs, l, t, Facts facts)) =
do_indent ind ^ do_have qs ^ " " ^
- do_label l ^ do_term t ^ "\n" ^ do_facts ind facts ^ "\n"
+ do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
| do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
space_implode (do_indent ind ^ "moreover\n")
(map (do_block ind) proofs) ^
- do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ "\n" ^
- do_facts ind facts ^ "\n"
+ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
+ do_facts facts ^ "\n"
and do_steps prefix suffix ind steps =
let val s = implode (map (do_step ind) steps) in
replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
@@ -829,14 +898,16 @@
suffix ^ "\n"
end
and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
- and do_proof proof =
- (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
- do_indent 0 ^ "proof -\n" ^
- do_steps "" "" 1 proof ^
- do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
- in setmp_CRITICAL show_sorts sorts do_proof end
+ (* One-step proofs are pointless; better use the Metis one-liner. *)
+ and do_proof [_] = ""
+ | do_proof proof =
+ (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
+ do_indent 0 ^ "proof -\n" ^
+ do_steps "" "" 1 proof ^
+ do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
+ in do_proof end
-fun isar_proof_text (pool, debug, shrink_factor, sorts, ctxt, conjecture_shape)
+fun isar_proof_text (pool, debug, shrink_factor, ctxt, conjecture_shape)
(minimize_command, atp_proof, thm_names, goal, i) =
let
val thy = ProofContext.theory_of ctxt
@@ -845,14 +916,15 @@
val (one_line_proof, lemma_names) =
metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
fun isar_proof_for () =
- case proof_from_atp_proof pool ctxt atp_proof thm_names frees
- |> direct_proof thy conjecture_shape hyp_ts concl_t
+ case proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names
+ frees
+ |> redirect_proof thy conjecture_shape hyp_ts concl_t
|> kill_duplicate_assumptions_in_proof
- |> shrink_proof shrink_factor
+ |> map unskolemize_step
|> then_chain_proof
|> kill_useless_labels_in_proof
|> relabel_proof
- |> string_for_proof ctxt sorts i n of
+ |> string_for_proof ctxt i n of
"" => ""
| proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Apr 28 17:29:58 2010 +0200
@@ -6,6 +6,7 @@
signature SLEDGEHAMMER_UTIL =
sig
+ val is_new_spass_version : bool
val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
val plural_s : int -> string
val serial_commas : string -> string list -> string list
@@ -14,11 +15,26 @@
val timestamp : unit -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
+ val nat_subscript : int -> string
+ val unyxml : string -> string
+ val maybe_quote : string -> string
end;
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
+val is_new_spass_version =
+ case getenv "SPASS_VERSION" of
+ "" => (case getenv "SPASS_HOME" of
+ "" => false
+ | s =>
+ (* Hack: Preliminary versions of the SPASS 3.7 package don't set
+ "SPASS_VERSION". *)
+ String.isSubstring "/spass-3.7/" s)
+ | s => (case s |> space_explode "." |> map Int.fromString of
+ SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
+ | _ => false)
+
fun pairf f g x = (f x, g x)
fun plural_s n = if n = 1 then "" else "s"
@@ -72,4 +88,19 @@
SOME (Time.fromMilliseconds msecs)
end
+val subscript = implode o map (prefix "\<^isub>") o explode
+val nat_subscript = subscript o string_of_int
+
+fun plain_string_from_xml_tree t =
+ Buffer.empty |> XML.add_content t |> Buffer.content
+val unyxml = plain_string_from_xml_tree o YXML.parse
+
+val is_long_identifier = forall Syntax.is_identifier o space_explode "."
+fun maybe_quote y =
+ let val s = unyxml y in
+ y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
+ not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
+ OuterKeyword.is_keyword s) ? quote
+ end
+
end;
--- a/src/HOL/Tools/inductive.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Apr 28 17:29:58 2010 +0200
@@ -323,11 +323,11 @@
(* prove monotonicity *)
-fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
+fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos ctxt =
(message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
" Proving monotonicity ...";
(if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
- [] []
+ (map (fst o dest_Free) params) []
(HOLogic.mk_Trueprop
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
(fn _ => EVERY [rtac @{thm monoI} 1,
@@ -689,7 +689,7 @@
||> Local_Theory.restore_naming lthy';
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
- val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
+ val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos lthy'';
val ((_, [mono']), lthy''') =
Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
--- a/src/Pure/Isar/class.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/Pure/Isar/class.ML Wed Apr 28 17:29:58 2010 +0200
@@ -100,10 +100,14 @@
(* reading and processing class specifications *)
-fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems =
+fun prep_class_elems prep_decl thy sups raw_elems =
let
(* user space type system: only permits 'a type variable, improves towards 'a *)
+ val algebra = Sign.classes_of thy;
+ val inter_sort = curry (Sorts.inter_sort algebra);
+ val proto_base_sort = if null sups then Sign.defaultS thy
+ else fold inter_sort (map (base_sort thy) sups) [];
val base_constraints = (map o apsnd)
(map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
(these_operations thy sups);
@@ -111,17 +115,17 @@
if v = Name.aT then T
else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
| T => T);
- fun singleton_fixate thy algebra Ts =
+ fun singleton_fixate Ts =
let
fun extract f = (fold o fold_atyps) f Ts [];
val tfrees = extract
(fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
val inferred_sort = extract
- (fn TVar (_, sort) => curry (Sorts.inter_sort algebra) sort | _ => I);
+ (fn TVar (_, sort) => inter_sort sort | _ => I);
val fixate_sort = if null tfrees then inferred_sort
else case tfrees
of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
- then Sorts.inter_sort algebra (a_sort, inferred_sort)
+ then inter_sort a_sort inferred_sort
else error ("Type inference imposes additional sort constraint "
^ Syntax.string_of_sort_global thy inferred_sort
^ " of type parameter " ^ Name.aT ^ " of sort "
@@ -136,7 +140,7 @@
val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
#> redeclare_operations thy sups
#> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
- #> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy));
+ #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
val raw_supexpr = (map (fn sup => (sup, (("", false),
Expression.Positional []))) sups, []);
val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
@@ -183,11 +187,10 @@
then error ("Duplicate parameter(s) in superclasses: "
^ (commas o map quote o duplicates (op =)) raw_supparam_names)
else ();
- val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
(* infer types and base sort *)
val (base_sort, supparam_names, supexpr, inferred_elems) =
- prep_class_elems thy sups given_basesort raw_elems;
+ prep_class_elems thy sups raw_elems;
val sup_sort = inter_sort base_sort sups;
(* process elements as class specification *)
@@ -287,8 +290,7 @@
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
#-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
- Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph
- (*FIXME should not modify base_morph, although admissible*)
+ Locale.add_registration (class, base_morph $> eq_morph (*FIXME duplication*)) (SOME (eq_morph, true)) export_morph
#> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
|> Theory_Target.init (SOME class)
|> pair class
--- a/src/Pure/Isar/class_target.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Wed Apr 28 17:29:58 2010 +0200
@@ -209,6 +209,9 @@
(eq_morph, true) (export_morphism thy cls) thy;
in fold amend (heritage thy [class]) thy end;
+(*fun activate_defs class thms thy = Locale.amend_registration (class, base_morphism thy class)
+ (Element.eq_morphism thy thms, true) (export_morphism thy class) thy;*)
+
fun register_operation class (c, (t, some_def)) thy =
let
val base_sort = base_sort thy class;
--- a/src/Tools/Code/code_eval.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Wed Apr 28 17:29:58 2010 +0200
@@ -9,7 +9,7 @@
val target: string
val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
-> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
- val evaluation_code: theory -> string list -> string list
+ val evaluation_code: theory -> string -> string list -> string list
-> string * ((string * string) list * (string * string) list)
val setup: theory -> theory
end;
@@ -23,12 +23,14 @@
val eval_struct_name = "Code";
-fun evaluation_code thy tycos consts =
+fun evaluation_code thy struct_name_hint tycos consts =
let
val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
+ val struct_name = if struct_name_hint = "" then eval_struct_name
+ else struct_name_hint;
val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
- eval_struct_name naming program (consts' @ tycos');
+ struct_name naming program (consts' @ tycos');
val (consts'', tycos'') = chop (length consts') target_names;
val consts_map = map2 (fn const => fn NONE =>
error ("Constant " ^ (quote o Code.string_of_const thy) const
@@ -84,7 +86,8 @@
val (struct_name', ctxt') = if struct_name = ""
then ML_Antiquote.variant eval_struct_name ctxt
else (struct_name, ctxt);
- val acc_code = Lazy.lazy (fn () => evaluation_code (ProofContext.theory_of ctxt) tycos' consts');
+ val acc_code = Lazy.lazy
+ (fn () => evaluation_code (ProofContext.theory_of ctxt) eval_struct_name tycos' consts');
in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
fun register_const const = register_code [] [const];
@@ -140,6 +143,71 @@
end; (*local*)
+(** reflection support **)
+
+fun check_datatype thy tyco consts =
+ let
+ val constrs = (map fst o snd o Code.get_type thy) tyco;
+ val missing_constrs = subtract (op =) consts constrs;
+ val _ = if null missing_constrs then []
+ else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
+ ^ " for datatype " ^ quote tyco);
+ val false_constrs = subtract (op =) constrs consts;
+ val _ = if null false_constrs then []
+ else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
+ ^ " for datatype " ^ quote tyco);
+ in () end;
+
+fun add_eval_tyco (tyco, tyco') thy =
+ let
+ val k = Sign.arity_number thy tyco;
+ fun pr pr' fxy [] = tyco'
+ | pr pr' fxy [ty] =
+ Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
+ | pr pr' fxy tys =
+ Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
+ in
+ thy
+ |> Code_Target.add_syntax_tyco target tyco (SOME (k, pr))
+ end;
+
+fun add_eval_const (const, const') = Code_Target.add_syntax_const target
+ const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
+
+fun process (code_body, (tyco_map, const_map)) module_name NONE thy =
+ let
+ val pr = Code_Printer.str o Long_Name.append module_name;
+ in
+ thy
+ |> Code_Target.add_reserved target module_name
+ |> Context.theory_map (ML_Context.exec (fn () => ML_Context.eval true Position.none code_body))
+ |> fold (add_eval_tyco o apsnd pr) tyco_map
+ |> fold (add_eval_const o apsnd pr) const_map
+ end
+ | process (code_body, _) _ (SOME file_name) thy =
+ let
+ val preamble = "(* Generated from " ^ Path.implode (ThyLoad.thy_path (Context.theory_name thy))
+ ^ "; DO NOT EDIT! *)";
+ val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
+ in
+ thy
+ end;
+
+fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy =
+ let
+ val datatypes = map (fn (raw_tyco, raw_cos) =>
+ (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
+ val functions = map (prep_const thy) raw_functions;
+ val _ = map (uncurry (check_datatype thy)) datatypes;
+ in
+ thy
+ |> process (evaluation_code thy module_name (map fst datatypes) (maps snd datatypes @ functions)) module_name some_file
+ end;
+
+val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const;
+val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
+
+
(** Isar setup **)
val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
@@ -148,6 +216,35 @@
-- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
>> ml_code_datatype_antiq);
+local
+
+structure P = OuterParse
+and K = OuterKeyword
+
+val datatypesK = "datatypes";
+val functionsK = "functions";
+val module_nameK = "module_name";
+val fileK = "file";
+val andK = "and"
+
+val _ = List.app K.keyword [datatypesK, functionsK];
+
+val parse_datatype = (P.name --| P.$$$ "=" -- (P.term ::: (Scan.repeat (P.$$$ "|" |-- P.term))));
+
+in
+
+val _ =
+ OuterSyntax.command "code_reflect" "enrich runtime environment with generated code"
+ K.thy_decl (Scan.optional (P.$$$ datatypesK |-- (parse_datatype
+ ::: Scan.repeat (P.$$$ andK |-- parse_datatype))) []
+ -- Scan.optional (P.$$$ functionsK |-- Scan.repeat1 P.name) []
+ --| P.$$$ module_nameK -- P.name
+ -- Scan.option (P.$$$ fileK |-- P.name)
+ >> (fn (((raw_datatypes, raw_functions), module_name), some_file) => Toplevel.theory
+ (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
+
+end; (*local*)
+
val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
end; (*struct*)
--- a/src/Tools/Code/code_target.ML Wed Apr 28 16:56:51 2010 +0200
+++ b/src/Tools/Code/code_target.ML Wed Apr 28 17:29:58 2010 +0200
@@ -6,6 +6,9 @@
signature CODE_TARGET =
sig
+ val cert_tyco: theory -> string -> string
+ val read_tyco: theory -> string -> string
+
type serializer
type literals = Code_Printer.literals
val add_target: string * (serializer * literals) -> theory -> theory