--- a/Admin/isatest/isatest-makedist Fri Nov 20 07:24:08 2009 +0100
+++ b/Admin/isatest/isatest-makedist Fri Nov 20 07:24:21 2009 +0100
@@ -104,15 +104,15 @@
sleep 15
$SSH macbroy23 "$MAKEALL -l HOL images $HOME/settings/at-sml-dev-e"
sleep 15
-$SSH atbroy99 "$MAKEALL $HOME/settings/at64-poly"
+$SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8; $MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
sleep 15
$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
sleep 15
$SSH macbroy6 "sleep 10800; $MAKEALL $HOME/settings/at-mac-poly-5.1-para"
-sleep 15
-$SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly"
+#sleep 15
+#$SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly"
echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
--- a/CONTRIBUTORS Fri Nov 20 07:24:08 2009 +0100
+++ b/CONTRIBUTORS Fri Nov 20 07:24:21 2009 +0100
@@ -7,6 +7,9 @@
Contributions to this Isabelle version
--------------------------------------
+* November 2009: Robert Himmelmann, TUM
+ Derivation and Brouwer's fixpoint theorem in Multivariate Analysis
+
* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM
A tabled implementation of the reflexive transitive closure
--- a/NEWS Fri Nov 20 07:24:08 2009 +0100
+++ b/NEWS Fri Nov 20 07:24:21 2009 +0100
@@ -96,6 +96,14 @@
zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
INCOMPATIBILITY.
+* Extended Multivariate Analysis to include derivation and Brouwer's fixpoint
+theorem.
+
+* Removed predicate "M hassize n" (<--> card M = n & finite M). Was only used
+in Multivariate Analysis. Renamed vector_less_eq_def to vector_le_def, the
+more usual name.
+INCOMPATIBILITY.
+
* Added theorem List.map_map as [simp]. Removed List.map_compose.
INCOMPATIBILITY.
--- a/doc-src/TutorialI/Types/numerics.tex Fri Nov 20 07:24:08 2009 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Fri Nov 20 07:24:21 2009 +0100
@@ -347,8 +347,7 @@
\ 1.\ P\ (2\ /\ 5)
\end{isabelle}
Exponentiation can express floating-point values such as
-\isa{2 * 10\isacharcircum6}, but at present no special simplification
-is performed.
+\isa{2 * 10\isacharcircum6}, which will be simplified to integers.
\begin{warn}
Types \isa{rat}, \isa{real} and \isa{complex} are provided by theory HOL-Complex, which is
--- a/src/HOL/HOL.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/HOL.thy Fri Nov 20 07:24:21 2009 +0100
@@ -2060,7 +2060,6 @@
setup {*
Predicate_Compile_Alternative_Defs.setup
#> Predicate_Compile_Inline_Defs.setup
- #> Predicate_Compile_Preproc_Const_Defs.setup
*}
--- a/src/HOL/Library/SML_Quickcheck.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Library/SML_Quickcheck.thy Fri Nov 20 07:24:21 2009 +0100
@@ -6,6 +6,7 @@
begin
setup {*
+ InductiveCodegen.quickcheck_setup #>
Quickcheck.add_generator ("SML", Codegen.test_term)
*}
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Nov 20 07:24:21 2009 +0100
@@ -13,8 +13,8 @@
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
-(* Author: John Harrison
- Translated to from HOL light: Robert Himmelmann, TU Muenchen *)
+(* Author: John Harrison
+ Translation from HOL light: Robert Himmelmann, TU Muenchen *)
header {* Results connected with topological dimension. *}
@@ -1562,12 +1562,12 @@
obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
- hence "a \<le> b" unfolding interval_eq_empty vector_less_eq_def by(auto simp add: not_less)
- thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding vector_less_eq_def forall_2 by auto
+ hence "a \<le> b" unfolding interval_eq_empty vector_le_def by(auto simp add: not_less)
+ thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding vector_le_def forall_2 by auto
next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component)
apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
- unfolding pathstart_def by(auto simp add: vector_less_eq_def) then guess z .. note z=this
+ unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast
hence "z = f 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
using assms(3)[unfolded path_image_def subset_eq mem_interval,rule_format,of "f 0" 1]
@@ -1576,7 +1576,7 @@
next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component)
apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
- unfolding pathstart_def by(auto simp add: vector_less_eq_def) then guess z .. note z=this
+ unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast
hence "z = g 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
using assms(4)[unfolded path_image_def subset_eq mem_interval,rule_format,of "g 0" 2]
@@ -1693,7 +1693,7 @@
path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
by(auto simp add: pathstart_join pathfinish_join path_image_join path_image_linepath path_join path_linepath)
- have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_less_eq_def forall_2 vector_2)
+ have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2)
guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
show "path ?P1" "path ?P2" using assms by(auto simp add: pathstart_join pathfinish_join path_join)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 20 07:24:21 2009 +0100
@@ -23,7 +23,7 @@
lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto
-lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_less_eq_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component
+lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component
lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id
@@ -61,7 +61,7 @@
lemma mem_interval_1: fixes x :: "real^1" shows
"(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
"(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def all_1)
+by(simp_all add: Cart_eq vector_less_def vector_le_def dest_vec1_def all_1)
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} =
(if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
@@ -77,7 +77,7 @@
apply(rule_tac [!] allI)apply(rule_tac [!] impI)
apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
- by (auto simp add: vector_less_def vector_less_eq_def all_1 dest_vec1_def
+ by (auto simp add: vector_less_def vector_le_def all_1 dest_vec1_def
vec1_dest_vec1[unfolded dest_vec1_def One_nat_def])
lemma dest_vec1_setsum: assumes "finite S"
@@ -2354,7 +2354,7 @@
assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
shows "\<exists>x\<in>{a..b}. (f x)$k = y"
proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI)
- using assms(1) by(auto simp add: vector_less_eq_def dest_vec1_def)
+ using assms(1) by(auto simp add: vector_le_def dest_vec1_def)
thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y]
using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]]
using assms by(auto intro!: imageI) qed
@@ -2415,10 +2415,10 @@
show ?thesis proof(cases "x$i=1")
case True have "\<forall>j\<in>{i. x$i \<noteq> 0}. x$j = 1" apply(rule, rule ccontr) unfolding mem_Collect_eq proof-
fix j assume "x $ j \<noteq> 0" "x $ j \<noteq> 1"
- hence j:"x$j \<in> {0<..<1}" using Suc(2) by(auto simp add: vector_less_eq_def elim!:allE[where x=j])
+ hence j:"x$j \<in> {0<..<1}" using Suc(2) by(auto simp add: vector_le_def elim!:allE[where x=j])
hence "x$j \<in> op $ x ` {i. x $ i \<noteq> 0}" by auto
hence "x$j \<ge> x$i" unfolding i'(1) xi_def apply(rule_tac Min_le) by auto
- thus False using True Suc(2) j by(auto simp add: vector_less_eq_def elim!:ballE[where x=j]) qed
+ thus False using True Suc(2) j by(auto simp add: vector_le_def elim!:ballE[where x=j]) qed
thus "x\<in>convex hull ?points" apply(rule_tac hull_subset[unfolded subset_eq, rule_format])
by(auto simp add: Cart_lambda_beta)
next let ?y = "\<lambda>j. if x$j = 0 then 0 else (x$j - x$i) / (1 - x$i)"
@@ -2439,7 +2439,7 @@
show ?thesis apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule
apply(rule_tac n2="CARD('n)" in *) prefer 3 apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
- by(auto simp add: vector_less_eq_def mem_def[of _ convex]) qed
+ by(auto simp add: vector_le_def mem_def[of _ convex]) qed
subsection {* And this is a finite set of vertices. *}
@@ -2469,7 +2469,7 @@
hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..1}" unfolding mem_interval using assms
by(auto simp add: Cart_eq vector_component_simps field_simps)
thus "\<exists>z\<in>{0..1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
- using assms by(auto simp add: Cart_eq vector_less_eq_def Cart_lambda_beta)
+ using assms by(auto simp add: Cart_eq vector_le_def Cart_lambda_beta)
next
fix y z assume as:"z\<in>{0..1}" "y = x - ?d + (2*d) *\<^sub>R z"
have "\<And>i. 0 \<le> d * z $ i \<and> d * z $ i \<le> d" using assms as(1)[unfolded mem_interval] apply(erule_tac x=i in allE)
@@ -2911,7 +2911,7 @@
lemma path_image_reversepath[simp]: "path_image(reversepath g) = path_image g" proof-
have *:"\<And>g. path_image(reversepath g) \<subseteq> path_image g"
unfolding path_image_def subset_eq reversepath_def Ball_def image_iff apply(rule,rule,erule bexE)
- apply(rule_tac x="1 - xa" in bexI) by(auto simp add:vector_less_eq_def vector_component_simps elim!:ballE)
+ apply(rule_tac x="1 - xa" in bexI) by(auto simp add:vector_le_def vector_component_simps elim!:ballE)
show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed
lemma path_reversepath[simp]: "path(reversepath g) \<longleftrightarrow> path g" proof-
@@ -2919,7 +2919,7 @@
apply(rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id)
apply(rule continuous_on_subset[of "{0..1}"], assumption)
- by (auto, auto simp add:vector_less_eq_def vector_component_simps elim!:ballE)
+ by (auto, auto simp add:vector_le_def vector_component_simps elim!:ballE)
show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed
lemmas reversepath_simps = path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath
@@ -2930,7 +2930,7 @@
have *:"g1 = (\<lambda>x. g1 (2 *\<^sub>R x)) \<circ> (\<lambda>x. (1/2) *\<^sub>R x)"
"g2 = (\<lambda>x. g2 (2 *\<^sub>R x - 1)) \<circ> (\<lambda>x. (1/2) *\<^sub>R (x + 1))" unfolding o_def by auto
have "op *\<^sub>R (1 / 2) ` {0::real^1..1} \<subseteq> {0..1}" "(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real^1)..1} \<subseteq> {0..1}"
- unfolding image_smult_interval by (auto, auto simp add:vector_less_eq_def vector_component_simps elim!:ballE)
+ unfolding image_smult_interval by (auto, auto simp add:vector_le_def vector_component_simps elim!:ballE)
thus "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" apply -apply rule
apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose)
apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Nov 20 07:24:21 2009 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Library/Convex_Euclidean_Space.thy
- Author: John Harrison
- Translated to from HOL light: Robert Himmelmann, TU Muenchen *)
+ Author: John Harrison
+ Translation from HOL light: Robert Himmelmann, TU Muenchen *)
header {* Multivariate calculus in Euclidean space. *}
@@ -627,7 +627,7 @@
subsection {* The traditional Rolle theorem in one dimension. *}
lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
- unfolding vector_less_eq_def by auto
+ unfolding vector_le_def by auto
lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
unfolding vector_less_def by auto
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Nov 20 07:24:21 2009 +0100
@@ -94,7 +94,7 @@
instantiation "^" :: (ord,type) ord
begin
-definition vector_less_eq_def:
+definition vector_le_def:
"less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Nov 20 07:24:21 2009 +0100
@@ -4619,17 +4619,17 @@
lemma interval: fixes a :: "'a::ord^'n::finite" shows
"{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
"{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
- by (auto simp add: expand_set_eq vector_less_def vector_less_eq_def)
+ by (auto simp add: expand_set_eq vector_less_def vector_le_def)
lemma mem_interval: fixes a :: "'a::ord^'n::finite" shows
"x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
"x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
- using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_less_eq_def)
+ using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def)
lemma mem_interval_1: fixes x :: "real^1" shows
"(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
"(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def forall_1)
+by(simp_all add: Cart_eq vector_less_def vector_le_def dest_vec1_def forall_1)
lemma vec1_interval:fixes a::"real" shows
"vec1 ` {a .. b} = {vec1 a .. vec1 b}"
@@ -4690,7 +4690,7 @@
lemma interval_sing: fixes a :: "'a::linorder^'n::finite" shows
"{a .. a} = {a} \<and> {a<..<a} = {}"
-apply(auto simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq)
+apply(auto simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
apply (simp add: order_eq_iff)
apply (auto simp add: not_less less_imp_le)
done
@@ -4703,17 +4703,17 @@
{ fix i
have "a $ i \<le> x $ i"
using x order_less_imp_le[of "a$i" "x$i"]
- by(simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq)
+ by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
}
moreover
{ fix i
have "x $ i \<le> b $ i"
using x order_less_imp_le[of "x$i" "b$i"]
- by(simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq)
+ by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
}
ultimately
show "a \<le> x \<and> x \<le> b"
- by(simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq)
+ by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
qed
lemma subset_interval: fixes a :: "real^'n::finite" shows
@@ -5026,12 +5026,12 @@
lemma interval_cases_1: fixes x :: "real^1" shows
"x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
- by(simp add: Cart_eq vector_less_def vector_less_eq_def all_1, auto)
+ by(simp add: Cart_eq vector_less_def vector_le_def all_1, auto)
lemma in_interval_1: fixes x :: "real^1" shows
"(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp add: Cart_eq vector_less_def vector_less_eq_def all_1 dest_vec1_def)
+by(simp add: Cart_eq vector_less_def vector_le_def all_1 dest_vec1_def)
lemma interval_eq_empty_1: fixes a :: "real^1" shows
"{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
@@ -5067,10 +5067,10 @@
lemma open_closed_interval_1: fixes a :: "real^1" shows
"{a<..<b} = {a .. b} - {a, b}"
- unfolding expand_set_eq apply simp unfolding vector_less_def and vector_less_eq_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
+ unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
- unfolding expand_set_eq apply simp unfolding vector_less_def and vector_less_eq_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
+ unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
(* Some stuff for half-infinite intervals too; FIXME: notation? *)
@@ -5742,30 +5742,30 @@
else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
proof(cases "m=0")
{ fix x assume "x \<le> c" "c \<le> x"
- hence "x=c" unfolding vector_less_eq_def and Cart_eq by (auto intro: order_antisym) }
+ hence "x=c" unfolding vector_le_def and Cart_eq by (auto intro: order_antisym) }
moreover case True
- moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}" unfolding True by(auto simp add: vector_less_eq_def)
+ moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}" unfolding True by(auto simp add: vector_le_def)
ultimately show ?thesis by auto
next
case False
{ fix y assume "a \<le> y" "y \<le> b" "m > 0"
hence "m *\<^sub>R a + c \<le> m *\<^sub>R y + c" "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
- unfolding vector_less_eq_def by(auto simp add: vector_smult_component vector_add_component)
+ unfolding vector_le_def by(auto simp add: vector_smult_component vector_add_component)
} moreover
{ fix y assume "a \<le> y" "y \<le> b" "m < 0"
hence "m *\<^sub>R b + c \<le> m *\<^sub>R y + c" "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
- unfolding vector_less_eq_def by(auto simp add: vector_smult_component vector_add_component mult_left_mono_neg elim!:ballE)
+ unfolding vector_le_def by(auto simp add: vector_smult_component vector_add_component mult_left_mono_neg elim!:ballE)
} moreover
{ fix y assume "m > 0" "m *\<^sub>R a + c \<le> y" "y \<le> m *\<^sub>R b + c"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
- unfolding image_iff Bex_def mem_interval vector_less_eq_def
+ unfolding image_iff Bex_def mem_interval vector_le_def
apply(auto simp add: vector_smult_component vector_add_component vector_minus_component vector_smult_assoc pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: pos_le_divide_eq pos_divide_le_eq real_mult_commute diff_le_iff)
} moreover
{ fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
- unfolding image_iff Bex_def mem_interval vector_less_eq_def
+ unfolding image_iff Bex_def mem_interval vector_le_def
apply(auto simp add: vector_smult_component vector_add_component vector_minus_component vector_smult_assoc pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: neg_le_divide_eq neg_divide_le_eq real_mult_commute diff_le_iff)
--- a/src/HOL/Nominal/Examples/ROOT.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML Fri Nov 20 07:24:21 2009 +0100
@@ -1,3 +1,3 @@
use_thys ["Nominal_Examples"];
-setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; (*FIXME*)
+setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"];
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Nov 20 07:24:21 2009 +0100
@@ -15,9 +15,9 @@
struct
val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
+val inductive_forall_def = @{thm induct_forall_def};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Nov 20 07:24:21 2009 +0100
@@ -15,9 +15,9 @@
struct
val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
+val inductive_forall_def = @{thm induct_forall_def};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
--- a/src/HOL/Predicate.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Predicate.thy Fri Nov 20 07:24:21 2009 +0100
@@ -570,6 +570,9 @@
definition if_pred :: "bool \<Rightarrow> unit pred" where
if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
+definition holds :: "unit pred \<Rightarrow> bool" where
+ holds_eq: "holds P = eval P ()"
+
definition not_pred :: "unit pred \<Rightarrow> unit pred" where
not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())"
@@ -592,7 +595,54 @@
lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
unfolding not_pred_eq
by (auto split: split_if_asm elim: botE)
+lemma "f () = False \<or> f () = True"
+by simp
+lemma closure_of_bool_cases:
+assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
+assumes "f = (%u. True) \<Longrightarrow> P f"
+shows "P f"
+proof -
+ have "f = (%u. False) \<or> f = (%u. True)"
+ apply (cases "f ()")
+ apply (rule disjI2)
+ apply (rule ext)
+ apply (simp add: unit_eq)
+ apply (rule disjI1)
+ apply (rule ext)
+ apply (simp add: unit_eq)
+ done
+ from this prems show ?thesis by blast
+qed
+
+lemma unit_pred_cases:
+assumes "P \<bottom>"
+assumes "P (single ())"
+shows "P Q"
+using assms
+unfolding bot_pred_def Collect_def empty_def single_def
+apply (cases Q)
+apply simp
+apply (rule_tac f="fun" in closure_of_bool_cases)
+apply auto
+apply (subgoal_tac "(%x. () = x) = (%x. True)")
+apply auto
+done
+
+lemma holds_if_pred:
+ "holds (if_pred b) = b"
+unfolding if_pred_eq holds_eq
+by (cases b) (auto intro: singleI elim: botE)
+
+lemma if_pred_holds:
+ "if_pred (holds P) = P"
+unfolding if_pred_eq holds_eq
+by (rule unit_pred_cases) (auto intro: singleI elim: botE)
+
+lemma is_empty_holds:
+ "is_empty P \<longleftrightarrow> \<not> holds P"
+unfolding is_empty_def holds_eq
+by (rule unit_pred_cases) (auto elim: botE intro: singleI)
subsubsection {* Implementation *}
@@ -838,7 +888,7 @@
bind (infixl "\<guillemotright>=" 70)
hide (open) type pred seq
-hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
+hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
end
--- a/src/HOL/Tools/Function/function_common.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Fri Nov 20 07:24:21 2009 +0100
@@ -259,12 +259,18 @@
(fname, length args)
end
- val _ = AList.group (op =) (map check eqs)
+ val grouped_args = AList.group (op =) (map check eqs)
+ val _ = grouped_args
|> map (fn (fname, ars) =>
length (distinct (op =) ars) = 1
orelse error ("Function " ^ quote fname ^
" has different numbers of arguments in different equations"))
+ val not_defined = subtract (op =) (map fst grouped_args) fnames
+ val _ = null not_defined
+ orelse error ("No defining equations for function" ^
+ plural " " "s " not_defined ^ commas_quote not_defined)
+
fun check_sorts ((fname, fT), _) =
Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
orelse error (cat_lines
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Nov 20 07:24:21 2009 +0100
@@ -111,10 +111,10 @@
in
Options {
expected_modes = Option.map (pair const) expected_modes,
- proposed_modes = if not (null proposed_modes) then [(const, map fst proposed_modes)] else [],
+ proposed_modes = Option.map (pair const o map fst) proposed_modes,
proposed_names =
- map_filter
- (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name)) proposed_modes,
+ the_default [] (Option.map (map_filter
+ (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name))) proposed_modes),
show_steps = chk "show_steps",
show_intermediate_results = chk "show_intermediate_results",
show_proof_trace = chk "show_proof_trace",
@@ -176,7 +176,7 @@
val opt_modes =
Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |--
- P.enum1 "," mode_and_opt_proposal --| P.$$$ ")") []
+ P.enum "," mode_and_opt_proposal --| P.$$$ ")" >> SOME) NONE
val opt_expected_modes =
Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |--
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Nov 20 07:24:21 2009 +0100
@@ -282,7 +282,7 @@
datatype options = Options of {
expected_modes : (string * mode' list) option,
- proposed_modes : (string * mode' list) list,
+ proposed_modes : (string * mode' list) option,
proposed_names : ((string * mode') * string) list,
show_steps : bool,
show_proof_trace : bool,
@@ -299,7 +299,7 @@
};
fun expected_modes (Options opt) = #expected_modes opt
-fun proposed_modes (Options opt) name = AList.lookup (op =) (#proposed_modes opt) name
+fun proposed_modes (Options opt) = #proposed_modes opt
fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode')
(#proposed_names opt) (name, mode)
@@ -318,7 +318,7 @@
val default_options = Options {
expected_modes = NONE,
- proposed_modes = [],
+ proposed_modes = NONE,
proposed_names = [],
show_steps = false,
show_intermediate_results = false,
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 20 07:24:21 2009 +0100
@@ -82,10 +82,6 @@
^ "\n" ^ Pretty.string_of (Pretty.chunks
(Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
-(* reference to preprocessing of InductiveSet package *)
-
-val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*)
-
(** fundamentals **)
(* syntactic operations *)
@@ -417,22 +413,45 @@
end
(* validity checks *)
+(* EXPECTED MODE and PROPOSED_MODE are largely the same; define a clear semantics for those! *)
-fun check_expected_modes preds (options : Predicate_Compile_Aux.options) modes =
- case expected_modes options of
- SOME (s, ms) => (case AList.lookup (op =) modes s of
- SOME modes =>
- let
- val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes
- in
- if not (eq_set eq_mode' (ms, modes')) then
- error ("expected modes were not inferred:\n"
- ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes') ^ "\n"
- ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms))
- else ()
- end
- | NONE => ())
- | NONE => ()
+fun check_expected_modes preds options modes =
+ case expected_modes options of
+ SOME (s, ms) => (case AList.lookup (op =) modes s of
+ SOME modes =>
+ let
+ val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes
+ in
+ if not (eq_set eq_mode' (ms, modes')) then
+ error ("expected modes were not inferred:\n"
+ ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes') ^ "\n"
+ ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms))
+ else ()
+ end
+ | NONE => ())
+ | NONE => ()
+
+fun check_proposed_modes preds options modes extra_modes errors =
+ case proposed_modes options of
+ SOME (s, ms) => (case AList.lookup (op =) modes s of
+ SOME inferred_ms =>
+ let
+ val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes))
+ val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) inferred_ms
+ in
+ if not (eq_set eq_mode' (ms, modes')) then
+ error ("expected modes were not inferred:\n"
+ ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes') ^ "\n"
+ ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms) ^ "\n"
+ ^ "For the following clauses, the following modes could not be inferred: " ^ "\n"
+ ^ cat_lines errors ^
+ (if not (null preds_without_modes) then
+ "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
+ else ""))
+ else ()
+ end
+ | NONE => ())
+ | NONE => ()
(* importing introduction rules *)
@@ -584,13 +603,13 @@
let
val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
in (fst (dest_Const const) = name) end;
- val intros = ind_set_codegen_preproc thy
+ val intros =
(map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result)))
val index = find_index (fn s => s = name) (#names (fst info))
val pre_elim = nth (#elims result) index
val pred = nth (#preds result) index
val nparams = length (Inductive.params_of (#raw_induct result))
- (*val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams
+ (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams
(expand_tuples_elim pre_elim))*)
val elim =
(Drule.standard o Skip_Proof.make_thm thy)
@@ -659,8 +678,8 @@
fun register_predicate (constname, pre_intros, pre_elim, nparams) thy =
let
(* preprocessing *)
- val intros = ind_set_codegen_preproc thy (map (preprocess_intro thy) pre_intros)
- val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim)
+ val intros = map (preprocess_intro thy) pre_intros
+ val elim = preprocess_elim thy nparams pre_elim
in
if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
PredData.map
@@ -1042,21 +1061,34 @@
else NONE
end;
-fun print_failed_mode options thy modes p m rs i =
+fun print_failed_mode options thy modes p m rs is =
if show_mode_inference options then
let
- val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
- p ^ " violates mode " ^ string_of_mode thy p m)
+ val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
+ p ^ " violates mode " ^ string_of_mode thy p m)
in () end
else ()
+fun error_of thy p m is =
+ (" Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
+ p ^ " violates mode " ^ string_of_mode thy p m)
+
+fun find_indices f xs =
+ map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
+
fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) =
let
val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => []
- in (p, filter (fn m => case find_index
- (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
- ~1 => true
- | i => (print_failed_mode options thy modes p m rs i; false)) ms)
+ fun invalid_mode m =
+ case find_indices
+ (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
+ [] => NONE
+ | is => SOME (error_of thy p m is)
+ val res = map (fn m => (m, invalid_mode m)) ms
+ val ms' = map_filter (fn (m, NONE) => SOME m | _ => NONE) res
+ val errors = map_filter snd res
+ in
+ ((p, ms'), errors)
end;
fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
@@ -1071,14 +1103,24 @@
let val y = f x
in if x = y then x else fixp f y end;
+fun fixp_with_state f ((x : (string * mode list) list), state) =
+ let
+ val (y, state') = f (x, state)
+ in
+ if x = y then (y, state') else fixp_with_state f (y, state')
+ end
+
fun infer_modes options thy extra_modes all_modes param_vs clauses =
let
- val modes =
- fixp (fn modes =>
- map (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes)
- all_modes
+ val (modes, errors) =
+ fixp_with_state (fn (modes, errors) =>
+ let
+ val res = map
+ (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes
+ in (map fst res, errors @ maps snd res) end)
+ (all_modes, [])
in
- map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes
+ (map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes, errors)
end;
fun remove_from rem [] = []
@@ -1087,7 +1129,7 @@
NONE => (k, vs)
| SOME vs' => (k, subtract (op =) vs' vs))
:: remove_from rem xs
-
+
fun infer_modes_with_generator options thy extra_modes all_modes param_vs clauses =
let
val prednames = map fst clauses
@@ -1096,16 +1138,21 @@
|> filter_out (fn (name, _) => member (op =) prednames name)
val starting_modes = remove_from extra_modes' all_modes
fun eq_mode (m1, m2) = (m1 = m2)
- val modes =
- fixp (fn modes =>
- map (check_modes_pred options true thy param_vs clauses extra_modes'
- (gen_modes @ modes)) modes) starting_modes
+ val (modes, errors) =
+ fixp_with_state (fn (modes, errors) =>
+ let
+ val res = map
+ (check_modes_pred options true thy param_vs clauses extra_modes'
+ (gen_modes @ modes)) modes
+ in (map fst res, errors @ maps snd res) end) (starting_modes, [])
+ val moded_clauses =
+ map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes
+ val (moded_clauses', _) = infer_modes options thy extra_modes all_modes param_vs clauses
+ val join_moded_clauses_table = AList.join (op =)
+ (fn _ => fn ((mps1, mps2)) =>
+ merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2))
in
- AList.join (op =)
- (fn _ => fn ((mps1, mps2)) =>
- merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2))
- (infer_modes options thy extra_modes all_modes param_vs clauses,
- map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes)
+ (join_moded_clauses_table (moded_clauses', moded_clauses), errors)
end;
(* term construction *)
@@ -1524,66 +1571,67 @@
let
val compfuns = PredicateCompFuns.compfuns
val T = AList.lookup (op =) preds name |> the
- fun create_definition (mode as (iss, is)) thy = let
- val mode_cname = create_constname_of_mode options thy "" name T mode
- val mode_cbasename = Long_Name.base_name mode_cname
- val Ts = binder_types T
- val (Ts1, Ts2) = chop (length iss) Ts
- val (Us1, Us2) = split_smodeT is Ts2
- val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1
- val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2))
- val names = Name.variant_list []
- (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
- val param_names = Name.variant_list []
- (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
- val xparams = map2 (curry Free) param_names Ts1'
- fun mk_vars (i, T) names =
- let
- val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
- in
- case AList.lookup (op =) is i of
- NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
- | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
- | SOME (SOME pis) =>
- let
- val (Tins, Touts) = split_tupleT pis T
- val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
- val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
- val xin = Free (name_in, HOLogic.mk_tupleT Tins)
- val xout = Free (name_out, HOLogic.mk_tupleT Touts)
- val xarg = mk_arg xin xout pis T
- in
- (((if null Tins then [] else [xin],
- if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
- end
- val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
- val (xinout, xargs) = split_list xinoutargs
- val (xins, xouts) = pairself flat (split_list xinout)
- val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
- fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
- | mk_split_lambda [x] t = lambda x t
- | mk_split_lambda xs t =
- let
- fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
- | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
- in
- mk_split_lambda' xs t
+ fun create_definition (mode as (iss, is)) thy =
+ let
+ val mode_cname = create_constname_of_mode options thy "" name T mode
+ val mode_cbasename = Long_Name.base_name mode_cname
+ val Ts = binder_types T
+ val (Ts1, Ts2) = chop (length iss) Ts
+ val (Us1, Us2) = split_smodeT is Ts2
+ val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1
+ val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2))
+ val names = Name.variant_list []
+ (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
+ val param_names = Name.variant_list []
+ (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
+ val xparams = map2 (curry Free) param_names Ts1'
+ fun mk_vars (i, T) names =
+ let
+ val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
+ in
+ case AList.lookup (op =) is i of
+ NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
+ | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
+ | SOME (SOME pis) =>
+ let
+ val (Tins, Touts) = split_tupleT pis T
+ val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
+ val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
+ val xin = Free (name_in, HOLogic.mk_tupleT Tins)
+ val xout = Free (name_out, HOLogic.mk_tupleT Touts)
+ val xarg = mk_arg xin xout pis T
+ in
+ (((if null Tins then [] else [xin],
+ if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
+ end
+ val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
+ val (xinout, xargs) = split_list xinoutargs
+ val (xins, xouts) = pairself flat (split_list xinout)
+ val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
+ fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
+ | mk_split_lambda [x] t = lambda x t
+ | mk_split_lambda xs t =
+ let
+ fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
+ | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
+ in
+ mk_split_lambda' xs t
+ end;
+ val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts
+ (list_comb (Const (name, T), xparams' @ xargs)))
+ val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
+ val def = Logic.mk_equals (lhs, predterm)
+ val ([definition], thy') = thy |>
+ Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
+ PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
+ val (intro, elim) =
+ create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
+ in thy'
+ |> add_predfun name mode (mode_cname, definition, intro, elim)
+ |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
+ |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd
+ |> Theory.checkpoint
end;
- val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts
- (list_comb (Const (name, T), xparams' @ xargs)))
- val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
- val def = Logic.mk_equals (lhs, predterm)
- val ([definition], thy') = thy |>
- Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
- PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
- val (intro, elim) =
- create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
- in thy'
- |> add_predfun name mode (mode_cname, definition, intro, elim)
- |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
- |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd
- |> Theory.checkpoint
- end;
in
fold create_definition modes thy
end;
@@ -1626,8 +1674,8 @@
(* MAJOR FIXME: prove_params should be simple
- different form of introrule for parameters ? *)
-fun prove_param thy NONE t = TRY (rtac @{thm refl} 1)
- | prove_param thy (m as SOME (Mode (mode, is, ms))) t =
+fun prove_param options thy NONE t = TRY (rtac @{thm refl} 1)
+ | prove_param options thy (m as SOME (Mode (mode, is, ms))) t =
let
val (f, args) = strip_comb (Envir.eta_contract t)
val (params, _) = chop (length ms) args
@@ -1639,16 +1687,15 @@
| Free _ => TRY (rtac @{thm refl} 1)
| Abs _ => error "prove_param: No valid parameter term"
in
- REPEAT_DETERM (etac @{thm thin_rl} 1)
- THEN REPEAT_DETERM (rtac @{thm ext} 1)
- THEN print_tac "prove_param"
+ REPEAT_DETERM (rtac @{thm ext} 1)
+ THEN print_tac' options "prove_param"
THEN f_tac
- THEN print_tac "after simplification in prove_args"
- THEN (EVERY (map2 (prove_param thy) ms params))
+ THEN print_tac' options "after simplification in prove_args"
+ THEN (EVERY (map2 (prove_param options thy) ms params))
THEN (REPEAT_DETERM (atac 1))
end
-fun prove_expr thy (Mode (mode, is, ms), t, us) (premposition : int) =
+fun prove_expr options thy (Mode (mode, is, ms), t, us) (premposition : int) =
case strip_comb t of
(Const (name, T), args) =>
let
@@ -1656,16 +1703,16 @@
val (args1, args2) = chop (length ms) args
in
rtac @{thm bindI} 1
- THEN print_tac "before intro rule:"
+ THEN print_tac' options "before intro rule:"
(* for the right assumption in first position *)
THEN rotate_tac premposition 1
THEN debug_tac (Display.string_of_thm (ProofContext.init thy) introrule)
THEN rtac introrule 1
- THEN print_tac "after intro rule"
+ THEN print_tac' options "after intro rule"
(* work with parameter arguments *)
- THEN (atac 1)
- THEN (print_tac "parameter goal")
- THEN (EVERY (map2 (prove_param thy) ms args1))
+ THEN atac 1
+ THEN print_tac' options "parameter goal"
+ THEN (EVERY (map2 (prove_param options thy) ms args1))
THEN (REPEAT_DETERM (atac 1))
end
| _ => rtac @{thm bindI} 1
@@ -1673,7 +1720,7 @@
(HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
@{thm "snd_conv"}, @{thm pair_collapse}]) 1
THEN (atac 1)
- THEN print_tac "after prove parameter call"
+ THEN print_tac' options "after prove parameter call"
fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
@@ -1725,9 +1772,9 @@
val (in_ts, clause_out_ts) = split_smode is ts;
fun prove_prems out_ts [] =
(prove_match thy out_ts)
- THEN print_tac "before simplifying assumptions"
+ THEN print_tac' options "before simplifying assumptions"
THEN asm_full_simp_tac HOL_basic_ss' 1
- THEN print_tac "before single intro rule"
+ THEN print_tac' options "before single intro rule"
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
| prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
let
@@ -1737,11 +1784,11 @@
val (_, out_ts''') = split_smode is us
val rec_tac = prove_prems out_ts''' ps
in
- print_tac "before clause:"
+ print_tac' options "before clause:"
THEN asm_simp_tac HOL_basic_ss 1
- THEN print_tac "before prove_expr:"
- THEN prove_expr thy (mode, t, us) premposition
- THEN print_tac "after prove_expr:"
+ THEN print_tac' options "before prove_expr:"
+ THEN prove_expr options thy (mode, t, us) premposition
+ THEN print_tac' options "after prove_expr:"
THEN rec_tac
end
| Negprem (us, t) =>
@@ -1752,13 +1799,18 @@
val (_, params) = strip_comb t
in
rtac @{thm bindI} 1
+ THEN print_tac' options "before prove_neg_expr:"
THEN (if (is_some name) then
- simp_tac (HOL_basic_ss addsimps
+ print_tac' options ("before unfolding definition " ^
+ (Display.string_of_thm_global thy
+ (predfun_definition_of thy (the name) (iss, is))))
+ THEN simp_tac (HOL_basic_ss addsimps
[predfun_definition_of thy (the name) (iss, is)]) 1
THEN rtac @{thm not_predI} 1
+ THEN print_tac' options "after applying rule not_predI"
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
THEN (REPEAT_DETERM (atac 1))
- THEN (EVERY (map2 (prove_param thy) param_modes params))
+ THEN (EVERY (map2 (prove_param options thy) param_modes params))
else
rtac @{thm not_predI'} 1)
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
@@ -1767,9 +1819,9 @@
| Sidecond t =>
rtac @{thm bindI} 1
THEN rtac @{thm if_predI} 1
- THEN print_tac "before sidecond:"
+ THEN print_tac' options "before sidecond:"
THEN prove_sidecond thy modes t
- THEN print_tac "after sidecond:"
+ THEN print_tac' options "after sidecond:"
THEN prove_prems [] ps)
in (prove_match thy out_ts)
THEN rest_tac
@@ -1800,7 +1852,7 @@
(fn i => EVERY' (select_sup (length moded_clauses) i) i)
(1 upto (length moded_clauses))))
THEN (EVERY (map2 (prove_clause options thy nargs modes mode) clauses moded_clauses))
- THEN print_tac "proved one direction"
+ THEN print_tac' options "proved one direction"
end;
(** Proof in the other direction **)
@@ -2106,9 +2158,10 @@
map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us)
end
val all_modes = map (fn (s, T) =>
- case proposed_modes options s of
+ case proposed_modes options of
NONE => (s, modes_of_typ T)
- | SOME modes' => (s, map (translate_mode' nparams) modes'))
+ | SOME (s', modes') =>
+ if s = s' then (s, map (translate_mode' nparams) modes') else (s, modes_of_typ T))
preds
in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end;
@@ -2173,12 +2226,12 @@
val args = map2 (curry Free) arg_names Ts
val predfun = Const (predfun_name_of thy predname full_mode,
Ts ---> PredicateCompFuns.mk_predT @{typ unit})
- val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"})
+ val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
val eq_term = HOLogic.mk_Trueprop
(HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
val def = predfun_definition_of thy predname full_mode
val tac = fn _ => Simplifier.simp_tac
- (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1
+ (HOL_basic_ss addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
in
(pred, result_thms @ [eq])
@@ -2199,7 +2252,7 @@
define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory,
infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list
-> string list -> (string * (term list * indprem list) list) list
- -> moded_clause list pred_mode_table,
+ -> moded_clause list pred_mode_table * string list,
prove : options -> theory -> (string * (term list * indprem list) list) list
-> (string * typ) list -> (string * mode list) list
-> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
@@ -2220,10 +2273,11 @@
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
prepare_intrs options thy prednames (maps (intros_of thy) prednames)
val _ = print_step options "Infering modes..."
- val moded_clauses =
+ val (moded_clauses, errors) =
#infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
val _ = check_expected_modes preds options modes
+ val _ = check_proposed_modes preds options modes extra_modes errors
val _ = print_modes options thy modes
(*val _ = print_moded_clauses thy moded_clauses*)
val _ = print_step options "Defining executable functions..."
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Nov 20 07:24:21 2009 +0100
@@ -137,7 +137,7 @@
th'
end
-fun store_thm_in_table options ignore_consts thy th=
+fun store_thm_in_table options ignore thy th=
let
val th = th
|> inline_equations options thy
@@ -153,29 +153,29 @@
else if (is_introlike th) then (defining_const_of_introrule th, th)
else error "store_thm: unexpected definition format"
in
- if not (member (op =) ignore_consts const) then
- Symtab.cons_list (const, th)
- else I
+ if ignore const then I else Symtab.cons_list (const, th)
end
fun make_const_spec_table options thy =
let
- fun store ignore_const f =
- fold (store_thm_in_table options ignore_const thy)
+ fun store ignore f =
+ fold (store_thm_in_table options ignore thy)
(map (Thm.transfer thy) (f (ProofContext.init thy)))
val table = Symtab.empty
- |> store [] Predicate_Compile_Alternative_Defs.get
- val ignore_consts = Symtab.keys table
+ |> store (K false) Predicate_Compile_Alternative_Defs.get
+ val ignore = Symtab.defined table
in
table
- |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
- |> store ignore_consts Nitpick_Simps.get
- |> store ignore_consts Nitpick_Intros.get
+ |> store ignore (fn ctxt => maps
+ (fn (roughly, (ts, ths)) => if roughly = Spec_Rules.Equational then ths else [])
+ (Spec_Rules.get ctxt))
+ |> store ignore Nitpick_Simps.get
+ |> store ignore Nitpick_Intros.get
end
fun get_specification table constname =
case Symtab.lookup table constname of
- SOME thms => thms
+ SOME thms => thms
| NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
val logic_operator_names =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Nov 20 07:24:21 2009 +0100
@@ -89,9 +89,7 @@
fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
| mk_param thy lookup_pred t =
- let
- val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t))
- in if Predicate_Compile_Aux.is_predT (fastype_of t) then
+ if Predicate_Compile_Aux.is_predT (fastype_of t) then
t
else
let
@@ -109,7 +107,7 @@
val pred_body = HOLogic.mk_eq (body', resvar)
val param = fold_rev lambda (vs' @ [resvar]) pred_body
in param end
- end
+
(* creates the list of premises for every intro rule *)
(* theory -> term -> (string list, term list list) *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 20 07:24:21 2009 +0100
@@ -23,7 +23,7 @@
val options = Options {
expected_modes = NONE,
- proposed_modes = [],
+ proposed_modes = NONE,
proposed_names = [],
show_steps = true,
show_intermediate_results = true,
@@ -83,7 +83,7 @@
val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
val _ = tracing (Display.string_of_thm ctxt' intro)
val thy'' = thy'
- |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
+ |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro)
|> Predicate_Compile.preprocess options full_constname
|> Predicate_Compile_Core.add_equations options [full_constname]
(* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
--- a/src/HOL/Tools/dseq.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/dseq.ML Fri Nov 20 07:24:21 2009 +0100
@@ -6,7 +6,7 @@
signature DSEQ =
sig
- type 'a seq = int -> 'a Seq.seq;
+ type 'a seq = int * int * int -> 'a Seq.seq;
val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
val map: ('a -> 'b) -> 'a seq -> 'b seq
val append: 'a seq -> 'a seq -> 'a seq
@@ -16,37 +16,42 @@
val guard: bool -> unit seq
val of_list: 'a list -> 'a seq
val list_of: 'a seq -> 'a list
- val pull: 'a seq -> ('a * 'a seq) option
+ val pull: 'a seq -> ('a * 'a Seq.seq) option
val hd: 'a seq -> 'a
+ val generator: (int -> 'a * 'b) -> 'a seq
end;
structure DSeq : DSEQ =
struct
-type 'a seq = int -> 'a Seq.seq;
+type 'a seq = int * int * int -> 'a Seq.seq;
-fun maps f s 0 = Seq.empty
- | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
+fun maps f s (0, _, _) = Seq.empty
+ | maps f s (i, j, k) = Seq.maps (fn a => f a (i, j, k)) (s (i - 1, j, k));
-fun map f s i = Seq.map f (s i);
+fun map f s p = Seq.map f (s p);
-fun append s1 s2 i = Seq.append (s1 i) (s2 i);
+fun append s1 s2 p = Seq.append (s1 p) (s2 p);
-fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
+fun interleave s1 s2 p = Seq.interleave (s1 p, s2 p);
-fun single x i = Seq.single x;
+fun single x _ = Seq.single x;
-fun empty i = Seq.empty;
+fun empty _ = Seq.empty;
fun guard b = if b then single () else empty;
-fun of_list xs i = Seq.of_list xs;
+fun of_list xs _ = Seq.of_list xs;
-fun list_of s = Seq.list_of (s ~1);
+fun list_of s = Seq.list_of (s (~1, 0, 0));
+
+fun pull s = Seq.pull (s (~1, 0, 0));
-fun pull s = Seq.pull (s ~1) |> (Option.map o apsnd) K; (*FIXME*)
+fun hd s = Seq.hd (s (~1, 0, 0));
-fun hd s = Seq.hd (s ~1);
+fun generator g (i, 0, k) = Seq.empty
+ | generator g (i, j, k) =
+ Seq.make (fn () => SOME (fst (g k), generator g (i, j-1, k)));
end;
--- a/src/HOL/Tools/inductive_codegen.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Nov 20 07:24:21 2009 +0100
@@ -7,7 +7,10 @@
signature INDUCTIVE_CODEGEN =
sig
val add : string option -> int option -> attribute
+ val test_fn : (int * int * int -> term list option) Unsynchronized.ref
+ val test_term: Proof.context -> term -> int -> term list option
val setup : theory -> theory
+ val quickcheck_setup : theory -> theory
end;
structure InductiveCodegen : INDUCTIVE_CODEGEN =
@@ -124,7 +127,8 @@
fun print_modes modes = message ("Inferred modes:\n" ^
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
- string_of_mode ms)) modes));
+ (fn (m, rnd) => string_of_mode m ^
+ (if rnd then " (random)" else "")) ms)) modes));
val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
val terms_vs = distinct (op =) o maps term_vs;
@@ -152,14 +156,17 @@
fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
-datatype mode = Mode of (int list option list * int list) * int list * mode option list;
+datatype mode = Mode of ((int list option list * int list) * bool) * int list * mode option list;
+
+fun needs_random (Mode ((_, b), _, ms)) =
+ b orelse exists (fn NONE => false | SOME m => needs_random m) ms;
fun modes_of modes t =
let
val ks = 1 upto length (binder_types (fastype_of t));
- val default = [Mode (([], ks), ks, [])];
+ val default = [Mode ((([], ks), false), ks, [])];
fun mk_modes name args = Option.map
- (maps (fn (m as (iss, is)) =>
+ (maps (fn (m as ((iss, is), _)) =>
let
val (args1, args2) =
if length args < length iss then
@@ -180,8 +187,8 @@
in (case strip_comb t of
(Const ("op =", Type (_, [T, _])), _) =>
- [Mode (([], [1]), [1], []), Mode (([], [2]), [2], [])] @
- (if is_eqT T then [Mode (([], [1, 2]), [1, 2], [])] else [])
+ [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
+ (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
| (Const (name, _), args) => the_default default (mk_modes name args)
| (Var ((name, _), _), args) => the (mk_modes name args)
| (Free (name, _), args) => the (mk_modes name args)
@@ -190,68 +197,101 @@
datatype indprem = Prem of term list * term * bool | Sidecond of term;
+fun missing_vars vs ts = subtract (fn (x, ((y, _), _)) => x = y) vs
+ (fold Term.add_vars ts []);
+
+fun monomorphic_vars vs = null (fold (Term.add_tvarsT o snd) vs []);
+
+fun mode_ord p = int_ord (pairself (fn (Mode ((_, rnd), _, _), vs) =>
+ length vs + (if null vs then 0 else 1) + (if rnd then 1 else 0)) p);
+
fun select_mode_prem thy modes vs ps =
- find_first (is_some o snd) (ps ~~ map
- (fn Prem (us, t, is_set) => find_first (fn Mode (_, is, _) =>
- let
- val (in_ts, out_ts) = get_args is 1 us;
- val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
- val vTs = maps term_vTs out_ts';
- val dupTs = map snd (duplicates (op =) vTs) @
- map_filter (AList.lookup (op =) vTs) vs;
- in
- subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
- forall (is_eqT o fastype_of) in_ts' andalso
- subset (op =) (term_vs t, vs) andalso
- forall is_eqT dupTs
- end)
- (if is_set then [Mode (([], []), [], [])]
- else modes_of modes t handle Option =>
- error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
- | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
- else NONE) ps);
+ sort (mode_ord o pairself (hd o snd))
+ (filter_out (null o snd) (ps ~~ map
+ (fn Prem (us, t, is_set) => sort mode_ord
+ (List.mapPartial (fn m as Mode (_, is, _) =>
+ let
+ val (in_ts, out_ts) = get_args is 1 us;
+ val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
+ val vTs = maps term_vTs out_ts';
+ val dupTs = map snd (duplicates (op =) vTs) @
+ map_filter (AList.lookup (op =) vTs) vs;
+ val missing_vs = missing_vars vs (t :: in_ts @ in_ts')
+ in
+ if forall (is_eqT o fastype_of) in_ts' andalso forall is_eqT dupTs
+ andalso monomorphic_vars missing_vs
+ then SOME (m, missing_vs)
+ else NONE
+ end)
+ (if is_set then [Mode ((([], []), false), [], [])]
+ else modes_of modes t handle Option =>
+ error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)))
+ | Sidecond t =>
+ let val missing_vs = missing_vars vs [t]
+ in
+ if monomorphic_vars missing_vs
+ then [(Mode ((([], []), false), [], []), missing_vs)]
+ else []
+ end)
+ ps));
-fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
+fun use_random () = "random_ind" mem !Codegen.mode;
+
+fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) =
let
val modes' = modes @ map_filter
- (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
+ (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
(arg_vs ~~ iss);
- fun check_mode_prems vs [] = SOME vs
- | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
- NONE => NONE
- | SOME (x, _) => check_mode_prems
+ fun check_mode_prems vs rnd [] = SOME (vs, rnd)
+ | check_mode_prems vs rnd ps = (case select_mode_prem thy modes' vs ps of
+ (x, (m, []) :: _) :: _ => check_mode_prems
(case x of Prem (us, _, _) => union (op =) vs (terms_vs us) | _ => vs)
- (filter_out (equal x) ps));
+ (rnd orelse needs_random m)
+ (filter_out (equal x) ps)
+ | (_, (_, vs') :: _) :: _ =>
+ if use_random () then
+ check_mode_prems (union (op =) vs (map (fst o fst) vs')) true ps
+ else NONE
+ | _ => NONE);
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
val in_vs = terms_vs in_ts;
- val concl_vs = terms_vs ts
in
- forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
- forall (is_eqT o fastype_of) in_ts' andalso
- (case check_mode_prems (union (op =) arg_vs in_vs) ps of
- NONE => false
- | SOME vs => subset (op =) (concl_vs, vs))
+ if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
+ forall (is_eqT o fastype_of) in_ts'
+ then (case check_mode_prems (union (op =) arg_vs in_vs) rnd ps of
+ NONE => NONE
+ | SOME (vs, rnd') =>
+ let val missing_vs = missing_vars vs ts
+ in
+ if null missing_vs orelse
+ use_random () andalso monomorphic_vars missing_vs
+ then SOME (rnd' orelse not (null missing_vs))
+ else NONE
+ end)
+ else NONE
end;
fun check_modes_pred thy arg_vs preds modes (p, ms) =
let val SOME rs = AList.lookup (op =) preds p
- in (p, filter (fn m => case find_index
- (not o check_mode_clause thy arg_vs modes m) rs of
- ~1 => true
- | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
- p ^ " violates mode " ^ string_of_mode m); false)) ms)
+ in (p, List.mapPartial (fn m as (m', _) =>
+ let val xs = map (check_mode_clause thy arg_vs modes m) rs
+ in case find_index is_none xs of
+ ~1 => SOME (m', exists (fn SOME b => b) xs)
+ | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
+ p ^ " violates mode " ^ string_of_mode m'); NONE)
+ end) ms)
end;
-fun fixp f (x : (string * (int list option list * int list) list) list) =
+fun fixp f (x : (string * ((int list option list * int list) * bool) list) list) =
let val y = f x
in if x = y then x else fixp f y end;
fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes =>
map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)
- (map (fn (s, (ks, k)) => (s, cprod (cprods (map
+ (map (fn (s, (ks, k)) => (s, map (rpair false) (cprod (cprods (map
(fn NONE => [NONE]
| SOME k' => map SOME (subsets 1 k')) ks),
- subsets 1 k))) arities);
+ subsets 1 k)))) arities);
(**** code generation ****)
@@ -318,7 +358,7 @@
apfst single (invoke_codegen thy defs dep module brack t gr)
| compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
([str name], gr)
- | compile_expr thy defs dep module brack modes (SOME (Mode (mode, _, ms)), t) gr =
+ | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
(case strip_comb t of
(Const (name, _), args) =>
if name = @{const_name "op ="} orelse AList.defined op = modes name then
@@ -344,7 +384,7 @@
fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
let
val modes' = modes @ map_filter
- (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
+ (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
(arg_vs ~~ iss);
fun check_constrt t (names, eqs) =
@@ -371,24 +411,41 @@
val (out_ps', gr4) =
fold_map (invoke_codegen thy defs dep module false) out_ts''' gr3;
val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
+ val vs' = distinct (op =) (flat (vs :: map term_vs out_ts'));
+ val missing_vs = missing_vars vs' out_ts;
+ val final_p = Pretty.block
+ [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps]
in
- (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
- (Pretty.block [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps])
- (exists (not o is_exhaustive) out_ts'''), gr5)
+ if null missing_vs then
+ (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
+ final_p (exists (not o is_exhaustive) out_ts'''), gr5)
+ else
+ let
+ val (pat_p, gr6) = invoke_codegen thy defs dep module true
+ (HOLogic.mk_tuple (map Var missing_vs)) gr5;
+ val gen_p = mk_gen gr6 module true [] ""
+ (HOLogic.mk_tupleT (map snd missing_vs))
+ in
+ (compile_match (snd nvs) eq_ps' out_ps'
+ (Pretty.block [str "DSeq.generator ", gen_p,
+ str " :->", Pretty.brk 1,
+ compile_match [] eq_ps [pat_p] final_p false])
+ (exists (not o is_exhaustive) out_ts'''),
+ gr6)
+ end
end
| compile_prems out_ts vs names ps gr =
let
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
- val SOME (p, mode as SOME (Mode (_, js, _))) = select_mode_prem thy modes' vs' ps;
- val ps' = filter_out (equal p) ps;
val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []);
val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs);
val (out_ps, gr0) = fold_map (invoke_codegen thy defs dep module false) out_ts'' gr;
val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
in
- (case p of
- Prem (us, t, is_set) =>
+ (case hd (select_mode_prem thy modes' vs' ps) of
+ (p as Prem (us, t, is_set), (mode as Mode (_, js, _), []) :: _) =>
let
+ val ps' = filter_out (equal p) ps;
val (in_ts, out_ts''') = get_args js 1 us;
val (in_ps, gr2) = fold_map
(invoke_codegen thy defs dep module true) in_ts gr1;
@@ -398,7 +455,7 @@
(if null in_ps then [] else [Pretty.brk 1]) @
separate (Pretty.brk 1) in_ps)
(compile_expr thy defs dep module false modes
- (mode, t) gr2)
+ (SOME mode, t) gr2)
else
apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p,
str "of", str "Set", str "xs", str "=>", str "xs)"])
@@ -411,8 +468,9 @@
[str " :->", Pretty.brk 1, rest]))
(exists (not o is_exhaustive) out_ts''), gr4)
end
- | Sidecond t =>
+ | (p as Sidecond t, [(_, [])]) =>
let
+ val ps' = filter_out (equal p) ps;
val (side_p, gr2) = invoke_codegen thy defs dep module true t gr1;
val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2;
in
@@ -420,6 +478,19 @@
(Pretty.block [str "?? ", side_p,
str " :->", Pretty.brk 1, rest])
(exists (not o is_exhaustive) out_ts''), gr3)
+ end
+ | (_, (_, missing_vs) :: _) =>
+ let
+ val T = HOLogic.mk_tupleT (map snd missing_vs);
+ val (_, gr2) = invoke_tycodegen thy defs dep module false T gr1;
+ val gen_p = mk_gen gr2 module true [] "" T;
+ val (rest, gr3) = compile_prems
+ [HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2
+ in
+ (compile_match (snd nvs) eq_ps out_ps
+ (Pretty.block [str "DSeq.generator", Pretty.brk 1,
+ gen_p, str " :->", Pretty.brk 1, rest])
+ (exists (not o is_exhaustive) out_ts''), gr3)
end)
end;
@@ -450,7 +521,7 @@
fun compile_preds thy defs dep module all_vs arg_vs modes preds gr =
let val (prs, (gr', _)) = fold_map (fn (s, cls) =>
- fold_map (fn mode => fn (gr', prfx') => compile_pred thy defs
+ fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs
dep module prfx' all_vs arg_vs modes s cls mode gr')
(((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
in
@@ -460,7 +531,7 @@
(**** processing of introduction rules ****)
exception Modes of
- (string * (int list option list * int list) list) list *
+ (string * ((int list option list * int list) * bool) list) list *
(string * (int option list * int)) list;
fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip
@@ -480,7 +551,7 @@
(s,
case AList.lookup (op =) cs (s : string) of
NONE => xs
- | SOME xs' => inter (op =) xs' xs) :: constrain cs ys;
+ | SOME xs' => inter (op = o apfst fst) xs' xs) :: constrain cs ys;
fun mk_extra_defs thy defs gr dep names module ts =
fold (fn name => fn gr =>
@@ -573,6 +644,8 @@
if is_query then fst (fold mk_mode ts2 (([], []), 1))
else (ts2, 1 upto length (binder_types T) - k);
val mode = find_mode gr1 dep s u modes is;
+ val _ = if is_query orelse not (needs_random (the mode)) then ()
+ else warning ("Illegal use of random data generators in " ^ s);
val (in_ps, gr2) = fold_map (invoke_codegen thy defs dep module true) ts' gr1;
val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2;
in
@@ -700,4 +773,91 @@
Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
"introduction rules for executable predicates";
+(**** Quickcheck involving inductive predicates ****)
+
+val test_fn : (int * int * int -> term list option) Unsynchronized.ref =
+ Unsynchronized.ref (fn _ => NONE);
+
+fun strip_imp p =
+ let val (q, r) = HOLogic.dest_imp p
+ in strip_imp r |>> cons q end
+ handle TERM _ => ([], p);
+
+fun deepen bound f i =
+ if i > bound then NONE
+ else (case f i of
+ NONE => deepen bound f (i + 1)
+ | SOME x => SOME x);
+
+val depth_bound_value =
+ Config.declare false "ind_quickcheck_depth" (Config.Int 10);
+val depth_bound = Config.int depth_bound_value;
+
+val depth_start_value =
+ Config.declare false "ind_quickcheck_depth_start" (Config.Int 1);
+val depth_start = Config.int depth_start_value;
+
+val random_values_value =
+ Config.declare false "ind_quickcheck_random" (Config.Int 5);
+val random_values = Config.int random_values_value;
+
+val size_offset_value =
+ Config.declare false "ind_quickcheck_size_offset" (Config.Int 0);
+val size_offset = Config.int size_offset_value;
+
+fun test_term ctxt t =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val (xs, p) = strip_abs t;
+ val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
+ val args = map Free args';
+ val (ps, q) = strip_imp p;
+ val Ts = map snd xs;
+ val T = Ts ---> HOLogic.boolT;
+ val rl = Logic.list_implies
+ (map (HOLogic.mk_Trueprop o curry subst_bounds (rev args)) ps @
+ [HOLogic.mk_Trueprop (HOLogic.mk_not (subst_bounds (rev args, q)))],
+ HOLogic.mk_Trueprop (list_comb (Free ("quickcheckp", T), args)));
+ val (_, thy') = Inductive.add_inductive_global
+ {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false,
+ no_elim=true, no_ind=false, skip_mono=false, fork_mono=false}
+ [((Binding.name "quickcheckp", T), NoSyn)] []
+ [(Attrib.empty_binding, rl)] [] (Theory.copy thy);
+ val pred = HOLogic.mk_Trueprop (list_comb
+ (Const (Sign.intern_const thy' "quickcheckp", T),
+ map Term.dummy_pattern Ts));
+ val (code, gr) = setmp_CRITICAL mode ["term_of", "test", "random_ind"]
+ (generate_code_i thy' [] "Generated") [("testf", pred)];
+ val s = "structure TestTerm =\nstruct\n\n" ^
+ cat_lines (map snd code) ^
+ "\nopen Generated;\n\n" ^ string_of
+ (Pretty.block [str "val () = InductiveCodegen.test_fn :=",
+ Pretty.brk 1, str "(fn p =>", Pretty.brk 1,
+ str "case Seq.pull (testf p) of", Pretty.brk 1,
+ str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
+ str " =>", Pretty.brk 1, str "SOME ",
+ Pretty.block (str "[" ::
+ Pretty.commas (map (fn (s, T) => Pretty.block
+ [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @
+ [str "]"]), Pretty.brk 1,
+ str "| NONE => NONE);"]) ^
+ "\n\nend;\n";
+ val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
+ val values = Config.get ctxt random_values;
+ val bound = Config.get ctxt depth_bound;
+ val start = Config.get ctxt depth_start;
+ val offset = Config.get ctxt size_offset;
+ val test_fn' = !test_fn;
+ fun test k = deepen bound (fn i =>
+ (priority ("Search depth: " ^ string_of_int i);
+ test_fn' (i, values, k+offset))) start;
+ in test end;
+
+val quickcheck_setup =
+ Attrib.register_config depth_bound_value #>
+ Attrib.register_config depth_start_value #>
+ Attrib.register_config random_values_value #>
+ Attrib.register_config size_offset_value #>
+ Quickcheck.add_generator ("SML_inductive", test_term);
+
end;
--- a/src/HOL/Tools/primrec.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/Tools/primrec.ML Fri Nov 20 07:24:21 2009 +0100
@@ -198,7 +198,7 @@
(list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
val rhs = singleton (Syntax.check_terms ctxt)
(TypeInfer.constrain varT raw_rhs);
- in (var, ((Binding.name def_name, []), rhs)) end;
+ in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
(* find datatypes which contain all datatypes in tnames' *)
--- a/src/HOL/ex/Predicate_Compile_ex.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Fri Nov 20 07:24:21 2009 +0100
@@ -87,6 +87,9 @@
values "{(c, a, b). JamesBond a b c}"
values "{(c, b, a). JamesBond a b c}"
+values "{(a, b). JamesBond 0 b a}"
+values "{(c, a). JamesBond a 0 c}"
+values "{(a, c). JamesBond a 0 c}"
subsection {* Alternative Rules *}
@@ -476,6 +479,8 @@
subsection {* transitive predicate *}
+text {* Also look at the tabled transitive closure in the Library *}
+
code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
(o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool,
(o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
@@ -509,6 +514,28 @@
values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
values 20 "{(n, m). tranclp succ n m}"
+inductive example_graph :: "int => int => bool"
+where
+ "example_graph 0 1"
+| "example_graph 1 2"
+| "example_graph 1 3"
+| "example_graph 4 7"
+| "example_graph 4 5"
+| "example_graph 5 6"
+| "example_graph 7 6"
+| "example_graph 7 8"
+
+inductive not_reachable_in_example_graph :: "int => int => bool"
+where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
+
+code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
+
+thm not_reachable_in_example_graph.equation
+
+value "not_reachable_in_example_graph 0 3"
+value "not_reachable_in_example_graph 4 8"
+value "not_reachable_in_example_graph 5 6"
+
subsection {* IMP *}
types
@@ -724,7 +751,7 @@
subsection {* Inverting list functions *}
-code_pred [inductify, show_intermediate_results] length .
+code_pred [inductify] length .
code_pred [inductify, random] length .
thm size_listP.equation
thm size_listP.random_equation
@@ -804,8 +831,6 @@
thm spliceP.equation
values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
-(* TODO: correct error messages:*)
-(* values {(xs, ys, zs). spliceP xs ... } *)
code_pred [inductify] List.rev .
code_pred [inductify] map .
@@ -965,13 +990,8 @@
| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
-(* TODO: breaks if code_pred_intro is used? *)
-(*
-lemmas [code_pred_intro] = irconst objaddr plus
-*)
-thm eval_var.cases
-code_pred eval_var . (*by (rule eval_var.cases)*)
+code_pred eval_var .
thm eval_var.equation
values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
--- a/src/HOLCF/Domain.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOLCF/Domain.thy Fri Nov 20 07:24:21 2009 +0100
@@ -5,7 +5,7 @@
header {* Domain package *}
theory Domain
-imports Ssum Sprod Up One Tr Fixrec
+imports Ssum Sprod Up One Tr Fixrec Representable
uses
("Tools/cont_consts.ML")
("Tools/cont_proc.ML")
--- a/src/HOLCF/IsaMakefile Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOLCF/IsaMakefile Fri Nov 20 07:24:21 2009 +0100
@@ -52,6 +52,7 @@
Pcpo.thy \
Porder.thy \
Product_Cpo.thy \
+ Representable.thy \
Sprod.thy \
Ssum.thy \
Sum_Cpo.thy \
@@ -64,11 +65,13 @@
Tools/cont_proc.ML \
Tools/Domain/domain_extender.ML \
Tools/Domain/domain_axioms.ML \
+ Tools/Domain/domain_isomorphism.ML \
Tools/Domain/domain_library.ML \
Tools/Domain/domain_syntax.ML \
Tools/Domain/domain_theorems.ML \
Tools/fixrec.ML \
Tools/pcpodef.ML \
+ Tools/repdef.ML \
holcf_logic.ML \
document/root.tex
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
--- a/src/HOLCF/Representable.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOLCF/Representable.thy Fri Nov 20 07:24:21 2009 +0100
@@ -5,8 +5,10 @@
header {* Representable Types *}
theory Representable
-imports Algebraic Universal Ssum Sprod One ConvexPD
-uses ("Tools/repdef.ML")
+imports Algebraic Universal Ssum Sprod One ConvexPD Fixrec
+uses
+ ("Tools/repdef.ML")
+ ("Tools/Domain/domain_isomorphism.ML")
begin
subsection {* Class of representable types *}
@@ -159,6 +161,25 @@
apply simp
done
+text {* Isomorphism lemmas used internally by the domain package: *}
+
+lemma domain_abs_iso:
+ fixes abs and rep
+ assumes REP: "REP('b) = REP('a)"
+ assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+ assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ shows "rep\<cdot>(abs\<cdot>x) = x"
+unfolding abs_def rep_def by (simp add: REP)
+
+lemma domain_rep_iso:
+ fixes abs and rep
+ assumes REP: "REP('b) = REP('a)"
+ assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+ assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ shows "abs\<cdot>(rep\<cdot>x) = x"
+unfolding abs_def rep_def by (simp add: REP [symmetric])
+
+
subsection {* Proving a subtype is representable *}
text {*
@@ -671,16 +692,14 @@
Abs_fin_defl (udom_emb oo
f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj))))"
-definition "one_typ = REP(one)"
-definition "tr_typ = REP(tr)"
-definition "cfun_typ = TypeRep_fun2 cfun_map"
-definition "ssum_typ = TypeRep_fun2 ssum_map"
-definition "sprod_typ = TypeRep_fun2 sprod_map"
-definition "cprod_typ = TypeRep_fun2 cprod_map"
-definition "u_typ = TypeRep_fun1 u_map"
-definition "upper_typ = TypeRep_fun1 upper_map"
-definition "lower_typ = TypeRep_fun1 lower_map"
-definition "convex_typ = TypeRep_fun1 convex_map"
+definition "cfun_defl = TypeRep_fun2 cfun_map"
+definition "ssum_defl = TypeRep_fun2 ssum_map"
+definition "sprod_defl = TypeRep_fun2 sprod_map"
+definition "cprod_defl = TypeRep_fun2 cprod_map"
+definition "u_defl = TypeRep_fun1 u_map"
+definition "upper_defl = TypeRep_fun1 upper_map"
+definition "lower_defl = TypeRep_fun1 lower_map"
+definition "convex_defl = TypeRep_fun1 convex_map"
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
unfolding below_fin_defl_def .
@@ -729,138 +748,130 @@
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
qed
-lemma cast_cfun_typ:
- "cast\<cdot>(cfun_typ\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cfun_typ_def
+lemma cast_cfun_defl:
+ "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding cfun_defl_def
apply (rule cast_TypeRep_fun2)
apply (erule (1) finite_deflation_cfun_map)
done
-lemma cast_ssum_typ:
- "cast\<cdot>(ssum_typ\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding ssum_typ_def
+lemma cast_ssum_defl:
+ "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding ssum_defl_def
apply (rule cast_TypeRep_fun2)
apply (erule (1) finite_deflation_ssum_map)
done
-lemma cast_sprod_typ:
- "cast\<cdot>(sprod_typ\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding sprod_typ_def
+lemma cast_sprod_defl:
+ "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding sprod_defl_def
apply (rule cast_TypeRep_fun2)
apply (erule (1) finite_deflation_sprod_map)
done
-lemma cast_cprod_typ:
- "cast\<cdot>(cprod_typ\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cprod_typ_def
+lemma cast_cprod_defl:
+ "cast\<cdot>(cprod_defl\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding cprod_defl_def
apply (rule cast_TypeRep_fun2)
apply (erule (1) finite_deflation_cprod_map)
done
-lemma cast_u_typ:
- "cast\<cdot>(u_typ\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding u_typ_def
+lemma cast_u_defl:
+ "cast\<cdot>(u_defl\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding u_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_u_map)
done
-lemma cast_upper_typ:
- "cast\<cdot>(upper_typ\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding upper_typ_def
+lemma cast_upper_defl:
+ "cast\<cdot>(upper_defl\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding upper_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_upper_map)
done
-lemma cast_lower_typ:
- "cast\<cdot>(lower_typ\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding lower_typ_def
+lemma cast_lower_defl:
+ "cast\<cdot>(lower_defl\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding lower_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_lower_map)
done
-lemma cast_convex_typ:
- "cast\<cdot>(convex_typ\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding convex_typ_def
+lemma cast_convex_defl:
+ "cast\<cdot>(convex_defl\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding convex_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_convex_map)
done
text {* REP of type constructor = type combinator *}
-lemma REP_one: "REP(one) = one_typ"
-by (simp only: one_typ_def)
-
-lemma REP_tr: "REP(tr) = tr_typ"
-by (simp only: tr_typ_def)
-
-lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>REP('b)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_cfun_typ)
+apply (simp add: cast_REP cast_cfun_defl)
apply (simp add: cfun_map_def)
apply (simp only: prj_cfun_def emb_cfun_def)
apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom])
done
-lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>REP('b)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_ssum_typ)
+apply (simp add: cast_REP cast_ssum_defl)
apply (simp add: prj_ssum_def)
apply (simp add: emb_ssum_def)
apply (simp add: ssum_map_map cfcomp1)
done
-lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_defl\<cdot>REP('a)\<cdot>REP('b)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_sprod_typ)
+apply (simp add: cast_REP cast_sprod_defl)
apply (simp add: prj_sprod_def)
apply (simp add: emb_sprod_def)
apply (simp add: sprod_map_map cfcomp1)
done
-lemma REP_cprod: "REP('a \<times> 'b) = cprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cprod: "REP('a \<times> 'b) = cprod_defl\<cdot>REP('a)\<cdot>REP('b)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_cprod_typ)
+apply (simp add: cast_REP cast_cprod_defl)
apply (simp add: prj_cprod_def)
apply (simp add: emb_cprod_def)
apply (simp add: cprod_map_map cfcomp1)
done
-lemma REP_up: "REP('a u) = u_typ\<cdot>REP('a)"
+lemma REP_up: "REP('a u) = u_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_u_typ)
+apply (simp add: cast_REP cast_u_defl)
apply (simp add: prj_u_def)
apply (simp add: emb_u_def)
apply (simp add: u_map_map cfcomp1)
done
-lemma REP_upper: "REP('a upper_pd) = upper_typ\<cdot>REP('a)"
+lemma REP_upper: "REP('a upper_pd) = upper_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_upper_typ)
+apply (simp add: cast_REP cast_upper_defl)
apply (simp add: prj_upper_pd_def)
apply (simp add: emb_upper_pd_def)
apply (simp add: upper_map_map cfcomp1)
done
-lemma REP_lower: "REP('a lower_pd) = lower_typ\<cdot>REP('a)"
+lemma REP_lower: "REP('a lower_pd) = lower_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_lower_typ)
+apply (simp add: cast_REP cast_lower_defl)
apply (simp add: prj_lower_pd_def)
apply (simp add: emb_lower_pd_def)
apply (simp add: lower_map_map cfcomp1)
done
-lemma REP_convex: "REP('a convex_pd) = convex_typ\<cdot>REP('a)"
+lemma REP_convex: "REP('a convex_pd) = convex_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_convex_typ)
+apply (simp add: cast_REP cast_convex_defl)
apply (simp add: prj_convex_pd_def)
apply (simp add: emb_convex_pd_def)
apply (simp add: convex_map_map cfcomp1)
done
lemmas REP_simps =
- REP_one
- REP_tr
REP_cfun
REP_ssum
REP_sprod
@@ -944,69 +955,111 @@
apply (simp add: emb_coerce coerce_prj REP)
done
+lemma isodefl_abs_rep:
+ fixes abs and rep and d
+ assumes REP: "REP('b) = REP('a)"
+ assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+ assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
+unfolding abs_def rep_def using REP by (rule isodefl_coerce)
+
lemma isodefl_cfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_typ\<cdot>t1\<cdot>t2)"
+ isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_cfun_typ cast_isodefl)
+apply (simp add: cast_cfun_defl cast_isodefl)
apply (simp add: emb_cfun_def prj_cfun_def)
apply (simp add: cfun_map_map cfcomp1)
done
lemma isodefl_ssum:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_typ\<cdot>t1\<cdot>t2)"
+ isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_ssum_typ cast_isodefl)
+apply (simp add: cast_ssum_defl cast_isodefl)
apply (simp add: emb_ssum_def prj_ssum_def)
apply (simp add: ssum_map_map isodefl_strict)
done
lemma isodefl_sprod:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_typ\<cdot>t1\<cdot>t2)"
+ isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_sprod_typ cast_isodefl)
+apply (simp add: cast_sprod_defl cast_isodefl)
apply (simp add: emb_sprod_def prj_sprod_def)
apply (simp add: sprod_map_map isodefl_strict)
done
+lemma isodefl_cprod:
+ "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+ isodefl (cprod_map\<cdot>d1\<cdot>d2) (cprod_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_cprod_defl cast_isodefl)
+apply (simp add: emb_cprod_def prj_cprod_def)
+apply (simp add: cprod_map_map cfcomp1)
+done
+
lemma isodefl_u:
- "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_u_typ cast_isodefl)
+apply (simp add: cast_u_defl cast_isodefl)
apply (simp add: emb_u_def prj_u_def)
apply (simp add: u_map_map)
done
-lemma isodefl_one: "isodefl (ID :: one \<rightarrow> one) one_typ"
-unfolding one_typ_def by (rule isodefl_ID_REP)
-
-lemma isodefl_tr: "isodefl (ID :: tr \<rightarrow> tr) tr_typ"
-unfolding tr_typ_def by (rule isodefl_ID_REP)
-
lemma isodefl_upper:
- "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_upper_typ cast_isodefl)
+apply (simp add: cast_upper_defl cast_isodefl)
apply (simp add: emb_upper_pd_def prj_upper_pd_def)
apply (simp add: upper_map_map)
done
lemma isodefl_lower:
- "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_lower_typ cast_isodefl)
+apply (simp add: cast_lower_defl cast_isodefl)
apply (simp add: emb_lower_pd_def prj_lower_pd_def)
apply (simp add: lower_map_map)
done
lemma isodefl_convex:
- "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_convex_typ cast_isodefl)
+apply (simp add: cast_convex_defl cast_isodefl)
apply (simp add: emb_convex_pd_def prj_convex_pd_def)
apply (simp add: convex_map_map)
done
+subsection {* Constructing Domain Isomorphisms *}
+
+use "Tools/Domain/domain_isomorphism.ML"
+
+setup {*
+ fold Domain_Isomorphism.add_type_constructor
+ [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map},
+ @{thm REP_cfun}, @{thm isodefl_cfun}),
+
+ (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map},
+ @{thm REP_ssum}, @{thm isodefl_ssum}),
+
+ (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map},
+ @{thm REP_sprod}, @{thm isodefl_sprod}),
+
+ (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map},
+ @{thm REP_cprod}, @{thm isodefl_cprod}),
+
+ (@{type_name "u"}, @{term u_defl}, @{const_name u_map},
+ @{thm REP_up}, @{thm isodefl_u}),
+
+ (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
+ @{thm REP_upper}, @{thm isodefl_upper}),
+
+ (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
+ @{thm REP_lower}, @{thm isodefl_lower}),
+
+ (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
+ @{thm REP_convex}, @{thm isodefl_convex})]
+*}
+
end
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Fri Nov 20 07:24:21 2009 +0100
@@ -6,13 +6,16 @@
signature DOMAIN_AXIOMS =
sig
- val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
+ val copy_of_dtyp :
+ string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
val calc_axioms :
+ bool -> string Symtab.table ->
string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
string * (string * term) list * (string * term) list
val add_axioms :
+ bool ->
bstring -> Domain_Library.eq list -> theory -> theory
end;
@@ -34,119 +37,124 @@
(@{type_name "*"}, @{const_name "cprod_map"}),
(@{type_name "u"}, @{const_name "u_map"})];
-fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
-and copy r (DatatypeAux.DtRec i) = r i
- | copy r (DatatypeAux.DtTFree a) = ID
- | copy r (DatatypeAux.DtType (c, ds)) =
- case Symtab.lookup copy_tab c of
- SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds)
+fun copy_of_dtyp tab r dt =
+ if DatatypeAux.is_rec_type dt then copy tab r dt else ID
+and copy tab r (DatatypeAux.DtRec i) = r i
+ | copy tab r (DatatypeAux.DtTFree a) = ID
+ | copy tab r (DatatypeAux.DtType (c, ds)) =
+ case Symtab.lookup tab c of
+ SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
| NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
fun calc_axioms
- (comp_dname : string)
- (eqs : eq list)
- (n : int)
- (eqn as ((dname,_),cons) : eq)
+ (definitional : bool)
+ (map_tab : string Symtab.table)
+ (comp_dname : string)
+ (eqs : eq list)
+ (n : int)
+ (eqn as ((dname,_),cons) : eq)
: string * (string * term) list * (string * term) list =
- let
-
- (* ----- axioms and definitions concerning the isomorphism ------------------ *)
+ let
- val dc_abs = %%:(dname^"_abs");
- val dc_rep = %%:(dname^"_rep");
- val x_name'= "x";
- val x_name = idx_name eqs x_name' (n+1);
- val dnam = Long_Name.base_name dname;
+(* ----- axioms and definitions concerning the isomorphism ------------------ *)
- val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
- val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
+ val dc_abs = %%:(dname^"_abs");
+ val dc_rep = %%:(dname^"_rep");
+ val x_name'= "x";
+ val x_name = idx_name eqs x_name' (n+1);
+ val dnam = Long_Name.base_name dname;
+
+ val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
+ val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
- val when_def = ("when_def",%%:(dname^"_when") ==
- List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
- Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
-
- val copy_def =
- let fun r i = proj (Bound 0) eqs i;
- in ("copy_def", %%:(dname^"_copy") ==
- /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end;
-
- (* -- definitions concerning the constructors, discriminators and selectors - *)
+ val when_def = ("when_def",%%:(dname^"_when") ==
+ List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
+ Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
- fun con_def m n (_,args) = let
- fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
- fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
- fun inj y 1 _ = y
- | inj y _ 0 = mk_sinl y
- | inj y i j = mk_sinr (inj y (i-1) (j-1));
- in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
-
- val con_defs = mapn (fn n => fn (con,args) =>
- (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
+ val copy_def =
+ let fun r i = proj (Bound 0) eqs i;
+ in
+ ("copy_def", %%:(dname^"_copy") == /\ "f"
+ (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
+ end;
+
+(* -- definitions concerning the constructors, discriminators and selectors - *)
+
+ fun con_def m n (_,args) = let
+ fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
+ fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
+ fun inj y 1 _ = y
+ | inj y _ 0 = mk_sinl y
+ | inj y i j = mk_sinr (inj y (i-1) (j-1));
+ in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
- val dis_defs = let
- fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
- list_ccomb(%%:(dname^"_when"),map
- (fn (con',args) => (List.foldr /\#
+ val con_defs = mapn (fn n => fn (con,args) =>
+ (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
+
+ val dis_defs = let
+ fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
+ list_ccomb(%%:(dname^"_when"),map
+ (fn (con',args) => (List.foldr /\#
(if con'=con then TT else FF) args)) cons))
- in map ddef cons end;
-
- val mat_defs =
- let
- fun mdef (con,_) =
- let
- val k = Bound 0
- val x = Bound 1
- fun one_con (con', args') =
- if con'=con then k else List.foldr /\# mk_fail args'
- val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
- val rhs = /\ "x" (/\ "k" (w ` x))
- in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
- in map mdef cons end;
+ in map ddef cons end;
- val pat_defs =
+ val mat_defs =
+ let
+ fun mdef (con,_) =
+ let
+ val k = Bound 0
+ val x = Bound 1
+ fun one_con (con', args') =
+ if con'=con then k else List.foldr /\# mk_fail args'
+ val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
+ val rhs = /\ "x" (/\ "k" (w ` x))
+ in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
+ in map mdef cons end;
+
+ val pat_defs =
+ let
+ fun pdef (con,args) =
let
- fun pdef (con,args) =
- let
- val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
- val xs = map (bound_arg args) args;
- val r = Bound (length args);
- val rhs = case args of [] => mk_return HOLogic.unit
- | _ => mk_ctuple_pat ps ` mk_ctuple xs;
- fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
- in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) ==
- list_ccomb(%%:(dname^"_when"), map one_con cons))
- end
- in map pdef cons end;
+ val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
+ val xs = map (bound_arg args) args;
+ val r = Bound (length args);
+ val rhs = case args of [] => mk_return HOLogic.unit
+ | _ => mk_ctuple_pat ps ` mk_ctuple xs;
+ fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
+ in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) ==
+ list_ccomb(%%:(dname^"_when"), map one_con cons))
+ end
+ in map pdef cons end;
- val sel_defs = let
- fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel ==
- list_ccomb(%%:(dname^"_when"),map
- (fn (con',args) => if con'<>con then UU else
- List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
- in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
+ val sel_defs = let
+ fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel ==
+ list_ccomb(%%:(dname^"_when"),map
+ (fn (con',args) => if con'<>con then UU else
+ List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
+ in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
- (* ----- axiom and definitions concerning induction ------------------------- *)
+(* ----- axiom and definitions concerning induction ------------------------- *)
- val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
- `%x_name === %:x_name));
- val take_def =
- ("take_def",
- %%:(dname^"_take") ==
- mk_lam("n",proj
- (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
- val finite_def =
- ("finite_def",
- %%:(dname^"_finite") ==
- mk_lam(x_name,
- mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
+ val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
+ `%x_name === %:x_name));
+ val take_def =
+ ("take_def",
+ %%:(dname^"_take") ==
+ mk_lam("n",proj
+ (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
+ val finite_def =
+ ("finite_def",
+ %%:(dname^"_finite") ==
+ mk_lam(x_name,
+ mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
- in (dnam,
- [abs_iso_ax, rep_iso_ax, reach_ax],
- [when_def, copy_def] @
- con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
- [take_def, finite_def])
- end; (* let (calc_axioms) *)
+ in (dnam,
+ (if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax]),
+ (if definitional then [when_def] else [when_def, copy_def]) @
+ con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
+ [take_def, finite_def])
+ end; (* let (calc_axioms) *)
(* legacy type inference *)
@@ -173,16 +181,17 @@
val ms = map qualify con_names ~~ map qualify mat_names;
in Fixrec.add_matchers ms thy end;
-fun add_axioms comp_dnam (eqs : eq list) thy' =
- let
- val comp_dname = Sign.full_bname thy' comp_dnam;
- val dnames = map (fst o fst) eqs;
- val x_name = idx_name dnames "x";
- fun copy_app dname = %%:(dname^"_copy")`Bound 0;
- val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
- /\ "f"(mk_ctuple (map copy_app dnames)));
+fun add_axioms definitional comp_dnam (eqs : eq list) thy' =
+ let
+ val comp_dname = Sign.full_bname thy' comp_dnam;
+ val dnames = map (fst o fst) eqs;
+ val x_name = idx_name dnames "x";
+ fun copy_app dname = %%:(dname^"_copy")`Bound 0;
+ val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
+ /\ "f"(mk_ctuple (map copy_app dnames)));
- fun one_con (con,args) = let
+ fun one_con (con,args) =
+ let
val nonrec_args = filter_out is_rec args;
val rec_args = filter is_rec args;
val recs_cnt = length rec_args;
@@ -199,37 +208,45 @@
fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $
Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
val capps =
- List.foldr mk_conj
- (mk_conj(
- Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
- Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
- (mapn rel_app 1 rec_args);
- in List.foldr mk_ex
- (Library.foldr mk_conj
- (map (defined o Bound) nonlazy_idxs,capps)) allvns
+ List.foldr
+ mk_conj
+ (mk_conj(
+ Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
+ Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
+ (mapn rel_app 1 rec_args);
+ in
+ List.foldr
+ mk_ex
+ (Library.foldr mk_conj
+ (map (defined o Bound) nonlazy_idxs,capps)) allvns
end;
- fun one_comp n (_,cons) =
- mk_all(x_name(n+1),
- mk_all(x_name(n+1)^"'",
- mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
- foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
- ::map one_con cons))));
- val bisim_def =
- ("bisim_def",
- %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
-
- fun add_one (dnam, axs, dfs) =
- Sign.add_path dnam
+ fun one_comp n (_,cons) =
+ mk_all (x_name(n+1),
+ mk_all (x_name(n+1)^"'",
+ mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
+ foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
+ ::map one_con cons))));
+ val bisim_def =
+ ("bisim_def", %%:(comp_dname^"_bisim") ==
+ mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
+
+ fun add_one (dnam, axs, dfs) =
+ Sign.add_path dnam
#> add_defs_infer dfs
#> add_axioms_infer axs
#> Sign.parent_path;
- val thy = fold add_one (mapn (calc_axioms comp_dname eqs) 0 eqs) thy';
+ val map_tab = Domain_Isomorphism.get_map_tab thy';
+
+ val thy = thy'
+ |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs);
- in thy |> Sign.add_path comp_dnam
- |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
- |> Sign.parent_path
- |> fold add_matchers eqs
- end; (* let (add_axioms) *)
+ in
+ thy
+ |> Sign.add_path comp_dnam
+ |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
+ |> Sign.parent_path
+ |> fold add_matchers eqs
+ end; (* let (add_axioms) *)
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Fri Nov 20 07:24:21 2009 +0100
@@ -6,14 +6,29 @@
signature DOMAIN_EXTENDER =
sig
- val add_domain_cmd: string ->
- ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * string) list * mixfix) list) list
- -> theory -> theory
- val add_domain: string ->
- ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * typ) list * mixfix) list) list
- -> theory -> theory
+ val add_domain_cmd:
+ string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list
+ -> theory -> theory
+
+ val add_domain:
+ string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
+ -> theory -> theory
+
+ val add_new_domain_cmd:
+ string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list
+ -> theory -> theory
+
+ val add_new_domain:
+ string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
+ -> theory -> theory
end;
structure Domain_Extender :> DOMAIN_EXTENDER =
@@ -23,132 +38,231 @@
(* ----- general testing and preprocessing of constructor list -------------- *)
fun check_and_sort_domain
- (dtnvs : (string * typ list) list)
- (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
- (sg : theory)
+ (definitional : bool)
+ (dtnvs : (string * typ list) list)
+ (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
+ (thy : theory)
: ((string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list) list =
- let
- val defaultS = Sign.defaultS sg;
- val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
- [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
- val test_dupl_cons =
- (case duplicates (op =) (map (Binding.name_of o first) (flat cons'')) of
- [] => false | dups => error ("Duplicate constructors: "
- ^ commas_quote dups));
- val test_dupl_sels =
- (case duplicates (op =) (map Binding.name_of (map_filter second
- (maps second (flat cons'')))) of
- [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
- val test_dupl_tvars =
- exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
- [] => false | dups => error("Duplicate type arguments: "
- ^commas_quote dups)) (map snd dtnvs);
- (* test for free type variables, illegal sort constraints on rhs,
- non-pcpo-types and invalid use of recursive type;
- replace sorts in type variables on rhs *)
- fun analyse_equation ((dname,typevars),cons') =
- let
- val tvars = map dest_TFree typevars;
- val distinct_typevars = map TFree tvars;
- fun rm_sorts (TFree(s,_)) = TFree(s,[])
- | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
- | rm_sorts (TVar(s,_)) = TVar(s,[])
- and remove_sorts l = map rm_sorts l;
- val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
- fun analyse indirect (TFree(v,s)) =
- (case AList.lookup (op =) tvars v of
- NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
- | SOME sort => if eq_set (op =) (s, defaultS) orelse
- eq_set (op =) (s, sort)
- then TFree(v,sort)
- else error ("Inconsistent sort constraint" ^
- " for type variable " ^ quote v))
- | analyse indirect (t as Type(s,typl)) =
- (case AList.lookup (op =) dtnvs s of
- NONE => if s mem indirect_ok
- then Type(s,map (analyse false) typl)
- else Type(s,map (analyse true) typl)
- | SOME typevars => if indirect
- then error ("Indirect recursion of type " ^
- quote (string_of_typ sg t))
- else if dname <> s orelse
- (** BUG OR FEATURE?:
- mutual recursion may use different arguments **)
- remove_sorts typevars = remove_sorts typl
- then Type(s,map (analyse true) typl)
- else error ("Direct recursion of type " ^
- quote (string_of_typ sg t) ^
- " with different arguments"))
- | analyse indirect (TVar _) = Imposs "extender:analyse";
- fun check_pcpo lazy T =
- let val ok = if lazy then cpo_type else pcpo_type
- in if ok sg T then T else error
- ("Constructor argument type is not of sort pcpo: " ^
- string_of_typ sg T)
- end;
- fun analyse_arg (lazy, sel, T) =
- (lazy, sel, check_pcpo lazy (analyse false T));
- fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
- in ((dname,distinct_typevars), map analyse_con cons') end;
- in ListPair.map analyse_equation (dtnvs,cons'')
- end; (* let *)
+ let
+ val defaultS = Sign.defaultS thy;
+
+ val test_dupl_typs =
+ case duplicates (op =) (map fst dtnvs) of
+ [] => false | dups => error ("Duplicate types: " ^ commas_quote dups);
+
+ val all_cons = map (Binding.name_of o first) (flat cons'');
+ val test_dupl_cons =
+ case duplicates (op =) all_cons of
+ [] => false | dups => error ("Duplicate constructors: "
+ ^ commas_quote dups);
+ val all_sels =
+ (map Binding.name_of o map_filter second o maps second) (flat cons'');
+ val test_dupl_sels =
+ case duplicates (op =) all_sels of
+ [] => false | dups => error("Duplicate selectors: "^commas_quote dups);
+
+ fun test_dupl_tvars s =
+ case duplicates (op =) (map(fst o dest_TFree)s) of
+ [] => false | dups => error("Duplicate type arguments: "
+ ^commas_quote dups);
+ val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs);
+
+ (* test for free type variables, illegal sort constraints on rhs,
+ non-pcpo-types and invalid use of recursive type;
+ replace sorts in type variables on rhs *)
+ fun analyse_equation ((dname,typevars),cons') =
+ let
+ val tvars = map dest_TFree typevars;
+ val distinct_typevars = map TFree tvars;
+ fun rm_sorts (TFree(s,_)) = TFree(s,[])
+ | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
+ | rm_sorts (TVar(s,_)) = TVar(s,[])
+ and remove_sorts l = map rm_sorts l;
+ val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
+ fun analyse indirect (TFree(v,s)) =
+ (case AList.lookup (op =) tvars v of
+ NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
+ | SOME sort => if eq_set (op =) (s, defaultS) orelse
+ eq_set (op =) (s, sort)
+ then TFree(v,sort)
+ else error ("Inconsistent sort constraint" ^
+ " for type variable " ^ quote v))
+ | analyse indirect (t as Type(s,typl)) =
+ (case AList.lookup (op =) dtnvs s of
+ NONE =>
+ if definitional orelse s mem indirect_ok
+ then Type(s,map (analyse false) typl)
+ else Type(s,map (analyse true) typl)
+ | SOME typevars =>
+ if indirect
+ then error ("Indirect recursion of type " ^
+ quote (string_of_typ thy t))
+ else if dname <> s orelse
+ (** BUG OR FEATURE?:
+ mutual recursion may use different arguments **)
+ remove_sorts typevars = remove_sorts typl
+ then Type(s,map (analyse true) typl)
+ else error ("Direct recursion of type " ^
+ quote (string_of_typ thy t) ^
+ " with different arguments"))
+ | analyse indirect (TVar _) = Imposs "extender:analyse";
+ fun check_pcpo lazy T =
+ let val ok = if lazy then cpo_type else pcpo_type
+ in if ok thy T then T
+ else error ("Constructor argument type is not of sort pcpo: " ^
+ string_of_typ thy T)
+ end;
+ fun analyse_arg (lazy, sel, T) =
+ (lazy, sel, check_pcpo lazy (analyse false T));
+ fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
+ in ((dname,distinct_typevars), map analyse_con cons') end;
+ in ListPair.map analyse_equation (dtnvs,cons'')
+ end; (* let *)
(* ----- calls for building new thy and thms -------------------------------- *)
fun gen_add_domain
- (prep_typ : theory -> 'a -> typ)
- (comp_dnam : string)
- (eqs''' : ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * 'a) list * mixfix) list) list)
- (thy''' : theory) =
- let
- fun readS (SOME s) = Syntax.read_sort_global thy''' s
- | readS NONE = Sign.defaultS thy''';
- fun readTFree (a, s) = TFree (a, readS s);
+ (prep_typ : theory -> 'a -> typ)
+ (comp_dnam : string)
+ (eqs''' : ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * 'a) list * mixfix) list) list)
+ (thy''' : theory) =
+ let
+ fun readS (SOME s) = Syntax.read_sort_global thy''' s
+ | readS NONE = Sign.defaultS thy''';
+ fun readTFree (a, s) = TFree (a, readS s);
+
+ val dtnvs = map (fn (vs,dname:binding,mx,_) =>
+ (dname, map readTFree vs, mx)) eqs''';
+ val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
+ fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
+ fun thy_arity (dname,tvars,mx) =
+ (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
+ val thy'' =
+ thy'''
+ |> Sign.add_types (map thy_type dtnvs)
+ |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+ val cons'' =
+ map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
+ val dtnvs' =
+ map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+ val eqs' : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list =
+ check_and_sort_domain false dtnvs' cons'' thy'';
+ val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
+ val dts = map (Type o fst) eqs';
+ val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+ fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
+ fun typid (Type (id,_)) =
+ let val c = hd (Symbol.explode (Long_Name.base_name id))
+ in if Symbol.is_letter c then c else "t" end
+ | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
+ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
+ fun one_con (con,args,mx) =
+ ((Syntax.const_name mx (Binding.name_of con)),
+ ListPair.map (fn ((lazy,sel,tp),vn) =>
+ mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
+ Option.map Binding.name_of sel,vn))
+ (args,(mk_var_names(map (typid o third) args)))
+ ) : cons;
+ val eqs : eq list =
+ map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
+ val thy = thy' |> Domain_Axioms.add_axioms false comp_dnam eqs;
+ val ((rewss, take_rews), theorems_thy) =
+ thy
+ |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+ in
+ theorems_thy
+ |> Sign.add_path (Long_Name.base_name comp_dnam)
+ |> PureThy.add_thmss
+ [((Binding.name "rews", flat rewss @ take_rews), [])]
+ |> snd
+ |> Sign.parent_path
+ end;
- val dtnvs = map (fn (vs,dname:binding,mx,_) =>
- (dname, map readTFree vs, mx)) eqs''';
- val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
- fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
- fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
- val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
- |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
- val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
- val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
- val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list =
- check_and_sort_domain dtnvs' cons'' thy'';
- val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
- val dts = map (Type o fst) eqs';
- val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
- fun typid (Type (id,_)) =
- let val c = hd (Symbol.explode (Long_Name.base_name id))
- in if Symbol.is_letter c then c else "t" end
- | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
- | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
- fun one_con (con,args,mx) =
- ((Syntax.const_name mx (Binding.name_of con)),
- ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
- DatatypeAux.dtyp_of_typ new_dts tp),
- Option.map Binding.name_of sel,vn))
- (args,(mk_var_names(map (typid o third) args)))
- ) : cons;
- val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
- val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
- val ((rewss, take_rews), theorems_thy) =
- thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
- ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
- in
- theorems_thy
- |> Sign.add_path (Long_Name.base_name comp_dnam)
- |> (snd o (PureThy.add_thmss [((Binding.name "rews", flat rewss @ take_rews), [])]))
- |> Sign.parent_path
- end;
+fun gen_add_new_domain
+ (prep_typ : theory -> 'a -> typ)
+ (comp_dnam : string)
+ (eqs''' : ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * 'a) list * mixfix) list) list)
+ (thy''' : theory) =
+ let
+ fun readS (SOME s) = Syntax.read_sort_global thy''' s
+ | readS NONE = Sign.defaultS thy''';
+ fun readTFree (a, s) = TFree (a, readS s);
+
+ val dtnvs = map (fn (vs,dname:binding,mx,_) =>
+ (dname, map readTFree vs, mx)) eqs''';
+ val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
+ fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
+ fun thy_arity (dname,tvars,mx) =
+ (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, @{sort rep});
+
+ (* this theory is used just for parsing and error checking *)
+ val tmp_thy = thy'''
+ |> Theory.copy
+ |> Sign.add_types (map thy_type dtnvs)
+ |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+
+ val cons'' : (binding * (bool * binding option * typ) list * mixfix) list list =
+ map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
+ val dtnvs' : (string * typ list) list =
+ map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+ val eqs' : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list =
+ check_and_sort_domain true dtnvs' cons'' tmp_thy;
+
+ fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
+ fun mk_con_typ (bind, args, mx) =
+ if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
+ fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
+
+ val thy'' = thy''' |>
+ Domain_Isomorphism.domain_isomorphism
+ (map (fn ((vs, dname, mx, _), eq) =>
+ (map fst vs, dname, mx, mk_eq_typ eq))
+ (eqs''' ~~ eqs'))
+
+ val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
+ val dts = map (Type o fst) eqs';
+ val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+ fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
+ fun typid (Type (id,_)) =
+ let val c = hd (Symbol.explode (Long_Name.base_name id))
+ in if Symbol.is_letter c then c else "t" end
+ | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
+ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
+ fun one_con (con,args,mx) =
+ ((Syntax.const_name mx (Binding.name_of con)),
+ ListPair.map (fn ((lazy,sel,tp),vn) =>
+ mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
+ Option.map Binding.name_of sel,vn))
+ (args,(mk_var_names(map (typid o third) args)))
+ ) : cons;
+ val eqs : eq list =
+ map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
+ val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs;
+ val ((rewss, take_rews), theorems_thy) =
+ thy
+ |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+ in
+ theorems_thy
+ |> Sign.add_path (Long_Name.base_name comp_dnam)
+ |> PureThy.add_thmss
+ [((Binding.name "rews", flat rewss @ take_rews), [])]
+ |> snd
+ |> Sign.parent_path
+ end;
val add_domain = gen_add_domain Sign.certify_typ;
val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
+val add_new_domain = gen_add_new_domain Sign.certify_typ;
+val add_new_domain_cmd = gen_add_new_domain Syntax.read_typ_global;
+
(** outer syntax **)
@@ -157,47 +271,57 @@
val _ = OuterKeyword.keyword "lazy";
val dest_decl : (bool * binding option * string) parser =
- P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
- (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
- || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
- >> (fn t => (true,NONE,t))
- || P.typ >> (fn t => (false,NONE,t));
+ P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
+ (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
+ || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
+ >> (fn t => (true,NONE,t))
+ || P.typ >> (fn t => (false,NONE,t));
val cons_decl =
- P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
+ P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
val type_var' : (string * string option) parser =
- (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
+ (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
val type_args' : (string * string option) list parser =
- type_var' >> single ||
- P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
- Scan.succeed [];
+ type_var' >> single
+ || P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")")
+ || Scan.succeed [];
val domain_decl =
- (type_args' -- P.binding -- P.opt_infix) --
- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+ (type_args' -- P.binding -- P.opt_infix) --
+ (P.$$$ "=" |-- P.enum1 "|" cons_decl);
val domains_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
- P.and_list1 domain_decl;
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+ P.and_list1 domain_decl;
-fun mk_domain (opt_name : string option,
- doms : ((((string * string option) list * binding) * mixfix) *
- ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
- let
- val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
- val specs : ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * string) list * mixfix) list) list =
- map (fn (((vs, t), mx), cons) =>
- (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
- val comp_dnam =
- case opt_name of NONE => space_implode "_" names | SOME s => s;
- in add_domain_cmd comp_dnam specs end;
+fun mk_domain
+ (definitional : bool)
+ (opt_name : string option,
+ doms : ((((string * string option) list * binding) * mixfix) *
+ ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
+ let
+ val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
+ val specs : ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list =
+ map (fn (((vs, t), mx), cons) =>
+ (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
+ val comp_dnam =
+ case opt_name of NONE => space_implode "_" names | SOME s => s;
+ in
+ if definitional
+ then add_new_domain_cmd comp_dnam specs
+ else add_domain_cmd comp_dnam specs
+ end;
val _ =
- OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
- (domains_decl >> (Toplevel.theory o mk_domain));
+ OuterSyntax.command "domain" "define recursive domains (HOLCF)"
+ K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
+
+val _ =
+ OuterSyntax.command "new_domain" "define recursive domains (HOLCF)"
+ K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 20 07:24:21 2009 +0100
@@ -0,0 +1,636 @@
+(* Title: HOLCF/Tools/domain/domain_isomorphism.ML
+ Author: Brian Huffman
+
+Defines new types satisfying the given domain equations.
+*)
+
+signature DOMAIN_ISOMORPHISM =
+sig
+ val domain_isomorphism:
+ (string list * binding * mixfix * typ) list -> theory -> theory
+ val domain_isomorphism_cmd:
+ (string list * binding * mixfix * string) list -> theory -> theory
+ val add_type_constructor:
+ (string * term * string * thm * thm) -> theory -> theory
+ val get_map_tab:
+ theory -> string Symtab.table
+end;
+
+structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM =
+struct
+
+val beta_ss =
+ HOL_basic_ss
+ addsimps simp_thms
+ addsimps [@{thm beta_cfun}]
+ addsimprocs [@{simproc cont_proc}];
+
+val beta_tac = simp_tac beta_ss;
+
+(******************************************************************************)
+(******************************** theory data *********************************)
+(******************************************************************************)
+
+structure DeflData = Theory_Data
+(
+ type T = term Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I;
+ fun merge data = Symtab.merge (K true) data;
+);
+
+structure MapData = Theory_Data
+(
+ type T = string Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I;
+ fun merge data = Symtab.merge (K true) data;
+);
+
+structure RepData = Theory_Data
+(
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ val merge = Thm.merge_thms;
+);
+
+structure IsodeflData = Theory_Data
+(
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ val merge = Thm.merge_thms;
+);
+
+fun add_type_constructor
+ (tname, defl_const, map_name, REP_thm, isodefl_thm) =
+ DeflData.map (Symtab.insert (K true) (tname, defl_const))
+ #> MapData.map (Symtab.insert (K true) (tname, map_name))
+ #> RepData.map (Thm.add_thm REP_thm)
+ #> IsodeflData.map (Thm.add_thm isodefl_thm);
+
+val get_map_tab = MapData.get;
+
+
+(******************************************************************************)
+(******************************* building types *******************************)
+(******************************************************************************)
+
+(* ->> is taken from holcf_logic.ML *)
+fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+
+infixr 6 ->>; val (op ->>) = cfunT;
+
+fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+ | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
+
+fun tupleT [] = HOLogic.unitT
+ | tupleT [T] = T
+ | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
+
+val deflT = @{typ "udom alg_defl"};
+
+fun mapT (T as Type (_, Ts)) =
+ Library.foldr cfunT (map (fn T => T ->> T) Ts, T ->> T);
+
+(******************************************************************************)
+(******************************* building terms *******************************)
+(******************************************************************************)
+
+(* builds the expression (v1,v2,..,vn) *)
+fun mk_tuple [] = HOLogic.unit
+| mk_tuple (t::[]) = t
+| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
+
+(* builds the expression (%(v1,v2,..,vn). rhs) *)
+fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
+ | lambda_tuple (v::[]) rhs = Term.lambda v rhs
+ | lambda_tuple (v::vs) rhs =
+ HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
+
+(* continuous application and abstraction *)
+
+fun capply_const (S, T) =
+ Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
+
+fun cabs_const (S, T) =
+ Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
+
+fun mk_cabs t =
+ let val T = Term.fastype_of t
+ in cabs_const (Term.domain_type T, Term.range_type T) $ t end
+
+(* builds the expression (LAM v. rhs) *)
+fun big_lambda v rhs =
+ cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
+
+(* builds the expression (LAM v1 v2 .. vn. rhs) *)
+fun big_lambdas [] rhs = rhs
+ | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
+
+fun mk_capply (t, u) =
+ let val (S, T) =
+ case Term.fastype_of t of
+ Type(@{type_name "->"}, [S, T]) => (S, T)
+ | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
+ in capply_const (S, T) $ t $ u end;
+
+(* miscellaneous term constructions *)
+
+val mk_trp = HOLogic.mk_Trueprop;
+
+val mk_fst = HOLogic.mk_fst;
+val mk_snd = HOLogic.mk_snd;
+
+fun mk_cont t =
+ let val T = Term.fastype_of t
+ in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
+
+fun mk_fix t =
+ let val (T, _) = dest_cfunT (Term.fastype_of t)
+ in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end;
+
+fun ID_const T = Const (@{const_name ID}, cfunT (T, T));
+
+fun cfcomp_const (T, U, V) =
+ Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V));
+
+fun mk_cfcomp (f, g) =
+ let
+ val (U, V) = dest_cfunT (Term.fastype_of f);
+ val (T, U') = dest_cfunT (Term.fastype_of g);
+ in
+ if U = U'
+ then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g)
+ else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
+ end;
+
+fun mk_Rep_of T =
+ Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
+
+fun coerce_const T = Const (@{const_name coerce}, T);
+
+fun isodefl_const T =
+ Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
+
+(* splits a cterm into the right and lefthand sides of equality *)
+fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
+
+fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
+
+(******************************************************************************)
+(*************** fixed-point definitions and unfolding theorems ***************)
+(******************************************************************************)
+
+fun add_fixdefs
+ (spec : (binding * term) list)
+ (thy : theory) : (thm list * thm list) * theory =
+ let
+ val binds = map fst spec;
+ val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
+ val functional = lambda_tuple lhss (mk_tuple rhss);
+ val fixpoint = mk_fix (mk_cabs functional);
+
+ (* project components of fixpoint *)
+ fun mk_projs (x::[]) t = [(x, t)]
+ | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+ val projs = mk_projs lhss fixpoint;
+
+ (* convert parameters to lambda abstractions *)
+ fun mk_eqn (lhs, rhs) =
+ case lhs of
+ Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) =>
+ mk_eqn (f, big_lambda x rhs)
+ | Const _ => Logic.mk_equals (lhs, rhs)
+ | _ => raise TERM ("lhs not of correct form", [lhs, rhs]);
+ val eqns = map mk_eqn projs;
+
+ (* register constant definitions *)
+ val (fixdef_thms, thy) =
+ (PureThy.add_defs false o map Thm.no_attributes)
+ (map (Binding.suffix_name "_def") binds ~~ eqns) thy;
+
+ (* prove applied version of definitions *)
+ fun prove_proj (lhs, rhs) =
+ let
+ val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1;
+ val goal = Logic.mk_equals (lhs, rhs);
+ in Goal.prove_global thy [] [] goal (K tac) end;
+ val proj_thms = map prove_proj projs;
+
+ (* mk_tuple lhss == fixpoint *)
+ fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
+ val tuple_fixdef_thm = foldr1 pair_equalI proj_thms;
+
+ val cont_thm =
+ Goal.prove_global thy [] [] (mk_trp (mk_cont functional))
+ (K (beta_tac 1));
+ val tuple_unfold_thm =
+ (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
+ |> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv};
+
+ fun mk_unfold_thms [] thm = []
+ | mk_unfold_thms (n::[]) thm = [(n, thm)]
+ | mk_unfold_thms (n::ns) thm = let
+ val thmL = thm RS @{thm Pair_eqD1};
+ val thmR = thm RS @{thm Pair_eqD2};
+ in (n, thmL) :: mk_unfold_thms ns thmR end;
+ val unfold_binds = map (Binding.suffix_name "_unfold") binds;
+
+ (* register unfold theorems *)
+ val (unfold_thms, thy) =
+ (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+ (mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
+ in
+ ((proj_thms, unfold_thms), thy)
+ end;
+
+
+(******************************************************************************)
+(****************** deflation combinators and map functions *******************)
+(******************************************************************************)
+
+fun defl_of_typ
+ (tab : term Symtab.table)
+ (T : typ) : term =
+ let
+ fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
+ | is_closed_typ _ = false;
+ fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
+ | defl_of (TVar _) = error ("defl_of_typ: TVar")
+ | defl_of (T as Type (c, Ts)) =
+ case Symtab.lookup tab c of
+ SOME t => Library.foldl mk_capply (t, map defl_of Ts)
+ | NONE => if is_closed_typ T
+ then mk_Rep_of T
+ else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
+ in defl_of T end;
+
+fun map_of_typ
+ (tab : string Symtab.table)
+ (T : typ) : term =
+ let
+ fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
+ | is_closed_typ _ = false;
+ fun map_of (T as TFree (a, _)) = Free (Library.unprefix "'" a, T ->> T)
+ | map_of (T as TVar _) = error ("map_of_typ: TVar")
+ | map_of (T as Type (c, Ts)) =
+ case Symtab.lookup tab c of
+ SOME t => Library.foldl mk_capply (Const (t, mapT T), map map_of Ts)
+ | NONE => if is_closed_typ T
+ then ID_const T
+ else error ("map_of_typ: type variable under unsupported type constructor " ^ c);
+ in map_of T end;
+
+
+(******************************************************************************)
+(* prepare datatype specifications *)
+
+fun read_typ thy str sorts =
+ let
+ val ctxt = ProofContext.init thy
+ |> fold (Variable.declare_typ o TFree) sorts;
+ val T = Syntax.read_typ ctxt str;
+ in (T, Term.add_tfreesT T sorts) end;
+
+fun cert_typ sign raw_T sorts =
+ let
+ val T = Type.no_tvars (Sign.certify_typ sign raw_T)
+ handle TYPE (msg, _, _) => error msg;
+ val sorts' = Term.add_tfreesT T sorts;
+ val _ =
+ case duplicates (op =) (map fst sorts') of
+ [] => ()
+ | dups => error ("Inconsistent sort constraints for " ^ commas dups)
+ in (T, sorts') end;
+
+fun gen_domain_isomorphism
+ (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
+ (doms_raw: (string list * binding * mixfix * 'a) list)
+ (thy: theory)
+ : theory =
+ let
+ val _ = Theory.requires thy "Representable" "domain isomorphisms";
+
+ (* this theory is used just for parsing *)
+ val tmp_thy = thy |>
+ Theory.copy |>
+ Sign.add_types (map (fn (tvs, tname, mx, _) =>
+ (tname, length tvs, mx)) doms_raw);
+
+ fun prep_dom thy (vs, t, mx, typ_raw) sorts =
+ let val (typ, sorts') = prep_typ thy typ_raw sorts
+ in ((vs, t, mx, typ), sorts') end;
+
+ val (doms : (string list * binding * mixfix * typ) list,
+ sorts : (string * sort) list) =
+ fold_map (prep_dom tmp_thy) doms_raw [];
+
+ (* domain equations *)
+ fun mk_dom_eqn (vs, tbind, mx, rhs) =
+ let fun arg v = TFree (v, the (AList.lookup (op =) sorts v));
+ in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end;
+ val dom_eqns = map mk_dom_eqn doms;
+
+ (* check for valid type parameters *)
+ val (tyvars, _, _, _)::_ = doms;
+ val new_doms = map (fn (tvs, tname, mx, _) =>
+ let val full_tname = Sign.full_name tmp_thy tname
+ in
+ (case duplicates (op =) tvs of
+ [] =>
+ if eq_set (op =) (tyvars, tvs) then (full_tname, tvs)
+ else error ("Mutually recursive domains must have same type parameters")
+ | dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^
+ " : " ^ commas dups))
+ end) doms;
+ val dom_binds = map (fn (_, tbind, _, _) => tbind) doms;
+
+ (* declare deflation combinator constants *)
+ fun declare_defl_const (vs, tbind, mx, rhs) thy =
+ let
+ val defl_type = Library.foldr cfunT (map (K deflT) vs, deflT);
+ val defl_bind = Binding.suffix_name "_defl" tbind;
+ in
+ Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
+ end;
+ val (defl_consts, thy) = fold_map declare_defl_const doms thy;
+
+ (* defining equations for type combinators *)
+ val defl_tab1 = DeflData.get thy;
+ val defl_tab2 =
+ Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts);
+ val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2);
+ val thy = DeflData.put defl_tab' thy;
+ fun mk_defl_spec (lhsT, rhsT) =
+ mk_eqs (defl_of_typ defl_tab' lhsT,
+ defl_of_typ defl_tab' rhsT);
+ val defl_specs = map mk_defl_spec dom_eqns;
+
+ (* register recursive definition of deflation combinators *)
+ val defl_binds = map (Binding.suffix_name "_defl") dom_binds;
+ val ((defl_apply_thms, defl_unfold_thms), thy) =
+ add_fixdefs (defl_binds ~~ defl_specs) thy;
+
+ (* define types using deflation combinators *)
+ fun make_repdef ((vs, tbind, mx, _), defl_const) thy =
+ let
+ fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
+ val reps = map (mk_Rep_of o tfree) vs;
+ val defl = Library.foldl mk_capply (defl_const, reps);
+ val ((_, _, _, {REP, ...}), thy) =
+ Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy;
+ in
+ (REP, thy)
+ end;
+ val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
+ val thy = RepData.map (fold Thm.add_thm REP_thms) thy;
+
+ (* prove REP equations *)
+ fun mk_REP_eq_thm (lhsT, rhsT) =
+ let
+ val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
+ val REP_simps = RepData.get thy;
+ val tac =
+ simp_tac (HOL_basic_ss addsimps REP_simps) 1
+ THEN resolve_tac defl_unfold_thms 1;
+ in
+ Goal.prove_global thy [] [] goal (K tac)
+ end;
+ val REP_eq_thms = map mk_REP_eq_thm dom_eqns;
+
+ (* register REP equations *)
+ val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dom_binds;
+ val (_, thy) = thy |>
+ (PureThy.add_thms o map Thm.no_attributes)
+ (REP_eq_binds ~~ REP_eq_thms);
+
+ (* define rep/abs functions *)
+ fun mk_rep_abs (tbind, (lhsT, rhsT)) thy =
+ let
+ val rep_type = cfunT (lhsT, rhsT);
+ val abs_type = cfunT (rhsT, lhsT);
+ val rep_bind = Binding.suffix_name "_rep" tbind;
+ val abs_bind = Binding.suffix_name "_abs" tbind;
+ val (rep_const, thy) = thy |>
+ Sign.declare_const ((rep_bind, rep_type), NoSyn);
+ val (abs_const, thy) = thy |>
+ Sign.declare_const ((abs_bind, abs_type), NoSyn);
+ val rep_eqn = Logic.mk_equals (rep_const, coerce_const rep_type);
+ val abs_eqn = Logic.mk_equals (abs_const, coerce_const abs_type);
+ val ([rep_def, abs_def], thy) = thy |>
+ (PureThy.add_defs false o map Thm.no_attributes)
+ [(Binding.suffix_name "_rep_def" tbind, rep_eqn),
+ (Binding.suffix_name "_abs_def" tbind, abs_eqn)];
+ in
+ (((rep_const, abs_const), (rep_def, abs_def)), thy)
+ end;
+ val ((rep_abs_consts, rep_abs_defs), thy) = thy
+ |> fold_map mk_rep_abs (dom_binds ~~ dom_eqns)
+ |>> ListPair.unzip;
+
+ (* prove isomorphism and isodefl rules *)
+ fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
+ let
+ fun make thm = Drule.standard (thm OF [REP_eq, abs_def, rep_def]);
+ val rep_iso_thm = make @{thm domain_rep_iso};
+ val abs_iso_thm = make @{thm domain_abs_iso};
+ val isodefl_thm = make @{thm isodefl_abs_rep};
+ val rep_iso_bind = Binding.name "rep_iso";
+ val abs_iso_bind = Binding.name "abs_iso";
+ val isodefl_bind = Binding.name "isodefl_abs_rep";
+ val (_, thy) = thy
+ |> Sign.add_path (Binding.name_of tbind)
+ |> (PureThy.add_thms o map Thm.no_attributes)
+ [(rep_iso_bind, rep_iso_thm),
+ (abs_iso_bind, abs_iso_thm),
+ (isodefl_bind, isodefl_thm)]
+ ||> Sign.parent_path;
+ in
+ (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy)
+ end;
+ val ((iso_thms, isodefl_abs_rep_thms), thy) = thy
+ |> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs)
+ |>> ListPair.unzip;
+
+ (* declare map functions *)
+ fun declare_map_const (tbind, (lhsT, rhsT)) thy =
+ let
+ val map_type = mapT lhsT;
+ val map_bind = Binding.suffix_name "_map" tbind;
+ in
+ Sign.declare_const ((map_bind, map_type), NoSyn) thy
+ end;
+ val (map_consts, thy) = thy |>
+ fold_map declare_map_const (dom_binds ~~ dom_eqns);
+
+ (* defining equations for map functions *)
+ val map_tab1 = MapData.get thy;
+ val map_tab2 =
+ Symtab.make (map (fst o dest_Type o fst) dom_eqns
+ ~~ map (fst o dest_Const) map_consts);
+ val map_tab' = Symtab.merge (K true) (map_tab1, map_tab2);
+ val thy = MapData.put map_tab' thy;
+ fun mk_map_spec ((rep_const, abs_const), (lhsT, rhsT)) =
+ let
+ val lhs = map_of_typ map_tab' lhsT;
+ val body = map_of_typ map_tab' rhsT;
+ val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
+ in mk_eqs (lhs, rhs) end;
+ val map_specs = map mk_map_spec (rep_abs_consts ~~ dom_eqns);
+
+ (* register recursive definition of map functions *)
+ val map_binds = map (Binding.suffix_name "_map") dom_binds;
+ val ((map_apply_thms, map_unfold_thms), thy) =
+ add_fixdefs (map_binds ~~ map_specs) thy;
+
+ (* prove isodefl rules for map functions *)
+ val isodefl_thm =
+ let
+ fun unprime a = Library.unprefix "'" a;
+ fun mk_d (TFree (a, _)) = Free ("d" ^ unprime a, deflT);
+ fun mk_f (T as TFree (a, _)) = Free ("f" ^ unprime a, T ->> T);
+ fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T);
+ fun mk_goal ((map_const, defl_const), (T as Type (c, Ts), rhsT)) =
+ let
+ val map_term = Library.foldl mk_capply (map_const, map mk_f Ts);
+ val defl_term = Library.foldl mk_capply (defl_const, map mk_d Ts);
+ in isodefl_const T $ map_term $ defl_term end;
+ val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns;
+ val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns);
+ val goal = mk_trp (foldr1 HOLogic.mk_conj goals);
+ val start_thms =
+ @{thm split_def} :: defl_apply_thms @ map_apply_thms;
+ val adm_rules =
+ @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
+ val bottom_rules =
+ @{thms fst_strict snd_strict isodefl_bottom simp_thms};
+ val isodefl_rules =
+ @{thms conjI isodefl_ID_REP}
+ @ isodefl_abs_rep_thms
+ @ IsodeflData.get thy;
+ fun tacf {prems, ...} = EVERY
+ [simp_tac (HOL_basic_ss addsimps start_thms) 1,
+ (* FIXME: how reliable is unification here? *)
+ (* Maybe I should instantiate the rule. *)
+ rtac @{thm parallel_fix_ind} 1,
+ REPEAT (resolve_tac adm_rules 1),
+ simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
+ simp_tac beta_ss 1,
+ simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
+ REPEAT (etac @{thm conjE} 1),
+ REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)];
+ in
+ Goal.prove_global thy [] assms goal tacf
+ end;
+ val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds;
+ fun conjuncts [] thm = []
+ | conjuncts (n::[]) thm = [(n, thm)]
+ | conjuncts (n::ns) thm = let
+ val thmL = thm RS @{thm conjunct1};
+ val thmR = thm RS @{thm conjunct2};
+ in (n, thmL):: conjuncts ns thmR end;
+ val (isodefl_thms, thy) = thy |>
+ (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+ (conjuncts isodefl_binds isodefl_thm);
+ val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
+
+ (* prove map_ID theorems *)
+ fun prove_map_ID_thm
+ (((map_const, (lhsT, _)), REP_thm), isodefl_thm) =
+ let
+ val Ts = snd (dest_Type lhsT);
+ val lhs = Library.foldl mk_capply (map_const, map ID_const Ts);
+ val goal = mk_eqs (lhs, ID_const lhsT);
+ val tac = EVERY
+ [rtac @{thm isodefl_REP_imp_ID} 1,
+ stac REP_thm 1,
+ rtac isodefl_thm 1,
+ REPEAT (rtac @{thm isodefl_ID_REP} 1)];
+ in
+ Goal.prove_global thy [] [] goal (K tac)
+ end;
+ val map_ID_binds = map (Binding.suffix_name "_map_ID") dom_binds;
+ val map_ID_thms =
+ map prove_map_ID_thm
+ (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms);
+ val (_, thy) = thy |>
+ (PureThy.add_thms o map Thm.no_attributes)
+ (map_ID_binds ~~ map_ID_thms);
+
+ (* define copy combinators *)
+ val new_dts =
+ map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns;
+ val copy_arg_type = tupleT (map (fn (T, _) => T ->> T) dom_eqns);
+ val copy_args =
+ let fun mk_copy_args [] t = []
+ | mk_copy_args (_::[]) t = [t]
+ | mk_copy_args (_::xs) t =
+ HOLogic.mk_fst t :: mk_copy_args xs (HOLogic.mk_snd t);
+ in mk_copy_args doms (Free ("f", copy_arg_type)) end;
+ fun copy_of_dtyp (T, dt) =
+ if DatatypeAux.is_rec_type dt
+ then copy_of_dtyp' (T, dt)
+ else ID_const T
+ and copy_of_dtyp' (T, DatatypeAux.DtRec i) = nth copy_args i
+ | copy_of_dtyp' (T, DatatypeAux.DtTFree a) = ID_const T
+ | copy_of_dtyp' (T as Type (_, Ts), DatatypeAux.DtType (c, ds)) =
+ case Symtab.lookup map_tab' c of
+ SOME f =>
+ Library.foldl mk_capply
+ (Const (f, mapT T), map copy_of_dtyp (Ts ~~ ds))
+ | NONE =>
+ (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID_const T);
+ fun define_copy ((tbind, (rep_const, abs_const)), (lhsT, rhsT)) thy =
+ let
+ val copy_type = copy_arg_type ->> (lhsT ->> lhsT);
+ val copy_bind = Binding.suffix_name "_copy" tbind;
+ val (copy_const, thy) = thy |>
+ Sign.declare_const ((copy_bind, copy_type), NoSyn);
+ val dtyp = DatatypeAux.dtyp_of_typ new_dts rhsT;
+ val body = copy_of_dtyp (rhsT, dtyp);
+ val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
+ val rhs = big_lambda (Free ("f", copy_arg_type)) comp;
+ val eqn = Logic.mk_equals (copy_const, rhs);
+ val ([copy_def], thy) =
+ thy
+ |> Sign.add_path (Binding.name_of tbind)
+ |> (PureThy.add_defs false o map Thm.no_attributes)
+ [(Binding.name "copy_def", eqn)]
+ ||> Sign.parent_path;
+ in ((copy_const, copy_def), thy) end;
+ val ((copy_consts, copy_defs), thy) = thy
+ |> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns)
+ |>> ListPair.unzip;
+
+ in
+ thy
+ end;
+
+val domain_isomorphism = gen_domain_isomorphism cert_typ;
+val domain_isomorphism_cmd = gen_domain_isomorphism read_typ;
+
+(******************************************************************************)
+(******************************** outer syntax ********************************)
+(******************************************************************************)
+
+local
+
+structure P = OuterParse and K = OuterKeyword
+
+val parse_domain_iso : (string list * binding * mixfix * string) parser =
+ (P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ))
+ >> (fn (((vs, t), mx), rhs) => (vs, t, mx, rhs));
+
+val parse_domain_isos = P.and_list1 parse_domain_iso;
+
+in
+
+val _ =
+ OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl
+ (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd));
+
+end;
+
+end;
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Fri Nov 20 07:24:21 2009 +0100
@@ -7,12 +7,14 @@
signature DOMAIN_SYNTAX =
sig
val calc_syntax:
+ bool ->
typ ->
(string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list ->
(binding * typ * mixfix) list * ast Syntax.trrule list
val add_syntax:
+ bool ->
string ->
((string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list) list ->
@@ -27,155 +29,176 @@
infixr 5 -->; infixr 6 ->>;
fun calc_syntax
- (dtypeprod : typ)
- ((dname : string, typevars : typ list),
- (cons': (binding * (bool * binding option * typ) list * mixfix) list))
+ (definitional : bool)
+ (dtypeprod : typ)
+ ((dname : string, typevars : typ list),
+ (cons': (binding * (bool * binding option * typ) list * mixfix) list))
: (binding * typ * mixfix) list * ast Syntax.trrule list =
- let
- (* ----- constants concerning the isomorphism ------------------------------- *)
+ let
+(* ----- constants concerning the isomorphism ------------------------------- *)
+ local
+ fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
+ fun prod (_,args,_) = case args of [] => oneT
+ | _ => foldr1 mk_sprodT (map opt_lazy args);
+ fun freetvar s = let val tvar = mk_TFree s in
+ if tvar mem typevars then freetvar ("t"^s) else tvar end;
+ fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
+ in
+ val dtype = Type(dname,typevars);
+ val dtype2 = foldr1 mk_ssumT (map prod cons');
+ val dnam = Long_Name.base_name dname;
+ fun dbind s = Binding.name (dnam ^ s);
+ val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn);
+ val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn);
+ val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
+ val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
+ end;
- local
- fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
- fun prod (_,args,_) = case args of [] => oneT
- | _ => foldr1 mk_sprodT (map opt_lazy args);
- fun freetvar s = let val tvar = mk_TFree s in
- if tvar mem typevars then freetvar ("t"^s) else tvar end;
- fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
- in
- val dtype = Type(dname,typevars);
- val dtype2 = foldr1 mk_ssumT (map prod cons');
- val dnam = Long_Name.base_name dname;
- fun dbind s = Binding.name (dnam ^ s);
- val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn);
- val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn);
- val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
- val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
- end;
+(* ----- constants concerning constructors, discriminators, and selectors --- *)
+
+ local
+ val escape = let
+ fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
+ else c::esc cs
+ | esc [] = []
+ in implode o esc o Symbol.explode end;
- (* ----- constants concerning constructors, discriminators, and selectors --- *)
+ fun dis_name_ con =
+ Binding.name ("is_" ^ strip_esc (Binding.name_of con));
+ fun mat_name_ con =
+ Binding.name ("match_" ^ strip_esc (Binding.name_of con));
+ fun pat_name_ con =
+ Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
+ fun con (name,args,mx) =
+ (name, List.foldr (op ->>) dtype (map third args), mx);
+ fun dis (con,args,mx) =
+ (dis_name_ con, dtype->>trT,
+ Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
+ (* strictly speaking, these constants have one argument,
+ but the mixfix (without arguments) is introduced only
+ to generate parse rules for non-alphanumeric names*)
+ fun freetvar s n =
+ let val tvar = mk_TFree (s ^ string_of_int n)
+ in if tvar mem typevars then freetvar ("t"^s) n else tvar end;
- local
- val escape = let
- fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
- else c::esc cs
- | esc [] = []
- in implode o esc o Symbol.explode end;
- fun dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con));
- fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con));
- fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
- fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx);
- fun dis (con,args,mx) = (dis_name_ con, dtype->>trT,
- Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
- (* strictly speaking, these constants have one argument,
- but the mixfix (without arguments) is introduced only
- to generate parse rules for non-alphanumeric names*)
- fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in
- if tvar mem typevars then freetvar ("t"^s) n else tvar end;
- fun mk_matT (a,bs,c) = a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
- fun mat (con,args,mx) = (mat_name_ con,
- mk_matT(dtype, map third args, freetvar "t" 1),
- Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
- fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
- fun sel (con,args,mx) = map_filter sel1 args;
- fun mk_patT (a,b) = a ->> mk_maybeT b;
- fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
- fun pat (con,args,mx) = (pat_name_ con,
- (mapn pat_arg_typ 1 args)
- --->
- mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
- Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
+ fun mk_matT (a,bs,c) =
+ a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
+ fun mat (con,args,mx) =
+ (mat_name_ con,
+ mk_matT(dtype, map third args, freetvar "t" 1),
+ Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
+ fun sel1 (_,sel,typ) =
+ Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
+ fun sel (con,args,mx) = map_filter sel1 args;
+ fun mk_patT (a,b) = a ->> mk_maybeT b;
+ fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
+ fun pat (con,args,mx) =
+ (pat_name_ con,
+ (mapn pat_arg_typ 1 args)
+ --->
+ mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
+ Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
+ in
+ val consts_con = map con cons';
+ val consts_dis = map dis cons';
+ val consts_mat = map mat cons';
+ val consts_pat = map pat cons';
+ val consts_sel = maps sel cons';
+ end;
+
+(* ----- constants concerning induction ------------------------------------- *)
+
+ val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
+ val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
+
+(* ----- case translation --------------------------------------------------- *)
+ local open Syntax in
+ local
+ fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
+ fun expvar n = Variable ("e"^(string_of_int n));
+ fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
+ (string_of_int m));
+ fun argvars n args = mapn (argvar n) 1 args;
+ fun app s (l,r) = mk_appl (Constant s) [l,r];
+ val cabs = app "_cabs";
+ val capp = app "Rep_CFun";
+ fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
+ fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
+ fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
+ fun when1 n m = if n = m then arg1 n else K (Constant "UU");
+
+ fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
+ fun app_pat x = mk_appl (Constant "_pat") [x];
+ fun args_list [] = Constant "_noargs"
+ | args_list xs = foldr1 (app "_args") xs;
+ in
+ val case_trans =
+ ParsePrintRule
+ (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
+ capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
+
+ fun one_abscon_trans n (con,mx,args) =
+ ParsePrintRule
+ (cabs (con1 n (con,mx,args), expvar n),
+ Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'));
+ val abscon_trans = mapn one_abscon_trans 1 cons';
+
+ fun one_case_trans (con,args,mx) =
+ let
+ val cname = c_ast con mx;
+ val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
+ val ns = 1 upto length args;
+ val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
+ val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
+ val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
in
- val consts_con = map con cons';
- val consts_dis = map dis cons';
- val consts_mat = map mat cons';
- val consts_pat = map pat cons';
- val consts_sel = maps sel cons';
- end;
-
- (* ----- constants concerning induction ------------------------------------- *)
-
- val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
- val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
-
- (* ----- case translation --------------------------------------------------- *)
-
- local open Syntax in
- local
- fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
- fun expvar n = Variable ("e"^(string_of_int n));
- fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
- (string_of_int m));
- fun argvars n args = mapn (argvar n) 1 args;
- fun app s (l,r) = mk_appl (Constant s) [l,r];
- val cabs = app "_cabs";
- val capp = app "Rep_CFun";
- fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
- fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
- fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
- fun when1 n m = if n = m then arg1 n else K (Constant "UU");
+ [ParseRule (app_pat (Library.foldl capp (cname, xs)),
+ mk_appl pname (map app_pat xs)),
+ ParseRule (app_var (Library.foldl capp (cname, xs)),
+ app_var (args_list xs)),
+ PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
+ app "_match" (mk_appl pname ps, args_list vs))]
+ end;
+ val Case_trans = maps one_case_trans cons';
+ end;
+ end;
+ val optional_consts =
+ if definitional then [] else [const_rep, const_abs, const_copy];
- fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
- fun app_pat x = mk_appl (Constant "_pat") [x];
- fun args_list [] = Constant "_noargs"
- | args_list xs = foldr1 (app "_args") xs;
- in
- val case_trans =
- ParsePrintRule
- (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
- capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
-
- fun one_abscon_trans n (con,mx,args) =
- ParsePrintRule
- (cabs (con1 n (con,mx,args), expvar n),
- Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'));
- val abscon_trans = mapn one_abscon_trans 1 cons';
-
- fun one_case_trans (con,args,mx) =
- let
- val cname = c_ast con mx;
- val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
- val ns = 1 upto length args;
- val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
- val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
- val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
- in
- [ParseRule (app_pat (Library.foldl capp (cname, xs)),
- mk_appl pname (map app_pat xs)),
- ParseRule (app_var (Library.foldl capp (cname, xs)),
- app_var (args_list xs)),
- PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
- app "_match" (mk_appl pname ps, args_list vs))]
- end;
- val Case_trans = maps one_case_trans cons';
- end;
- end;
-
- in ([const_rep, const_abs, const_when, const_copy] @
- consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
- [const_take, const_finite],
- (case_trans::(abscon_trans @ Case_trans)))
- end; (* let *)
+ in (optional_consts @ [const_when] @
+ consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
+ [const_take, const_finite],
+ (case_trans::(abscon_trans @ Case_trans)))
+ end; (* let *)
(* ----- putting all the syntax stuff together ------------------------------ *)
fun add_syntax
- (comp_dnam : string)
- (eqs' : ((string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list) list)
- (thy'' : theory) =
- let
- val dtypes = map (Type o fst) eqs';
- val boolT = HOLogic.boolT;
- val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
- val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
- val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
- val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
- val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
- in thy'' |> ContConsts.add_consts_i (maps fst ctt @
- (if length eqs'>1 then [const_copy] else[])@
- [const_bisim])
- |> Sign.add_trrules_i (maps snd ctt)
- end; (* let *)
+ (definitional : bool)
+ (comp_dnam : string)
+ (eqs' : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list)
+ (thy'' : theory) =
+ let
+ val dtypes = map (Type o fst) eqs';
+ val boolT = HOLogic.boolT;
+ val funprod =
+ foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
+ val relprod =
+ foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+ val const_copy =
+ (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
+ val const_bisim =
+ (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
+ val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list =
+ map (calc_syntax definitional funprod) eqs';
+ in thy''
+ |> ContConsts.add_consts_i
+ (maps fst ctt @
+ (if length eqs'>1 then [const_copy] else[])@
+ [const_bisim])
+ |> Sign.add_trrules_i (maps snd ctt)
+ end; (* let *)
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Nov 20 07:24:21 2009 +0100
@@ -141,6 +141,8 @@
val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
val pg = pg' thy;
+val map_tab = Domain_Isomorphism.get_map_tab thy;
+
(* ----- getting the axioms and definitions --------------------------------- *)
@@ -599,7 +601,8 @@
val lhs = dc_copy`%"f"`(con_app con args);
fun one_rhs arg =
if DatatypeAux.is_rec_type (dtyp_of arg)
- then Domain_Axioms.copy_of_dtyp (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
+ then Domain_Axioms.copy_of_dtyp map_tab
+ (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
else (%# arg);
val rhs = con_app2 con one_rhs args;
val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
@@ -660,6 +663,7 @@
fun comp_theorems (comp_dnam, eqs: eq list) thy =
let
val global_ctxt = ProofContext.init thy;
+val map_tab = Domain_Isomorphism.get_map_tab thy;
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
@@ -727,7 +731,8 @@
fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
fun one_rhs arg =
if DatatypeAux.is_rec_type (dtyp_of arg)
- then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg)
+ then Domain_Axioms.copy_of_dtyp map_tab
+ mk_take (dtyp_of arg) ` (%# arg)
else (%# arg);
val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
val rhs = con_app2 con one_rhs args;
--- a/src/HOLCF/ex/Domain_Proofs.thy Fri Nov 20 07:24:08 2009 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy Fri Nov 20 07:24:21 2009 +0100
@@ -16,8 +16,8 @@
datatypes:
domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
- and 'a bar = Bar (lazy 'a) (lazy "'a baz")
- and 'a baz = Baz (lazy 'a) (lazy "'a foo convex_pd")
+ and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
+ and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
*)
@@ -28,47 +28,47 @@
text {* Start with the one-step non-recursive version *}
definition
- foo_bar_baz_typF ::
+ foo_bar_baz_deflF ::
"TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep"
where
- "foo_bar_baz_typF = (\<Lambda> a (t1, t2, t3).
- ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2))
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t3)
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1))))"
+ "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3).
+ ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+ , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>REP(tr))
+ , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>REP(tr)))))"
-lemma foo_bar_baz_typF_beta:
- "foo_bar_baz_typF\<cdot>a\<cdot>t =
- ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(fst (snd t))))
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(snd (snd t)))
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(fst t))))"
-unfolding foo_bar_baz_typF_def
-by (simp add: csplit_def cfst_def csnd_def)
+lemma foo_bar_baz_deflF_beta:
+ "foo_bar_baz_deflF\<cdot>a\<cdot>t =
+ ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+ , u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>REP(tr))
+ , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>REP(tr)))"
+unfolding foo_bar_baz_deflF_def
+by (simp add: split_def)
text {* Individual type combinators are projected from the fixed point. *}
-definition foo_typ :: "TypeRep \<rightarrow> TypeRep"
-where "foo_typ = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_typF\<cdot>a)))"
+definition foo_defl :: "TypeRep \<rightarrow> TypeRep"
+where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
-definition bar_typ :: "TypeRep \<rightarrow> TypeRep"
-where "bar_typ = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition bar_defl :: "TypeRep \<rightarrow> TypeRep"
+where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
-definition baz_typ :: "TypeRep \<rightarrow> TypeRep"
-where "baz_typ = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition baz_defl :: "TypeRep \<rightarrow> TypeRep"
+where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
text {* Unfold rules for each combinator. *}
-lemma foo_typ_unfold:
- "foo_typ\<cdot>a = ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(bar_typ\<cdot>a)))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma foo_defl_unfold:
+ "foo_defl\<cdot>a = ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma bar_typ_unfold: "bar_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(baz_typ\<cdot>a))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>REP(tr))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma baz_typ_unfold: "baz_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(foo_typ\<cdot>a)))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>REP(tr))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
text "The automation for the previous steps will be quite similar to
how the fixrec package works."
@@ -79,13 +79,13 @@
text {* Use @{text pcpodef} with the appropriate type combinator. *}
-pcpodef (open) 'a foo = "{x. x ::: foo_typ\<cdot>REP('a)}"
+pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>REP('a)}"
by (simp_all add: adm_in_deflation)
-pcpodef (open) 'a bar = "{x. x ::: bar_typ\<cdot>REP('a)}"
+pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>REP('a)}"
by (simp_all add: adm_in_deflation)
-pcpodef (open) 'a baz = "{x. x ::: baz_typ\<cdot>REP('a)}"
+pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>REP('a)}"
by (simp_all add: adm_in_deflation)
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
@@ -97,10 +97,10 @@
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
definition prj_foo :: "udom \<rightarrow> 'a foo"
-where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>REP('a))\<cdot>y))"
definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
-where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_typ\<cdot>REP('a))"
+where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_defl\<cdot>REP('a))"
instance
apply (rule typedef_rep_class)
@@ -120,10 +120,10 @@
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
definition prj_bar :: "udom \<rightarrow> 'a bar"
-where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>REP('a))\<cdot>y))"
definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
-where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_typ\<cdot>REP('a))"
+where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_defl\<cdot>REP('a))"
instance
apply (rule typedef_rep_class)
@@ -143,10 +143,10 @@
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
definition prj_baz :: "udom \<rightarrow> 'a baz"
-where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>REP('a))\<cdot>y))"
definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
-where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_typ\<cdot>REP('a))"
+where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_defl\<cdot>REP('a))"
instance
apply (rule typedef_rep_class)
@@ -161,7 +161,7 @@
text {* Prove REP rules using lemma @{text typedef_REP}. *}
-lemma REP_foo: "REP('a foo) = foo_typ\<cdot>REP('a)"
+lemma REP_foo: "REP('a foo) = foo_defl\<cdot>REP('a)"
apply (rule typedef_REP)
apply (rule type_definition_foo)
apply (rule below_foo_def)
@@ -169,7 +169,7 @@
apply (rule prj_foo_def)
done
-lemma REP_bar: "REP('a bar) = bar_typ\<cdot>REP('a)"
+lemma REP_bar: "REP('a bar) = bar_defl\<cdot>REP('a)"
apply (rule typedef_REP)
apply (rule type_definition_bar)
apply (rule below_bar_def)
@@ -177,7 +177,7 @@
apply (rule prj_bar_def)
done
-lemma REP_baz: "REP('a baz) = baz_typ\<cdot>REP('a)"
+lemma REP_baz: "REP('a baz) = baz_defl\<cdot>REP('a)"
apply (rule typedef_REP)
apply (rule type_definition_baz)
apply (rule below_baz_def)
@@ -189,15 +189,15 @@
lemma REP_foo': "REP('a foo) = REP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule foo_typ_unfold)
+by (rule foo_defl_unfold)
-lemma REP_bar': "REP('a bar) = REP('a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>)"
+lemma REP_bar': "REP('a bar) = REP(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule bar_typ_unfold)
+by (rule bar_defl_unfold)
-lemma REP_baz': "REP('a baz) = REP('a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>)"
+lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule baz_typ_unfold)
+by (rule baz_defl_unfold)
(********************************************************************)
@@ -206,41 +206,56 @@
text {* Define them all using @{text coerce}! *}
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-where "foo_rep = coerce"
+where "foo_rep \<equiv> coerce"
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
-where "foo_abs = coerce"
+where "foo_abs \<equiv> coerce"
+
+definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
+where "bar_rep \<equiv> coerce"
+
+definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
+where "bar_abs \<equiv> coerce"
-definition bar_rep :: "'a bar \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>"
-where "bar_rep = coerce"
+definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
+where "baz_rep \<equiv> coerce"
+
+definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
+where "baz_abs \<equiv> coerce"
+
+text {* Prove isomorphism rules. *}
-definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar"
-where "bar_abs = coerce"
+lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_foo' foo_abs_def foo_rep_def])
+
+lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_foo' foo_abs_def foo_rep_def])
+
+lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_bar' bar_abs_def bar_rep_def])
-definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>"
-where "baz_rep = coerce"
+lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_bar' bar_abs_def bar_rep_def])
-definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz"
-where "baz_abs = coerce"
+lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_baz' baz_abs_def baz_rep_def])
+
+lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_baz' baz_abs_def baz_rep_def])
text {* Prove isodefl rules using @{text isodefl_coerce}. *}
lemma isodefl_foo_abs:
"isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
-unfolding foo_abs_def foo_rep_def
-by (rule isodefl_coerce [OF REP_foo'])
+by (rule isodefl_abs_rep [OF REP_foo' foo_abs_def foo_rep_def])
lemma isodefl_bar_abs:
"isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
-unfolding bar_abs_def bar_rep_def
-by (rule isodefl_coerce [OF REP_bar'])
+by (rule isodefl_abs_rep [OF REP_bar' bar_abs_def bar_rep_def])
lemma isodefl_baz_abs:
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
-unfolding baz_abs_def baz_rep_def
-by (rule isodefl_coerce [OF REP_baz'])
-
-text {* TODO: prove iso predicate for rep and abs. *}
+by (rule isodefl_abs_rep [OF REP_baz' baz_abs_def baz_rep_def])
(********************************************************************)
@@ -253,20 +268,20 @@
definition
foo_bar_baz_mapF ::
- "('a \<rightarrow> 'b)
- \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)
- \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)"
+ "('a \<rightarrow> 'b) \<rightarrow>
+ ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
+ ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
where
- "foo_bar_baz_mapF = (\<Lambda> f (d1, d2, d3).
+ "foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3).
(
foo_abs oo
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
oo foo_rep
,
- bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep
+ bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
,
- baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep
- ))"
+ baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
+ )))"
lemma foo_bar_baz_mapF_beta:
"foo_bar_baz_mapF\<cdot>f\<cdot>d =
@@ -275,12 +290,12 @@
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d))))
oo foo_rep
,
- bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(snd (snd d))) oo bar_rep
+ bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep
,
- baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep
+ baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep
)"
unfolding foo_bar_baz_mapF_def
-by (simp add: csplit_def cfst_def csnd_def)
+by (simp add: split_def)
text {* Individual map functions are projected from the fixed point. *}
@@ -290,7 +305,7 @@
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
-definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a baz \<rightarrow> 'b baz)"
+definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
text {* Prove isodefl rules for all map functions simultaneously. *}
@@ -298,17 +313,16 @@
lemma isodefl_foo_bar_baz:
assumes isodefl_d: "isodefl d t"
shows
- "isodefl (foo_map\<cdot>d) (foo_typ\<cdot>t) \<and>
- isodefl (bar_map\<cdot>d) (bar_typ\<cdot>t) \<and>
- isodefl (baz_map\<cdot>d) (baz_typ\<cdot>t)"
+ "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
+ isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
+ isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
apply (simp add: foo_map_def bar_map_def baz_map_def)
- apply (simp add: foo_typ_def bar_typ_def baz_typ_def)
- apply (rule parallel_fix_ind
- [where F="foo_bar_baz_typF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"])
+ apply (simp add: foo_defl_def bar_defl_def baz_defl_def)
+ apply (rule parallel_fix_ind)
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
apply (simp only: foo_bar_baz_mapF_beta
- foo_bar_baz_typF_beta
+ foo_bar_baz_deflF_beta
fst_conv snd_conv)
apply (elim conjE)
apply (intro
@@ -316,7 +330,8 @@
isodefl_foo_abs
isodefl_bar_abs
isodefl_baz_abs
- isodefl_ssum isodefl_sprod isodefl_one isodefl_u isodefl_convex
+ isodefl_ssum isodefl_sprod isodefl_ID_REP
+ isodefl_u isodefl_convex isodefl_cfun
isodefl_d
)
apply assumption+
@@ -353,23 +368,63 @@
subsection {* Step 5: Define copy functions, prove reach lemmas *}
-definition "foo_bar_baz_copy = foo_bar_baz_mapF\<cdot>ID"
-definition "foo_copy = (\<Lambda> f. fst (foo_bar_baz_copy\<cdot>f))"
-definition "bar_copy = (\<Lambda> f. fst (snd (foo_bar_baz_copy\<cdot>f)))"
-definition "baz_copy = (\<Lambda> f. snd (snd (foo_bar_baz_copy\<cdot>f)))"
+text {* Define copy functions just like the old domain package does. *}
+
+definition
+ foo_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ 'a foo \<rightarrow> 'a foo"
+where
+ "foo_copy = (\<Lambda> p. foo_abs oo
+ ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
+ oo foo_rep)"
+
+definition
+ bar_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ 'a bar \<rightarrow> 'a bar"
+where
+ "bar_copy = (\<Lambda> p. bar_abs oo
+ u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep)"
+
+definition
+ baz_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ 'a baz \<rightarrow> 'a baz"
+where
+ "baz_copy = (\<Lambda> p. baz_abs oo
+ u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep)"
+
+definition
+ foo_bar_baz_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
+where
+ "foo_bar_baz_copy = (\<Lambda> f. (foo_copy\<cdot>f, bar_copy\<cdot>f, baz_copy\<cdot>f))"
lemma fix_foo_bar_baz_copy:
"fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)"
-unfolding foo_bar_baz_copy_def foo_map_def bar_map_def baz_map_def
-by simp
+unfolding foo_map_def bar_map_def baz_map_def
+apply (subst beta_cfun, simp)+
+apply (subst pair_collapse)+
+apply (rule cfun_arg_cong)
+unfolding foo_bar_baz_mapF_def split_def
+unfolding foo_bar_baz_copy_def
+unfolding foo_copy_def bar_copy_def baz_copy_def
+apply (subst beta_cfun, simp)+
+apply (rule refl)
+done
lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy by (simp add: foo_map_ID)
+unfolding fix_foo_bar_baz_copy fst_conv snd_conv
+unfolding foo_map_ID by (rule ID1)
lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy by (simp add: bar_map_ID)
+unfolding fix_foo_bar_baz_copy fst_conv snd_conv
+unfolding bar_map_ID by (rule ID1)
lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy by (simp add: baz_map_ID)
+unfolding fix_foo_bar_baz_copy fst_conv snd_conv
+unfolding baz_map_ID by (rule ID1)
end
--- a/src/Pure/Isar/code.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/Pure/Isar/code.ML Fri Nov 20 07:24:21 2009 +0100
@@ -775,49 +775,4 @@
end;
-(** datastructure to log definitions for preprocessing of the predicate compiler **)
-(* obviously a clone of Named_Thms *)
-
-signature PREDICATE_COMPILE_PREPROC_CONST_DEFS =
-sig
- val get: Proof.context -> thm list
- val add_thm: thm -> Context.generic -> Context.generic
- val del_thm: thm -> Context.generic -> Context.generic
-
- val add_attribute : attribute
- val del_attribute : attribute
-
- val add_attrib : Attrib.src
-
- val setup: theory -> theory
-end;
-
-structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS =
-struct
-
-structure Data = Generic_Data
-(
- type T = thm list;
- val empty = [];
- val extend = I;
- val merge = Thm.merge_thms;
-);
-
-val get = Data.get o Context.Proof;
-
-val add_thm = Data.map o Thm.add_thm;
-val del_thm = Data.map o Thm.del_thm;
-
-val add_attribute = Thm.declaration_attribute add_thm;
-val del_attribute = Thm.declaration_attribute del_thm;
-
-val add_attrib = Attrib.internal (K add_attribute)
-
-val setup =
- Attrib.setup (Binding.name "pred_compile_preproc") (Attrib.add_del add_attribute del_attribute)
- ("declaration of definition for preprocessing of the predicate compiler") #>
- PureThy.add_thms_dynamic (Binding.name "pred_compile_preproc", Data.get);
-
-end;
-
structure Code : CODE = struct open Code; end;
--- a/src/Pure/Isar/constdefs.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Fri Nov 20 07:24:21 2009 +0100
@@ -55,8 +55,7 @@
|> PureThy.add_defs false [((name, def), atts)]
|-> (fn [thm] => (* FIXME thm vs. atts !? *)
Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #>
- Code.add_default_eqn thm #>
- Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
+ Code.add_default_eqn thm);
in ((c, T), thy') end;
fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
--- a/src/Pure/Isar/specification.ML Fri Nov 20 07:24:08 2009 +0100
+++ b/src/Pure/Isar/specification.ML Fri Nov 20 07:24:21 2009 +0100
@@ -212,8 +212,7 @@
val ([(def_name, [th'])], lthy4) = lthy3
|> Local_Theory.notes_kind Thm.definitionK
- [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
- Code.add_default_eqn_attrib :: atts), [([th], [])])];
+ [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
val _ =