--- a/src/HOL/FunDef.thy Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/FunDef.thy Thu Apr 29 10:35:09 2010 +0200
@@ -314,8 +314,8 @@
ML_val -- "setup inactive"
{*
- Context.theory_map (Function_Common.set_termination_prover (ScnpReconstruct.decomp_scnp
- [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
+ Context.theory_map (Function_Common.set_termination_prover
+ (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
*}
end
--- a/src/HOL/IsaMakefile Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/IsaMakefile Thu Apr 29 10:35:09 2010 +0200
@@ -1295,8 +1295,8 @@
HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
- Quotient_Examples/FSet.thy \
- Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy
+ Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \
+ Quotient_Examples/Quotient_Message.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
--- a/src/HOL/Metis_Examples/BT.thy Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Metis_Examples/TransClosure.thy Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 29 10:35:09 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/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Thu Apr 29 10:35:09 2010 +0200
@@ -686,6 +686,13 @@
(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
+subsection {* Free function variable *}
+
+inductive FF :: "nat => nat => bool"
+where
+ "f x = y ==> FF x y"
+
+code_pred FF .
subsection {* IMP *}
--- a/src/HOL/Quotient_Examples/FSet.thy Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Thu Apr 29 10:35:09 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Quotient_Examples/Quotient.thy
+(* Title: HOL/Quotient_Examples/FSet.thy
Author: Cezary Kaliszyk, TU Munich
Author: Christian Urban, TU Munich
--- a/src/HOL/Quotient_Examples/LarryDatatype.thy Wed Apr 28 21:41:06 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,394 +0,0 @@
-theory LarryDatatype
-imports Main Quotient_Syntax
-begin
-
-subsection{*Defining the Free Algebra*}
-
-datatype
- freemsg = NONCE nat
- | MPAIR freemsg freemsg
- | CRYPT nat freemsg
- | DECRYPT nat freemsg
-
-inductive
- msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
-where
- CD: "CRYPT K (DECRYPT K X) \<sim> X"
-| DC: "DECRYPT K (CRYPT K X) \<sim> X"
-| NONCE: "NONCE N \<sim> NONCE N"
-| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
-| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
-| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
-| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
-| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
-
-lemmas msgrel.intros[intro]
-
-text{*Proving that it is an equivalence relation*}
-
-lemma msgrel_refl: "X \<sim> X"
-by (induct X, (blast intro: msgrel.intros)+)
-
-theorem equiv_msgrel: "equivp msgrel"
-proof (rule equivpI)
- show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
- show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
- show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
-qed
-
-subsection{*Some Functions on the Free Algebra*}
-
-subsubsection{*The Set of Nonces*}
-
-fun
- freenonces :: "freemsg \<Rightarrow> nat set"
-where
- "freenonces (NONCE N) = {N}"
-| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
-| "freenonces (CRYPT K X) = freenonces X"
-| "freenonces (DECRYPT K X) = freenonces X"
-
-theorem msgrel_imp_eq_freenonces:
- assumes a: "U \<sim> V"
- shows "freenonces U = freenonces V"
- using a by (induct) (auto)
-
-subsubsection{*The Left Projection*}
-
-text{*A function to return the left part of the top pair in a message. It will
-be lifted to the initial algrebra, to serve as an example of that process.*}
-fun
- freeleft :: "freemsg \<Rightarrow> freemsg"
-where
- "freeleft (NONCE N) = NONCE N"
-| "freeleft (MPAIR X Y) = X"
-| "freeleft (CRYPT K X) = freeleft X"
-| "freeleft (DECRYPT K X) = freeleft X"
-
-text{*This theorem lets us prove that the left function respects the
-equivalence relation. It also helps us prove that MPair
- (the abstract constructor) is injective*}
-lemma msgrel_imp_eqv_freeleft_aux:
- shows "freeleft U \<sim> freeleft U"
- by (induct rule: freeleft.induct) (auto)
-
-theorem msgrel_imp_eqv_freeleft:
- assumes a: "U \<sim> V"
- shows "freeleft U \<sim> freeleft V"
- using a
- by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
-
-subsubsection{*The Right Projection*}
-
-text{*A function to return the right part of the top pair in a message.*}
-fun
- freeright :: "freemsg \<Rightarrow> freemsg"
-where
- "freeright (NONCE N) = NONCE N"
-| "freeright (MPAIR X Y) = Y"
-| "freeright (CRYPT K X) = freeright X"
-| "freeright (DECRYPT K X) = freeright X"
-
-text{*This theorem lets us prove that the right function respects the
-equivalence relation. It also helps us prove that MPair
- (the abstract constructor) is injective*}
-lemma msgrel_imp_eqv_freeright_aux:
- shows "freeright U \<sim> freeright U"
- by (induct rule: freeright.induct) (auto)
-
-theorem msgrel_imp_eqv_freeright:
- assumes a: "U \<sim> V"
- shows "freeright U \<sim> freeright V"
- using a
- by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
-
-subsubsection{*The Discriminator for Constructors*}
-
-text{*A function to distinguish nonces, mpairs and encryptions*}
-fun
- freediscrim :: "freemsg \<Rightarrow> int"
-where
- "freediscrim (NONCE N) = 0"
- | "freediscrim (MPAIR X Y) = 1"
- | "freediscrim (CRYPT K X) = freediscrim X + 2"
- | "freediscrim (DECRYPT K X) = freediscrim X - 2"
-
-text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
-theorem msgrel_imp_eq_freediscrim:
- assumes a: "U \<sim> V"
- shows "freediscrim U = freediscrim V"
- using a by (induct) (auto)
-
-subsection{*The Initial Algebra: A Quotiented Message Type*}
-
-quotient_type msg = freemsg / msgrel
- by (rule equiv_msgrel)
-
-text{*The abstract message constructors*}
-
-quotient_definition
- "Nonce :: nat \<Rightarrow> msg"
-is
- "NONCE"
-
-quotient_definition
- "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-is
- "MPAIR"
-
-quotient_definition
- "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
- "CRYPT"
-
-quotient_definition
- "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
- "DECRYPT"
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
-by (auto intro: CRYPT)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
-by (auto intro: DECRYPT)
-
-text{*Establishing these two equations is the point of the whole exercise*}
-theorem CD_eq [simp]:
- shows "Crypt K (Decrypt K X) = X"
- by (lifting CD)
-
-theorem DC_eq [simp]:
- shows "Decrypt K (Crypt K X) = X"
- by (lifting DC)
-
-subsection{*The Abstract Function to Return the Set of Nonces*}
-
-quotient_definition
- "nonces:: msg \<Rightarrow> nat set"
-is
- "freenonces"
-
-text{*Now prove the four equations for @{term nonces}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freenonces freenonces"
- by (simp add: msgrel_imp_eq_freenonces)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim>) NONCE NONCE"
- by (simp add: NONCE)
-
-lemma nonces_Nonce [simp]:
- shows "nonces (Nonce N) = {N}"
- by (lifting freenonces.simps(1))
-
-lemma [quot_respect]:
- shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
- by (simp add: MPAIR)
-
-lemma nonces_MPair [simp]:
- shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
- by (lifting freenonces.simps(2))
-
-lemma nonces_Crypt [simp]:
- shows "nonces (Crypt K X) = nonces X"
- by (lifting freenonces.simps(3))
-
-lemma nonces_Decrypt [simp]:
- shows "nonces (Decrypt K X) = nonces X"
- by (lifting freenonces.simps(4))
-
-subsection{*The Abstract Function to Return the Left Part*}
-
-quotient_definition
- "left:: msg \<Rightarrow> msg"
-is
- "freeleft"
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
- by (simp add: msgrel_imp_eqv_freeleft)
-
-lemma left_Nonce [simp]:
- shows "left (Nonce N) = Nonce N"
- by (lifting freeleft.simps(1))
-
-lemma left_MPair [simp]:
- shows "left (MPair X Y) = X"
- by (lifting freeleft.simps(2))
-
-lemma left_Crypt [simp]:
- shows "left (Crypt K X) = left X"
- by (lifting freeleft.simps(3))
-
-lemma left_Decrypt [simp]:
- shows "left (Decrypt K X) = left X"
- by (lifting freeleft.simps(4))
-
-subsection{*The Abstract Function to Return the Right Part*}
-
-quotient_definition
- "right:: msg \<Rightarrow> msg"
-is
- "freeright"
-
-text{*Now prove the four equations for @{term right}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeright freeright"
- by (simp add: msgrel_imp_eqv_freeright)
-
-lemma right_Nonce [simp]:
- shows "right (Nonce N) = Nonce N"
- by (lifting freeright.simps(1))
-
-lemma right_MPair [simp]:
- shows "right (MPair X Y) = Y"
- by (lifting freeright.simps(2))
-
-lemma right_Crypt [simp]:
- shows "right (Crypt K X) = right X"
- by (lifting freeright.simps(3))
-
-lemma right_Decrypt [simp]:
- shows "right (Decrypt K X) = right X"
- by (lifting freeright.simps(4))
-
-subsection{*Injectivity Properties of Some Constructors*}
-
-lemma NONCE_imp_eq:
- shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
- by (drule msgrel_imp_eq_freenonces, simp)
-
-text{*Can also be proved using the function @{term nonces}*}
-lemma Nonce_Nonce_eq [iff]:
- shows "(Nonce m = Nonce n) = (m = n)"
-proof
- assume "Nonce m = Nonce n"
- then show "m = n" by (lifting NONCE_imp_eq)
-next
- assume "m = n"
- then show "Nonce m = Nonce n" by simp
-qed
-
-lemma MPAIR_imp_eqv_left:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
- by (drule msgrel_imp_eqv_freeleft) (simp)
-
-lemma MPair_imp_eq_left:
- assumes eq: "MPair X Y = MPair X' Y'"
- shows "X = X'"
- using eq by (lifting MPAIR_imp_eqv_left)
-
-lemma MPAIR_imp_eqv_right:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
- by (drule msgrel_imp_eqv_freeright) (simp)
-
-lemma MPair_imp_eq_right:
- shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
- by (lifting MPAIR_imp_eqv_right)
-
-theorem MPair_MPair_eq [iff]:
- shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
- by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
-
-lemma NONCE_neqv_MPAIR:
- shows "\<not>(NONCE m \<sim> MPAIR X Y)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Nonce_neq_MPair [iff]:
- shows "Nonce N \<noteq> MPair X Y"
- by (lifting NONCE_neqv_MPAIR)
-
-text{*Example suggested by a referee*}
-
-lemma CRYPT_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Crypt_Nonce_neq_Nonce:
- shows "Crypt K (Nonce M) \<noteq> Nonce N"
- by (lifting CRYPT_NONCE_neq_NONCE)
-
-text{*...and many similar results*}
-lemma CRYPT2_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Crypt2_Nonce_neq_Nonce:
- shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
- by (lifting CRYPT2_NONCE_neq_NONCE)
-
-theorem Crypt_Crypt_eq [iff]:
- shows "(Crypt K X = Crypt K X') = (X=X')"
-proof
- assume "Crypt K X = Crypt K X'"
- hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
- thus "X = X'" by simp
-next
- assume "X = X'"
- thus "Crypt K X = Crypt K X'" by simp
-qed
-
-theorem Decrypt_Decrypt_eq [iff]:
- shows "(Decrypt K X = Decrypt K X') = (X=X')"
-proof
- assume "Decrypt K X = Decrypt K X'"
- hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
- thus "X = X'" by simp
-next
- assume "X = X'"
- thus "Decrypt K X = Decrypt K X'" by simp
-qed
-
-lemma msg_induct_aux:
- shows "\<lbrakk>\<And>N. P (Nonce N);
- \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
- \<And>K X. P X \<Longrightarrow> P (Crypt K X);
- \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
- by (lifting freemsg.induct)
-
-lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
- assumes N: "\<And>N. P (Nonce N)"
- and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
- and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
- and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
- shows "P msg"
- using N M C D by (rule msg_induct_aux)
-
-subsection{*The Abstract Discriminator*}
-
-text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
-need this function in order to prove discrimination theorems.*}
-
-quotient_definition
- "discrim:: msg \<Rightarrow> int"
-is
- "freediscrim"
-
-text{*Now prove the four equations for @{term discrim}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freediscrim freediscrim"
- by (auto simp add: msgrel_imp_eq_freediscrim)
-
-lemma discrim_Nonce [simp]:
- shows "discrim (Nonce N) = 0"
- by (lifting freediscrim.simps(1))
-
-lemma discrim_MPair [simp]:
- shows "discrim (MPair X Y) = 1"
- by (lifting freediscrim.simps(2))
-
-lemma discrim_Crypt [simp]:
- shows "discrim (Crypt K X) = discrim X + 2"
- by (lifting freediscrim.simps(3))
-
-lemma discrim_Decrypt [simp]:
- shows "discrim (Decrypt K X) = discrim X - 2"
- by (lifting freediscrim.simps(4))
-
-end
-
--- a/src/HOL/Quotient_Examples/LarryInt.thy Wed Apr 28 21:41:06 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,395 +0,0 @@
-
-header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
-
-theory LarryInt
-imports Main Quotient_Product
-begin
-
-fun
- intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
- "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type int = "nat \<times> nat" / intrel
- by (auto simp add: equivp_def expand_fun_eq)
-
-instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
-begin
-
-quotient_definition
- Zero_int_def: "0::int" is "(0::nat, 0::nat)"
-
-quotient_definition
- One_int_def: "1::int" is "(1::nat, 0::nat)"
-
-definition
- "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
-
-quotient_definition
- "(op +) :: int \<Rightarrow> int \<Rightarrow> int"
-is
- "add_raw"
-
-definition
- "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
-
-quotient_definition
- "uminus :: int \<Rightarrow> int"
-is
- "uminus_raw"
-
-fun
- mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
-where
- "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
-
-quotient_definition
- "(op *) :: int \<Rightarrow> int \<Rightarrow> int"
-is
- "mult_raw"
-
-definition
- "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
-
-quotient_definition
- le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
-is
- "le_raw"
-
-definition
- less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
-
-definition
- diff_int_def: "z - (w::int) \<equiv> z + (-w)"
-
-instance ..
-
-end
-
-subsection{*Construction of the Integers*}
-
-lemma zminus_zminus_raw:
- "uminus_raw (uminus_raw z) = z"
- by (cases z) (simp add: uminus_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel) uminus_raw uminus_raw"
- by (simp add: uminus_raw_def)
-
-lemma zminus_zminus:
- fixes z::"int"
- shows "- (- z) = z"
- by(lifting zminus_zminus_raw)
-
-lemma zminus_0_raw:
- shows "uminus_raw (0, 0) = (0, 0::nat)"
- by (simp add: uminus_raw_def)
-
-lemma zminus_0:
- shows "- 0 = (0::int)"
- by (lifting zminus_0_raw)
-
-subsection{*Integer Addition*}
-
-lemma zminus_zadd_distrib_raw:
- shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
-by (cases z, cases w)
- (auto simp add: add_raw_def uminus_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
-by (simp add: add_raw_def)
-
-lemma zminus_zadd_distrib:
- fixes z w::"int"
- shows "- (z + w) = (- z) + (- w)"
- by(lifting zminus_zadd_distrib_raw)
-
-lemma zadd_commute_raw:
- shows "add_raw z w = add_raw w z"
-by (cases z, cases w)
- (simp add: add_raw_def)
-
-lemma zadd_commute:
- fixes z w::"int"
- shows "(z::int) + w = w + z"
- by (lifting zadd_commute_raw)
-
-lemma zadd_assoc_raw:
- shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
- by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
-
-lemma zadd_assoc:
- fixes z1 z2 z3::"int"
- shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
- by (lifting zadd_assoc_raw)
-
-lemma zadd_0_raw:
- shows "add_raw (0, 0) z = z"
- by (simp add: add_raw_def)
-
-
-text {*also for the instance declaration int :: plus_ac0*}
-lemma zadd_0:
- fixes z::"int"
- shows "0 + z = z"
- by (lifting zadd_0_raw)
-
-lemma zadd_zminus_inverse_raw:
- shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
- by (cases z) (simp add: add_raw_def uminus_raw_def)
-
-lemma zadd_zminus_inverse2:
- fixes z::"int"
- shows "(- z) + z = 0"
- by (lifting zadd_zminus_inverse_raw)
-
-subsection{*Integer Multiplication*}
-
-lemma zmult_zminus_raw:
- shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
-apply(cases z, cases w)
-apply(simp add: uminus_raw_def)
-done
-
-lemma mult_raw_fst:
- assumes a: "intrel x z"
- shows "intrel (mult_raw x y) (mult_raw z y)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma mult_raw_snd:
- assumes a: "intrel x z"
- shows "intrel (mult_raw y x) (mult_raw y z)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule equivp_transp[OF int_equivp])
-apply(rule mult_raw_fst)
-apply(assumption)
-apply(rule mult_raw_snd)
-apply(assumption)
-done
-
-lemma zmult_zminus:
- fixes z w::"int"
- shows "(- z) * w = - (z * w)"
- by (lifting zmult_zminus_raw)
-
-lemma zmult_commute_raw:
- shows "mult_raw z w = mult_raw w z"
-apply(cases z, cases w)
-apply(simp add: add_ac mult_ac)
-done
-
-lemma zmult_commute:
- fixes z w::"int"
- shows "z * w = w * z"
- by (lifting zmult_commute_raw)
-
-lemma zmult_assoc_raw:
- shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
-apply(cases z1, cases z2, cases z3)
-apply(simp add: add_mult_distrib2 mult_ac)
-done
-
-lemma zmult_assoc:
- fixes z1 z2 z3::"int"
- shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
- by (lifting zmult_assoc_raw)
-
-lemma zadd_mult_distrib_raw:
- shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
-apply(cases z1, cases z2, cases w)
-apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
-done
-
-lemma zadd_zmult_distrib:
- fixes z1 z2 w::"int"
- shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
- by(lifting zadd_mult_distrib_raw)
-
-lemma zadd_zmult_distrib2:
- fixes w z1 z2::"int"
- shows "w * (z1 + z2) = (w * z1) + (w * z2)"
- by (simp add: zmult_commute [of w] zadd_zmult_distrib)
-
-lemma zdiff_zmult_distrib:
- fixes w z1 z2::"int"
- shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
- by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
-
-lemma zdiff_zmult_distrib2:
- fixes w z1 z2::"int"
- shows "w * (z1 - z2) = (w * z1) - (w * z2)"
- by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
-
-lemmas int_distrib =
- zadd_zmult_distrib zadd_zmult_distrib2
- zdiff_zmult_distrib zdiff_zmult_distrib2
-
-lemma zmult_1_raw:
- shows "mult_raw (1, 0) z = z"
- by (cases z) (auto)
-
-lemma zmult_1:
- fixes z::"int"
- shows "1 * z = z"
- by (lifting zmult_1_raw)
-
-lemma zmult_1_right:
- fixes z::"int"
- shows "z * 1 = z"
- by (rule trans [OF zmult_commute zmult_1])
-
-lemma zero_not_one:
- shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
- by auto
-
-text{*The Integers Form A Ring*}
-instance int :: comm_ring_1
-proof
- fix i j k :: int
- show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
- show "i + j = j + i" by (simp add: zadd_commute)
- show "0 + i = i" by (rule zadd_0)
- show "- i + i = 0" by (rule zadd_zminus_inverse2)
- show "i - j = i + (-j)" by (simp add: diff_int_def)
- show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
- show "i * j = j * i" by (rule zmult_commute)
- show "1 * i = i" by (rule zmult_1)
- show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
- show "0 \<noteq> (1::int)" by (lifting zero_not_one)
-qed
-
-
-subsection{*The @{text "\<le>"} Ordering*}
-
-lemma zle_refl_raw:
- shows "le_raw w w"
- by (cases w) (simp add: le_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> op =) le_raw le_raw"
- by (auto) (simp_all add: le_raw_def)
-
-lemma zle_refl:
- fixes w::"int"
- shows "w \<le> w"
- by (lifting zle_refl_raw)
-
-
-lemma zle_trans_raw:
- shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
-apply(cases i, cases j, cases k)
-apply(auto simp add: le_raw_def)
-done
-
-lemma zle_trans:
- fixes i j k::"int"
- shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
- by (lifting zle_trans_raw)
-
-lemma zle_anti_sym_raw:
- shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
-apply(cases z, cases w)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_anti_sym:
- fixes z w::"int"
- shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
- by (lifting zle_anti_sym_raw)
-
-
-(* Axiom 'order_less_le' of class 'order': *)
-lemma zless_le:
- fixes w z::"int"
- shows "(w < z) = (w \<le> z & w \<noteq> z)"
- by (simp add: less_int_def)
-
-instance int :: order
-apply (default)
-apply(auto simp add: zless_le zle_anti_sym)[1]
-apply(rule zle_refl)
-apply(erule zle_trans, assumption)
-apply(erule zle_anti_sym, assumption)
-done
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-
-lemma zle_linear_raw:
- shows "le_raw z w \<or> le_raw w z"
-apply(cases w, cases z)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_linear:
- fixes z w::"int"
- shows "z \<le> w \<or> w \<le> z"
- by (lifting zle_linear_raw)
-
-instance int :: linorder
-apply(default)
-apply(rule zle_linear)
-done
-
-lemma zadd_left_mono_raw:
- shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
-apply(cases k)
-apply(auto simp add: add_raw_def le_raw_def)
-done
-
-lemma zadd_left_mono:
- fixes i j::"int"
- shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
- by (lifting zadd_left_mono_raw)
-
-
-subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
-
-definition
- "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
-
-quotient_definition
- "nat2::int \<Rightarrow> nat"
-is
- "nat_raw"
-
-abbreviation
- "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
-
-lemma nat_le_eq_zle_raw:
- shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
- apply (cases w)
- apply (cases z)
- apply (simp add: nat_raw_def le_raw_def)
- by auto
-
-lemma [quot_respect]:
- shows "(intrel ===> op =) nat_raw nat_raw"
- by (auto iff: nat_raw_def)
-
-lemma nat_le_eq_zle:
- fixes w z::"int"
- shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
- unfolding less_int_def
- by (lifting nat_le_eq_zle_raw)
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Thu Apr 29 10:35:09 2010 +0200
@@ -0,0 +1,380 @@
+(* Title: HOL/Quotient_Examples/Quotient_Int.thy
+ Author: Cezary Kaliszyk
+ Author: Christian Urban
+
+Integers based on Quotients, based on an older version by Larry Paulson.
+*)
+theory Quotient_Int
+imports Quotient_Product Nat
+begin
+
+fun
+ intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+ "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type int = "nat \<times> nat" / intrel
+ by (auto simp add: equivp_def expand_fun_eq)
+
+instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
+begin
+
+quotient_definition
+ "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
+
+quotient_definition
+ "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
+
+fun
+ plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
+
+quotient_definition
+ "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
+
+fun
+ uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "uminus_int_raw (x, y) = (y, x)"
+
+quotient_definition
+ "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
+
+definition
+ minus_int_def [code del]: "z - w = z + (-w\<Colon>int)"
+
+fun
+ times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_definition
+ "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+
+fun
+ le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+ "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
+
+quotient_definition
+ le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
+
+definition
+ less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
+
+definition
+ zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
+definition
+ zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
+
+instance ..
+
+end
+
+lemma [quot_respect]:
+ shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
+ and "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
+ and "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
+ by auto
+
+lemma times_int_raw_fst:
+ assumes a: "x \<approx> z"
+ shows "times_int_raw x y \<approx> times_int_raw z y"
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+ done
+
+lemma times_int_raw_snd:
+ assumes a: "x \<approx> z"
+ shows "times_int_raw y x \<approx> times_int_raw y z"
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+ done
+
+lemma [quot_respect]:
+ shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
+ apply(simp only: fun_rel_def)
+ apply(rule allI | rule impI)+
+ apply(rule equivp_transp[OF int_equivp])
+ apply(rule times_int_raw_fst)
+ apply(assumption)
+ apply(rule times_int_raw_snd)
+ apply(assumption)
+ done
+
+lemma plus_assoc_raw:
+ shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
+ by (cases i, cases j, cases k) (simp)
+
+lemma plus_sym_raw:
+ shows "plus_int_raw i j \<approx> plus_int_raw j i"
+ by (cases i, cases j) (simp)
+
+lemma plus_zero_raw:
+ shows "plus_int_raw (0, 0) i \<approx> i"
+ by (cases i) (simp)
+
+lemma plus_minus_zero_raw:
+ shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
+ by (cases i) (simp)
+
+lemma times_assoc_raw:
+ shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
+ by (cases i, cases j, cases k)
+ (simp add: algebra_simps)
+
+lemma times_sym_raw:
+ shows "times_int_raw i j \<approx> times_int_raw j i"
+ by (cases i, cases j) (simp add: algebra_simps)
+
+lemma times_one_raw:
+ shows "times_int_raw (1, 0) i \<approx> i"
+ by (cases i) (simp)
+
+lemma times_plus_comm_raw:
+ shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
+by (cases i, cases j, cases k)
+ (simp add: algebra_simps)
+
+lemma one_zero_distinct:
+ shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
+ by simp
+
+text{* The integers form a @{text comm_ring_1}*}
+
+instance int :: comm_ring_1
+proof
+ fix i j k :: int
+ show "(i + j) + k = i + (j + k)"
+ by (lifting plus_assoc_raw)
+ show "i + j = j + i"
+ by (lifting plus_sym_raw)
+ show "0 + i = (i::int)"
+ by (lifting plus_zero_raw)
+ show "- i + i = 0"
+ by (lifting plus_minus_zero_raw)
+ show "i - j = i + - j"
+ by (simp add: minus_int_def)
+ show "(i * j) * k = i * (j * k)"
+ by (lifting times_assoc_raw)
+ show "i * j = j * i"
+ by (lifting times_sym_raw)
+ show "1 * i = i"
+ by (lifting times_one_raw)
+ show "(i + j) * k = i * k + j * k"
+ by (lifting times_plus_comm_raw)
+ show "0 \<noteq> (1::int)"
+ by (lifting one_zero_distinct)
+qed
+
+lemma plus_int_raw_rsp_aux:
+ assumes a: "a \<approx> b" "c \<approx> d"
+ shows "plus_int_raw a c \<approx> plus_int_raw b d"
+ using a
+ by (cases a, cases b, cases c, cases d)
+ (simp)
+
+lemma add_abs_int:
+ "(abs_int (x,y)) + (abs_int (u,v)) =
+ (abs_int (x + u, y + v))"
+ apply(simp add: plus_int_def id_simps)
+ apply(fold plus_int_raw.simps)
+ apply(rule Quotient_rel_abs[OF Quotient_int])
+ apply(rule plus_int_raw_rsp_aux)
+ apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
+ done
+
+definition int_of_nat_raw:
+ "int_of_nat_raw m = (m :: nat, 0 :: nat)"
+
+quotient_definition
+ "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
+
+lemma[quot_respect]:
+ shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
+ by (simp add: equivp_reflp[OF int_equivp])
+
+lemma int_of_nat:
+ shows "of_nat m = int_of_nat m"
+ by (induct m)
+ (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
+
+lemma le_antisym_raw:
+ shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
+ by (cases i, cases j) (simp)
+
+lemma le_refl_raw:
+ shows "le_int_raw i i"
+ by (cases i) (simp)
+
+lemma le_trans_raw:
+ shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
+ by (cases i, cases j, cases k) (simp)
+
+lemma le_cases_raw:
+ shows "le_int_raw i j \<or> le_int_raw j i"
+ by (cases i, cases j)
+ (simp add: linorder_linear)
+
+instance int :: linorder
+proof
+ fix i j k :: int
+ show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
+ by (lifting le_antisym_raw)
+ show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
+ by (auto simp add: less_int_def dest: antisym)
+ show "i \<le> i"
+ by (lifting le_refl_raw)
+ show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
+ by (lifting le_trans_raw)
+ show "i \<le> j \<or> j \<le> i"
+ by (lifting le_cases_raw)
+qed
+
+instantiation int :: distrib_lattice
+begin
+
+definition
+ "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+ "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
+ by default
+ (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+
+end
+
+lemma le_plus_int_raw:
+ shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
+ by (cases i, cases j, cases k) (simp)
+
+instance int :: ordered_cancel_ab_semigroup_add
+proof
+ fix i j k :: int
+ show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+ by (lifting le_plus_int_raw)
+qed
+
+abbreviation
+ "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
+
+lemma zmult_zless_mono2_lemma:
+ fixes i j::int
+ and k::nat
+ shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
+ apply(induct "k")
+ apply(simp)
+ apply(case_tac "k = 0")
+ apply(simp_all add: left_distrib add_strict_mono)
+ done
+
+lemma zero_le_imp_eq_int_raw:
+ fixes k::"(nat \<times> nat)"
+ shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
+ apply(cases k)
+ apply(simp add:int_of_nat_raw)
+ apply(auto)
+ apply(rule_tac i="b" and j="a" in less_Suc_induct)
+ apply(auto)
+ done
+
+lemma zero_le_imp_eq_int:
+ fixes k::int
+ shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
+ unfolding less_int_def int_of_nat
+ by (lifting zero_le_imp_eq_int_raw)
+
+lemma zmult_zless_mono2:
+ fixes i j k::int
+ assumes a: "i < j" "0 < k"
+ shows "k * i < k * j"
+ using a
+ by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
+
+text{*The integers form an ordered integral domain*}
+
+instance int :: linordered_idom
+proof
+ fix i j k :: int
+ show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
+ by (rule zmult_zless_mono2)
+ show "\<bar>i\<bar> = (if i < 0 then -i else i)"
+ by (simp only: zabs_def)
+ show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+ by (simp only: zsgn_def)
+qed
+
+lemmas int_distrib =
+ left_distrib [of "z1::int" "z2" "w", standard]
+ right_distrib [of "w::int" "z1" "z2", standard]
+ left_diff_distrib [of "z1::int" "z2" "w", standard]
+ right_diff_distrib [of "w::int" "z1" "z2", standard]
+ minus_add_distrib[of "z1::int" "z2", standard]
+
+lemma int_induct_raw:
+ assumes a: "P (0::nat, 0)"
+ and b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))"
+ and c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))"
+ shows "P x"
+proof (cases x, clarify)
+ fix a b
+ show "P (a, b)"
+ proof (induct a arbitrary: b rule: Nat.induct)
+ case zero
+ show "P (0, b)" using assms by (induct b) auto
+ next
+ case (Suc n)
+ then show ?case using assms by auto
+ qed
+qed
+
+lemma int_induct:
+ fixes x :: int
+ assumes a: "P 0"
+ and b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
+ and c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
+ shows "P x"
+ using a b c unfolding minus_int_def
+ by (lifting int_induct_raw)
+
+text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
+
+definition
+ "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
+
+quotient_definition
+ "int_to_nat::int \<Rightarrow> nat"
+is
+ "int_to_nat_raw"
+
+lemma [quot_respect]:
+ shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
+ by (auto iff: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle_raw:
+ assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
+ shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
+ using a
+ by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle:
+ fixes w z::"int"
+ shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
+ unfolding less_int_def
+ by (lifting nat_le_eq_zle_raw)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Apr 29 10:35:09 2010 +0200
@@ -0,0 +1,399 @@
+(* Title: HOL/Quotient_Examples/Quotient_Message.thy
+ Author: Christian Urban
+
+Message datatype, based on an older version by Larry Paulson.
+*)
+theory Quotient_Message
+imports Main Quotient_Syntax
+begin
+
+subsection{*Defining the Free Algebra*}
+
+datatype
+ freemsg = NONCE nat
+ | MPAIR freemsg freemsg
+ | CRYPT nat freemsg
+ | DECRYPT nat freemsg
+
+inductive
+ msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
+where
+ CD: "CRYPT K (DECRYPT K X) \<sim> X"
+| DC: "DECRYPT K (CRYPT K X) \<sim> X"
+| NONCE: "NONCE N \<sim> NONCE N"
+| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
+| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
+| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
+| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
+| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
+
+lemmas msgrel.intros[intro]
+
+text{*Proving that it is an equivalence relation*}
+
+lemma msgrel_refl: "X \<sim> X"
+by (induct X, (blast intro: msgrel.intros)+)
+
+theorem equiv_msgrel: "equivp msgrel"
+proof (rule equivpI)
+ show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
+ show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
+ show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
+qed
+
+subsection{*Some Functions on the Free Algebra*}
+
+subsubsection{*The Set of Nonces*}
+
+fun
+ freenonces :: "freemsg \<Rightarrow> nat set"
+where
+ "freenonces (NONCE N) = {N}"
+| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
+| "freenonces (CRYPT K X) = freenonces X"
+| "freenonces (DECRYPT K X) = freenonces X"
+
+theorem msgrel_imp_eq_freenonces:
+ assumes a: "U \<sim> V"
+ shows "freenonces U = freenonces V"
+ using a by (induct) (auto)
+
+subsubsection{*The Left Projection*}
+
+text{*A function to return the left part of the top pair in a message. It will
+be lifted to the initial algrebra, to serve as an example of that process.*}
+fun
+ freeleft :: "freemsg \<Rightarrow> freemsg"
+where
+ "freeleft (NONCE N) = NONCE N"
+| "freeleft (MPAIR X Y) = X"
+| "freeleft (CRYPT K X) = freeleft X"
+| "freeleft (DECRYPT K X) = freeleft X"
+
+text{*This theorem lets us prove that the left function respects the
+equivalence relation. It also helps us prove that MPair
+ (the abstract constructor) is injective*}
+lemma msgrel_imp_eqv_freeleft_aux:
+ shows "freeleft U \<sim> freeleft U"
+ by (induct rule: freeleft.induct) (auto)
+
+theorem msgrel_imp_eqv_freeleft:
+ assumes a: "U \<sim> V"
+ shows "freeleft U \<sim> freeleft V"
+ using a
+ by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
+
+subsubsection{*The Right Projection*}
+
+text{*A function to return the right part of the top pair in a message.*}
+fun
+ freeright :: "freemsg \<Rightarrow> freemsg"
+where
+ "freeright (NONCE N) = NONCE N"
+| "freeright (MPAIR X Y) = Y"
+| "freeright (CRYPT K X) = freeright X"
+| "freeright (DECRYPT K X) = freeright X"
+
+text{*This theorem lets us prove that the right function respects the
+equivalence relation. It also helps us prove that MPair
+ (the abstract constructor) is injective*}
+lemma msgrel_imp_eqv_freeright_aux:
+ shows "freeright U \<sim> freeright U"
+ by (induct rule: freeright.induct) (auto)
+
+theorem msgrel_imp_eqv_freeright:
+ assumes a: "U \<sim> V"
+ shows "freeright U \<sim> freeright V"
+ using a
+ by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
+
+subsubsection{*The Discriminator for Constructors*}
+
+text{*A function to distinguish nonces, mpairs and encryptions*}
+fun
+ freediscrim :: "freemsg \<Rightarrow> int"
+where
+ "freediscrim (NONCE N) = 0"
+ | "freediscrim (MPAIR X Y) = 1"
+ | "freediscrim (CRYPT K X) = freediscrim X + 2"
+ | "freediscrim (DECRYPT K X) = freediscrim X - 2"
+
+text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
+theorem msgrel_imp_eq_freediscrim:
+ assumes a: "U \<sim> V"
+ shows "freediscrim U = freediscrim V"
+ using a by (induct) (auto)
+
+subsection{*The Initial Algebra: A Quotiented Message Type*}
+
+quotient_type msg = freemsg / msgrel
+ by (rule equiv_msgrel)
+
+text{*The abstract message constructors*}
+
+quotient_definition
+ "Nonce :: nat \<Rightarrow> msg"
+is
+ "NONCE"
+
+quotient_definition
+ "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "MPAIR"
+
+quotient_definition
+ "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "CRYPT"
+
+quotient_definition
+ "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "DECRYPT"
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
+by (auto intro: CRYPT)
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
+by (auto intro: DECRYPT)
+
+text{*Establishing these two equations is the point of the whole exercise*}
+theorem CD_eq [simp]:
+ shows "Crypt K (Decrypt K X) = X"
+ by (lifting CD)
+
+theorem DC_eq [simp]:
+ shows "Decrypt K (Crypt K X) = X"
+ by (lifting DC)
+
+subsection{*The Abstract Function to Return the Set of Nonces*}
+
+quotient_definition
+ "nonces:: msg \<Rightarrow> nat set"
+is
+ "freenonces"
+
+text{*Now prove the four equations for @{term nonces}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op =) freenonces freenonces"
+ by (simp add: msgrel_imp_eq_freenonces)
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim>) NONCE NONCE"
+ by (simp add: NONCE)
+
+lemma nonces_Nonce [simp]:
+ shows "nonces (Nonce N) = {N}"
+ by (lifting freenonces.simps(1))
+
+lemma [quot_respect]:
+ shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
+ by (simp add: MPAIR)
+
+lemma nonces_MPair [simp]:
+ shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
+ by (lifting freenonces.simps(2))
+
+lemma nonces_Crypt [simp]:
+ shows "nonces (Crypt K X) = nonces X"
+ by (lifting freenonces.simps(3))
+
+lemma nonces_Decrypt [simp]:
+ shows "nonces (Decrypt K X) = nonces X"
+ by (lifting freenonces.simps(4))
+
+subsection{*The Abstract Function to Return the Left Part*}
+
+quotient_definition
+ "left:: msg \<Rightarrow> msg"
+is
+ "freeleft"
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
+ by (simp add: msgrel_imp_eqv_freeleft)
+
+lemma left_Nonce [simp]:
+ shows "left (Nonce N) = Nonce N"
+ by (lifting freeleft.simps(1))
+
+lemma left_MPair [simp]:
+ shows "left (MPair X Y) = X"
+ by (lifting freeleft.simps(2))
+
+lemma left_Crypt [simp]:
+ shows "left (Crypt K X) = left X"
+ by (lifting freeleft.simps(3))
+
+lemma left_Decrypt [simp]:
+ shows "left (Decrypt K X) = left X"
+ by (lifting freeleft.simps(4))
+
+subsection{*The Abstract Function to Return the Right Part*}
+
+quotient_definition
+ "right:: msg \<Rightarrow> msg"
+is
+ "freeright"
+
+text{*Now prove the four equations for @{term right}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op \<sim>) freeright freeright"
+ by (simp add: msgrel_imp_eqv_freeright)
+
+lemma right_Nonce [simp]:
+ shows "right (Nonce N) = Nonce N"
+ by (lifting freeright.simps(1))
+
+lemma right_MPair [simp]:
+ shows "right (MPair X Y) = Y"
+ by (lifting freeright.simps(2))
+
+lemma right_Crypt [simp]:
+ shows "right (Crypt K X) = right X"
+ by (lifting freeright.simps(3))
+
+lemma right_Decrypt [simp]:
+ shows "right (Decrypt K X) = right X"
+ by (lifting freeright.simps(4))
+
+subsection{*Injectivity Properties of Some Constructors*}
+
+lemma NONCE_imp_eq:
+ shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
+ by (drule msgrel_imp_eq_freenonces, simp)
+
+text{*Can also be proved using the function @{term nonces}*}
+lemma Nonce_Nonce_eq [iff]:
+ shows "(Nonce m = Nonce n) = (m = n)"
+proof
+ assume "Nonce m = Nonce n"
+ then show "m = n" by (lifting NONCE_imp_eq)
+next
+ assume "m = n"
+ then show "Nonce m = Nonce n" by simp
+qed
+
+lemma MPAIR_imp_eqv_left:
+ shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
+ by (drule msgrel_imp_eqv_freeleft) (simp)
+
+lemma MPair_imp_eq_left:
+ assumes eq: "MPair X Y = MPair X' Y'"
+ shows "X = X'"
+ using eq by (lifting MPAIR_imp_eqv_left)
+
+lemma MPAIR_imp_eqv_right:
+ shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
+ by (drule msgrel_imp_eqv_freeright) (simp)
+
+lemma MPair_imp_eq_right:
+ shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
+ by (lifting MPAIR_imp_eqv_right)
+
+theorem MPair_MPair_eq [iff]:
+ shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
+ by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
+
+lemma NONCE_neqv_MPAIR:
+ shows "\<not>(NONCE m \<sim> MPAIR X Y)"
+ by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Nonce_neq_MPair [iff]:
+ shows "Nonce N \<noteq> MPair X Y"
+ by (lifting NONCE_neqv_MPAIR)
+
+text{*Example suggested by a referee*}
+
+lemma CRYPT_NONCE_neq_NONCE:
+ shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
+ by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Crypt_Nonce_neq_Nonce:
+ shows "Crypt K (Nonce M) \<noteq> Nonce N"
+ by (lifting CRYPT_NONCE_neq_NONCE)
+
+text{*...and many similar results*}
+lemma CRYPT2_NONCE_neq_NONCE:
+ shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
+ by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Crypt2_Nonce_neq_Nonce:
+ shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
+ by (lifting CRYPT2_NONCE_neq_NONCE)
+
+theorem Crypt_Crypt_eq [iff]:
+ shows "(Crypt K X = Crypt K X') = (X=X')"
+proof
+ assume "Crypt K X = Crypt K X'"
+ hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
+ thus "X = X'" by simp
+next
+ assume "X = X'"
+ thus "Crypt K X = Crypt K X'" by simp
+qed
+
+theorem Decrypt_Decrypt_eq [iff]:
+ shows "(Decrypt K X = Decrypt K X') = (X=X')"
+proof
+ assume "Decrypt K X = Decrypt K X'"
+ hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
+ thus "X = X'" by simp
+next
+ assume "X = X'"
+ thus "Decrypt K X = Decrypt K X'" by simp
+qed
+
+lemma msg_induct_aux:
+ shows "\<lbrakk>\<And>N. P (Nonce N);
+ \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
+ \<And>K X. P X \<Longrightarrow> P (Crypt K X);
+ \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
+ by (lifting freemsg.induct)
+
+lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
+ assumes N: "\<And>N. P (Nonce N)"
+ and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
+ and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
+ and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
+ shows "P msg"
+ using N M C D by (rule msg_induct_aux)
+
+subsection{*The Abstract Discriminator*}
+
+text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
+need this function in order to prove discrimination theorems.*}
+
+quotient_definition
+ "discrim:: msg \<Rightarrow> int"
+is
+ "freediscrim"
+
+text{*Now prove the four equations for @{term discrim}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op =) freediscrim freediscrim"
+ by (auto simp add: msgrel_imp_eq_freediscrim)
+
+lemma discrim_Nonce [simp]:
+ shows "discrim (Nonce N) = 0"
+ by (lifting freediscrim.simps(1))
+
+lemma discrim_MPair [simp]:
+ shows "discrim (MPair X Y) = 1"
+ by (lifting freediscrim.simps(2))
+
+lemma discrim_Crypt [simp]:
+ shows "discrim (Crypt K X) = discrim X + 2"
+ by (lifting freediscrim.simps(3))
+
+lemma discrim_Decrypt [simp]:
+ shows "discrim (Decrypt K X) = discrim X - 2"
+ by (lifting freediscrim.simps(4))
+
+end
+
--- a/src/HOL/Quotient_Examples/ROOT.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML Thu Apr 29 10:35:09 2010 +0200
@@ -4,5 +4,5 @@
Testing the quotient package.
*)
-use_thys ["FSet", "LarryInt", "LarryDatatype"];
+use_thys ["FSet", "Quotient_Int", "Quotient_Message"];
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Thu Apr 29 10:35:09 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/Function/fun.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML Thu Apr 29 10:35:09 2010 +0200
@@ -7,12 +7,12 @@
signature FUNCTION_FUN =
sig
- val add_fun : Function_Common.function_config ->
- (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
- bool -> local_theory -> Proof.context
- val add_fun_cmd : Function_Common.function_config ->
- (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
- bool -> local_theory -> Proof.context
+ val add_fun : (binding * typ option * mixfix) list ->
+ (Attrib.binding * term) list -> Function_Common.function_config ->
+ local_theory -> Proof.context
+ val add_fun_cmd : (binding * string option * mixfix) list ->
+ (Attrib.binding * string) list -> Function_Common.function_config ->
+ local_theory -> Proof.context
val setup : theory -> theory
end
@@ -56,15 +56,6 @@
()
end
-val by_pat_completeness_auto =
- Proof.global_future_terminal_proof
- (Method.Basic Pat_Completeness.pat_completeness,
- SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
-
-fun termination_by method int =
- Function.termination_proof NONE
- #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
-
fun mk_catchall fixes arity_of =
let
fun mk_eqn ((fname, fT), _) =
@@ -148,24 +139,32 @@
val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*),
domintros=false, partials=false, tailrec=false }
-fun gen_fun add config fixes statements int lthy =
- lthy
- |> add fixes statements config
- |> by_pat_completeness_auto int
- |> Local_Theory.restore
- |> termination_by (Function_Common.get_termination_prover lthy) int
+fun gen_add_fun add fixes statements config lthy =
+ let
+ fun pat_completeness_auto ctxt =
+ Pat_Completeness.pat_completeness_tac ctxt 1
+ THEN auto_tac (clasimpset_of ctxt)
+ fun prove_termination lthy =
+ Function.prove_termination NONE
+ (Function_Common.get_termination_prover lthy lthy) lthy
+ in
+ lthy
+ |> add fixes statements config pat_completeness_auto |> snd
+ |> Local_Theory.restore
+ |> prove_termination
+ end
-val add_fun = gen_fun Function.add_function
-val add_fun_cmd = gen_fun Function.add_function_cmd
+val add_fun = gen_add_fun Function.add_function
+val add_fun_cmd = gen_add_fun Function.add_function_cmd
local structure P = OuterParse and K = OuterKeyword in
val _ =
- OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
+ OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
(function_parser fun_config
- >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
+ >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config));
end
--- a/src/HOL/Tools/Function/function.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML Thu Apr 29 10:35:09 2010 +0200
@@ -11,14 +11,25 @@
val add_function: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> Function_Common.function_config ->
- local_theory -> Proof.state
+ (Proof.context -> tactic) -> local_theory -> info * local_theory
val add_function_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> Function_Common.function_config ->
+ (Proof.context -> tactic) -> local_theory -> info * local_theory
+
+ val function: (binding * typ option * mixfix) list ->
+ (Attrib.binding * term) list -> Function_Common.function_config ->
local_theory -> Proof.state
- val termination_proof : term option -> local_theory -> Proof.state
- val termination_proof_cmd : string option -> local_theory -> Proof.state
+ val function_cmd: (binding * string option * mixfix) list ->
+ (Attrib.binding * string) list -> Function_Common.function_config ->
+ local_theory -> Proof.state
+
+ val prove_termination: term option -> tactic -> local_theory -> local_theory
+ val prove_termination_cmd: string option -> tactic -> local_theory -> local_theory
+
+ val termination : term option -> local_theory -> Proof.state
+ val termination_cmd : string option -> local_theory -> Proof.state
val setup : theory -> theory
val get_congs : Proof.context -> thm list
@@ -65,7 +76,7 @@
(saved_simps, fold2 add_for_f fnames simps_by_f lthy)
end
-fun gen_add_function is_external prep default_constraint fixspec eqns config lthy =
+fun prepare_function is_external prep default_constraint fixspec eqns config lthy =
let
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
@@ -76,7 +87,7 @@
val defname = mk_defname fixes
val FunctionConfig {partials, ...} = config
- val ((goalstate, cont), lthy) =
+ val ((goal_state, cont), lthy') =
Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
fun afterqed [[proof]] lthy =
@@ -115,20 +126,45 @@
if not is_external then ()
else Specification.print_consts lthy (K false) (map fst fixes)
in
- lthy
- |> Local_Theory.declaration false (add_function_data o morph_function_data info)
+ (info,
+ lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
end
in
- lthy
- |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
- |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
+ ((goal_state, afterqed), lthy')
+ end
+
+fun gen_add_function is_external prep default_constraint fixspec eqns config tac lthy =
+ let
+ val ((goal_state, afterqed), lthy') =
+ prepare_function is_external prep default_constraint fixspec eqns config lthy
+ val pattern_thm =
+ case SINGLE (tac lthy') goal_state of
+ NONE => error "pattern completeness and compatibility proof failed"
+ | SOME st => Goal.finish lthy' st
+ in
+ lthy'
+ |> afterqed [[pattern_thm]]
end
val add_function =
gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
-
-fun gen_termination_proof prep_term raw_term_opt lthy =
+
+fun gen_function is_external prep default_constraint fixspec eqns config lthy =
+ let
+ val ((goal_state, afterqed), lthy') =
+ prepare_function is_external prep default_constraint fixspec eqns config lthy
+ in
+ lthy'
+ |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
+ |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
+ end
+
+val function =
+ gen_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+val function_cmd = gen_function true Specification.read_spec "_::type"
+
+fun prepare_termination_proof prep_term raw_term_opt lthy =
let
val term_opt = Option.map (prep_term lthy) raw_term_opt
val info = the (case term_opt of
@@ -169,6 +205,26 @@
end)
end
in
+ (goal, afterqed, termination)
+ end
+
+fun gen_prove_termination prep_term raw_term_opt tac lthy =
+ let
+ val (goal, afterqed, termination) =
+ prepare_termination_proof prep_term raw_term_opt lthy
+
+ val totality = Goal.prove lthy [] [] goal (K tac)
+ in
+ afterqed [[totality]] lthy
+end
+
+val prove_termination = gen_prove_termination Syntax.check_term
+val prove_termination_cmd = gen_prove_termination Syntax.read_term
+
+fun gen_termination prep_term raw_term_opt lthy =
+ let
+ val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
+ in
lthy
|> ProofContext.note_thmss ""
[((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
@@ -180,8 +236,8 @@
|> Proof.theorem NONE afterqed [[(goal, [])]]
end
-val termination_proof = gen_termination_proof Syntax.check_term
-val termination_proof_cmd = gen_termination_proof Syntax.read_term
+val termination = gen_termination Syntax.check_term
+val termination_cmd = gen_termination Syntax.read_term
(* Datatype hook to declare datatype congs as "function_congs" *)
@@ -221,11 +277,11 @@
val _ =
OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
(function_parser default_config
- >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config))
+ >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
val _ =
OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
- (Scan.option P.term >> termination_proof_cmd)
+ (Scan.option P.term >> termination_cmd)
end
--- a/src/HOL/Tools/Function/function_common.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Thu Apr 29 10:35:09 2010 +0200
@@ -172,7 +172,7 @@
structure TerminationProver = Generic_Data
(
- type T = Proof.context -> Proof.method
+ type T = Proof.context -> tactic
val empty = (fn _ => error "Termination prover not configured")
val extend = I
fun merge (a, b) = b (* FIXME ? *)
--- a/src/HOL/Tools/Function/lexicographic_order.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Apr 29 10:35:09 2010 +0200
@@ -225,6 +225,6 @@
Method.setup @{binding lexicographic_order}
(Method.sections clasimp_modifiers >> (K lexicographic_order))
"termination prover for lexicographic orderings"
- #> Context.theory_map (Function_Common.set_termination_prover lexicographic_order)
+ #> Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
end;
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Apr 29 10:35:09 2010 +0200
@@ -10,7 +10,7 @@
val sizechange_tac : Proof.context -> tactic -> tactic
- val decomp_scnp : ScnpSolve.label list -> Proof.context -> Proof.method
+ val decomp_scnp_tac : ScnpSolve.label list -> Proof.context -> tactic
val setup : theory -> theory
@@ -396,13 +396,12 @@
fun sizechange_tac ctxt autom_tac =
gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt (K (K all_tac))
-fun decomp_scnp orders ctxt =
+fun decomp_scnp_tac orders ctxt =
let
val extra_simps = Function_Common.Termination_Simps.get ctxt
val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
in
- SIMPLE_METHOD
- (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
+ gen_sizechange_tac orders autom_tac ctxt (print_error ctxt)
end
@@ -416,7 +415,8 @@
|| Scan.succeed [MAX, MS, MIN]
val setup = Method.setup @{binding size_change}
- (Scan.lift orders --| Method.sections clasimp_modifiers >> decomp_scnp)
+ (Scan.lift orders --| Method.sections clasimp_modifiers >>
+ (fn orders => SIMPLE_METHOD o decomp_scnp_tac orders))
"termination prover with graph decomposition and the NP subset of size change termination"
end
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Apr 29 10:35:09 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/Predicate_Compile/predicate_compile_core.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Apr 29 10:35:09 2010 +0200
@@ -529,16 +529,19 @@
fun instantiate i n {context = ctxt, params = p, prems = prems,
asms = a, concl = cl, schematics = s} =
let
+ fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
+ fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
+ |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
val case_th = MetaSimplifier.simplify true
- (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs)
- (nth cases (i - 1))
+ (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
- val (_, tenv) = fold (Pattern.match thy) pats (Vartab.empty, Vartab.empty)
- fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
- val inst = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
- val thesis = Thm.instantiate ([], inst) case_th OF (replicate nargs @{thm refl}) OF prems'
+ val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
+ OF (replicate nargs @{thm refl})
+ val thesis =
+ Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th'
+ OF prems'
in
(rtac thesis 1)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Apr 29 10:35:09 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 21:41:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Apr 29 10:35:09 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/HOLCF/IOA/meta_theory/Sequence.thy Wed Apr 28 21:41:06 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Thu Apr 29 10:35:09 2010 +0200
@@ -10,7 +10,7 @@
default_sort type
-types 'a Seq = "'a::type lift seq"
+types 'a Seq = "'a lift seq"
consts
--- a/src/Pure/Isar/typedecl.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML Thu Apr 29 10:35:09 2010 +0200
@@ -82,10 +82,12 @@
(* type abbreviations *)
+local
+
fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy =
let
val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
- val rhs = prep_typ lthy raw_rhs
+ val rhs = prep_typ b lthy raw_rhs
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
in
lthy
@@ -94,8 +96,23 @@
|> pair name
end;
-val abbrev = gen_abbrev ProofContext.cert_typ_syntax;
-val abbrev_cmd = gen_abbrev ProofContext.read_typ_syntax;
+fun read_abbrev b ctxt raw_rhs =
+ let
+ val rhs = ProofContext.read_typ_syntax (ctxt |> ProofContext.set_defsort []) raw_rhs;
+ val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
+ val _ =
+ if null ignored then ()
+ else warning ("Ignoring sort constraints in type variables(s): " ^
+ commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
+ "\nin type abbreviation " ^ quote (Binding.str_of b));
+ in rhs end;
+
+in
+
+val abbrev = gen_abbrev (K ProofContext.cert_typ_syntax);
+val abbrev_cmd = gen_abbrev read_abbrev;
+
+end;
fun abbrev_global decl rhs =
Theory_Target.init NONE
--- a/src/Pure/axclass.ML Wed Apr 28 21:41:06 2010 +0200
+++ b/src/Pure/axclass.ML Thu Apr 29 10:35:09 2010 +0200
@@ -190,9 +190,9 @@
infix 0 RSO;
-fun (SOME a RSO SOME b) = SOME (a RS b)
- | (x RSO NONE) = x
- | (NONE RSO y) = y;
+fun (SOME a) RSO (SOME b) = SOME (a RS b)
+ | x RSO NONE = x
+ | NONE RSO y = y;
fun the_classrel thy (c1, c2) =
(case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
--- a/src/Tools/jEdit/README_BUILD Wed Apr 28 21:41:06 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD Thu Apr 29 10:35:09 2010 +0200
@@ -74,3 +74,17 @@
releases. (See
http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html)
-----------------------------------------------------------------------
+
+
+Known problems with Mac OS
+==========================
+
+- The MacOSX plugin disrupts regular C-X/C/V operations, e.g. between
+ the editor and the Console plugin, which is a standard swing text
+ box. Similar for search boxes etc.
+
+- Anti-aliasing does not really work as well as for Linux or Windows.
+ (General Apple/Swing problem?)
+
+- Font.createFont mangles the font family of non-regular fonts,
+ e.g. bold.