--- a/src/HOL/IsaMakefile Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOL/IsaMakefile Tue Mar 02 17:36:40 2010 +0000
@@ -756,7 +756,7 @@
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
-$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/Helper.thy ZF/LProd.thy \
+$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
--- a/src/HOL/RealPow.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOL/RealPow.thy Tue Mar 02 17:36:40 2010 +0000
@@ -113,9 +113,6 @@
lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
by auto
-lemma real_minus_half_eq [simp]: "(x::real) - x/2 = x/2"
-by auto
-
lemma real_mult_inverse_cancel:
"[|(0::real) < x; 0 < x1; x1 * y < x * u |]
==> inverse x * y < inverse x1 * u"
--- a/src/HOL/ZF/HOLZF.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOL/ZF/HOLZF.thy Tue Mar 02 17:36:40 2010 +0000
@@ -6,7 +6,7 @@
*)
theory HOLZF
-imports Helper
+imports Main
begin
typedecl ZF
@@ -298,7 +298,7 @@
apply (rule_tac x="Fst z" in exI)
apply (simp add: isOpair_def)
apply (auto simp add: Fst Snd Opair)
- apply (rule theI2')
+ apply (rule the1I2)
apply auto
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair x ya" and y="Opair x yb" in PFun_inj)
@@ -306,7 +306,7 @@
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair x y" and y="Opair x ya" in PFun_inj)
apply (auto simp add: Fst Snd)
- apply (rule theI2')
+ apply (rule the1I2)
apply (auto simp add: Fun_total)
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair a x" and y="Opair a y" in PFun_inj)
--- a/src/HOL/ZF/Helper.thy Tue Mar 02 17:36:16 2010 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: HOL/ZF/Helper.thy
- ID: $Id$
- Author: Steven Obua
-
- Some helpful lemmas that probably will end up elsewhere.
-*)
-
-theory Helper
-imports Main
-begin
-
-lemma theI2' : "?! x. P x \<Longrightarrow> (!! x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (THE x. P x)"
- apply auto
- apply (subgoal_tac "P (THE x. P x)")
- apply blast
- apply (rule theI)
- apply auto
- done
-
-lemma in_range_superfluous: "(z \<in> range f & z \<in> (f ` x)) = (z \<in> f ` x)"
- by auto
-
-lemma f_x_in_range_f: "f x \<in> range f"
- by (blast intro: image_eqI)
-
-lemma comp_inj: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (g o f)"
- by (blast intro: comp_inj_on subset_inj_on)
-
-lemma comp_image_eq: "(g o f) ` x = g ` f ` x"
- by auto
-
-end
\ No newline at end of file
--- a/src/HOL/ZF/Zet.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOL/ZF/Zet.thy Tue Mar 02 17:36:40 2010 +0000
@@ -35,7 +35,7 @@
apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
apply (simp add: explode_Repl_eq)
apply (subgoal_tac "explode z = f ` A")
- apply (simp_all add: comp_image_eq)
+ apply (simp_all add: image_compose)
done
lemma zet_image_mem:
@@ -56,7 +56,7 @@
apply (auto simp add: subset injf)
done
show ?thesis
- apply (simp add: zet_def' comp_image_eq[symmetric])
+ apply (simp add: zet_def' image_compose[symmetric])
apply (rule exI[where x="?w"])
apply (simp add: injw image_zet_rep Azet)
done
@@ -108,7 +108,7 @@
lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
apply (simp add: zimage_def)
apply (subst Abs_zet_inverse)
- apply (simp_all add: comp_image_eq zet_image_mem Rep_zet)
+ apply (simp_all add: image_compose zet_image_mem Rep_zet)
done
definition zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet" where
--- a/src/HOL/ex/Gauge_Integration.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOL/ex/Gauge_Integration.thy Tue Mar 02 17:36:40 2010 +0000
@@ -28,7 +28,7 @@
definition
gauge :: "[real set, real => real] => bool" where
- [code del]:"gauge E g = (\<forall>x\<in>E. 0 < g(x))"
+ [code del]: "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
subsection {* Gauge-fine divisions *}
@@ -63,14 +63,20 @@
apply (drule fine_imp_le, simp)
done
-lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
-by (induct set: fine, simp_all)
+lemma fine_Nil_iff: "fine \<delta> (a, b) [] \<longleftrightarrow> a = b"
+by (auto elim: fine.cases intro: fine.intros)
-lemma fine_eq: "fine \<delta> (a, b) D \<Longrightarrow> a = b \<longleftrightarrow> D = []"
-apply (cases "D = []")
-apply (drule (1) empty_fine_imp_eq, simp)
-apply (drule (1) nonempty_fine_imp_less, simp)
-done
+lemma fine_same_iff: "fine \<delta> (a, a) D \<longleftrightarrow> D = []"
+proof
+ assume "fine \<delta> (a, a) D" thus "D = []"
+ by (metis nonempty_fine_imp_less less_irrefl)
+next
+ assume "D = []" thus "fine \<delta> (a, a) D"
+ by (simp add: fine_Nil)
+qed
+
+lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
+by (simp add: fine_Nil_iff)
lemma mem_fine:
"\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
@@ -174,7 +180,7 @@
lemma fine_\<delta>_expand:
assumes "fine \<delta> (a,b) D"
- and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x"
+ and "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<delta> x \<le> \<delta>' x"
shows "fine \<delta>' (a,b) D"
using assms proof induct
case 1 show ?case by (rule fine_Nil)
@@ -258,6 +264,22 @@
(\<forall>D. fine \<delta> (a,b) D -->
\<bar>rsum D f - k\<bar> < e)))"
+lemma Integral_eq:
+ "Integral (a, b) f k \<longleftrightarrow>
+ (\<forall>e>0. \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a,b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e))"
+unfolding Integral_def by simp
+
+lemma IntegralI:
+ assumes "\<And>e. 0 < e \<Longrightarrow>
+ \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e)"
+ shows "Integral (a, b) f k"
+using assms unfolding Integral_def by auto
+
+lemma IntegralE:
+ assumes "Integral (a, b) f k" and "0 < e"
+ obtains \<delta> where "gauge {a..b} \<delta>" and "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e"
+using assms unfolding Integral_def by auto
+
lemma Integral_def2:
"Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
(\<forall>D. fine \<delta> (a,b) D -->
@@ -272,60 +294,69 @@
text{*The integral is unique if it exists*}
lemma Integral_unique:
- "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"
-apply (simp add: Integral_def)
-apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
-apply auto
-apply (drule gauge_min, assumption)
-apply (drule_tac \<delta> = "%x. min (\<delta> x) (\<delta>' x)"
- in fine_exists, assumption, auto)
-apply (drule fine_min)
-apply (drule spec)+
-apply auto
-apply (subgoal_tac "\<bar>(rsum D f - k2) - (rsum D f - k1)\<bar> < \<bar>k1 - k2\<bar>")
-apply arith
-apply (drule add_strict_mono, assumption)
-apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
- mult_less_cancel_right)
+ assumes le: "a \<le> b"
+ assumes 1: "Integral (a, b) f k1"
+ assumes 2: "Integral (a, b) f k2"
+ shows "k1 = k2"
+proof (rule ccontr)
+ assume "k1 \<noteq> k2"
+ hence e: "0 < \<bar>k1 - k2\<bar> / 2" by simp
+ obtain d1 where "gauge {a..b} d1" and
+ d1: "\<forall>D. fine d1 (a, b) D \<longrightarrow> \<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2"
+ using 1 e by (rule IntegralE)
+ obtain d2 where "gauge {a..b} d2" and
+ d2: "\<forall>D. fine d2 (a, b) D \<longrightarrow> \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
+ using 2 e by (rule IntegralE)
+ have "gauge {a..b} (\<lambda>x. min (d1 x) (d2 x))"
+ using `gauge {a..b} d1` and `gauge {a..b} d2`
+ by (rule gauge_min)
+ then obtain D where "fine (\<lambda>x. min (d1 x) (d2 x)) (a, b) D"
+ using fine_exists [OF le] by fast
+ hence "fine d1 (a, b) D" and "fine d2 (a, b) D"
+ by (auto dest: fine_min)
+ hence "\<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2" and "\<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
+ using d1 d2 by simp_all
+ hence "\<bar>rsum D f - k1\<bar> + \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2 + \<bar>k1 - k2\<bar> / 2"
+ by (rule add_strict_mono)
+ thus False by auto
+qed
+
+lemma Integral_zero: "Integral(a,a) f 0"
+apply (rule IntegralI)
+apply (rule_tac x = "\<lambda>x. 1" in exI)
+apply (simp add: fine_same_iff gauge_def)
done
-lemma Integral_zero [simp]: "Integral(a,a) f 0"
-apply (auto simp add: Integral_def)
-apply (rule_tac x = "%x. 1" in exI)
-apply (auto dest: fine_eq simp add: gauge_def rsum_def)
+lemma Integral_same_iff [simp]: "Integral (a, a) f k \<longleftrightarrow> k = 0"
+ by (auto intro: Integral_zero Integral_unique)
+
+lemma Integral_zero_fun: "Integral (a,b) (\<lambda>x. 0) 0"
+apply (rule IntegralI)
+apply (rule_tac x="\<lambda>x. 1" in exI, simp add: gauge_def)
done
lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
unfolding rsum_def
by (induct set: fine, auto simp add: algebra_simps)
-lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
+lemma Integral_mult_const: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. c) (c * (b - a))"
apply (cases "a = b", simp)
-apply (simp add: Integral_def, clarify)
-apply (rule_tac x = "%x. b - a" in exI)
+apply (rule IntegralI)
+apply (rule_tac x = "\<lambda>x. b - a" in exI)
apply (rule conjI, simp add: gauge_def)
apply (clarify)
apply (subst fine_rsum_const, assumption, simp)
done
-lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b - a))"
-apply (cases "a = b", simp)
-apply (simp add: Integral_def, clarify)
-apply (rule_tac x = "%x. b - a" in exI)
-apply (rule conjI, simp add: gauge_def)
-apply (clarify)
-apply (subst fine_rsum_const, assumption, simp)
-done
+lemma Integral_eq_diff_bounds: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. 1) (b - a)"
+ using Integral_mult_const [of a b 1] by simp
lemma Integral_mult:
"[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
-apply (auto simp add: order_le_less
- dest: Integral_unique [OF order_refl Integral_zero])
-apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc)
-apply (case_tac "c = 0", force)
-apply (drule_tac x = "e/abs c" in spec)
-apply (simp add: divide_pos_pos)
-apply clarify
+apply (auto simp add: order_le_less)
+apply (cases "c = 0", simp add: Integral_zero_fun)
+apply (rule IntegralI)
+apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp add: divide_pos_pos)
apply (rule_tac x="\<delta>" in exI, clarify)
apply (drule_tac x="D" in spec, clarify)
apply (simp add: pos_less_divide_eq abs_mult [symmetric]
@@ -337,22 +368,20 @@
assumes "Integral (b, c) f x2"
assumes "a \<le> b" and "b \<le> c"
shows "Integral (a, c) f (x1 + x2)"
-proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI)
+proof (cases "a < b \<and> b < c", rule IntegralI)
fix \<epsilon> :: real assume "0 < \<epsilon>"
hence "0 < \<epsilon> / 2" by auto
assume "a < b \<and> b < c"
hence "a < b" and "b < c" by auto
- from `Integral (a, b) f x1`[simplified Integral_def split_conv,
- rule_format, OF `0 < \<epsilon>/2`]
obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
- and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" by auto
+ and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)"
+ using IntegralE [OF `Integral (a, b) f x1` `0 < \<epsilon>/2`] by auto
- from `Integral (b, c) f x2`[simplified Integral_def split_conv,
- rule_format, OF `0 < \<epsilon>/2`]
obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
- and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" by auto
+ and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)"
+ using IntegralE [OF `Integral (b, c) f x2` `0 < \<epsilon>/2`] by auto
def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
else if x = b then min (\<delta>1 b) (\<delta>2 b)
@@ -360,6 +389,7 @@
have "gauge {a..c} \<delta>"
using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
+
moreover {
fix D :: "(real \<times> real \<times> real) list"
assume fine: "fine \<delta> (a,c) D"
@@ -462,12 +492,12 @@
thus ?thesis
proof (rule disjE)
assume "a = b" hence "x1 = 0"
- using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto
- thus ?thesis using `a = b` `Integral (b, c) f x2` by auto
+ using `Integral (a, b) f x1` by simp
+ thus ?thesis using `a = b` `Integral (b, c) f x2` by simp
next
assume "b = c" hence "x2 = 0"
- using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto
- thus ?thesis using `b = c` `Integral (a, b) f x1` by auto
+ using `Integral (b, c) f x2` by simp
+ thus ?thesis using `b = c` `Integral (a, b) f x1` by simp
qed
qed
@@ -486,7 +516,7 @@
apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>"
in real_mult_le_cancel_iff2 [THEN iffD1])
apply simp
-apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric]
+apply (simp del: abs_inverse add: abs_mult [symmetric]
mult_assoc [symmetric])
apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x))
= (f z - f x) / (z - x) - f' x")
@@ -543,31 +573,51 @@
qed
lemma fundamental_theorem_of_calculus:
- "\<lbrakk> a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) \<rbrakk>
- \<Longrightarrow> Integral(a,b) f' (f(b) - f(a))"
- apply (drule order_le_imp_less_or_eq, auto)
- apply (auto simp add: Integral_def2)
- apply (drule_tac e = "e / (b - a)" in lemma_straddle)
- apply (simp add: divide_pos_pos)
- apply clarify
- apply (rule_tac x="g" in exI, clarify)
- apply (clarsimp simp add: rsum_def)
- apply (frule fine_listsum_eq_diff [where f=f])
- apply (erule subst)
- apply (subst listsum_subtractf [symmetric])
- apply (rule listsum_abs [THEN order_trans])
- apply (subst map_map [unfolded o_def])
- apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
- apply (erule ssubst)
- apply (simp add: abs_minus_commute)
- apply (rule listsum_mono)
- apply (clarify, rename_tac u x v)
- apply ((drule spec)+, erule mp)
- apply (simp add: mem_fine mem_fine2 mem_fine3)
- apply (frule fine_listsum_eq_diff [where f="\<lambda>x. x"])
- apply (simp only: split_def)
- apply (subst listsum_const_mult)
- apply simp
-done
+ assumes "a \<le> b"
+ assumes f': "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> DERIV f x :> f'(x)"
+ shows "Integral (a, b) f' (f(b) - f(a))"
+proof (cases "a = b")
+ assume "a = b" thus ?thesis by simp
+next
+ assume "a \<noteq> b" with `a \<le> b` have "a < b" by simp
+ show ?thesis
+ proof (simp add: Integral_def2, clarify)
+ fix e :: real assume "0 < e"
+ with `a < b` have "0 < e / (b - a)" by (simp add: divide_pos_pos)
+
+ from lemma_straddle [OF f' this]
+ obtain \<delta> where "gauge {a..b} \<delta>"
+ and \<delta>: "\<And>x u v. \<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
+ \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" by auto
+
+ have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
+ proof (clarify)
+ fix D assume D: "fine \<delta> (a, b) D"
+ hence "(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
+ by (rule fine_listsum_eq_diff)
+ hence "\<bar>rsum D f' - (f b - f a)\<bar> = \<bar>rsum D f' - (\<Sum>(u, x, v)\<leftarrow>D. f v - f u)\<bar>"
+ by simp
+ also have "\<dots> = \<bar>(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) - rsum D f'\<bar>"
+ by (rule abs_minus_commute)
+ also have "\<dots> = \<bar>\<Sum>(u, x, v)\<leftarrow>D. (f v - f u) - f' x * (v - u)\<bar>"
+ by (simp only: rsum_def listsum_subtractf split_def)
+ also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. \<bar>(f v - f u) - f' x * (v - u)\<bar>)"
+ by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def)
+ also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))"
+ apply (rule listsum_mono, clarify, rename_tac u x v)
+ using D apply (simp add: \<delta> mem_fine mem_fine2 mem_fine3)
+ done
+ also have "\<dots> = e"
+ using fine_listsum_eq_diff [OF D, where f="\<lambda>x. x"]
+ unfolding split_def listsum_const_mult
+ using `a < b` by simp
+ finally show "\<bar>rsum D f' - (f b - f a)\<bar> \<le> e" .
+ qed
+
+ with `gauge {a..b} \<delta>`
+ show "\<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e)"
+ by auto
+ qed
+qed
end
--- a/src/HOLCF/Domain.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Domain.thy Tue Mar 02 17:36:40 2010 +0000
@@ -9,6 +9,7 @@
uses
("Tools/cont_consts.ML")
("Tools/cont_proc.ML")
+ ("Tools/Domain/domain_constructors.ML")
("Tools/Domain/domain_library.ML")
("Tools/Domain/domain_syntax.ML")
("Tools/Domain/domain_axioms.ML")
@@ -86,7 +87,10 @@
lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
-lemma (in iso) compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
+lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P"
+ by (simp add: rep_defined_iff)
+
+lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
proof (unfold compact_def)
assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
with cont_Rep_CFun2
@@ -228,11 +232,51 @@
lemmas con_eq_iff_rules =
sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
+lemmas sel_strict_rules =
+ cfcomp2 sscase1 sfst_strict ssnd_strict fup1
+
+lemma sel_app_extra_rules:
+ "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>"
+ "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x"
+ "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>"
+ "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x"
+ "fup\<cdot>ID\<cdot>(up\<cdot>x) = x"
+by (cases "x = \<bottom>", simp, simp)+
+
+lemmas sel_app_rules =
+ sel_strict_rules sel_app_extra_rules
+ ssnd_spair sfst_spair up_defined spair_defined
+
+lemmas sel_defined_iff_rules =
+ cfcomp2 sfst_defined_iff ssnd_defined_iff
+
+lemmas take_con_rules =
+ ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict
+ sprod_map_spair' sprod_map_strict u_map_up u_map_strict
+
+lemma lub_ID_take_lemma:
+ assumes "chain t" and "(\<Squnion>n. t n) = ID"
+ assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
+proof -
+ have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
+ using assms(3) by simp
+ then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
+ using assms(1) by (simp add: lub_distribs)
+ then show "x = y"
+ using assms(2) by simp
+qed
+
+lemma lub_ID_reach:
+ assumes "chain t" and "(\<Squnion>n. t n) = ID"
+ shows "(\<Squnion>n. t n\<cdot>x) = x"
+using assms by (simp add: lub_distribs)
+
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
use "Tools/Domain/domain_library.ML"
use "Tools/Domain/domain_syntax.ML"
use "Tools/Domain/domain_axioms.ML"
+use "Tools/Domain/domain_constructors.ML"
use "Tools/Domain/domain_theorems.ML"
use "Tools/Domain/domain_extender.ML"
--- a/src/HOLCF/Fixrec.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Fixrec.thy Tue Mar 02 17:36:40 2010 +0000
@@ -265,7 +265,7 @@
*}
translations
- "x" <= "_match Fixrec.return (_variable x)"
+ "x" <= "_match (CONST Fixrec.return) (_variable x)"
subsection {* Pattern combinators for data constructors *}
--- a/src/HOLCF/HOLCF.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/HOLCF.thy Tue Mar 02 17:36:40 2010 +0000
@@ -6,8 +6,10 @@
theory HOLCF
imports
- Domain ConvexPD Algebraic Universal Sum_Cpo Main
- Representable
+ Main
+ Domain
+ Powerdomains
+ Sum_Cpo
uses
"holcf_logic.ML"
"Tools/adm_tac.ML"
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 02 17:36:40 2010 +0000
@@ -902,15 +902,10 @@
shows "s1<<s2"
apply (rule_tac t="s1" in seq.reach [THEN subst])
apply (rule_tac t="s2" in seq.reach [THEN subst])
-apply (rule fix_def2 [THEN ssubst])
-apply (subst contlub_cfun_fun)
-apply (rule chain_iterate)
-apply (subst contlub_cfun_fun)
-apply (rule chain_iterate)
apply (rule lub_mono)
-apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
-apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
-apply (rule prems [unfolded seq.take_def])
+apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
+apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
+apply (rule assms)
done
--- a/src/HOLCF/IsaMakefile Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/IsaMakefile Tue Mar 02 17:36:40 2010 +0000
@@ -51,6 +51,7 @@
Pcpodef.thy \
Pcpo.thy \
Porder.thy \
+ Powerdomains.thy \
Product_Cpo.thy \
Representable.thy \
Sprod.thy \
@@ -63,8 +64,10 @@
Tools/adm_tac.ML \
Tools/cont_consts.ML \
Tools/cont_proc.ML \
+ Tools/holcf_library.ML \
Tools/Domain/domain_extender.ML \
Tools/Domain/domain_axioms.ML \
+ Tools/Domain/domain_constructors.ML \
Tools/Domain/domain_isomorphism.ML \
Tools/Domain/domain_library.ML \
Tools/Domain/domain_syntax.ML \
--- a/src/HOLCF/Pcpo.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Pcpo.thy Tue Mar 02 17:36:40 2010 +0000
@@ -91,6 +91,10 @@
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
by (simp only: expand_fun_eq [symmetric])
+lemma lub_eq:
+ "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
+ by simp
+
text {* more results about mono and = of lubs of chains *}
lemma lub_mono2:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Powerdomains.thy Tue Mar 02 17:36:40 2010 +0000
@@ -0,0 +1,313 @@
+(* Title: HOLCF/Powerdomains.thy
+ Author: Brian Huffman
+*)
+
+header {* Powerdomains *}
+
+theory Powerdomains
+imports Representable ConvexPD
+begin
+
+subsection {* Powerdomains are representable *}
+
+text "Upper powerdomain of a representable type is representable."
+
+instantiation upper_pd :: (rep) rep
+begin
+
+definition emb_upper_pd_def: "emb = udom_emb oo upper_map\<cdot>emb"
+definition prj_upper_pd_def: "prj = upper_map\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_upper_pd_def prj_upper_pd_def)
+ apply (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+text "Lower powerdomain of a representable type is representable."
+
+instantiation lower_pd :: (rep) rep
+begin
+
+definition emb_lower_pd_def: "emb = udom_emb oo lower_map\<cdot>emb"
+definition prj_lower_pd_def: "prj = lower_map\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_lower_pd_def prj_lower_pd_def)
+ apply (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+text "Convex powerdomain of a representable type is representable."
+
+instantiation convex_pd :: (rep) rep
+begin
+
+definition emb_convex_pd_def: "emb = udom_emb oo convex_map\<cdot>emb"
+definition prj_convex_pd_def: "prj = convex_map\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_convex_pd_def prj_convex_pd_def)
+ apply (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+subsection {* Finite deflation lemmas *}
+
+text "TODO: move these lemmas somewhere else"
+
+lemma finite_compact_range_imp_finite_range:
+ fixes d :: "'a::profinite \<rightarrow> 'b::cpo"
+ assumes "finite ((\<lambda>x. d\<cdot>x) ` {x. compact x})"
+ shows "finite (range (\<lambda>x. d\<cdot>x))"
+proof (rule finite_subset [OF _ prems])
+ {
+ fix x :: 'a
+ have "range (\<lambda>i. d\<cdot>(approx i\<cdot>x)) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
+ by auto
+ hence "finite (range (\<lambda>i. d\<cdot>(approx i\<cdot>x)))"
+ using prems by (rule finite_subset)
+ hence "finite_chain (\<lambda>i. d\<cdot>(approx i\<cdot>x))"
+ by (simp add: finite_range_imp_finch)
+ hence "\<exists>i. (\<Squnion>i. d\<cdot>(approx i\<cdot>x)) = d\<cdot>(approx i\<cdot>x)"
+ by (simp add: finite_chain_def maxinch_is_thelub)
+ hence "\<exists>i. d\<cdot>x = d\<cdot>(approx i\<cdot>x)"
+ by (simp add: lub_distribs)
+ hence "d\<cdot>x \<in> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
+ by auto
+ }
+ thus "range (\<lambda>x. d\<cdot>x) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
+ by clarsimp
+qed
+
+lemma finite_deflation_upper_map:
+ assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+ interpret d: finite_deflation d by fact
+ have "deflation d" by fact
+ thus "deflation (upper_map\<cdot>d)" by (rule deflation_upper_map)
+ have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
+ hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
+ by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
+ hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
+ hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
+ by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
+ hence "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
+ hence "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` range upper_principal)"
+ apply (rule finite_subset [COMP swap_prems_rl])
+ apply (clarsimp, rename_tac t)
+ apply (induct_tac t rule: pd_basis_induct)
+ apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit)
+ apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
+ apply clarsimp
+ apply (rule imageI)
+ apply (rule vimageI2)
+ apply (simp add: Rep_PDUnit)
+ apply (rule image_eqI)
+ apply (erule sym)
+ apply simp
+ apply (rule exI)
+ apply (rule Abs_compact_basis_inverse [symmetric])
+ apply (simp add: d.compact)
+ apply (simp only: upper_plus_principal [symmetric] upper_map_plus)
+ apply clarsimp
+ apply (rule imageI)
+ apply (rule vimageI2)
+ apply (simp add: Rep_PDPlus)
+ done
+ moreover have "{xs::'a upper_pd. compact xs} = range upper_principal"
+ by (auto dest: upper_pd.compact_imp_principal)
+ ultimately have "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` {xs::'a upper_pd. compact xs})"
+ by simp
+ hence "finite (range (\<lambda>xs. upper_map\<cdot>d\<cdot>xs))"
+ by (rule finite_compact_range_imp_finite_range)
+ thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}"
+ by (rule finite_range_imp_finite_fixes)
+qed
+
+lemma finite_deflation_lower_map:
+ assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>d)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+ interpret d: finite_deflation d by fact
+ have "deflation d" by fact
+ thus "deflation (lower_map\<cdot>d)" by (rule deflation_lower_map)
+ have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
+ hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
+ by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
+ hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
+ hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
+ by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
+ hence "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
+ hence "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` range lower_principal)"
+ apply (rule finite_subset [COMP swap_prems_rl])
+ apply (clarsimp, rename_tac t)
+ apply (induct_tac t rule: pd_basis_induct)
+ apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit)
+ apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
+ apply clarsimp
+ apply (rule imageI)
+ apply (rule vimageI2)
+ apply (simp add: Rep_PDUnit)
+ apply (rule image_eqI)
+ apply (erule sym)
+ apply simp
+ apply (rule exI)
+ apply (rule Abs_compact_basis_inverse [symmetric])
+ apply (simp add: d.compact)
+ apply (simp only: lower_plus_principal [symmetric] lower_map_plus)
+ apply clarsimp
+ apply (rule imageI)
+ apply (rule vimageI2)
+ apply (simp add: Rep_PDPlus)
+ done
+ moreover have "{xs::'a lower_pd. compact xs} = range lower_principal"
+ by (auto dest: lower_pd.compact_imp_principal)
+ ultimately have "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` {xs::'a lower_pd. compact xs})"
+ by simp
+ hence "finite (range (\<lambda>xs. lower_map\<cdot>d\<cdot>xs))"
+ by (rule finite_compact_range_imp_finite_range)
+ thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}"
+ by (rule finite_range_imp_finite_fixes)
+qed
+
+lemma finite_deflation_convex_map:
+ assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+ interpret d: finite_deflation d by fact
+ have "deflation d" by fact
+ thus "deflation (convex_map\<cdot>d)" by (rule deflation_convex_map)
+ have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
+ hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
+ by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
+ hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
+ hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
+ by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
+ hence "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
+ hence "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` range convex_principal)"
+ apply (rule finite_subset [COMP swap_prems_rl])
+ apply (clarsimp, rename_tac t)
+ apply (induct_tac t rule: pd_basis_induct)
+ apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit)
+ apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
+ apply clarsimp
+ apply (rule imageI)
+ apply (rule vimageI2)
+ apply (simp add: Rep_PDUnit)
+ apply (rule image_eqI)
+ apply (erule sym)
+ apply simp
+ apply (rule exI)
+ apply (rule Abs_compact_basis_inverse [symmetric])
+ apply (simp add: d.compact)
+ apply (simp only: convex_plus_principal [symmetric] convex_map_plus)
+ apply clarsimp
+ apply (rule imageI)
+ apply (rule vimageI2)
+ apply (simp add: Rep_PDPlus)
+ done
+ moreover have "{xs::'a convex_pd. compact xs} = range convex_principal"
+ by (auto dest: convex_pd.compact_imp_principal)
+ ultimately have "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` {xs::'a convex_pd. compact xs})"
+ by simp
+ hence "finite (range (\<lambda>xs. convex_map\<cdot>d\<cdot>xs))"
+ by (rule finite_compact_range_imp_finite_range)
+ thus "finite {xs. convex_map\<cdot>d\<cdot>xs = xs}"
+ by (rule finite_range_imp_finite_fixes)
+qed
+
+subsection {* Deflation combinators *}
+
+definition "upper_defl = TypeRep_fun1 upper_map"
+definition "lower_defl = TypeRep_fun1 lower_map"
+definition "convex_defl = TypeRep_fun1 convex_map"
+
+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_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_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
+
+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_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_defl\<cdot>REP('a)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+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_defl\<cdot>REP('a)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+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
+
+lemma isodefl_upper:
+ "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
+apply (rule isodeflI)
+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_defl\<cdot>t)"
+apply (rule isodeflI)
+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_defl\<cdot>t)"
+apply (rule isodeflI)
+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 {* Domain package setup for powerdomains *}
+
+setup {*
+ fold Domain_Isomorphism.add_type_constructor
+ [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
+ @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
+ @{thm deflation_upper_map}),
+
+ (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
+ @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
+ @{thm deflation_lower_map}),
+
+ (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
+ @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
+ @{thm deflation_convex_map})]
+*}
+
+end
--- a/src/HOLCF/Representable.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Representable.thy Tue Mar 02 17:36:40 2010 +0000
@@ -5,9 +5,10 @@
header {* Representable Types *}
theory Representable
-imports Algebraic Universal Ssum Sprod One ConvexPD Fixrec
+imports Algebraic Universal Ssum Sprod One Fixrec
uses
("Tools/repdef.ML")
+ ("Tools/holcf_library.ML")
("Tools/Domain/domain_isomorphism.ML")
begin
@@ -179,6 +180,33 @@
shows "abs\<cdot>(rep\<cdot>x) = x"
unfolding abs_def rep_def by (simp add: REP [symmetric])
+lemma deflation_abs_rep:
+ fixes abs and rep and d
+ assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
+ assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
+ shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
+by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
+
+lemma deflation_chain_min:
+ assumes chain: "chain d"
+ assumes defl: "\<And>i. deflation (d i)"
+ shows "d i\<cdot>(d j\<cdot>x) = d (min i j)\<cdot>x"
+proof (rule linorder_le_cases)
+ assume "i \<le> j"
+ with chain have "d i \<sqsubseteq> d j" by (rule chain_mono)
+ then have "d i\<cdot>(d j\<cdot>x) = d i\<cdot>x"
+ by (rule deflation_below_comp1 [OF defl defl])
+ moreover from `i \<le> j` have "min i j = i" by simp
+ ultimately show ?thesis by simp
+next
+ assume "j \<le> i"
+ with chain have "d j \<sqsubseteq> d i" by (rule chain_mono)
+ then have "d i\<cdot>(d j\<cdot>x) = d j\<cdot>x"
+ by (rule deflation_below_comp2 [OF defl defl])
+ moreover from `j \<le> i` have "min i j = j" by simp
+ ultimately show ?thesis by simp
+qed
+
subsection {* Proving a subtype is representable *}
@@ -460,214 +488,6 @@
end
-text "Upper powerdomain of a representable type is representable."
-
-instantiation upper_pd :: (rep) rep
-begin
-
-definition emb_upper_pd_def: "emb = udom_emb oo upper_map\<cdot>emb"
-definition prj_upper_pd_def: "prj = upper_map\<cdot>prj oo udom_prj"
-
-instance
- apply (intro_classes, unfold emb_upper_pd_def prj_upper_pd_def)
- apply (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj ep_pair_udom)
-done
-
-end
-
-text "Lower powerdomain of a representable type is representable."
-
-instantiation lower_pd :: (rep) rep
-begin
-
-definition emb_lower_pd_def: "emb = udom_emb oo lower_map\<cdot>emb"
-definition prj_lower_pd_def: "prj = lower_map\<cdot>prj oo udom_prj"
-
-instance
- apply (intro_classes, unfold emb_lower_pd_def prj_lower_pd_def)
- apply (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj ep_pair_udom)
-done
-
-end
-
-text "Convex powerdomain of a representable type is representable."
-
-instantiation convex_pd :: (rep) rep
-begin
-
-definition emb_convex_pd_def: "emb = udom_emb oo convex_map\<cdot>emb"
-definition prj_convex_pd_def: "prj = convex_map\<cdot>prj oo udom_prj"
-
-instance
- apply (intro_classes, unfold emb_convex_pd_def prj_convex_pd_def)
- apply (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj ep_pair_udom)
-done
-
-end
-
-subsection {* Finite deflation lemmas *}
-
-text "TODO: move these lemmas somewhere else"
-
-lemma finite_compact_range_imp_finite_range:
- fixes d :: "'a::profinite \<rightarrow> 'b::cpo"
- assumes "finite ((\<lambda>x. d\<cdot>x) ` {x. compact x})"
- shows "finite (range (\<lambda>x. d\<cdot>x))"
-proof (rule finite_subset [OF _ prems])
- {
- fix x :: 'a
- have "range (\<lambda>i. d\<cdot>(approx i\<cdot>x)) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
- by auto
- hence "finite (range (\<lambda>i. d\<cdot>(approx i\<cdot>x)))"
- using prems by (rule finite_subset)
- hence "finite_chain (\<lambda>i. d\<cdot>(approx i\<cdot>x))"
- by (simp add: finite_range_imp_finch)
- hence "\<exists>i. (\<Squnion>i. d\<cdot>(approx i\<cdot>x)) = d\<cdot>(approx i\<cdot>x)"
- by (simp add: finite_chain_def maxinch_is_thelub)
- hence "\<exists>i. d\<cdot>x = d\<cdot>(approx i\<cdot>x)"
- by (simp add: lub_distribs)
- hence "d\<cdot>x \<in> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
- by auto
- }
- thus "range (\<lambda>x. d\<cdot>x) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
- by clarsimp
-qed
-
-lemma finite_deflation_upper_map:
- assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
- interpret d: finite_deflation d by fact
- have "deflation d" by fact
- thus "deflation (upper_map\<cdot>d)" by (rule deflation_upper_map)
- have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
- hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
- by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
- hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
- hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
- by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
- hence "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
- hence "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` range upper_principal)"
- apply (rule finite_subset [COMP swap_prems_rl])
- apply (clarsimp, rename_tac t)
- apply (induct_tac t rule: pd_basis_induct)
- apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit)
- apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
- apply clarsimp
- apply (rule imageI)
- apply (rule vimageI2)
- apply (simp add: Rep_PDUnit)
- apply (rule image_eqI)
- apply (erule sym)
- apply simp
- apply (rule exI)
- apply (rule Abs_compact_basis_inverse [symmetric])
- apply (simp add: d.compact)
- apply (simp only: upper_plus_principal [symmetric] upper_map_plus)
- apply clarsimp
- apply (rule imageI)
- apply (rule vimageI2)
- apply (simp add: Rep_PDPlus)
- done
- moreover have "{xs::'a upper_pd. compact xs} = range upper_principal"
- by (auto dest: upper_pd.compact_imp_principal)
- ultimately have "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` {xs::'a upper_pd. compact xs})"
- by simp
- hence "finite (range (\<lambda>xs. upper_map\<cdot>d\<cdot>xs))"
- by (rule finite_compact_range_imp_finite_range)
- thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}"
- by (rule finite_range_imp_finite_fixes)
-qed
-
-lemma finite_deflation_lower_map:
- assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>d)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
- interpret d: finite_deflation d by fact
- have "deflation d" by fact
- thus "deflation (lower_map\<cdot>d)" by (rule deflation_lower_map)
- have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
- hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
- by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
- hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
- hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
- by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
- hence "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
- hence "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` range lower_principal)"
- apply (rule finite_subset [COMP swap_prems_rl])
- apply (clarsimp, rename_tac t)
- apply (induct_tac t rule: pd_basis_induct)
- apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit)
- apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
- apply clarsimp
- apply (rule imageI)
- apply (rule vimageI2)
- apply (simp add: Rep_PDUnit)
- apply (rule image_eqI)
- apply (erule sym)
- apply simp
- apply (rule exI)
- apply (rule Abs_compact_basis_inverse [symmetric])
- apply (simp add: d.compact)
- apply (simp only: lower_plus_principal [symmetric] lower_map_plus)
- apply clarsimp
- apply (rule imageI)
- apply (rule vimageI2)
- apply (simp add: Rep_PDPlus)
- done
- moreover have "{xs::'a lower_pd. compact xs} = range lower_principal"
- by (auto dest: lower_pd.compact_imp_principal)
- ultimately have "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` {xs::'a lower_pd. compact xs})"
- by simp
- hence "finite (range (\<lambda>xs. lower_map\<cdot>d\<cdot>xs))"
- by (rule finite_compact_range_imp_finite_range)
- thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}"
- by (rule finite_range_imp_finite_fixes)
-qed
-
-lemma finite_deflation_convex_map:
- assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
- interpret d: finite_deflation d by fact
- have "deflation d" by fact
- thus "deflation (convex_map\<cdot>d)" by (rule deflation_convex_map)
- have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
- hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
- by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
- hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
- hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
- by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
- hence "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
- hence "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` range convex_principal)"
- apply (rule finite_subset [COMP swap_prems_rl])
- apply (clarsimp, rename_tac t)
- apply (induct_tac t rule: pd_basis_induct)
- apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit)
- apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
- apply clarsimp
- apply (rule imageI)
- apply (rule vimageI2)
- apply (simp add: Rep_PDUnit)
- apply (rule image_eqI)
- apply (erule sym)
- apply simp
- apply (rule exI)
- apply (rule Abs_compact_basis_inverse [symmetric])
- apply (simp add: d.compact)
- apply (simp only: convex_plus_principal [symmetric] convex_map_plus)
- apply clarsimp
- apply (rule imageI)
- apply (rule vimageI2)
- apply (simp add: Rep_PDPlus)
- done
- moreover have "{xs::'a convex_pd. compact xs} = range convex_principal"
- by (auto dest: convex_pd.compact_imp_principal)
- ultimately have "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` {xs::'a convex_pd. compact xs})"
- by simp
- hence "finite (range (\<lambda>xs. convex_map\<cdot>d\<cdot>xs))"
- by (rule finite_compact_range_imp_finite_range)
- thus "finite {xs. convex_map\<cdot>d\<cdot>xs = xs}"
- by (rule finite_range_imp_finite_fixes)
-qed
-
subsection {* Type combinators *}
definition
@@ -697,9 +517,6 @@
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 .
@@ -783,27 +600,6 @@
apply (erule finite_deflation_u_map)
done
-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_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_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_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>REP('b)"
@@ -814,7 +610,6 @@
apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom])
done
-
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_defl)
@@ -847,39 +642,12 @@
apply (simp add: u_map_map cfcomp1)
done
-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_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_defl\<cdot>REP('a)"
-apply (rule cast_eq_imp_eq, rule ext_cfun)
-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_defl\<cdot>REP('a)"
-apply (rule cast_eq_imp_eq, rule ext_cfun)
-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_cfun
REP_ssum
REP_sprod
REP_cprod
REP_up
- REP_upper
- REP_lower
- REP_convex
subsection {* Isomorphic deflations *}
@@ -1007,59 +775,27 @@
apply (simp add: u_map_map)
done
-lemma isodefl_upper:
- "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
-apply (rule isodeflI)
-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_defl\<cdot>t)"
-apply (rule isodeflI)
-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_defl\<cdot>t)"
-apply (rule isodeflI)
-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/holcf_library.ML"
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}, @{thm cfun_map_ID}),
-
- (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map},
- @{thm REP_ssum}, @{thm isodefl_ssum}, @{thm ssum_map_ID}),
+ [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
+ @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
- (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map},
- @{thm REP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}),
-
- (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map},
- @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}),
+ (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
+ @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
- (@{type_name "u"}, @{term u_defl}, @{const_name u_map},
- @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID}),
-
- (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
- @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}),
+ (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
+ @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
- (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
- @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}),
+ (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
+ @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
- (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
- @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})]
+ (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up},
+ @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
*}
end
--- a/src/HOLCF/Sprod.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Sprod.thy Tue Mar 02 17:36:40 2010 +0000
@@ -245,6 +245,10 @@
"x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
by (simp add: sprod_map_def)
+lemma sprod_map_spair':
+ "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
+by (cases "x = \<bottom> \<or> y = \<bottom>") auto
+
lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
--- a/src/HOLCF/Ssum.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Ssum.thy Tue Mar 02 17:36:40 2010 +0000
@@ -226,6 +226,12 @@
lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
unfolding ssum_map_def by simp
+lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
+by (cases "x = \<bottom>") simp_all
+
+lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
+by (cases "x = \<bottom>") simp_all
+
lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 17:36:40 2010 +0000
@@ -11,12 +11,14 @@
val calc_axioms :
bool -> string Symtab.table ->
- string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
+ 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
+ ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list ->
+ Domain_Library.eq list -> theory -> theory
end;
@@ -49,7 +51,6 @@
fun calc_axioms
(definitional : bool)
(map_tab : string Symtab.table)
- (comp_dname : string)
(eqs : eq list)
(n : int)
(eqn as ((dname,_),cons) : eq)
@@ -67,82 +68,8 @@
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 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 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;
-
- val pat_defs =
- 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 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 ------------------------- *)
- 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") ==
@@ -150,10 +77,8 @@
mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
in (dnam,
- (if definitional then [] 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])
+ (if definitional then [] else [abs_iso_ax, rep_iso_ax]),
+ [finite_def])
end; (* let (calc_axioms) *)
@@ -173,81 +98,75 @@
fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
-fun add_matchers (((dname,_),cons) : eq) thy =
- let
- val con_names = map first cons;
- val mat_names = map mat_name con_names;
- fun qualify n = Sign.full_name thy (Binding.name n);
- val ms = map qualify con_names ~~ map qualify mat_names;
- in Fixrec.add_matchers ms thy end;
-
-fun add_axioms definitional comp_dnam (eqs : eq list) thy' =
+fun add_axioms definitional eqs' (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
- val nonrec_args = filter_out is_rec args;
- val rec_args = filter is_rec args;
- val recs_cnt = length rec_args;
- val allargs = nonrec_args @ rec_args
- @ map (upd_vname (fn s=> s^"'")) rec_args;
- val allvns = map vname allargs;
- fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
- val vns1 = map (vname_arg "" ) args;
- val vns2 = map (vname_arg "'") args;
- val allargs_cnt = length nonrec_args + 2*recs_cnt;
- val rec_idxs = (recs_cnt-1) downto 0;
- val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
- (allargs~~((allargs_cnt-1) downto 0)));
- 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
- 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
- #> add_defs_infer dfs
#> add_axioms_infer axs
#> Sign.parent_path;
val map_tab = Domain_Isomorphism.get_map_tab thy';
+ val axs = mapn (calc_axioms definitional map_tab eqs) 0 eqs;
+ val thy = thy' |> fold add_one axs;
- val thy = thy'
- |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs);
+ fun get_iso_info ((dname, tyvars), cons') =
+ let
+ 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);
+ val ax_abs_iso = PureThy.get_thm thy (dname ^ ".abs_iso");
+ val ax_rep_iso = PureThy.get_thm thy (dname ^ ".rep_iso");
+ val lhsT = Type(dname,tyvars);
+ val rhsT = foldr1 mk_ssumT (map prod cons');
+ val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
+ val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
+ in
+ {
+ absT = lhsT,
+ repT = rhsT,
+ abs_const = abs_const,
+ rep_const = rep_const,
+ abs_inverse = ax_abs_iso,
+ rep_inverse = ax_rep_iso
+ }
+ end;
+ val dom_binds = map (Binding.name o Long_Name.base_name) dnames;
+ val thy =
+ if definitional then thy
+ else snd (Domain_Isomorphism.define_take_functions
+ (dom_binds ~~ map get_iso_info eqs') thy);
- val use_copy_def = length eqs>1 andalso not definitional;
+ fun add_one' (dnam, axs, dfs) =
+ Sign.add_path dnam
+ #> add_defs_infer dfs
+ #> Sign.parent_path;
+ val thy = fold add_one' axs thy;
+
+ (* declare lub_take axioms *)
+ local
+ fun ax_lub_take dname =
+ let
+ val dnam : string = Long_Name.base_name dname;
+ val take_const = %%:(dname^"_take");
+ val lub = %%: @{const_name lub};
+ val image = %%: @{const_name image};
+ val UNIV = @{term "UNIV :: nat set"};
+ val lhs = lub $ (image $ take_const $ UNIV);
+ val ax = mk_trp (lhs === ID);
+ in
+ add_one (dnam, [("lub_take", ax)], [])
+ end
+ in
+ val thy =
+ if definitional then thy
+ else fold ax_lub_take dnames thy
+ end;
in
thy
- |> Sign.add_path comp_dnam
- |> add_defs_infer (bisim_def::(if use_copy_def then [copy_def] else []))
- |> Sign.parent_path
- |> fold add_matchers eqs
end; (* let (add_axioms) *)
end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 02 17:36:40 2010 +0000
@@ -0,0 +1,1123 @@
+(* Title: HOLCF/Tools/domain/domain_constructors.ML
+ Author: Brian Huffman
+
+Defines constructor functions for a given domain isomorphism
+and proves related theorems.
+*)
+
+signature DOMAIN_CONSTRUCTORS =
+sig
+ val add_domain_constructors :
+ string
+ -> (binding * (bool * binding option * typ) list * mixfix) list
+ -> Domain_Isomorphism.iso_info
+ -> theory
+ -> { con_consts : term list,
+ con_betas : thm list,
+ exhaust : thm,
+ casedist : thm,
+ con_compacts : thm list,
+ con_rews : thm list,
+ inverts : thm list,
+ injects : thm list,
+ dist_les : thm list,
+ dist_eqs : thm list,
+ cases : thm list,
+ sel_rews : thm list,
+ dis_rews : thm list,
+ match_rews : thm list,
+ pat_rews : thm list
+ } * theory;
+end;
+
+
+structure Domain_Constructors :> DOMAIN_CONSTRUCTORS =
+struct
+
+open HOLCF_Library;
+infixr 6 ->>;
+infix -->>;
+
+(************************** miscellaneous functions ***************************)
+
+val simple_ss =
+ HOL_basic_ss addsimps simp_thms;
+
+val beta_ss =
+ HOL_basic_ss
+ addsimps simp_thms
+ addsimps [@{thm beta_cfun}]
+ addsimprocs [@{simproc cont_proc}];
+
+fun define_consts
+ (specs : (binding * term * mixfix) list)
+ (thy : theory)
+ : (term list * thm list) * theory =
+ let
+ fun mk_decl (b, t, mx) = (b, fastype_of t, mx);
+ val decls = map mk_decl specs;
+ val thy = Cont_Consts.add_consts decls thy;
+ fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T);
+ val consts = map mk_const decls;
+ fun mk_def c (b, t, mx) =
+ (Binding.suffix_name "_def" b, Logic.mk_equals (c, t));
+ val defs = map2 mk_def consts specs;
+ val (def_thms, thy) =
+ PureThy.add_defs false (map Thm.no_attributes defs) thy;
+ in
+ ((consts, def_thms), thy)
+ end;
+
+fun prove
+ (thy : theory)
+ (defs : thm list)
+ (goal : term)
+ (tacs : {prems: thm list, context: Proof.context} -> tactic list)
+ : thm =
+ let
+ fun tac {prems, context} =
+ rewrite_goals_tac defs THEN
+ EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
+ in
+ Goal.prove_global thy [] [] goal tac
+ end;
+
+fun get_vars_avoiding
+ (taken : string list)
+ (args : (bool * typ) list)
+ : (term list * term list) =
+ let
+ val Ts = map snd args;
+ val ns = Name.variant_list taken (Datatype_Prop.make_tnames Ts);
+ val vs = map Free (ns ~~ Ts);
+ val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
+ in
+ (vs, nonlazy)
+ end;
+
+fun get_vars args = get_vars_avoiding [] args;
+
+(************** generating beta reduction rules from definitions **************)
+
+local
+ fun arglist (Const _ $ Abs (s, T, t)) =
+ let
+ val arg = Free (s, T);
+ val (args, body) = arglist (subst_bound (arg, t));
+ in (arg :: args, body) end
+ | arglist t = ([], t);
+in
+ fun beta_of_def thy def_thm =
+ let
+ val (con, lam) = Logic.dest_equals (concl_of def_thm);
+ val (args, rhs) = arglist lam;
+ val lhs = list_ccomb (con, args);
+ val goal = mk_equals (lhs, rhs);
+ val cs = ContProc.cont_thms lam;
+ val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs;
+ in
+ prove thy (def_thm::betas) goal (K [rtac reflexive_thm 1])
+ end;
+end;
+
+(******************************************************************************)
+(************* definitions and theorems for constructor functions *************)
+(******************************************************************************)
+
+fun add_constructors
+ (spec : (binding * (bool * typ) list * mixfix) list)
+ (abs_const : term)
+ (iso_locale : thm)
+ (thy : theory)
+ =
+ let
+
+ (* get theorems about rep and abs *)
+ val abs_strict = iso_locale RS @{thm iso.abs_strict};
+
+ (* get types of type isomorphism *)
+ val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const);
+
+ fun vars_of args =
+ let
+ val Ts = map snd args;
+ val ns = Datatype_Prop.make_tnames Ts;
+ in
+ map Free (ns ~~ Ts)
+ end;
+
+ (* define constructor functions *)
+ val ((con_consts, con_defs), thy) =
+ let
+ fun one_arg (lazy, T) var = if lazy then mk_up var else var;
+ fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args));
+ fun mk_abs t = abs_const ` t;
+ val rhss = map mk_abs (mk_sinjects (map one_con spec));
+ fun mk_def (bind, args, mx) rhs =
+ (bind, big_lambdas (vars_of args) rhs, mx);
+ in
+ define_consts (map2 mk_def spec rhss) thy
+ end;
+
+ (* prove beta reduction rules for constructors *)
+ val con_betas = map (beta_of_def thy) con_defs;
+
+ (* replace bindings with terms in constructor spec *)
+ val spec' : (term * (bool * typ) list) list =
+ let fun one_con con (b, args, mx) = (con, args);
+ in map2 one_con con_consts spec end;
+
+ (* prove exhaustiveness of constructors *)
+ local
+ fun arg2typ n (true, T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
+ | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo}));
+ fun args2typ n [] = (n, oneT)
+ | args2typ n [arg] = arg2typ n arg
+ | args2typ n (arg::args) =
+ let
+ val (n1, t1) = arg2typ n arg;
+ val (n2, t2) = args2typ n1 args
+ in (n2, mk_sprodT (t1, t2)) end;
+ fun cons2typ n [] = (n, oneT)
+ | cons2typ n [con] = args2typ n (snd con)
+ | cons2typ n (con::cons) =
+ let
+ val (n1, t1) = args2typ n (snd con);
+ val (n2, t2) = cons2typ n1 cons
+ in (n2, mk_ssumT (t1, t2)) end;
+ val ct = ctyp_of thy (snd (cons2typ 1 spec'));
+ val thm1 = instantiate' [SOME ct] [] @{thm exh_start};
+ val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1;
+ val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
+
+ val x = Free ("x", lhsT);
+ fun one_con (con, args) =
+ let
+ val (vs, nonlazy) = get_vars_avoiding ["x"] args;
+ val eqn = mk_eq (x, list_ccomb (con, vs));
+ val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy);
+ in Library.foldr mk_ex (vs, conj) end;
+ val goal = mk_trp (foldr1 mk_disj (mk_undef x :: map one_con spec'));
+ (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
+ val tacs = [
+ rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
+ rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
+ rtac thm3 1];
+ in
+ val exhaust = prove thy con_betas goal (K tacs);
+ val casedist =
+ (exhaust RS @{thm exh_casedist0})
+ |> rewrite_rule @{thms exh_casedists}
+ |> Drule.export_without_context;
+ end;
+
+ (* prove compactness rules for constructors *)
+ val con_compacts =
+ let
+ val rules = @{thms compact_sinl compact_sinr compact_spair
+ compact_up compact_ONE};
+ val tacs =
+ [rtac (iso_locale RS @{thm iso.compact_abs}) 1,
+ REPEAT (resolve_tac rules 1 ORELSE atac 1)];
+ fun con_compact (con, args) =
+ let
+ val vs = vars_of args;
+ val con_app = list_ccomb (con, vs);
+ val concl = mk_trp (mk_compact con_app);
+ val assms = map (mk_trp o mk_compact) vs;
+ val goal = Logic.list_implies (assms, concl);
+ in
+ prove thy con_betas goal (K tacs)
+ end;
+ in
+ map con_compact spec'
+ end;
+
+ (* prove strictness rules for constructors *)
+ local
+ fun con_strict (con, args) =
+ let
+ val rules = abs_strict :: @{thms con_strict_rules};
+ val (vs, nonlazy) = get_vars args;
+ fun one_strict v' =
+ let
+ val UU = mk_bottom (fastype_of v');
+ val vs' = map (fn v => if v = v' then UU else v) vs;
+ val goal = mk_trp (mk_undef (list_ccomb (con, vs')));
+ val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
+ in prove thy con_betas goal (K tacs) end;
+ in map one_strict nonlazy end;
+
+ fun con_defin (con, args) =
+ let
+ fun iff_disj (t, []) = HOLogic.mk_not t
+ | iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts);
+ val (vs, nonlazy) = get_vars args;
+ val lhs = mk_undef (list_ccomb (con, vs));
+ val rhss = map mk_undef nonlazy;
+ val goal = mk_trp (iff_disj (lhs, rhss));
+ val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
+ val rules = rule1 :: @{thms con_defined_iff_rules};
+ val tacs = [simp_tac (HOL_ss addsimps rules) 1];
+ in prove thy con_betas goal (K tacs) end;
+ in
+ val con_stricts = maps con_strict spec';
+ val con_defins = map con_defin spec';
+ val con_rews = con_stricts @ con_defins;
+ end;
+
+ (* prove injectiveness of constructors *)
+ local
+ fun pgterm rel (con, args) =
+ let
+ fun prime (Free (n, T)) = Free (n^"'", T)
+ | prime t = t;
+ val (xs, nonlazy) = get_vars args;
+ val ys = map prime xs;
+ val lhs = rel (list_ccomb (con, xs), list_ccomb (con, ys));
+ val rhs = foldr1 mk_conj (ListPair.map rel (xs, ys));
+ val concl = mk_trp (mk_eq (lhs, rhs));
+ val zs = case args of [_] => [] | _ => nonlazy;
+ val assms = map (mk_trp o mk_defined) zs;
+ val goal = Logic.list_implies (assms, concl);
+ in prove thy con_betas goal end;
+ val cons' = filter (fn (_, args) => not (null args)) spec';
+ in
+ val inverts =
+ let
+ val abs_below = iso_locale RS @{thm iso.abs_below};
+ val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below};
+ val rules2 = @{thms up_defined spair_defined ONE_defined}
+ val rules = rules1 @ rules2;
+ val tacs = [asm_simp_tac (simple_ss addsimps rules) 1];
+ in map (fn c => pgterm mk_below c (K tacs)) cons' end;
+ val injects =
+ let
+ val abs_eq = iso_locale RS @{thm iso.abs_eq};
+ val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq};
+ val rules2 = @{thms up_defined spair_defined ONE_defined}
+ val rules = rules1 @ rules2;
+ val tacs = [asm_simp_tac (simple_ss addsimps rules) 1];
+ in map (fn c => pgterm mk_eq c (K tacs)) cons' end;
+ end;
+
+ (* prove distinctness of constructors *)
+ local
+ fun map_dist (f : 'a -> 'a -> 'b) (xs : 'a list) : 'b list =
+ flat (map_index (fn (i, x) => map (f x) (nth_drop i xs)) xs);
+ fun prime (Free (n, T)) = Free (n^"'", T)
+ | prime t = t;
+ fun iff_disj (t, []) = mk_not t
+ | iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts);
+ fun iff_disj2 (t, [], us) = mk_not t
+ | iff_disj2 (t, ts, []) = mk_not t
+ | iff_disj2 (t, ts, us) =
+ mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us));
+ fun dist_le (con1, args1) (con2, args2) =
+ let
+ val (vs1, zs1) = get_vars args1;
+ val (vs2, zs2) = get_vars args2 |> pairself (map prime);
+ val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2));
+ val rhss = map mk_undef zs1;
+ val goal = mk_trp (iff_disj (lhs, rhss));
+ val rule1 = iso_locale RS @{thm iso.abs_below};
+ val rules = rule1 :: @{thms con_below_iff_rules};
+ val tacs = [simp_tac (HOL_ss addsimps rules) 1];
+ in prove thy con_betas goal (K tacs) end;
+ fun dist_eq (con1, args1) (con2, args2) =
+ let
+ val (vs1, zs1) = get_vars args1;
+ val (vs2, zs2) = get_vars args2 |> pairself (map prime);
+ val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2));
+ val rhss1 = map mk_undef zs1;
+ val rhss2 = map mk_undef zs2;
+ val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2));
+ val rule1 = iso_locale RS @{thm iso.abs_eq};
+ val rules = rule1 :: @{thms con_eq_iff_rules};
+ val tacs = [simp_tac (HOL_ss addsimps rules) 1];
+ in prove thy con_betas goal (K tacs) end;
+ in
+ val dist_les = map_dist dist_le spec';
+ val dist_eqs = map_dist dist_eq spec';
+ end;
+
+ val result =
+ {
+ con_consts = con_consts,
+ con_betas = con_betas,
+ exhaust = exhaust,
+ casedist = casedist,
+ con_compacts = con_compacts,
+ con_rews = con_rews,
+ inverts = inverts,
+ injects = injects,
+ dist_les = dist_les,
+ dist_eqs = dist_eqs
+ };
+ in
+ (result, thy)
+ end;
+
+(******************************************************************************)
+(**************** definition and theorems for case combinator *****************)
+(******************************************************************************)
+
+fun add_case_combinator
+ (spec : (term * (bool * typ) list) list)
+ (lhsT : typ)
+ (dname : string)
+ (con_betas : thm list)
+ (casedist : thm)
+ (iso_locale : thm)
+ (rep_const : term)
+ (thy : theory)
+ : ((typ -> term) * thm list) * theory =
+ let
+
+ (* TODO: move these to holcf_library.ML *)
+ fun one_when_const T = Const (@{const_name one_when}, T ->> oneT ->> T);
+ fun mk_one_when t = one_when_const (fastype_of t) ` t;
+ fun mk_sscase (t, u) =
+ let
+ val (T, V) = dest_cfunT (fastype_of t);
+ val (U, V) = dest_cfunT (fastype_of u);
+ in sscase_const (T, U, V) ` t ` u end;
+ fun strictify_const T = Const (@{const_name strictify}, T ->> T);
+ fun mk_strictify t = strictify_const (fastype_of t) ` t;
+ fun ssplit_const (T, U, V) =
+ Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V);
+ fun mk_ssplit t =
+ let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t));
+ in ssplit_const (T, U, V) ` t end;
+ fun lambda_stuple [] t = mk_one_when t
+ | lambda_stuple [x] t = mk_strictify (big_lambda x t)
+ | lambda_stuple [x,y] t = mk_ssplit (big_lambdas [x, y] t)
+ | lambda_stuple (x::xs) t = mk_ssplit (big_lambda x (lambda_stuple xs t));
+
+ (* eta contraction for simplifying definitions *)
+ fun cont_eta_contract (Const(@{const_name Abs_CFun},TT) $ Abs(a,T,body)) =
+ (case cont_eta_contract body of
+ body' as (Const(@{const_name Abs_CFun},Ta) $ f $ Bound 0) =>
+ if not (0 mem loose_bnos f) then incr_boundvars ~1 f
+ else Const(@{const_name Abs_CFun},TT) $ Abs(a,T,body')
+ | body' => Const(@{const_name Abs_CFun},TT) $ Abs(a,T,body'))
+ | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
+ | cont_eta_contract t = t;
+
+ (* prove rep/abs rules *)
+ val rep_strict = iso_locale RS @{thm iso.rep_strict};
+ val abs_inverse = iso_locale RS @{thm iso.abs_iso};
+
+ (* calculate function arguments of case combinator *)
+ val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+ val resultT = TFree (Name.variant tns "'t", @{sort pcpo});
+ fun fTs T = map (fn (_, args) => map snd args -->> T) spec;
+ val fns = Datatype_Prop.indexify_names (map (K "f") spec);
+ val fs = map Free (fns ~~ fTs resultT);
+ fun caseT T = fTs T -->> (lhsT ->> T);
+
+ (* definition of case combinator *)
+ local
+ val case_bind = Binding.name (dname ^ "_when");
+ fun one_con f (_, args) =
+ let
+ fun argT (lazy, T) = if lazy then mk_upT T else T;
+ fun down (lazy, T) v = if lazy then from_up T ` v else v;
+ val Ts = map argT args;
+ val ns = Name.variant_list fns (Datatype_Prop.make_tnames Ts);
+ val vs = map Free (ns ~~ Ts);
+ val xs = map2 down args vs;
+ in
+ cont_eta_contract (lambda_stuple vs (list_ccomb (f, xs)))
+ end;
+ val body = foldr1 mk_sscase (map2 one_con fs spec);
+ val rhs = big_lambdas fs (mk_cfcomp (body, rep_const));
+ val ((case_consts, case_defs), thy) =
+ define_consts [(case_bind, rhs, NoSyn)] thy;
+ val case_name = Sign.full_name thy case_bind;
+ in
+ val case_def = hd case_defs;
+ fun case_const T = Const (case_name, caseT T);
+ val case_app = list_ccomb (case_const resultT, fs);
+ val thy = thy;
+ end;
+
+ (* define syntax for case combinator *)
+ (* TODO: re-implement case syntax using a parse translation *)
+ local
+ open Syntax
+ fun syntax c = Syntax.mark_const (fst (dest_Const c));
+ fun xconst c = Long_Name.base_name (fst (dest_Const c));
+ fun c_ast authentic con =
+ Constant (if authentic then syntax con else xconst con);
+ fun showint n = string_of_int (n+1);
+ fun expvar n = Variable ("e" ^ showint n);
+ fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m);
+ fun argvars n args = map_index (argvar n) args;
+ fun app s (l, r) = mk_appl (Constant s) [l, r];
+ val cabs = app "_cabs";
+ val capp = app @{const_syntax Rep_CFun};
+ val capps = Library.foldl capp
+ fun con1 authentic n (con,args) =
+ Library.foldl capp (c_ast authentic con, argvars n args);
+ fun case1 authentic (n, c) =
+ app "_case1" (con1 authentic n c, expvar n);
+ fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args);
+ fun when1 n (m, c) =
+ if n = m then arg1 (n, c) else (Constant @{const_syntax UU});
+ val case_constant = Constant (syntax (case_const dummyT));
+ fun case_trans authentic =
+ ParsePrintRule
+ (app "_case_syntax"
+ (Variable "x",
+ foldr1 (app "_case2") (map_index (case1 authentic) spec)),
+ capp (capps (case_constant, map_index arg1 spec), Variable "x"));
+ fun one_abscon_trans authentic (n, c) =
+ ParsePrintRule
+ (cabs (con1 authentic n c, expvar n),
+ capps (case_constant, map_index (when1 n) spec));
+ fun abscon_trans authentic =
+ map_index (one_abscon_trans authentic) spec;
+ val trans_rules : ast Syntax.trrule list =
+ case_trans false :: case_trans true ::
+ abscon_trans false @ abscon_trans true;
+ in
+ val thy = Sign.add_trrules_i trans_rules thy;
+ end;
+
+ (* prove beta reduction rule for case combinator *)
+ val case_beta = beta_of_def thy case_def;
+
+ (* prove strictness of case combinator *)
+ val case_strict =
+ let
+ val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}];
+ val goal = mk_trp (mk_strict case_app);
+ val rules = @{thms sscase1 ssplit1 strictify1 one_when1};
+ val tacs = [resolve_tac rules 1];
+ in prove thy defs goal (K tacs) end;
+
+ (* prove rewrites for case combinator *)
+ local
+ fun one_case (con, args) f =
+ let
+ val (vs, nonlazy) = get_vars args;
+ val assms = map (mk_trp o mk_defined) nonlazy;
+ val lhs = case_app ` list_ccomb (con, vs);
+ val rhs = list_ccomb (f, vs);
+ val concl = mk_trp (mk_eq (lhs, rhs));
+ val goal = Logic.list_implies (assms, concl);
+ val defs = case_beta :: con_betas;
+ val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1};
+ val rules2 = @{thms con_defined_iff_rules};
+ val rules3 = @{thms cfcomp2 one_when2};
+ val rules = abs_inverse :: rules1 @ rules2 @ rules3;
+ val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
+ in prove thy defs goal (K tacs) end;
+ in
+ val case_apps = map2 one_case spec fs;
+ end
+
+ in
+ ((case_const, case_strict :: case_apps), thy)
+ end
+
+(******************************************************************************)
+(************** definitions and theorems for selector functions ***************)
+(******************************************************************************)
+
+fun add_selectors
+ (spec : (term * (bool * binding option * typ) list) list)
+ (rep_const : term)
+ (abs_inv : thm)
+ (rep_strict : thm)
+ (rep_strict_iff : thm)
+ (con_betas : thm list)
+ (thy : theory)
+ : thm list * theory =
+ let
+
+ (* define selector functions *)
+ val ((sel_consts, sel_defs), thy) =
+ let
+ fun rangeT s = snd (dest_cfunT (fastype_of s));
+ fun mk_outl s = mk_cfcomp (from_sinl (dest_ssumT (rangeT s)), s);
+ fun mk_outr s = mk_cfcomp (from_sinr (dest_ssumT (rangeT s)), s);
+ fun mk_sfst s = mk_cfcomp (sfst_const (dest_sprodT (rangeT s)), s);
+ fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s);
+ fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s);
+
+ fun sels_of_arg s (lazy, NONE, T) = []
+ | sels_of_arg s (lazy, SOME b, T) =
+ [(b, if lazy then mk_down s else s, NoSyn)];
+ fun sels_of_args s [] = []
+ | sels_of_args s (v :: []) = sels_of_arg s v
+ | sels_of_args s (v :: vs) =
+ sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs;
+ fun sels_of_cons s [] = []
+ | sels_of_cons s ((con, args) :: []) = sels_of_args s args
+ | sels_of_cons s ((con, args) :: cs) =
+ sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs;
+ val sel_eqns : (binding * term * mixfix) list =
+ sels_of_cons rep_const spec;
+ in
+ define_consts sel_eqns thy
+ end
+
+ (* replace bindings with terms in constructor spec *)
+ val spec2 : (term * (bool * term option * typ) list) list =
+ let
+ fun prep_arg (lazy, NONE, T) sels = ((lazy, NONE, T), sels)
+ | prep_arg (lazy, SOME _, T) sels =
+ ((lazy, SOME (hd sels), T), tl sels);
+ fun prep_con (con, args) sels =
+ apfst (pair con) (fold_map prep_arg args sels);
+ in
+ fst (fold_map prep_con spec sel_consts)
+ end;
+
+ (* prove selector strictness rules *)
+ val sel_stricts : thm list =
+ let
+ val rules = rep_strict :: @{thms sel_strict_rules};
+ val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
+ fun sel_strict sel =
+ let
+ val goal = mk_trp (mk_strict sel);
+ in
+ prove thy sel_defs goal (K tacs)
+ end
+ in
+ map sel_strict sel_consts
+ end
+
+ (* prove selector application rules *)
+ val sel_apps : thm list =
+ let
+ val defs = con_betas @ sel_defs;
+ val rules = abs_inv :: @{thms sel_app_rules};
+ val tacs = [asm_simp_tac (simple_ss addsimps rules) 1];
+ fun sel_apps_of (i, (con, args)) =
+ let
+ val Ts : typ list = map #3 args;
+ val ns : string list = Datatype_Prop.make_tnames Ts;
+ val vs : term list = map Free (ns ~~ Ts);
+ val con_app : term = list_ccomb (con, vs);
+ val vs' : (bool * term) list = map #1 args ~~ vs;
+ fun one_same (n, sel, T) =
+ let
+ val xs = map snd (filter_out fst (nth_drop n vs'));
+ val assms = map (mk_trp o mk_defined) xs;
+ val concl = mk_trp (mk_eq (sel ` con_app, nth vs n));
+ val goal = Logic.list_implies (assms, concl);
+ in
+ prove thy defs goal (K tacs)
+ end;
+ fun one_diff (n, sel, T) =
+ let
+ val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T));
+ in
+ prove thy defs goal (K tacs)
+ end;
+ fun one_con (j, (_, args')) : thm list =
+ let
+ fun prep (i, (lazy, NONE, T)) = NONE
+ | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T);
+ val sels : (int * term * typ) list =
+ map_filter prep (map_index I args');
+ in
+ if i = j
+ then map one_same sels
+ else map one_diff sels
+ end
+ in
+ flat (map_index one_con spec2)
+ end
+ in
+ flat (map_index sel_apps_of spec2)
+ end
+
+ (* prove selector definedness rules *)
+ val sel_defins : thm list =
+ let
+ val rules = rep_strict_iff :: @{thms sel_defined_iff_rules};
+ val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
+ fun sel_defin sel =
+ let
+ val (T, U) = dest_cfunT (fastype_of sel);
+ val x = Free ("x", T);
+ val lhs = mk_eq (sel ` x, mk_bottom U);
+ val rhs = mk_eq (x, mk_bottom T);
+ val goal = mk_trp (mk_eq (lhs, rhs));
+ in
+ prove thy sel_defs goal (K tacs)
+ end
+ fun one_arg (false, SOME sel, T) = SOME (sel_defin sel)
+ | one_arg _ = NONE;
+ in
+ case spec2 of
+ [(con, args)] => map_filter one_arg args
+ | _ => []
+ end;
+
+ in
+ (sel_stricts @ sel_defins @ sel_apps, thy)
+ end
+
+(******************************************************************************)
+(************ definitions and theorems for discriminator functions ************)
+(******************************************************************************)
+
+fun add_discriminators
+ (bindings : binding list)
+ (spec : (term * (bool * typ) list) list)
+ (lhsT : typ)
+ (casedist : thm)
+ (case_const : typ -> term)
+ (case_rews : thm list)
+ (thy : theory) =
+ let
+
+ fun vars_of args =
+ let
+ val Ts = map snd args;
+ val ns = Datatype_Prop.make_tnames Ts;
+ in
+ map Free (ns ~~ Ts)
+ end;
+
+ (* define discriminator functions *)
+ local
+ fun dis_fun i (j, (con, args)) =
+ let
+ val (vs, nonlazy) = get_vars args;
+ val tr = if i = j then @{term TT} else @{term FF};
+ in
+ big_lambdas vs tr
+ end;
+ fun dis_eqn (i, bind) : binding * term * mixfix =
+ let
+ val dis_bind = Binding.prefix_name "is_" bind;
+ val rhs = list_ccomb (case_const trT, map_index (dis_fun i) spec);
+ in
+ (dis_bind, rhs, NoSyn)
+ end;
+ in
+ val ((dis_consts, dis_defs), thy) =
+ define_consts (map_index dis_eqn bindings) thy
+ end;
+
+ (* prove discriminator strictness rules *)
+ local
+ fun dis_strict dis =
+ let val goal = mk_trp (mk_strict dis);
+ in prove thy dis_defs goal (K [rtac (hd case_rews) 1]) end;
+ in
+ val dis_stricts = map dis_strict dis_consts;
+ end;
+
+ (* prove discriminator/constructor rules *)
+ local
+ fun dis_app (i, dis) (j, (con, args)) =
+ let
+ val (vs, nonlazy) = get_vars args;
+ val lhs = dis ` list_ccomb (con, vs);
+ val rhs = if i = j then @{term TT} else @{term FF};
+ val assms = map (mk_trp o mk_defined) nonlazy;
+ val concl = mk_trp (mk_eq (lhs, rhs));
+ val goal = Logic.list_implies (assms, concl);
+ val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1];
+ in prove thy dis_defs goal (K tacs) end;
+ fun one_dis (i, dis) =
+ map_index (dis_app (i, dis)) spec;
+ in
+ val dis_apps = flat (map_index one_dis dis_consts);
+ end;
+
+ (* prove discriminator definedness rules *)
+ local
+ fun dis_defin dis =
+ let
+ val x = Free ("x", lhsT);
+ val simps = dis_apps @ @{thms dist_eq_tr};
+ val tacs =
+ [rtac @{thm iffI} 1,
+ asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2,
+ rtac casedist 1, atac 1,
+ DETERM_UNTIL_SOLVED (CHANGED
+ (asm_full_simp_tac (simple_ss addsimps simps) 1))];
+ val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x));
+ in prove thy [] goal (K tacs) end;
+ in
+ val dis_defins = map dis_defin dis_consts;
+ end;
+
+ in
+ (dis_stricts @ dis_defins @ dis_apps, thy)
+ end;
+
+(******************************************************************************)
+(*************** definitions and theorems for match combinators ***************)
+(******************************************************************************)
+
+fun add_match_combinators
+ (bindings : binding list)
+ (spec : (term * (bool * typ) list) list)
+ (lhsT : typ)
+ (casedist : thm)
+ (case_const : typ -> term)
+ (case_rews : thm list)
+ (thy : theory) =
+ let
+
+ (* get a fresh type variable for the result type *)
+ val resultT : typ =
+ let
+ val ts : string list = map (fst o dest_TFree) (snd (dest_Type lhsT));
+ val t : string = Name.variant ts "'t";
+ in TFree (t, @{sort pcpo}) end;
+
+ (* define match combinators *)
+ local
+ val x = Free ("x", lhsT);
+ fun k args = Free ("k", map snd args -->> mk_matchT resultT);
+ val fail = mk_fail resultT;
+ fun mat_fun i (j, (con, args)) =
+ let
+ val (vs, nonlazy) = get_vars_avoiding ["x","k"] args;
+ in
+ if i = j then k args else big_lambdas vs fail
+ end;
+ fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
+ let
+ val mat_bind = Binding.prefix_name "match_" bind;
+ val funs = map_index (mat_fun i) spec
+ val body = list_ccomb (case_const (mk_matchT resultT), funs);
+ val rhs = big_lambda x (big_lambda (k args) (body ` x));
+ in
+ (mat_bind, rhs, NoSyn)
+ end;
+ in
+ val ((match_consts, match_defs), thy) =
+ define_consts (map_index mat_eqn (bindings ~~ spec)) thy
+ end;
+
+ (* register match combinators with fixrec package *)
+ local
+ val con_names = map (fst o dest_Const o fst) spec;
+ val mat_names = map (fst o dest_Const) match_consts;
+ in
+ val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy;
+ end;
+
+ (* prove strictness of match combinators *)
+ local
+ fun match_strict mat =
+ let
+ val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat));
+ val k = Free ("k", U);
+ val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V));
+ val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1];
+ in prove thy match_defs goal (K tacs) end;
+ in
+ val match_stricts = map match_strict match_consts;
+ end;
+
+ (* prove match/constructor rules *)
+ local
+ val fail = mk_fail resultT;
+ fun match_app (i, mat) (j, (con, args)) =
+ let
+ val (vs, nonlazy) = get_vars_avoiding ["k"] args;
+ val (_, (kT, _)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat));
+ val k = Free ("k", kT);
+ val lhs = mat ` list_ccomb (con, vs) ` k;
+ val rhs = if i = j then list_ccomb (k, vs) else fail;
+ val assms = map (mk_trp o mk_defined) nonlazy;
+ val concl = mk_trp (mk_eq (lhs, rhs));
+ val goal = Logic.list_implies (assms, concl);
+ val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1];
+ in prove thy match_defs goal (K tacs) end;
+ fun one_match (i, mat) =
+ map_index (match_app (i, mat)) spec;
+ in
+ val match_apps = flat (map_index one_match match_consts);
+ end;
+
+ in
+ (match_stricts @ match_apps, thy)
+ end;
+
+(******************************************************************************)
+(************** definitions and theorems for pattern combinators **************)
+(******************************************************************************)
+
+fun add_pattern_combinators
+ (bindings : binding list)
+ (spec : (term * (bool * typ) list) list)
+ (lhsT : typ)
+ (casedist : thm)
+ (case_const : typ -> term)
+ (case_rews : thm list)
+ (thy : theory) =
+ let
+
+ (* utility functions *)
+ fun mk_pair_pat (p1, p2) =
+ let
+ val T1 = fastype_of p1;
+ val T2 = fastype_of p2;
+ val (U1, V1) = apsnd dest_matchT (dest_cfunT T1);
+ val (U2, V2) = apsnd dest_matchT (dest_cfunT T2);
+ val pat_typ = [T1, T2] --->
+ (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2)));
+ val pat_const = Const (@{const_name cpair_pat}, pat_typ);
+ in
+ pat_const $ p1 $ p2
+ end;
+ fun mk_tuple_pat [] = return_const HOLogic.unitT
+ | mk_tuple_pat ps = foldr1 mk_pair_pat ps;
+ fun branch_const (T,U,V) =
+ Const (@{const_name branch},
+ (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V);
+
+ (* define pattern combinators *)
+ local
+ val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+
+ fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
+ let
+ val pat_bind = Binding.suffix_name "_pat" bind;
+ val Ts = map snd args;
+ val Vs =
+ (map (K "'t") args)
+ |> Datatype_Prop.indexify_names
+ |> Name.variant_list tns
+ |> map (fn t => TFree (t, @{sort pcpo}));
+ val patNs = Datatype_Prop.indexify_names (map (K "pat") args);
+ val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
+ val pats = map Free (patNs ~~ patTs);
+ val fail = mk_fail (mk_tupleT Vs);
+ val (vs, nonlazy) = get_vars_avoiding patNs args;
+ val rhs = big_lambdas vs (mk_tuple_pat pats ` mk_tuple vs);
+ fun one_fun (j, (_, args')) =
+ let
+ val (vs', nonlazy) = get_vars_avoiding patNs args';
+ in if i = j then rhs else big_lambdas vs' fail end;
+ val funs = map_index one_fun spec;
+ val body = list_ccomb (case_const (mk_matchT (mk_tupleT Vs)), funs);
+ in
+ (pat_bind, lambdas pats body, NoSyn)
+ end;
+ in
+ val ((pat_consts, pat_defs), thy) =
+ define_consts (map_index pat_eqn (bindings ~~ spec)) thy
+ end;
+
+ (* syntax translations for pattern combinators *)
+ local
+ open Syntax
+ fun syntax c = Syntax.mark_const (fst (dest_Const c));
+ fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r];
+ val capp = app @{const_syntax Rep_CFun};
+ val capps = Library.foldl capp
+
+ fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"];
+ fun app_pat x = Syntax.mk_appl (Constant "_pat") [x];
+ fun args_list [] = Constant "_noargs"
+ | args_list xs = foldr1 (app "_args") xs;
+ fun one_case_trans (pat, (con, args)) =
+ let
+ val cname = Constant (syntax con);
+ val pname = Constant (syntax 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 (capps (cname, xs)),
+ mk_appl pname (map app_pat xs)),
+ ParseRule (app_var (capps (cname, xs)),
+ app_var (args_list xs)),
+ PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)),
+ app "_match" (mk_appl pname ps, args_list vs))]
+ end;
+ val trans_rules : Syntax.ast Syntax.trrule list =
+ maps one_case_trans (pat_consts ~~ spec);
+ in
+ val thy = Sign.add_trrules_i trans_rules thy;
+ end;
+
+ (* prove strictness and reduction rules of pattern combinators *)
+ local
+ val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+ val rn = Name.variant tns "'r";
+ val R = TFree (rn, @{sort pcpo});
+ fun pat_lhs (pat, args) =
+ let
+ val Ts = map snd args;
+ val Vs =
+ (map (K "'t") args)
+ |> Datatype_Prop.indexify_names
+ |> Name.variant_list (rn::tns)
+ |> map (fn t => TFree (t, @{sort pcpo}));
+ val patNs = Datatype_Prop.indexify_names (map (K "pat") args);
+ val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
+ val pats = map Free (patNs ~~ patTs);
+ val k = Free ("rhs", mk_tupleT Vs ->> R);
+ val branch1 = branch_const (lhsT, mk_tupleT Vs, R);
+ val fun1 = (branch1 $ list_comb (pat, pats)) ` k;
+ val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R);
+ val fun2 = (branch2 $ mk_tuple_pat pats) ` k;
+ val taken = "rhs" :: patNs;
+ in (fun1, fun2, taken) end;
+ fun pat_strict (pat, (con, args)) =
+ let
+ val (fun1, fun2, taken) = pat_lhs (pat, args);
+ val defs = @{thm branch_def} :: pat_defs;
+ val goal = mk_trp (mk_strict fun1);
+ val rules = @{thm Fixrec.bind_strict} :: case_rews;
+ val tacs = [simp_tac (beta_ss addsimps rules) 1];
+ in prove thy defs goal (K tacs) end;
+ fun pat_apps (i, (pat, (con, args))) =
+ let
+ val (fun1, fun2, taken) = pat_lhs (pat, args);
+ fun pat_app (j, (con', args')) =
+ let
+ val (vs, nonlazy) = get_vars_avoiding taken args';
+ val con_app = list_ccomb (con', vs);
+ val assms = map (mk_trp o mk_defined) nonlazy;
+ val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R;
+ val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
+ val goal = Logic.list_implies (assms, concl);
+ val defs = @{thm branch_def} :: pat_defs;
+ val rules = @{thms bind_fail left_unit} @ case_rews;
+ val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
+ in prove thy defs goal (K tacs) end;
+ in map_index pat_app spec end;
+ in
+ val pat_stricts = map pat_strict (pat_consts ~~ spec);
+ val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec));
+ end;
+
+ in
+ (pat_stricts @ pat_apps, thy)
+ end
+
+(******************************************************************************)
+(******************************* main function ********************************)
+(******************************************************************************)
+
+fun add_domain_constructors
+ (dname : string)
+ (spec : (binding * (bool * binding option * typ) list * mixfix) list)
+ (iso_info : Domain_Isomorphism.iso_info)
+ (thy : theory) =
+ let
+
+ (* retrieve facts about rep/abs *)
+ val lhsT = #absT iso_info;
+ val {rep_const, abs_const, ...} = iso_info;
+ val abs_iso_thm = #abs_inverse iso_info;
+ val rep_iso_thm = #rep_inverse iso_info;
+ val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
+ val rep_strict = iso_locale RS @{thm iso.rep_strict};
+ val abs_strict = iso_locale RS @{thm iso.abs_strict};
+ val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
+ val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
+
+ (* qualify constants and theorems with domain name *)
+ val thy = Sign.add_path dname thy;
+
+ (* define constructor functions *)
+ val (con_result, thy) =
+ let
+ fun prep_arg (lazy, sel, T) = (lazy, T);
+ fun prep_con (b, args, mx) = (b, map prep_arg args, mx);
+ val con_spec = map prep_con spec;
+ in
+ add_constructors con_spec abs_const iso_locale thy
+ end;
+ val {con_consts, con_betas, casedist, ...} = con_result;
+
+ (* define case combinator *)
+ val ((case_const : typ -> term, cases : thm list), thy) =
+ let
+ fun prep_arg (lazy, sel, T) = (lazy, T);
+ fun prep_con c (b, args, mx) = (c, map prep_arg args);
+ val case_spec = map2 prep_con con_consts spec;
+ in
+ add_case_combinator case_spec lhsT dname
+ con_betas casedist iso_locale rep_const thy
+ end;
+
+ (* define and prove theorems for selector functions *)
+ val (sel_thms : thm list, thy : theory) =
+ let
+ val sel_spec : (term * (bool * binding option * typ) list) list =
+ map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec;
+ in
+ add_selectors sel_spec rep_const
+ abs_iso_thm rep_strict rep_defined_iff con_betas thy
+ end;
+
+ (* define and prove theorems for discriminator functions *)
+ val (dis_thms : thm list, thy : theory) =
+ let
+ val bindings = map #1 spec;
+ fun prep_arg (lazy, sel, T) = (lazy, T);
+ fun prep_con c (b, args, mx) = (c, map prep_arg args);
+ val dis_spec = map2 prep_con con_consts spec;
+ in
+ add_discriminators bindings dis_spec lhsT
+ casedist case_const cases thy
+ end
+
+ (* define and prove theorems for match combinators *)
+ val (match_thms : thm list, thy : theory) =
+ let
+ val bindings = map #1 spec;
+ fun prep_arg (lazy, sel, T) = (lazy, T);
+ fun prep_con c (b, args, mx) = (c, map prep_arg args);
+ val mat_spec = map2 prep_con con_consts spec;
+ in
+ add_match_combinators bindings mat_spec lhsT
+ casedist case_const cases thy
+ end
+
+ (* define and prove theorems for pattern combinators *)
+ val (pat_thms : thm list, thy : theory) =
+ let
+ val bindings = map #1 spec;
+ fun prep_arg (lazy, sel, T) = (lazy, T);
+ fun prep_con c (b, args, mx) = (c, map prep_arg args);
+ val pat_spec = map2 prep_con con_consts spec;
+ in
+ add_pattern_combinators bindings pat_spec lhsT
+ casedist case_const cases thy
+ end
+
+ (* restore original signature path *)
+ val thy = Sign.parent_path thy;
+
+ val result =
+ { con_consts = con_consts,
+ con_betas = con_betas,
+ exhaust = #exhaust con_result,
+ casedist = casedist,
+ con_compacts = #con_compacts con_result,
+ con_rews = #con_rews con_result,
+ inverts = #inverts con_result,
+ injects = #injects con_result,
+ dist_les = #dist_les con_result,
+ dist_eqs = #dist_eqs con_result,
+ cases = cases,
+ sel_rews = sel_thms,
+ dis_rews = dis_thms,
+ match_rews = match_thms,
+ pat_rews = pat_thms };
+ in
+ (result, thy)
+ end;
+
+end;
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 17:36:40 2010 +0000
@@ -150,29 +150,26 @@
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 thy' = thy'' |> Domain_Syntax.add_syntax false 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 = 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) =
(Binding.name_of con, (* FIXME preverse binding (!?) *)
mx,
ListPair.map (fn ((lazy,sel,tp),vn) =>
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
Option.map Binding.name_of sel,vn))
- (args,(mk_var_names(map (typid o third) args)))
+ (args, Datatype_Prop.make_tnames (map 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 thy = thy' |> Domain_Axioms.add_axioms false eqs' eqs;
val ((rewss, take_rews), theorems_thy) =
thy
- |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
+ |> fold_map (fn (eq, (x,cs)) =>
+ Domain_Theorems.theorems (eq, eqs) (Type x, cs))
+ (eqs ~~ eqs')
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
in
theorems_thy
@@ -220,35 +217,32 @@
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''' |>
+ val (iso_infos, thy'') = thy''' |>
Domain_Isomorphism.domain_isomorphism
(map (fn ((vs, dname, mx, _), eq) =>
(map fst vs, dname, mx, mk_eq_typ eq, NONE))
(eqs''' ~~ eqs'))
- val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
+ val thy' = thy'' |> Domain_Syntax.add_syntax true 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 = 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) =
(Binding.name_of con, (* FIXME preverse binding (!?) *)
mx,
ListPair.map (fn ((lazy,sel,tp),vn) =>
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
Option.map Binding.name_of sel,vn))
- (args,(mk_var_names(map (typid o third) args)))
+ (args, Datatype_Prop.make_tnames (map 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 thy = thy' |> Domain_Axioms.add_axioms true eqs' eqs;
val ((rewss, take_rews), theorems_thy) =
thy
- |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
+ |> fold_map (fn (eq, (x,cs)) =>
+ Domain_Theorems.theorems (eq, eqs) (Type x, cs))
+ (eqs ~~ eqs')
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
in
theorems_thy
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 17:36:40 2010 +0000
@@ -6,16 +6,34 @@
signature DOMAIN_ISOMORPHISM =
sig
- val domain_isomorphism:
+ type iso_info =
+ {
+ repT : typ,
+ absT : typ,
+ rep_const : term,
+ abs_const : term,
+ rep_inverse : thm,
+ abs_inverse : thm
+ }
+ val domain_isomorphism :
(string list * binding * mixfix * typ * (binding * binding) option) list
- -> theory -> theory
- val domain_isomorphism_cmd:
+ -> theory -> iso_info list * theory
+ val domain_isomorphism_cmd :
(string list * binding * mixfix * string * (binding * binding) option) list
-> theory -> theory
- val add_type_constructor:
- (string * term * string * thm * thm * thm) -> theory -> theory
- val get_map_tab:
+ val add_type_constructor :
+ (string * term * string * thm * thm * thm * thm) -> theory -> theory
+ val get_map_tab :
theory -> string Symtab.table
+ val define_take_functions :
+ (binding * iso_info) list -> theory ->
+ { take_consts : term list,
+ take_defs : thm list,
+ chain_take_thms : thm list,
+ take_0_thms : thm list,
+ take_Suc_thms : thm list,
+ deflation_take_thms : thm list
+ } * theory;
end;
structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM =
@@ -49,133 +67,49 @@
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
-(
+structure Thm_List : THEORY_DATA_ARGS =
+struct
type T = thm list;
val empty = [];
val extend = I;
val merge = Thm.merge_thms;
-);
+end;
+
+structure RepData = Theory_Data (Thm_List);
-structure MapIdData = Theory_Data
-(
- type T = thm list;
- val empty = [];
- val extend = I;
- val merge = Thm.merge_thms;
-);
+structure IsodeflData = Theory_Data (Thm_List);
+
+structure MapIdData = Theory_Data (Thm_List);
+
+structure DeflMapData = Theory_Data (Thm_List);
fun add_type_constructor
- (tname, defl_const, map_name, REP_thm, isodefl_thm, map_ID_thm) =
+ (tname, defl_const, map_name, REP_thm,
+ isodefl_thm, map_ID_thm, defl_map_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)
- #> MapIdData.map (Thm.add_thm map_ID_thm);
+ #> MapIdData.map (Thm.add_thm map_ID_thm)
+ #> DeflMapData.map (Thm.add_thm defl_map_thm);
val get_map_tab = MapData.get;
(******************************************************************************)
-(******************************* building types *******************************)
+(************************** building types and terms **************************)
(******************************************************************************)
-(* ->> is taken from holcf_logic.ML *)
-fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
-
-infixr 6 ->>; val (op ->>) = cfunT;
+open HOLCF_Library;
-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);
+infixr 6 ->>;
+infix -->>;
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;
+ (map (fn T => T ->> T) Ts) -->> (T ->> T)
+ | mapT T = T ->> T;
fun mk_Rep_of T =
Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
@@ -185,12 +119,49 @@
fun isodefl_const T =
Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
+fun mk_deflation t =
+ Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
+
+fun mk_lub t =
+ let
+ val T = Term.range_type (Term.fastype_of t);
+ val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
+ val UNIV_const = @{term "UNIV :: nat set"};
+ val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
+ val image_const = Const (@{const_name image}, image_type);
+ in
+ lub_const $ (image_const $ t $ UNIV_const)
+ end;
+
(* 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));
(******************************************************************************)
+(****************************** isomorphism info ******************************)
+(******************************************************************************)
+
+type iso_info =
+ {
+ absT : typ,
+ repT : typ,
+ abs_const : term,
+ rep_const : term,
+ abs_inverse : thm,
+ rep_inverse : thm
+ }
+
+fun deflation_abs_rep (info : iso_info) : thm =
+ let
+ val abs_iso = #abs_inverse info;
+ val rep_iso = #rep_inverse info;
+ val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
+ in
+ Drule.export_without_context thm
+ end
+
+(******************************************************************************)
(*************** fixed-point definitions and unfolding theorems ***************)
(******************************************************************************)
@@ -204,7 +175,8 @@
val fixpoint = mk_fix (mk_cabs functional);
(* project components of fixpoint *)
- fun mk_projs (x::[]) t = [(x, t)]
+ fun mk_projs [] t = []
+ | 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;
@@ -272,7 +244,7 @@
| 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)
+ SOME t => list_ccomb (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);
@@ -288,15 +260,252 @@
| 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)
+ SOME t => list_ccomb (Const (t, mapT T), map map_of Ts)
| NONE => if is_closed_typ T
- then ID_const T
+ then mk_ID T
else error ("map_of_typ: type variable under unsupported type constructor " ^ c);
in map_of T end;
(******************************************************************************)
-(* prepare datatype specifications *)
+(********************* declaring definitions and theorems *********************)
+(******************************************************************************)
+
+fun define_const
+ (bind : binding, rhs : term)
+ (thy : theory)
+ : (term * thm) * theory =
+ let
+ val typ = Term.fastype_of rhs;
+ val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy;
+ val eqn = Logic.mk_equals (const, rhs);
+ val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn);
+ val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy;
+ in
+ ((const, def_thm), thy)
+ end;
+
+fun add_qualified_thm name (path, thm) thy =
+ thy
+ |> Sign.add_path path
+ |> yield_singleton PureThy.add_thms
+ (Thm.no_attributes (Binding.name name, thm))
+ ||> Sign.parent_path;
+
+(******************************************************************************)
+(************************** defining take functions ***************************)
+(******************************************************************************)
+
+fun define_take_functions
+ (spec : (binding * iso_info) list)
+ (thy : theory) =
+ let
+
+ (* retrieve components of spec *)
+ val dom_binds = map fst spec;
+ val iso_infos = map snd spec;
+ val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
+ val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
+ val dnames = map Binding.name_of dom_binds;
+
+ (* get table of map functions *)
+ val map_tab = MapData.get thy;
+
+ fun mk_projs [] t = []
+ | mk_projs (x::[]) t = [(x, t)]
+ | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+
+ fun mk_cfcomp2 ((rep_const, abs_const), f) =
+ mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
+
+ (* defining map functions over dtyps *)
+ fun copy_of_dtyp recs (T, dt) =
+ if Datatype_Aux.is_rec_type dt
+ then copy_of_dtyp' recs (T, dt)
+ else mk_ID T
+ and copy_of_dtyp' recs (T, Datatype_Aux.DtRec i) = nth recs i
+ | copy_of_dtyp' recs (T, Datatype_Aux.DtTFree a) = mk_ID T
+ | copy_of_dtyp' recs (T, Datatype_Aux.DtType (c, ds)) =
+ case Symtab.lookup map_tab c of
+ SOME f =>
+ list_ccomb
+ (Const (f, mapT T),
+ map (copy_of_dtyp recs) (snd (dest_Type T) ~~ ds))
+ | NONE =>
+ (warning ("copy_of_dtyp: unknown type constructor " ^ c); mk_ID T);
+
+ (* define take functional *)
+ val new_dts : (string * string list) list =
+ map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns;
+ val copy_arg_type = mk_tupleT (map (fn (T, _) => T ->> T) dom_eqns);
+ val copy_arg = Free ("f", copy_arg_type);
+ val copy_args = map snd (mk_projs dom_binds copy_arg);
+ fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
+ let
+ val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
+ val body = copy_of_dtyp copy_args (rhsT, dtyp);
+ in
+ mk_cfcomp2 (rep_abs, body)
+ end;
+ val take_functional =
+ big_lambda copy_arg
+ (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
+ val take_rhss =
+ let
+ val i = Free ("i", HOLogic.natT);
+ val rhs = mk_iterate (i, take_functional)
+ in
+ map (Term.lambda i o snd) (mk_projs dom_binds rhs)
+ end;
+
+ (* define take constants *)
+ fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy =
+ let
+ val take_type = HOLogic.natT --> lhsT ->> lhsT;
+ val take_bind = Binding.suffix_name "_take" tbind;
+ val (take_const, thy) =
+ Sign.declare_const ((take_bind, take_type), NoSyn) thy;
+ val take_eqn = Logic.mk_equals (take_const, take_rhs);
+ val (take_def_thm, thy) =
+ thy
+ |> Sign.add_path (Binding.name_of tbind)
+ |> yield_singleton
+ (PureThy.add_defs false o map Thm.no_attributes)
+ (Binding.name "take_def", take_eqn)
+ ||> Sign.parent_path;
+ in ((take_const, take_def_thm), thy) end;
+ val ((take_consts, take_defs), thy) = thy
+ |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns)
+ |>> ListPair.unzip;
+
+ (* prove chain_take lemmas *)
+ fun prove_chain_take (take_const, dname) thy =
+ let
+ val goal = mk_trp (mk_chain take_const);
+ val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
+ val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+ val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ add_qualified_thm "chain_take" (dname, chain_take_thm) thy
+ end;
+ val (chain_take_thms, thy) =
+ fold_map prove_chain_take (take_consts ~~ dnames) thy;
+
+ (* prove take_0 lemmas *)
+ fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy =
+ let
+ val lhs = take_const $ @{term "0::nat"};
+ val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
+ val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
+ val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+ val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ add_qualified_thm "take_0" (dname, take_0_thm) thy
+ end;
+ val (take_0_thms, thy) =
+ fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
+
+ (* prove take_Suc lemmas *)
+ val i = Free ("i", natT);
+ val take_is = map (fn t => t $ i) take_consts;
+ fun prove_take_Suc
+ (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
+ let
+ val lhs = take_const $ (@{term Suc} $ i);
+ val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
+ val body = copy_of_dtyp take_is (rhsT, dtyp);
+ val rhs = mk_cfcomp2 (rep_abs, body);
+ val goal = mk_eqs (lhs, rhs);
+ val simps = @{thms iterate_Suc fst_conv snd_conv}
+ val rules = take_defs @ simps;
+ val tac = simp_tac (beta_ss addsimps rules) 1;
+ val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy
+ end;
+ val (take_Suc_thms, thy) =
+ fold_map prove_take_Suc
+ (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy;
+
+ (* prove deflation theorems for take functions *)
+ val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
+ val deflation_take_thm =
+ let
+ val i = Free ("i", natT);
+ fun mk_goal take_const = mk_deflation (take_const $ i);
+ val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
+ val adm_rules =
+ @{thms adm_conj adm_subst [OF _ adm_deflation]
+ cont2cont_fst cont2cont_snd cont_id};
+ val bottom_rules =
+ take_0_thms @ @{thms deflation_UU simp_thms};
+ val deflation_rules =
+ @{thms conjI deflation_ID}
+ @ deflation_abs_rep_thms
+ @ DeflMapData.get thy;
+ in
+ Goal.prove_global thy [] [] goal (fn _ =>
+ EVERY
+ [rtac @{thm nat.induct} 1,
+ simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
+ asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
+ REPEAT (etac @{thm conjE} 1
+ ORELSE resolve_tac deflation_rules 1
+ ORELSE atac 1)])
+ end;
+ 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 (deflation_take_thms, thy) =
+ fold_map (add_qualified_thm "deflation_take")
+ (map (apsnd Drule.export_without_context)
+ (conjuncts dnames deflation_take_thm)) thy;
+
+ (* prove strictness of take functions *)
+ fun prove_take_strict (take_const, dname) thy =
+ let
+ val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
+ val tac = rtac @{thm deflation_strict} 1
+ THEN resolve_tac deflation_take_thms 1;
+ val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ add_qualified_thm "take_strict" (dname, take_strict_thm) thy
+ end;
+ val (take_strict_thms, thy) =
+ fold_map prove_take_strict (take_consts ~~ dnames) thy;
+
+ (* prove take/take rules *)
+ fun prove_take_take ((chain_take, deflation_take), dname) thy =
+ let
+ val take_take_thm =
+ @{thm deflation_chain_min} OF [chain_take, deflation_take];
+ in
+ add_qualified_thm "take_take" (dname, take_take_thm) thy
+ end;
+ val (take_take_thms, thy) =
+ fold_map prove_take_take
+ (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
+
+ val result =
+ {
+ take_consts = take_consts,
+ take_defs = take_defs,
+ chain_take_thms = chain_take_thms,
+ take_0_thms = take_0_thms,
+ take_Suc_thms = take_Suc_thms,
+ deflation_take_thms = deflation_take_thms
+ };
+
+ in
+ (result, thy)
+ end;
+
+(******************************************************************************)
+(******************************* main function ********************************)
+(******************************************************************************)
fun read_typ thy str sorts =
let
@@ -320,7 +529,7 @@
(prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
(doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
(thy: theory)
- : theory =
+ : iso_info list * theory =
let
val _ = Theory.requires thy "Representable" "domain isomorphisms";
@@ -345,7 +554,7 @@
val dom_eqns = map mk_dom_eqn doms;
(* check for valid type parameters *)
- val (tyvars, _, _, _, _)::_ = doms;
+ val (tyvars, _, _, _, _) = hd doms;
val new_doms = map (fn (tvs, tname, mx, _, _) =>
let val full_tname = Sign.full_name tmp_thy tname
in
@@ -362,7 +571,7 @@
(* declare deflation combinator constants *)
fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy =
let
- val defl_type = Library.foldr cfunT (map (K deflT) vs, deflT);
+ val defl_type = map (K deflT) vs -->> deflT;
val defl_bind = Binding.suffix_name "_defl" tbind;
in
Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
@@ -390,7 +599,7 @@
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 defl = list_ccomb (defl_const, reps);
val ((_, _, _, {REP, ...}), thy) =
Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy;
in
@@ -421,21 +630,12 @@
(* define rep/abs functions *)
fun mk_rep_abs ((tbind, morphs), (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_bind, abs_bind) = the_default (rep_bind, abs_bind) morphs;
- 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)];
+ val ((rep_const, rep_def), thy) =
+ define_const (rep_bind, coerce_const (lhsT ->> rhsT)) thy;
+ val ((abs_const, abs_def), thy) =
+ define_const (abs_bind, coerce_const (rhsT ->> lhsT)) thy;
in
(((rep_const, abs_const), (rep_def, abs_def)), thy)
end;
@@ -463,10 +663,27 @@
in
(((rep_iso_thm, abs_iso_thm), isodefl_thm), thy)
end;
- val ((iso_thms, isodefl_abs_rep_thms), thy) = thy
+ val ((iso_thms, isodefl_abs_rep_thms), thy) =
+ thy
|> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs)
|>> ListPair.unzip;
+ (* collect info about rep/abs *)
+ val iso_infos : iso_info list =
+ let
+ fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) =
+ {
+ repT = rhsT,
+ absT = lhsT,
+ rep_const = repC,
+ abs_const = absC,
+ rep_inverse = rep_iso,
+ abs_inverse = abs_iso
+ };
+ in
+ map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms)
+ end
+
(* declare map functions *)
fun declare_map_const (tbind, (lhsT, rhsT)) thy =
let
@@ -502,13 +719,14 @@
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_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT);
+ fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), 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)) =
+ fun mk_goal ((map_const, defl_const), (T, 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);
+ val (_, Ts) = dest_Type T;
+ val map_term = list_ccomb (map_const, map mk_f Ts);
+ val defl_term = list_ccomb (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);
@@ -554,8 +772,8 @@
(((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 lhs = list_ccomb (map_const, map mk_ID Ts);
+ val goal = mk_eqs (lhs, mk_ID lhsT);
val tac = EVERY
[rtac @{thm isodefl_REP_imp_ID} 1,
stac REP_thm 1,
@@ -573,121 +791,110 @@
(map_ID_binds ~~ map_ID_thms);
val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy;
- (* 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_arg = Free ("f", copy_arg_type);
- val copy_args =
- let fun mk_copy_args [] t = []
- | mk_copy_args (_::[]) t = [t]
- | mk_copy_args (_::xs) t =
- mk_fst t :: mk_copy_args xs (mk_snd t);
- in mk_copy_args doms copy_arg end;
- fun copy_of_dtyp (T, dt) =
- if Datatype_Aux.is_rec_type dt
- then copy_of_dtyp' (T, dt)
- else ID_const T
- and copy_of_dtyp' (T, Datatype_Aux.DtRec i) = nth copy_args i
- | copy_of_dtyp' (T, Datatype_Aux.DtTFree a) = ID_const T
- | copy_of_dtyp' (T as Type (_, Ts), Datatype_Aux.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 =
+ (* prove deflation theorems for map functions *)
+ val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
+ val deflation_map_thm =
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 = Datatype_Aux.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 copy_arg 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;
+ fun unprime a = Library.unprefix "'" a;
+ fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T);
+ fun mk_assm T = mk_trp (mk_deflation (mk_f T));
+ fun mk_goal (map_const, (lhsT, rhsT)) =
+ let
+ val (_, Ts) = dest_Type lhsT;
+ val map_term = list_ccomb (map_const, map mk_f Ts);
+ in mk_deflation map_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 ~~ dom_eqns);
+ val goal = mk_trp (foldr1 HOLogic.mk_conj goals);
+ val start_thms =
+ @{thm split_def} :: map_apply_thms;
+ val adm_rules =
+ @{thms adm_conj adm_subst [OF _ adm_deflation]
+ cont2cont_fst cont2cont_snd cont_id};
+ val bottom_rules =
+ @{thms fst_strict snd_strict deflation_UU simp_thms};
+ val deflation_rules =
+ @{thms conjI deflation_ID}
+ @ deflation_abs_rep_thms
+ @ DeflMapData.get thy;
+ in
+ Goal.prove_global thy [] assms goal (fn {prems, ...} =>
+ EVERY
+ [simp_tac (HOL_basic_ss addsimps start_thms) 1,
+ rtac @{thm 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 (deflation_rules @ prems) 1 ORELSE atac 1)])
+ end;
+ val deflation_map_binds = dom_binds |>
+ map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map");
+ val (deflation_map_thms, thy) = thy |>
+ (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
+ (conjuncts deflation_map_binds deflation_map_thm);
+ val thy = DeflMapData.map (fold Thm.add_thm deflation_map_thms) thy;
- (* define combined copy combinator *)
- val ((c_const, c_def_thms), thy) =
- if length doms = 1
- then ((hd copy_consts, []), thy)
- else
- let
- val c_type = copy_arg_type ->> copy_arg_type;
- val c_name = space_implode "_" (map Binding.name_of dom_binds);
- val c_bind = Binding.name (c_name ^ "_copy");
- val c_body =
- mk_tuple (map (mk_capply o rpair copy_arg) copy_consts);
- val c_rhs = big_lambda copy_arg c_body;
- val (c_const, thy) =
- Sign.declare_const ((c_bind, c_type), NoSyn) thy;
- val c_eqn = Logic.mk_equals (c_const, c_rhs);
- val (c_def_thms, thy) =
- thy
- |> Sign.add_path c_name
- |> (PureThy.add_defs false o map Thm.no_attributes)
- [(Binding.name "copy_def", c_eqn)]
- ||> Sign.parent_path;
- in ((c_const, c_def_thms), thy) end;
+ (* definitions and proofs related to take functions *)
+ val (take_info, thy) =
+ define_take_functions (dom_binds ~~ iso_infos) thy;
+ val {take_consts, take_defs, chain_take_thms, take_0_thms,
+ take_Suc_thms, deflation_take_thms} = take_info;
- (* fixed-point lemma for combined copy combinator *)
- val fix_copy_lemma =
+ (* least-upper-bound lemma for take functions *)
+ val lub_take_lemma =
let
- fun mk_map_ID (map_const, (Type (c, Ts), rhsT)) =
- Library.foldl mk_capply (map_const, map ID_const Ts);
+ val lhs = mk_tuple (map mk_lub take_consts);
+ fun mk_map_ID (map_const, (lhsT, rhsT)) =
+ list_ccomb (map_const, map mk_ID (snd (dest_Type lhsT)));
val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
- val goal = mk_eqs (mk_fix c_const, rhs);
- val rules =
- [@{thm pair_collapse}, @{thm split_def}]
- @ map_apply_thms
- @ c_def_thms @ copy_defs
- @ MapIdData.get thy;
- val tac = simp_tac (beta_ss addsimps rules) 1;
+ val goal = mk_trp (mk_eq (lhs, rhs));
+ val start_rules =
+ @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
+ @ @{thms pair_collapse split_def}
+ @ map_apply_thms @ MapIdData.get thy;
+ val rules0 =
+ @{thms iterate_0 Pair_strict} @ take_0_thms;
+ val rules1 =
+ @{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv}
+ @ take_Suc_thms;
+ val tac =
+ EVERY
+ [simp_tac (HOL_basic_ss addsimps start_rules) 1,
+ simp_tac (HOL_basic_ss addsimps @{thms fix_def2}) 1,
+ rtac @{thm lub_eq} 1,
+ rtac @{thm nat.induct} 1,
+ simp_tac (HOL_basic_ss addsimps rules0) 1,
+ asm_full_simp_tac (beta_ss addsimps rules1) 1];
in
Goal.prove_global thy [] [] goal (K tac)
end;
- (* prove reach lemmas *)
- val reach_thm_projs =
- let fun mk_projs (x::[]) t = [(x, t)]
- | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
- in mk_projs dom_binds (mk_fix c_const) end;
- fun prove_reach_thm (((bind, t), map_ID_thm), (lhsT, rhsT)) thy =
+ (* prove lub of take equals ID *)
+ fun prove_lub_take (((bind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
let
- val x = Free ("x", lhsT);
- val goal = mk_eqs (mk_capply (t, x), x);
- val rules =
- fix_copy_lemma :: map_ID_thm :: @{thms fst_conv snd_conv ID1};
- val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
- val reach_thm = Goal.prove_global thy [] [] goal (K tac);
+ val i = Free ("i", natT);
+ val goal = mk_eqs (mk_lub (lambda i (take_const $ i)), mk_ID lhsT);
+ val tac =
+ EVERY
+ [rtac @{thm trans} 1, rtac map_ID_thm 2,
+ cut_facts_tac [lub_take_lemma] 1,
+ REPEAT (etac @{thm Pair_inject} 1), atac 1];
+ val lub_take_thm = Goal.prove_global thy [] [] goal (K tac);
in
- thy
- |> Sign.add_path (Binding.name_of bind)
- |> yield_singleton (PureThy.add_thms o map Thm.no_attributes)
- (Binding.name "reach", reach_thm)
- ||> Sign.parent_path
+ add_qualified_thm "lub_take" (Binding.name_of bind, lub_take_thm) thy
end;
- val (reach_thms, thy) = thy |>
- fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns);
+ val (lub_take_thms, thy) =
+ fold_map prove_lub_take
+ (dom_binds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy;
in
- thy
+ (iso_infos, thy)
end;
val domain_isomorphism = gen_domain_isomorphism cert_typ;
-val domain_isomorphism_cmd = gen_domain_isomorphism read_typ;
+val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ;
(******************************************************************************)
(******************************** outer syntax ********************************)
--- a/src/HOLCF/Tools/Domain/domain_library.ML Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Tue Mar 02 17:36:40 2010 +0000
@@ -5,36 +5,6 @@
*)
-(* ----- general support ---------------------------------------------------- *)
-
-fun mapn f n [] = []
- | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
-
-fun foldr'' f (l,f2) =
- let fun itr [] = raise Fail "foldr''"
- | itr [a] = f2 a
- | itr (a::l) = f(a, itr l)
- in itr l end;
-
-fun map_cumulr f start xs =
- List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
- (y::ys,res2)) ([],start) xs;
-
-fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x;
-fun upd_first f (x,y,z) = (f x, y, z);
-fun upd_second f (x,y,z) = ( x, f y, z);
-fun upd_third f (x,y,z) = ( x, y, f z);
-
-fun atomize ctxt thm =
- let
- val r_inst = read_instantiate ctxt;
- fun at thm =
- case concl_of thm of
- _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
- | _ => [thm];
- in map zero_var_indexes (at thm) end;
-
(* infix syntax *)
infixr 5 -->;
@@ -44,8 +14,6 @@
infix 0 ==;
infix 1 ===;
infix 1 ~=;
-infix 1 <<;
-infix 1 ~<<;
infix 9 ` ;
infix 9 `% ;
@@ -56,19 +24,25 @@
signature DOMAIN_LIBRARY =
sig
+ val first : 'a * 'b * 'c -> 'a
+ val second : 'a * 'b * 'c -> 'b
+ val third : 'a * 'b * 'c -> 'c
+ val upd_second : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
+ val upd_third : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
+ val mapn : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+ val atomize : Proof.context -> thm -> thm list
+
val Imposs : string -> 'a;
val cpo_type : theory -> typ -> bool;
val pcpo_type : theory -> typ -> bool;
val string_of_typ : theory -> typ -> string;
(* Creating HOLCF types *)
- val mk_cfunT : typ * typ -> typ;
val ->> : typ * typ -> typ;
val mk_ssumT : typ * typ -> typ;
val mk_sprodT : typ * typ -> typ;
val mk_uT : typ -> typ;
val oneT : typ;
- val trT : typ;
val mk_maybeT : typ -> typ;
val mk_ctupleT : typ list -> typ;
val mk_TFree : string -> typ;
@@ -81,26 +55,17 @@
val `% : term * string -> term;
val /\ : string -> term -> term;
val UU : term;
- val TT : term;
- val FF : term;
val ID : term;
val oo : term * term -> term;
- val mk_up : term -> term;
- val mk_sinl : term -> term;
- val mk_sinr : term -> term;
- val mk_stuple : term list -> term;
val mk_ctuple : term list -> term;
val mk_fix : term -> term;
val mk_iterate : term * term * term -> term;
val mk_fail : term;
val mk_return : term -> term;
val list_ccomb : term * term list -> term;
- (*
- val con_app : string -> ('a * 'b * string) list -> term;
- *)
val con_app2 : string -> ('a -> term) -> 'a list -> term;
+ val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a
val proj : term -> 'a list -> int -> term;
- val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a;
val mk_ctuple_pat : term list -> term;
val mk_branch : term -> term;
@@ -111,15 +76,11 @@
val mk_lam : string * term -> term;
val mk_all : string * term -> term;
val mk_ex : string * term -> term;
- val mk_constrain : typ * term -> term;
val mk_constrainall : string * typ * term -> term;
val === : term * term -> term;
- val << : term * term -> term;
- val ~<< : term * term -> term;
val strict : term -> term;
val defined : term -> term;
val mk_adm : term -> term;
- val mk_compact : term -> term;
val lift : ('a -> term) -> 'a list * term -> term;
val lift_defined : ('a -> term) -> 'a list * term -> term;
@@ -162,12 +123,38 @@
val dis_name : string -> string;
val mat_name : string -> string;
val pat_name : string -> string;
- val mk_var_names : string list -> string list;
end;
structure Domain_Library :> DOMAIN_LIBRARY =
struct
+fun first (x,_,_) = x;
+fun second (_,x,_) = x;
+fun third (_,_,x) = x;
+
+fun upd_first f (x,y,z) = (f x, y, z);
+fun upd_second f (x,y,z) = ( x, f y, z);
+fun upd_third f (x,y,z) = ( x, y, f z);
+
+fun mapn f n [] = []
+ | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
+
+fun foldr'' f (l,f2) =
+ let fun itr [] = raise Fail "foldr''"
+ | itr [a] = f2 a
+ | itr (a::l) = f(a, itr l)
+ in itr l end;
+
+fun atomize ctxt thm =
+ let
+ val r_inst = read_instantiate ctxt;
+ fun at thm =
+ case concl_of thm of
+ _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
+ | _ => [thm];
+ in map zero_var_indexes (at thm) end;
+
exception Impossible of string;
fun Imposs msg = raise Impossible ("Domain:"^msg);
@@ -191,22 +178,6 @@
fun pat_name con = (extern_name con) ^ "_pat";
fun pat_name_ con = (strip_esc con) ^ "_pat";
-(* make distinct names out of the type list,
- forbidding "o","n..","x..","f..","P.." as names *)
-(* a number string is added if necessary *)
-fun mk_var_names ids : string list =
- let
- fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
- fun index_vnames(vn::vns,occupied) =
- (case AList.lookup (op =) occupied vn of
- NONE => if vn mem vns
- then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied)
- else vn :: index_vnames(vns, occupied)
- | SOME(i) => (vn^(string_of_int (i+1)))
- :: index_vnames(vns,(vn,i+1)::occupied))
- | index_vnames([],occupied) = [];
- in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
-
fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
@@ -270,7 +241,6 @@
fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
val oneT = @{typ one};
-val trT = @{typ tr};
val op ->> = mk_cfunT;
@@ -290,7 +260,6 @@
fun mk_lam (x,T) = Abs(x,dummyT,T);
fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-val mk_constrain = uncurry TypeInfer.constrain;
fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
end
@@ -301,29 +270,18 @@
infix 0 ==; fun S == T = %%:"==" $ S $ T;
infix 1 ===; fun S === T = %%:"op =" $ S $ T;
infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
-infix 1 <<; fun S << T = %%: @{const_name Porder.below} $ S $ T;
-infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T);
infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
infix 9 `% ; fun f`% s = f` %: s;
infix 9 `%%; fun f`%%s = f` %%:s;
fun mk_adm t = %%: @{const_name adm} $ t;
-fun mk_compact t = %%: @{const_name compact} $ t;
val ID = %%: @{const_name ID};
fun mk_strictify t = %%: @{const_name strictify}`t;
-(*val csplitN = "Cprod.csplit";*)
-(*val sfstN = "Sprod.sfst";*)
-(*val ssndN = "Sprod.ssnd";*)
fun mk_ssplit t = %%: @{const_name ssplit}`t;
-fun mk_sinl t = %%: @{const_name sinl}`t;
-fun mk_sinr t = %%: @{const_name sinr}`t;
fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y;
-fun mk_up t = %%: @{const_name up}`t;
fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u;
val ONE = @{term ONE};
-val TT = @{term TT};
-val FF = @{term FF};
fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z;
fun mk_fix t = %%: @{const_name fix}`t;
fun mk_return t = %%: @{const_name Fixrec.return}`t;
@@ -354,8 +312,6 @@
fun spair (t,u) = %%: @{const_name spair}`t`u;
fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
| mk_ctuple ts = foldr1 cpair ts;
-fun mk_stuple [] = ONE
- | mk_stuple ts = foldr1 spair ts;
fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *)
| mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 17:36:40 2010 +0000
@@ -9,14 +9,12 @@
val calc_syntax:
theory ->
bool ->
- typ ->
(string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list ->
- (binding * typ * mixfix) list * ast Syntax.trrule list
+ (binding * typ * mixfix) list
val add_syntax:
bool ->
- string ->
((string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list) list ->
theory -> theory
@@ -31,19 +29,15 @@
fun calc_syntax thy
(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 =
+ : (binding * typ * mixfix) list =
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');
@@ -51,160 +45,28 @@
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;
-
- 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));
- 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 --------------------------------------------------- *)
-
- fun syntax b = Syntax.mark_const (Sign.full_bname thy b);
+ val optional_consts =
+ if definitional then [] else [const_rep, const_abs];
- local open Syntax in
- local
- fun c_ast authentic con = Constant ((authentic ? syntax) (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 @{const_syntax Rep_CFun};
- fun con1 authentic n (con,args,mx) =
- Library.foldl capp (c_ast authentic con, argvars n args);
- fun case1 authentic n (con,args,mx) =
- app "_case1" (con1 authentic 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 @{const_syntax 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
- fun case_trans authentic =
- ParsePrintRule
- (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn (case1 authentic) 1 cons')),
- capp (Library.foldl capp
- (Constant (syntax (dnam ^ "_when")), mapn arg1 1 cons'), Variable "x"));
-
- fun one_abscon_trans authentic n (con,mx,args) =
- ParsePrintRule
- (cabs (con1 authentic n (con,mx,args), expvar n),
- Library.foldl capp (Constant (syntax (dnam ^ "_when")), mapn (when1 n) 1 cons'));
- fun abscon_trans authentic = mapn (one_abscon_trans authentic) 1 cons';
-
- fun one_case_trans authentic (con,args,mx) =
- let
- val cname = c_ast authentic con;
- val pname = Constant (syntax (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 false) cons' @ maps (one_case_trans true) cons';
- end;
- end;
- val optional_consts =
- if definitional then [] else [const_rep, const_abs, const_copy];
-
- in (optional_consts @ [const_when] @
- consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
- [const_take, const_finite],
- (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans)))
+ in (optional_consts @ [const_finite])
end; (* let *)
(* ----- putting all the syntax stuff together ------------------------------ *)
fun add_syntax
(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 thy'' definitional funprod) eqs';
+ val ctt : (binding * typ * mixfix) list list =
+ map (calc_syntax thy'' definitional) eqs';
in thy''
- |> Cont_Consts.add_consts
- (maps fst ctt @
- (if length eqs'>1 andalso not definitional
- then [const_copy] else []) @
- [const_bisim])
- |> Sign.add_trrules_i (maps snd ctt)
+ |> Cont_Consts.add_consts (flat ctt)
end; (* let *)
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 17:36:40 2010 +0000
@@ -9,7 +9,11 @@
signature DOMAIN_THEOREMS =
sig
- val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
+ val theorems:
+ Domain_Library.eq * Domain_Library.eq list
+ -> typ * (binding * (bool * binding option * typ) list * mixfix) list
+ -> theory -> thm list * theory;
+
val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
val quiet_mode: bool Unsynchronized.ref;
val trace_domain: bool Unsynchronized.ref;
@@ -28,20 +32,11 @@
val adm_all = @{thm adm_all};
val adm_conj = @{thm adm_conj};
val adm_subst = @{thm adm_subst};
-val antisym_less_inverse = @{thm below_antisym_inverse};
-val beta_cfun = @{thm beta_cfun};
-val cfun_arg_cong = @{thm cfun_arg_cong};
val ch2ch_fst = @{thm ch2ch_fst};
val ch2ch_snd = @{thm ch2ch_snd};
val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR};
val chain_iterate = @{thm chain_iterate};
-val compact_ONE = @{thm compact_ONE};
-val compact_sinl = @{thm compact_sinl};
-val compact_sinr = @{thm compact_sinr};
-val compact_spair = @{thm compact_spair};
-val compact_up = @{thm compact_up};
-val contlub_cfun_arg = @{thm contlub_cfun_arg};
val contlub_cfun_fun = @{thm contlub_cfun_fun};
val contlub_fst = @{thm contlub_fst};
val contlub_snd = @{thm contlub_snd};
@@ -52,35 +47,10 @@
val cont2cont_snd = @{thm cont2cont_snd};
val cont2cont_Rep_CFun = @{thm cont2cont_Rep_CFun};
val fix_def2 = @{thm fix_def2};
-val injection_eq = @{thm injection_eq};
-val injection_less = @{thm injection_below};
val lub_equal = @{thm lub_equal};
-val monofun_cfun_arg = @{thm monofun_cfun_arg};
val retraction_strict = @{thm retraction_strict};
-val spair_eq = @{thm spair_eq};
-val spair_less = @{thm spair_below};
-val sscase1 = @{thm sscase1};
-val ssplit1 = @{thm ssplit1};
-val strictify1 = @{thm strictify1};
val wfix_ind = @{thm wfix_ind};
-
-val iso_intro = @{thm iso.intro};
-val iso_abs_iso = @{thm iso.abs_iso};
-val iso_rep_iso = @{thm iso.rep_iso};
-val iso_abs_strict = @{thm iso.abs_strict};
-val iso_rep_strict = @{thm iso.rep_strict};
-val iso_abs_defin' = @{thm iso.abs_defin'};
-val iso_rep_defin' = @{thm iso.rep_defin'};
-val iso_abs_defined = @{thm iso.abs_defined};
-val iso_rep_defined = @{thm iso.rep_defined};
-val iso_compact_abs = @{thm iso.compact_abs};
-val iso_compact_rep = @{thm iso.compact_rep};
-val iso_iso_swap = @{thm iso.iso_swap};
-
-val exh_start = @{thm exh_start};
-val ex_defined_iffs = @{thms ex_defined_iffs};
-val exh_casedist0 = @{thm exh_casedist0};
-val exh_casedists = @{thms exh_casedists};
+val iso_intro = @{thm iso.intro};
open Domain_Library;
infixr 0 ===>;
@@ -118,6 +88,9 @@
else cut_facts_tac prems 1 :: tacsf context;
in pg'' thy defs t tacs end;
+(* FIXME!!!!!!!!! *)
+(* We should NEVER re-parse variable names as strings! *)
+(* The names can conflict with existing constants or other syntax! *)
fun case_UU_tac ctxt rews i v =
InductTacs.case_tac ctxt (v^"=UU") i THEN
asm_simp_tac (HOLCF_ss addsimps rews) i;
@@ -130,13 +103,13 @@
val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
-val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)}
-
-fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
+fun theorems
+ (((dname, _), cons) : eq, eqs : eq list)
+ (dom_eqn : typ * (binding * (bool * binding option * typ) list * mixfix) list)
+ (thy : theory) =
let
val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
-val pg = pg' thy;
val map_tab = Domain_Isomorphism.get_map_tab thy;
@@ -147,515 +120,97 @@
in
val ax_abs_iso = ga "abs_iso" dname;
val ax_rep_iso = ga "rep_iso" dname;
- val ax_when_def = ga "when_def" dname;
- fun get_def mk_name (con, _, _) = ga (mk_name con^"_def") dname;
- val axs_con_def = map (get_def extern_name) cons;
- val axs_dis_def = map (get_def dis_name) cons;
- val axs_mat_def = map (get_def mat_name) cons;
- val axs_pat_def = map (get_def pat_name) cons;
- val axs_sel_def =
- let
- fun def_of_sel sel = ga (sel^"_def") dname;
- fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
- fun defs_of_con (_, _, args) = map_filter def_of_arg args;
- in
- maps defs_of_con cons
- end;
- val ax_copy_def = ga "copy_def" dname;
+ val ax_take_0 = ga "take_0" dname;
+ val ax_take_Suc = ga "take_Suc" dname;
+ val ax_take_strict = ga "take_strict" dname;
end; (* local *)
+(* ----- define constructors ------------------------------------------------ *)
+
+val lhsT = fst dom_eqn;
+
+val rhsT =
+ let
+ fun mk_arg_typ (lazy, sel, 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);
+ in
+ mk_eq_typ dom_eqn
+ end;
+
+val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
+
+val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
+
+val iso_info : Domain_Isomorphism.iso_info =
+ {
+ absT = lhsT,
+ repT = rhsT,
+ abs_const = abs_const,
+ rep_const = rep_const,
+ abs_inverse = ax_abs_iso,
+ rep_inverse = ax_rep_iso
+ };
+
+val (result, thy) =
+ Domain_Constructors.add_domain_constructors
+ (Long_Name.base_name dname) (snd dom_eqn) iso_info thy;
+
+val con_appls = #con_betas result;
+val {exhaust, casedist, ...} = result;
+val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
+val {sel_rews, ...} = result;
+val when_rews = #cases result;
+val when_strict = hd when_rews;
+val dis_rews = #dis_rews result;
+val mat_rews = #match_rews result;
+val pat_rews = #pat_rews result;
+
(* ----- theorems concerning the isomorphism -------------------------------- *)
-val dc_abs = %%:(dname^"_abs");
-val dc_rep = %%:(dname^"_rep");
+val pg = pg' thy;
+
val dc_copy = %%:(dname^"_copy");
-val x_name = "x";
-val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
-val abs_defin' = iso_locale RS iso_abs_defin';
-val rep_defin' = iso_locale RS iso_rep_defin';
val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
-(* ----- generating beta reduction rules from definitions-------------------- *)
-
-val _ = trace " Proving beta reduction rules...";
-
-local
- fun arglist (Const _ $ Abs (s, _, t)) =
- let
- val (vars,body) = arglist t;
- in (s :: vars, body) end
- | arglist t = ([], t);
- fun bind_fun vars t = Library.foldr mk_All (vars, t);
- fun bound_vars 0 = []
- | bound_vars i = Bound (i-1) :: bound_vars (i - 1);
-in
- fun appl_of_def def =
- let
- val (_ $ con $ lam) = concl_of def;
- val (vars, rhs) = arglist lam;
- val lhs = list_ccomb (con, bound_vars (length vars));
- val appl = bind_fun vars (lhs == rhs);
- val cs = ContProc.cont_thms lam;
- val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
- in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
-end;
-
-val _ = trace "Proving when_appl...";
-val when_appl = appl_of_def ax_when_def;
-val _ = trace "Proving con_appls...";
-val con_appls = map appl_of_def axs_con_def;
-
-local
- fun arg2typ n arg =
- let val t = TVar (("'a", n), pcpoS)
- in (n + 1, if is_lazy arg then mk_uT t else t) end;
-
- fun args2typ n [] = (n, oneT)
- | args2typ n [arg] = arg2typ n arg
- | args2typ n (arg::args) =
- let
- val (n1, t1) = arg2typ n arg;
- val (n2, t2) = args2typ n1 args
- in (n2, mk_sprodT (t1, t2)) end;
-
- fun cons2typ n [] = (n,oneT)
- | cons2typ n [con] = args2typ n (third con)
- | cons2typ n (con::cons) =
- let
- val (n1, t1) = args2typ n (third con);
- val (n2, t2) = cons2typ n1 cons
- in (n2, mk_ssumT (t1, t2)) end;
-in
- fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
-end;
-
-local
- val iso_swap = iso_locale RS iso_iso_swap;
- fun one_con (con, _, args) =
- let
- val vns = map vname args;
- val eqn = %:x_name === con_app2 con %: vns;
- val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
- in Library.foldr mk_ex (vns, conj) end;
-
- val conj_assoc = @{thm conj_assoc};
- val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
- val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
- val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
- val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
-
- (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
- val tacs = [
- rtac disjE 1,
- etac (rep_defin' RS disjI1) 2,
- etac disjI2 2,
- rewrite_goals_tac [mk_meta_eq iso_swap],
- rtac thm3 1];
-in
- val _ = trace " Proving exhaust...";
- val exhaust = pg con_appls (mk_trp exh) (K tacs);
- val _ = trace " Proving casedist...";
- val casedist =
- Drule.export_without_context (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
-end;
-
-local
- fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
- fun bound_fun i _ = Bound (length cons - i);
- val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
-in
- val _ = trace " Proving when_strict...";
- val when_strict =
- let
- val axs = [when_appl, mk_meta_eq rep_strict];
- val goal = bind_fun (mk_trp (strict when_app));
- val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
- in pg axs goal (K tacs) end;
-
- val _ = trace " Proving when_apps...";
- val when_apps =
- let
- fun one_when n (con, _, args) =
- let
- val axs = when_appl :: con_appls;
- val goal = bind_fun (lift_defined %: (nonlazy args,
- mk_trp (when_app`(con_app con args) ===
- list_ccomb (bound_fun n 0, map %# args))));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
- in pg axs goal (K tacs) end;
- in mapn one_when 1 cons end;
-end;
-val when_rews = when_strict :: when_apps;
-
-(* ----- theorems concerning the constructors, discriminators and selectors - *)
-
-local
- fun dis_strict (con, _, _) =
- let
- val goal = mk_trp (strict (%%:(dis_name con)));
- in pg axs_dis_def goal (K [rtac when_strict 1]) end;
-
- fun dis_app c (con, _, args) =
- let
- val lhs = %%:(dis_name c) ` con_app con args;
- val rhs = if con = c then TT else FF;
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_dis_def goal (K tacs) end;
-
- val _ = trace " Proving dis_apps...";
- val dis_apps = maps (fn (c,_,_) => map (dis_app c) cons) cons;
-
- fun dis_defin (con, _, args) =
- let
- val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
- val tacs =
- [rtac casedist 1,
- contr_tac 1,
- DETERM_UNTIL_SOLVED (CHANGED
- (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
- in pg [] goal (K tacs) end;
-
- val _ = trace " Proving dis_stricts...";
- val dis_stricts = map dis_strict cons;
- val _ = trace " Proving dis_defins...";
- val dis_defins = map dis_defin cons;
-in
- val dis_rews = dis_stricts @ dis_defins @ dis_apps;
-end;
-
-local
- fun mat_strict (con, _, _) =
- let
- val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
- val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1];
- in pg axs_mat_def goal (K tacs) end;
-
- val _ = trace " Proving mat_stricts...";
- val mat_stricts = map mat_strict cons;
-
- fun one_mat c (con, _, args) =
- let
- val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs";
- val rhs =
- if con = c
- then list_ccomb (%:"rhs", map %# args)
- else mk_fail;
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_mat_def goal (K tacs) end;
-
- val _ = trace " Proving mat_apps...";
- val mat_apps =
- maps (fn (c,_,_) => map (one_mat c) cons) cons;
-in
- val mat_rews = mat_stricts @ mat_apps;
-end;
-
-local
- fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
-
- fun pat_lhs (con,_,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
-
- fun pat_rhs (con,_,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
- | pat_rhs (con,_,args) =
- (mk_branch (mk_ctuple_pat (ps args)))
- `(%:"rhs")`(mk_ctuple (map %# args));
-
- fun pat_strict c =
- let
- val axs = @{thm branch_def} :: axs_pat_def;
- val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
- val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
- in pg axs goal (K tacs) end;
-
- fun pat_app c (con, _, args) =
- let
- val axs = @{thm branch_def} :: axs_pat_def;
- val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
- val rhs = if con = first c then pat_rhs c else mk_fail;
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs goal (K tacs) end;
-
- val _ = trace " Proving pat_stricts...";
- val pat_stricts = map pat_strict cons;
- val _ = trace " Proving pat_apps...";
- val pat_apps = maps (fn c => map (pat_app c) cons) cons;
-in
- val pat_rews = pat_stricts @ pat_apps;
-end;
-
-local
- fun con_strict (con, _, args) =
- let
- val rules = abs_strict :: @{thms con_strict_rules};
- fun one_strict vn =
- let
- fun f arg = if vname arg = vn then UU else %# arg;
- val goal = mk_trp (con_app2 con f args === UU);
- val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
- in pg con_appls goal (K tacs) end;
- in map one_strict (nonlazy args) end;
-
- fun con_defin (con, _, args) =
- let
- fun iff_disj (t, []) = HOLogic.mk_not t
- | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
- val lhs = con_app con args === UU;
- val rhss = map (fn x => %:x === UU) (nonlazy args);
- val goal = mk_trp (iff_disj (lhs, rhss));
- val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
- val rules = rule1 :: @{thms con_defined_iff_rules};
- val tacs = [simp_tac (HOL_ss addsimps rules) 1];
- in pg con_appls goal (K tacs) end;
-in
- val _ = trace " Proving con_stricts...";
- val con_stricts = maps con_strict cons;
- val _ = trace " Proving con_defins...";
- val con_defins = map con_defin cons;
- val con_rews = con_stricts @ con_defins;
-end;
-
-local
- val rules =
- [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
- fun con_compact (con, _, args) =
- let
- val concl = mk_trp (mk_compact (con_app con args));
- val goal = lift (fn x => mk_compact (%#x)) (args, concl);
- val tacs = [
- rtac (iso_locale RS iso_compact_abs) 1,
- REPEAT (resolve_tac rules 1 ORELSE atac 1)];
- in pg con_appls goal (K tacs) end;
-in
- val _ = trace " Proving con_compacts...";
- val con_compacts = map con_compact cons;
-end;
-
-local
- fun one_sel sel =
- pg axs_sel_def (mk_trp (strict (%%:sel)))
- (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
-
- fun sel_strict (_, _, args) =
- map_filter (Option.map one_sel o sel_of) args;
-in
- val _ = trace " Proving sel_stricts...";
- val sel_stricts = maps sel_strict cons;
-end;
-
-local
- fun sel_app_same c n sel (con, args) =
- let
- val nlas = nonlazy args;
- val vns = map vname args;
- val vnn = List.nth (vns, n);
- val nlas' = filter (fn v => v <> vnn) nlas;
- val lhs = (%%:sel)`(con_app con args);
- val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
- fun tacs1 ctxt =
- if vnn mem nlas
- then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
- else [];
- val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
-
- fun sel_app_diff c n sel (con, args) =
- let
- val nlas = nonlazy args;
- val goal = mk_trp (%%:sel ` con_app con args === UU);
- fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
- val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
-
- fun sel_app c n sel (con, _, args) =
- if con = c
- then sel_app_same c n sel (con, args)
- else sel_app_diff c n sel (con, args);
-
- fun one_sel c n sel = map (sel_app c n sel) cons;
- fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
- fun one_con (c, _, args) =
- flat (map_filter I (mapn (one_sel' c) 0 args));
-in
- val _ = trace " Proving sel_apps...";
- val sel_apps = maps one_con cons;
-end;
-
-local
- fun sel_defin sel =
- let
- val goal = defined (%:x_name) ==> defined (%%:sel`%x_name);
- val tacs = [
- rtac casedist 1,
- contr_tac 1,
- DETERM_UNTIL_SOLVED (CHANGED
- (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
- in pg [] goal (K tacs) end;
-in
- val _ = trace " Proving sel_defins...";
- val sel_defins =
- if length cons = 1
- then map_filter (fn arg => Option.map sel_defin (sel_of arg))
- (filter_out is_lazy (third (hd cons)))
- else [];
-end;
-
-val sel_rews = sel_stricts @ sel_defins @ sel_apps;
-
-val _ = trace " Proving dist_les...";
-val dist_les =
- let
- fun dist (con1, args1) (con2, args2) =
- let
- fun iff_disj (t, []) = HOLogic.mk_not t
- | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
- val lhs = con_app con1 args1 << con_app con2 args2;
- val rhss = map (fn x => %:x === UU) (nonlazy args1);
- val goal = mk_trp (iff_disj (lhs, rhss));
- val rule1 = iso_locale RS @{thm iso.abs_below};
- val rules = rule1 :: @{thms con_below_iff_rules};
- val tacs = [simp_tac (HOL_ss addsimps rules) 1];
- in pg con_appls goal (K tacs) end;
-
- fun distinct (con1, _, args1) (con2, _, args2) =
- let
- val arg1 = (con1, args1);
- val arg2 =
- (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
- (args2, Name.variant_list (map vname args1) (map vname args2)));
- in [dist arg1 arg2, dist arg2 arg1] end;
- fun distincts [] = []
- | distincts (c::cs) = maps (distinct c) cs @ distincts cs;
- in distincts cons end;
-
-val _ = trace " Proving dist_eqs...";
-val dist_eqs =
- let
- fun dist (con1, args1) (con2, args2) =
- let
- fun iff_disj (t, [], us) = HOLogic.mk_not t
- | iff_disj (t, ts, []) = HOLogic.mk_not t
- | iff_disj (t, ts, us) =
- let
- val disj1 = foldr1 HOLogic.mk_disj ts;
- val disj2 = foldr1 HOLogic.mk_disj us;
- in t === HOLogic.mk_conj (disj1, disj2) end;
- val lhs = con_app con1 args1 === con_app con2 args2;
- val rhss1 = map (fn x => %:x === UU) (nonlazy args1);
- val rhss2 = map (fn x => %:x === UU) (nonlazy args2);
- val goal = mk_trp (iff_disj (lhs, rhss1, rhss2));
- val rule1 = iso_locale RS @{thm iso.abs_eq};
- val rules = rule1 :: @{thms con_eq_iff_rules};
- val tacs = [simp_tac (HOL_ss addsimps rules) 1];
- in pg con_appls goal (K tacs) end;
-
- fun distinct (con1, _, args1) (con2, _, args2) =
- let
- val arg1 = (con1, args1);
- val arg2 =
- (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
- (args2, Name.variant_list (map vname args1) (map vname args2)));
- in [dist arg1 arg2, dist arg2 arg1] end;
- fun distincts [] = []
- | distincts (c::cs) = maps (distinct c) cs @ distincts cs;
- in distincts cons end;
-
-local
- fun pgterm rel con args =
- let
- fun append s = upd_vname (fn v => v^s);
- val (largs, rargs) = (args, map (append "'") args);
- val concl =
- foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs));
- val prem = rel (con_app con largs, con_app con rargs);
- val sargs = case largs of [_] => [] | _ => nonlazy args;
- val prop = lift_defined %: (sargs, mk_trp (prem === concl));
- in pg con_appls prop end;
- val cons' = filter (fn (_, _, args) => args<>[]) cons;
-in
- val _ = trace " Proving inverts...";
- val inverts =
- let
- val abs_less = ax_abs_iso RS (allI RS injection_less);
- val tacs =
- [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
- in map (fn (con, _, args) => pgterm (op <<) con args (K tacs)) cons' end;
-
- val _ = trace " Proving injects...";
- val injects =
- let
- val abs_eq = ax_abs_iso RS (allI RS injection_eq);
- val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
- in map (fn (con, _, args) => pgterm (op ===) con args (K tacs)) cons' end;
-end;
-
(* ----- theorems concerning one induction step ----------------------------- *)
-val copy_strict =
- let
- val _ = trace " Proving copy_strict...";
- val goal = mk_trp (strict (dc_copy `% "f"));
- val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts};
- val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
- in
- SOME (pg [ax_copy_def] goal (K tacs))
- handle
- THM (s, _, _) => (trace s; NONE)
- | ERROR s => (trace s; NONE)
- end;
+local
+ fun dc_take dn = %%:(dn^"_take");
+ val dnames = map (fst o fst) eqs;
+ fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
+ val axs_take_strict = map get_take_strict dnames;
-local
- fun copy_app (con, _, args) =
+ fun one_take_app (con, _, args) =
let
- val lhs = dc_copy`%"f"`(con_app con args);
+ fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
fun one_rhs arg =
if Datatype_Aux.is_rec_type (dtyp_of arg)
then Domain_Axioms.copy_of_dtyp map_tab
- (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
+ mk_take (dtyp_of arg) ` (%# arg)
else (%# arg);
+ val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
val rhs = con_app2 con one_rhs args;
fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
- val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
- val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
- fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
- val rules = [ax_abs_iso] @ @{thms domain_map_simps};
- val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
- in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
+ val goal = mk_trp (lhs === rhs);
+ val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
+ val rules2 = @{thms take_con_rules ID1} @ axs_take_strict;
+ val tacs =
+ [simp_tac (HOL_basic_ss addsimps rules) 1,
+ asm_simp_tac (HOL_basic_ss addsimps rules2) 1];
+ in pg con_appls goal (K tacs) end;
+ val take_apps = map (Drule.export_without_context o one_take_app) cons;
in
- val _ = trace " Proving copy_apps...";
- val copy_apps = map copy_app cons;
+ val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
end;
-local
- fun one_strict (con, _, args) =
- let
- val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
- val rews = the_list copy_strict @ copy_apps @ con_rews;
- fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
- [asm_simp_tac (HOLCF_ss addsimps rews) 1];
- in
- SOME (pg [] goal tacs)
- handle
- THM (s, _, _) => (trace s; NONE)
- | ERROR s => (trace s; NONE)
- end;
-
- fun has_nonlazy_rec (_, _, args) = exists is_nonlazy_rec args;
-in
- val _ = trace " Proving copy_stricts...";
- val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons);
-end;
-
-val copy_rews = the_list copy_strict @ copy_apps @ copy_stricts;
-
in
thy
|> Sign.add_path (Long_Name.base_name dname)
@@ -674,17 +229,16 @@
((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]),
((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
((Binding.name "injects" , injects ), [Simplifier.simp_add]),
- ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]),
+ ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]),
((Binding.name "match_rews", mat_rews ),
[Simplifier.simp_add, Fixrec.fixrec_simp_add])]
|> Sign.parent_path
|> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
- pat_rews @ dist_les @ dist_eqs @ copy_rews)
+ pat_rews @ dist_les @ dist_eqs)
end; (* let *)
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;
@@ -692,6 +246,81 @@
val comp_dname = Sign.full_bname thy comp_dnam;
val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
+
+(* ----- define bisimulation predicate -------------------------------------- *)
+
+local
+ open HOLCF_Library
+ val dtypes = map (Type o fst) eqs;
+ val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes);
+ val bisim_bind = Binding.name (comp_dnam ^ "_bisim");
+ val bisim_type = relprod --> boolT;
+in
+ val (bisim_const, thy) =
+ Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy;
+end;
+
+local
+
+ fun legacy_infer_term thy t =
+ singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
+ fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+ fun infer_props thy = map (apsnd (legacy_infer_prop thy));
+ fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
+ fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
+
+ val comp_dname = Sign.full_bname thy comp_dnam;
+ val dnames = map (fst o fst) eqs;
+ val x_name = idx_name dnames "x";
+
+ 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;
+ val allargs = nonrec_args @ rec_args
+ @ map (upd_vname (fn s=> s^"'")) rec_args;
+ val allvns = map vname allargs;
+ fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
+ val vns1 = map (vname_arg "" ) args;
+ val vns2 = map (vname_arg "'") args;
+ val allargs_cnt = length nonrec_args + 2*recs_cnt;
+ val rec_idxs = (recs_cnt-1) downto 0;
+ val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
+ (allargs~~((allargs_cnt-1) downto 0)));
+ 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
+ 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_eqn =
+ %%:(comp_dname^"_bisim") ==
+ mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs));
+
+in
+ val ([ax_bisim_def], thy) =
+ thy
+ |> Sign.add_path comp_dnam
+ |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)]
+ ||> Sign.parent_path;
+end; (* local *)
+
val pg = pg' thy;
(* ----- getting the composite axiom and definitions ------------------------ *)
@@ -699,11 +328,10 @@
local
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
in
- val axs_reach = map (ga "reach" ) dnames;
val axs_take_def = map (ga "take_def" ) dnames;
+ val axs_chain_take = map (ga "chain_take") dnames;
+ val axs_lub_take = map (ga "lub_take" ) dnames;
val axs_finite_def = map (ga "finite_def") dnames;
- val ax_copy2_def = ga "copy_def" comp_dnam;
- val ax_bisim_def = ga "bisim_def" comp_dnam;
end;
local
@@ -712,7 +340,6 @@
in
val cases = map (gt "casedist" ) dnames;
val con_rews = maps (gts "con_rews" ) dnames;
- val copy_rews = maps (gts "copy_rews") dnames;
end;
fun dc_take dn = %%:(dn^"_take");
@@ -722,64 +349,20 @@
(* ----- theorems concerning finite approximation and finite induction ------ *)
-local
- val iterate_Cprod_ss = global_simpset_of @{theory Fix};
- val copy_con_rews = copy_rews @ con_rews;
- val copy_take_defs =
- (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
- val _ = trace " Proving take_stricts...";
- fun one_take_strict ((dn, args), _) =
- let
- val goal = mk_trp (strict (dc_take dn $ %:"n"));
- val rules = [
- @{thm monofun_fst [THEN monofunE]},
- @{thm monofun_snd [THEN monofunE]}];
- val tacs = [
- rtac @{thm UU_I} 1,
- rtac @{thm below_eq_trans} 1,
- resolve_tac axs_reach 2,
- rtac @{thm monofun_cfun_fun} 1,
- REPEAT (resolve_tac rules 1),
- rtac @{thm iterate_below_fix} 1];
- in pg axs_take_def goal (K tacs) end;
- val take_stricts = map one_take_strict eqs;
- fun take_0 n dn =
- let
- val goal = mk_trp ((dc_take dn $ @{term "0::nat"}) `% x_name n === UU);
- in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
- val take_0s = mapn take_0 1 dnames;
- val _ = trace " Proving take_apps...";
- fun one_take_app dn (con, _, args) =
- let
- fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
- fun one_rhs arg =
- if Datatype_Aux.is_rec_type (dtyp_of 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;
- fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
- fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
- fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
- val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1];
- in pg copy_take_defs goal (K tacs) end;
- fun one_take_apps ((dn, _), cons) = map (one_take_app dn) cons;
- val take_apps = maps one_take_apps eqs;
-in
- val take_rews = map Drule.export_without_context
- (take_stricts @ take_0s @ take_apps);
-end; (* local *)
+val take_rews =
+ maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
local
fun one_con p (con, _, args) =
let
+ val P_names = map P_name (1 upto (length dnames));
+ val vns = Name.variant_list P_names (map vname args);
+ val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
val t2 = lift ind_hyp (filter is_rec args, t1);
- val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
- in Library.foldr mk_All (map vname args, t3) end;
+ val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2);
+ in Library.foldr mk_All (vns, t3) end;
fun one_eq ((p, cons), concl) =
mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
@@ -787,7 +370,7 @@
fun ind_term concf = Library.foldr one_eq
(mapn (fn n => fn x => (P_name n, x)) 1 conss,
mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
- val take_ss = HOL_ss addsimps take_rews;
+ val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
fun quant_tac ctxt i = EVERY
(mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
@@ -838,6 +421,7 @@
simp_tac (take_ss addsimps prems) 1,
TRY (safe_tac HOL_cs)];
fun arg_tac arg =
+ (* FIXME! case_UU_tac *)
case_UU_tac context (prems @ con_rews) 1
(List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
fun con_tacs (con, _, args) =
@@ -860,31 +444,20 @@
val _ = trace " Proving take_lemmas...";
val take_lemmas =
let
- fun take_lemma n (dn, ax_reach) =
- let
- val lhs = dc_take dn $ Bound 0 `%(x_name n);
- val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
- val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
- val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
- val rules = [contlub_fst RS contlubE RS ssubst,
- contlub_snd RS contlubE RS ssubst];
- fun tacf {prems, context} = [
- res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
- res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
- stac fix_def2 1,
- REPEAT (CHANGED
- (resolve_tac rules 1 THEN chain_tac 1)),
- stac contlub_cfun_fun 1,
- stac contlub_cfun_fun 2,
- rtac lub_equal 3,
- chain_tac 1,
- rtac allI 1,
- resolve_tac prems 1];
- in pg'' thy axs_take_def goal tacf end;
- in mapn take_lemma 1 (dnames ~~ axs_reach) end;
+ fun take_lemma (ax_chain_take, ax_lub_take) =
+ @{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take];
+ in map take_lemma (axs_chain_take ~~ axs_lub_take) end;
+
+ val axs_reach =
+ let
+ fun reach (ax_chain_take, ax_lub_take) =
+ @{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take];
+ in map reach (axs_chain_take ~~ axs_lub_take) end;
(* ----- theorems concerning finiteness and induction ----------------------- *)
+ val global_ctxt = ProofContext.init thy;
+
val _ = trace " Proving finites, ind...";
val (finites, ind) =
(
@@ -948,6 +521,7 @@
let
val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
fun tacs ctxt = [
+ (* FIXME! case_UU_tac *)
case_UU_tac ctxt take_rews 1 "x",
eresolve_tac finite_lemmas1a 1,
step_tac HOL_cs 1,
@@ -990,22 +564,28 @@
val cont_rules =
[cont_id, cont_const, cont2cont_Rep_CFun,
cont2cont_fst, cont2cont_snd];
+ val subgoal =
+ let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n));
+ in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end;
+ val subgoal' = legacy_infer_term thy subgoal;
fun tacf {prems, context} =
- map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
- quant_tac context 1,
- rtac (adm_impl_admw RS wfix_ind) 1,
- REPEAT_DETERM (rtac adm_all 1),
- REPEAT_DETERM (
- TRY (rtac adm_conj 1) THEN
- rtac adm_subst 1 THEN
- REPEAT (resolve_tac cont_rules 1) THEN
- resolve_tac prems 1),
- strip_tac 1,
- rtac (rewrite_rule axs_take_def finite_ind) 1,
- ind_prems_tac prems];
+ let
+ val subtac =
+ EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
+ val subthm = Goal.prove context [] [] subgoal' (K subtac);
+ in
+ map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
+ cut_facts_tac (subthm :: take (length dnames) prems) 1,
+ REPEAT (rtac @{thm conjI} 1 ORELSE
+ EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
+ resolve_tac axs_chain_take 1,
+ asm_simp_tac HOL_basic_ss 1])
+ ]
+ end;
val ind = (pg'' thy [] goal tacf
handle ERROR _ =>
- (warning "Cannot prove infinite induction rule"; TrueI));
+ (warning "Cannot prove infinite induction rule"; TrueI)
+ );
in (finites, ind) end
)
handle THM _ =>
@@ -1013,7 +593,6 @@
| ERROR _ =>
(warning "Cannot prove induction rule"; ([], TrueI));
-
end; (* local *)
(* ----- theorem concerning coinduction ------------------------------------- *)
@@ -1021,7 +600,7 @@
local
val xs = mapn (fn n => K (x_name n)) 1 dnames;
fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
- val take_ss = HOL_ss addsimps take_rews;
+ val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
val _ = trace " Proving coind_lemma...";
val coind_lemma =
@@ -1075,8 +654,8 @@
in thy |> Sign.add_path comp_dnam
|> snd o PureThy.add_thmss [
- ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]),
((Binding.name "take_lemmas", take_lemmas ), []),
+ ((Binding.name "reach" , axs_reach ), []),
((Binding.name "finites" , finites ), []),
((Binding.name "finite_ind" , [finite_ind]), []),
((Binding.name "ind" , [ind] ), []),
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/holcf_library.ML Tue Mar 02 17:36:40 2010 +0000
@@ -0,0 +1,250 @@
+(* Title: HOLCF/Tools/holcf_library.ML
+ Author: Brian Huffman
+
+Functions for constructing HOLCF types and terms.
+*)
+
+structure HOLCF_Library =
+struct
+
+infixr 6 ->>;
+infix -->>;
+
+(*** Operations from Isabelle/HOL ***)
+
+val boolT = HOLogic.boolT;
+val natT = HOLogic.natT;
+
+val mk_equals = Logic.mk_equals;
+val mk_eq = HOLogic.mk_eq;
+val mk_trp = HOLogic.mk_Trueprop;
+val mk_fst = HOLogic.mk_fst;
+val mk_snd = HOLogic.mk_snd;
+val mk_not = HOLogic.mk_not;
+val mk_conj = HOLogic.mk_conj;
+val mk_disj = HOLogic.mk_disj;
+
+fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t;
+
+
+(*** Basic HOLCF concepts ***)
+
+fun mk_bottom T = Const (@{const_name UU}, T);
+
+fun below_const T = Const (@{const_name below}, [T, T] ---> boolT);
+fun mk_below (t, u) = below_const (fastype_of t) $ t $ u;
+
+fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t));
+
+fun mk_defined t = mk_not (mk_undef t);
+
+fun mk_compact t =
+ Const (@{const_name compact}, fastype_of t --> boolT) $ t;
+
+fun mk_cont t =
+ Const (@{const_name cont}, fastype_of t --> boolT) $ t;
+
+fun mk_chain t =
+ Const (@{const_name chain}, Term.fastype_of t --> boolT) $ t;
+
+
+(*** Continuous function space ***)
+
+(* ->> is taken from holcf_logic.ML *)
+fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+
+val (op ->>) = mk_cfunT;
+val (op -->>) = Library.foldr mk_cfunT;
+
+fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+ | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
+
+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 = fastype_of t
+ in cabs_const (Term.domain_type T, Term.range_type T) $ t end
+
+(* builds the expression (% v1 v2 .. vn. rhs) *)
+fun lambdas [] rhs = rhs
+ | lambdas (v::vs) rhs = Term.lambda v (lambdas vs rhs);
+
+(* builds the expression (LAM v. rhs) *)
+fun big_lambda v rhs =
+ cabs_const (fastype_of v, 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 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;
+
+infix 9 ` ; val (op `) = mk_capply;
+
+val list_ccomb : term * term list -> term = Library.foldl mk_capply;
+
+fun mk_ID T = Const (@{const_name ID}, 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 (fastype_of f);
+ val (T, U') = dest_cfunT (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_strict t =
+ let val (T, U) = dest_cfunT (fastype_of t);
+ in mk_eq (t ` mk_bottom T, mk_bottom U) end;
+
+
+(*** Product type ***)
+
+val mk_prodT = HOLogic.mk_prodT
+
+fun mk_tupleT [] = HOLogic.unitT
+ | mk_tupleT [T] = T
+ | mk_tupleT (T :: Ts) = mk_prodT (T, mk_tupleT Ts);
+
+(* 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));
+
+
+(*** Lifted cpo type ***)
+
+fun mk_upT T = Type(@{type_name "u"}, [T]);
+
+fun dest_upT (Type(@{type_name "u"}, [T])) = T
+ | dest_upT T = raise TYPE ("dest_upT", [T], []);
+
+fun up_const T = Const(@{const_name up}, T ->> mk_upT T);
+
+fun mk_up t = up_const (fastype_of t) ` t;
+
+fun fup_const (T, U) =
+ Const(@{const_name fup}, (T ->> U) ->> mk_upT T ->> U);
+
+fun from_up T = fup_const (T, T) ` mk_ID T;
+
+
+(*** Strict product type ***)
+
+val oneT = @{typ "one"};
+
+fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
+
+fun dest_sprodT (Type(@{type_name "**"}, [T, U])) = (T, U)
+ | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []);
+
+fun spair_const (T, U) =
+ Const(@{const_name spair}, T ->> U ->> mk_sprodT (T, U));
+
+(* builds the expression (:t, u:) *)
+fun mk_spair (t, u) =
+ spair_const (fastype_of t, fastype_of u) ` t ` u;
+
+(* builds the expression (:t1,t2,..,tn:) *)
+fun mk_stuple [] = @{term "ONE"}
+ | mk_stuple (t::[]) = t
+ | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts);
+
+fun sfst_const (T, U) =
+ Const(@{const_name sfst}, mk_sprodT (T, U) ->> T);
+
+fun ssnd_const (T, U) =
+ Const(@{const_name ssnd}, mk_sprodT (T, U) ->> U);
+
+
+(*** Strict sum type ***)
+
+fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+
+fun dest_ssumT (Type(@{type_name "++"}, [T, U])) = (T, U)
+ | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []);
+
+fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U));
+fun sinr_const (T, U) = Const(@{const_name sinr}, U ->> mk_ssumT (T, U));
+
+(* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *)
+fun mk_sinjects ts =
+ let
+ val Ts = map fastype_of ts;
+ fun combine (t, T) (us, U) =
+ let
+ val v = sinl_const (T, U) ` t;
+ val vs = map (fn u => sinr_const (T, U) ` u) us;
+ in
+ (v::vs, mk_ssumT (T, U))
+ end
+ fun inj [] = error "mk_sinjects: empty list"
+ | inj ((t, T)::[]) = ([t], T)
+ | inj ((t, T)::ts) = combine (t, T) (inj ts);
+ in
+ fst (inj (ts ~~ Ts))
+ end;
+
+fun sscase_const (T, U, V) =
+ Const(@{const_name sscase},
+ (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V);
+
+fun from_sinl (T, U) =
+ sscase_const (T, U, T) ` mk_ID T ` mk_bottom (U ->> T);
+
+fun from_sinr (T, U) =
+ sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U;
+
+
+(*** pattern match monad type ***)
+
+fun mk_matchT T = Type (@{type_name "maybe"}, [T]);
+
+fun dest_matchT (Type(@{type_name "maybe"}, [T])) = T
+ | dest_matchT T = raise TYPE ("dest_matchT", [T], []);
+
+fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T);
+
+fun return_const T = Const (@{const_name "Fixrec.return"}, T ->> mk_matchT T);
+fun mk_return t = return_const (fastype_of t) ` t;
+
+
+(*** lifted boolean type ***)
+
+val trT = @{typ "tr"};
+
+
+(*** theory of fixed points ***)
+
+fun mk_fix t =
+ let val (T, _) = dest_cfunT (fastype_of t)
+ in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end;
+
+fun iterate_const T =
+ Const (@{const_name iterate}, natT --> (T ->> T) ->> (T ->> T));
+
+fun mk_iterate (n, f) =
+ let val (T, _) = dest_cfunT (Term.fastype_of f);
+ in (iterate_const T $ n) ` f ` mk_bottom T end;
+
+end;
--- a/src/HOLCF/ex/Dnat.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/ex/Dnat.thy Tue Mar 02 17:36:40 2010 +0000
@@ -62,10 +62,10 @@
apply (rule allI)
apply (rule_tac x = y in dnat.casedist)
apply (fast intro!: UU_I)
- apply (thin_tac "ALL y. d << y --> d = UU | d = y")
+ apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
apply simp
apply (simp (no_asm_simp))
- apply (drule_tac x="da" in spec)
+ apply (drule_tac x="dnata" in spec)
apply simp
done
--- a/src/HOLCF/ex/Domain_Proofs.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/ex/Domain_Proofs.thy Tue Mar 02 17:36:40 2010 +0000
@@ -196,7 +196,7 @@
by (rule bar_defl_unfold)
lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding REP_foo REP_bar REP_baz REP_simps
+unfolding REP_foo REP_bar REP_baz REP_simps REP_convex
by (rule baz_defl_unfold)
(********************************************************************)
--- a/src/HOLCF/ex/Domain_ex.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/ex/Domain_ex.thy Tue Mar 02 17:36:40 2010 +0000
@@ -99,7 +99,7 @@
text {* Trivial datatypes will produce a warning message. *}
-domain triv = triv1 triv triv
+domain triv = Triv triv triv
-- "domain Domain_ex.triv is empty!"
lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
@@ -122,7 +122,7 @@
text {* Rules about constructors *}
term Leaf
term Node
-thm tree.Leaf_def tree.Node_def
+thm Leaf_def Node_def
thm tree.exhaust
thm tree.casedist
thm tree.compacts
@@ -134,7 +134,7 @@
text {* Rules about case combinator *}
term tree_when
-thm tree.when_def
+thm tree.tree_when_def
thm tree.when_rews
text {* Rules about selectors *}
@@ -157,16 +157,17 @@
term match_Node
thm tree.match_rews
-text {* Rules about copy function *}
-term tree_copy
-thm tree.copy_def
-thm tree.copy_rews
-
text {* Rules about take function *}
term tree_take
thm tree.take_def
+thm tree.take_0
+thm tree.take_Suc
thm tree.take_rews
+thm tree.chain_take
+thm tree.take_take
+thm tree.deflation_take
thm tree.take_lemmas
+thm tree.reach
thm tree.finite_ind
text {* Rules about finiteness predicate *}
--- a/src/HOLCF/ex/New_Domain.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/ex/New_Domain.thy Tue Mar 02 17:36:40 2010 +0000
@@ -51,12 +51,12 @@
thm ltree.reach
text {*
- The definition of the copy function uses map functions associated with
+ The definition of the take function uses map functions associated with
each type constructor involved in the definition. A map function
for the lazy list type has been generated by the new domain package.
*}
-thm ltree.copy_def
+thm ltree.take_rews
thm llist_map_def
lemma ltree_induct:
@@ -67,24 +67,24 @@
assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
shows "P x"
proof -
- have "\<forall>x. P (fix\<cdot>ltree_copy\<cdot>x)"
- proof (rule fix_ind)
- show "adm (\<lambda>a. \<forall>x. P (a\<cdot>x))"
- by (simp add: adm_subst [OF _ adm])
- next
- show "\<forall>x. P (\<bottom>\<cdot>x)"
- by (simp add: bot)
- next
- fix f :: "'a ltree \<rightarrow> 'a ltree"
- assume f: "\<forall>x. P (f\<cdot>x)"
- show "\<forall>x. P (ltree_copy\<cdot>f\<cdot>x)"
- apply (rule allI)
- apply (case_tac x)
- apply (simp add: bot)
- apply (simp add: Leaf)
- apply (simp add: Branch [OF f])
- done
- qed
+ have "P (\<Squnion>i. ltree_take i\<cdot>x)"
+ using adm
+ proof (rule admD)
+ fix i
+ show "P (ltree_take i\<cdot>x)"
+ proof (induct i arbitrary: x)
+ case (0 x)
+ show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
+ next
+ case (Suc n x)
+ show "P (ltree_take (Suc n)\<cdot>x)"
+ apply (cases x)
+ apply (simp add: bot)
+ apply (simp add: Leaf)
+ apply (simp add: Branch Suc)
+ done
+ qed
+ qed (simp add: ltree.chain_take)
thus ?thesis
by (simp add: ltree.reach)
qed
--- a/src/HOLCF/ex/Stream.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/ex/Stream.thy Tue Mar 02 17:36:40 2010 +0000
@@ -143,16 +143,10 @@
lemma stream_reach2: "(LUB i. stream_take i$s) = s"
-apply (insert stream.reach [of s], erule subst) back
-apply (simp add: fix_def2 stream.take_def)
-apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym])
-by simp
+by (rule stream.reach)
lemma chain_stream_take: "chain (%i. stream_take i$s)"
-apply (rule chainI)
-apply (rule monofun_cfun_fun)
-apply (simp add: stream.take_def del: iterate_Suc)
-by (rule chainE, simp)
+by (simp add: stream.chain_take)
lemma stream_take_prefix [simp]: "stream_take n$s << s"
apply (insert stream_reach2 [of s])
@@ -259,10 +253,9 @@
lemma stream_ind2:
"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s) |] ==> P x"
apply (insert stream.reach [of x],erule subst)
-apply (frule adm_impl_admw, rule wfix_ind, auto)
-apply (rule adm_subst [THEN adm_impl_admw],auto)
+apply (erule admD, rule chain_stream_take)
apply (insert stream_finite_ind2 [of P])
-by (simp add: stream.take_def)
+by simp
@@ -275,16 +268,9 @@
lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R"
apply (simp add: stream.bisim_def,clarsimp)
- apply (case_tac "x=UU",clarsimp)
- apply (erule_tac x="UU" in allE,simp)
- apply (case_tac "x'=UU",simp)
- apply (drule stream_exhaust_eq [THEN iffD1],auto)+
- apply (case_tac "x'=UU",auto)
- apply (erule_tac x="a && y" in allE)
- apply (erule_tac x="UU" in allE)+
- apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
- apply (erule_tac x="a && y" in allE)
- apply (erule_tac x="aa && ya" in allE) back
+ apply (drule spec, drule spec, drule (1) mp)
+ apply (case_tac "x", simp)
+ apply (case_tac "x'", simp)
by auto
@@ -379,8 +365,8 @@
lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < Fin (Suc n))"
apply (rule stream.casedist [of x], auto)
apply (simp add: zero_inat_def)
- apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
- apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
+ apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
+ apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
done
lemma slen_take_lemma4 [rule_format]:
--- a/src/HOLCF/ex/Strict_Fun.thy Tue Mar 02 17:36:16 2010 +0000
+++ b/src/HOLCF/ex/Strict_Fun.thy Tue Mar 02 17:36:40 2010 +0000
@@ -232,8 +232,8 @@
setup {*
Domain_Isomorphism.add_type_constructor
- (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map},
- @{thm REP_sfun}, @{thm isodefl_sfun}, @{thm sfun_map_ID})
+ (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm REP_sfun},
+ @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map})
*}
end
--- a/src/Tools/nbe.ML Tue Mar 02 17:36:16 2010 +0000
+++ b/src/Tools/nbe.ML Tue Mar 02 17:36:40 2010 +0000
@@ -235,7 +235,7 @@
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
fun nbe_bound v = "v_" ^ v;
fun nbe_bound_optional NONE = "_"
- | nbe_bound_optional (SOME v) = nbe_bound v;
+ | nbe_bound_optional (SOME v) = nbe_bound v;
fun nbe_default v = "w_" ^ v;
(*note: these three are the "turning spots" where proper argument order is established!*)
@@ -434,7 +434,7 @@
#-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
end;
-fun ensure_stmts ctxt naming program =
+fun ensure_stmts ctxt program =
let
fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
then (gr, (maxidx, idx_tab))
@@ -443,7 +443,6 @@
Graph.imm_succs program name)) names);
in
fold_rev add_stmts (Graph.strong_conn program)
- #> pair naming
end;
@@ -513,18 +512,18 @@
structure Nbe_Functions = Code_Data
(
- type T = Code_Thingol.naming * ((Univ option * int) Graph.T * (int * string Inttab.table));
- val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty)));
+ type T = (Univ option * int) Graph.T * (int * string Inttab.table);
+ val empty = (Graph.empty, (0, Inttab.empty));
);
(* compilation, evaluation and reification *)
-fun compile_eval thy naming program vs_t deps =
+fun compile_eval thy program vs_t deps =
let
val ctxt = ProofContext.init thy;
- val (_, (gr, (_, idx_tab))) =
- Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
+ val (gr, (_, idx_tab)) =
+ Nbe_Functions.change thy (ensure_stmts ctxt program);
in
vs_t
|> eval_term ctxt gr deps
@@ -534,7 +533,7 @@
(* evaluation with type reconstruction *)
-fun normalize thy naming program ((vs0, (vs, ty)), t) deps =
+fun normalize thy program ((vs0, (vs, ty)), t) deps =
let
val ty' = typ_of_itype program vs0 ty;
fun type_infer t =
@@ -546,7 +545,7 @@
^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy);
in
- compile_eval thy naming program (vs, t) deps
+ compile_eval thy program (vs, t) deps
|> traced (fn t => "Normalized:\n" ^ string_of_term t)
|> type_infer
|> traced (fn t => "Types inferred:\n" ^ string_of_term t)
@@ -565,11 +564,11 @@
in Thm.mk_binop eq lhs rhs end;
val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "norm", fn (thy, naming, program, vsp_ty_t, deps, ct) =>
- mk_equals thy ct (normalize thy naming program vsp_ty_t deps))));
+ (Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
+ mk_equals thy ct (normalize thy program vsp_ty_t deps))));
-fun norm_oracle thy naming program vsp_ty_t deps ct =
- raw_norm_oracle (thy, naming, program, vsp_ty_t, deps, ct);
+fun norm_oracle thy program vsp_ty_t deps ct =
+ raw_norm_oracle (thy, program, vsp_ty_t, deps, ct);
fun no_frees_conv conv ct =
let
@@ -597,9 +596,9 @@
val norm_conv = no_frees_conv (fn ct =>
let
val thy = Thm.theory_of_cterm ct;
- in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (norm_oracle thy)) ct end);
+ in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (K (norm_oracle thy))) ct end);
-fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (normalize thy)));
+fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (K (normalize thy))));
(* evaluation command *)