--- a/src/HOLCF/Domain.thy Mon Mar 08 17:37:09 2010 +0100
+++ b/src/HOLCF/Domain.thy Mon Mar 08 15:20:40 2010 -0800
@@ -19,107 +19,6 @@
defaultsort pcpo
-subsection {* Continuous isomorphisms *}
-
-text {* A locale for continuous isomorphisms *}
-
-locale iso =
- fixes abs :: "'a \<rightarrow> 'b"
- fixes rep :: "'b \<rightarrow> 'a"
- assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"
- assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"
-begin
-
-lemma swap: "iso rep abs"
- by (rule iso.intro [OF rep_iso abs_iso])
-
-lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
-proof
- assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
- then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
- then show "x \<sqsubseteq> y" by simp
-next
- assume "x \<sqsubseteq> y"
- then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
-qed
-
-lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
- by (rule iso.abs_below [OF swap])
-
-lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
- by (simp add: po_eq_conv abs_below)
-
-lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
- by (rule iso.abs_eq [OF swap])
-
-lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>"
-proof -
- have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
- then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
- then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
- then show ?thesis by (rule UU_I)
-qed
-
-lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
- by (rule iso.abs_strict [OF swap])
-
-lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>"
-proof -
- have "x = rep\<cdot>(abs\<cdot>x)" by simp
- also assume "abs\<cdot>x = \<bottom>"
- also note rep_strict
- finally show "x = \<bottom>" .
-qed
-
-lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
- by (rule iso.abs_defin' [OF swap])
-
-lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"
- by (erule contrapos_nn, erule abs_defin')
-
-lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
- by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
-
-lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
- by (auto elim: abs_defin' intro: abs_strict)
-
-lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
- by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
-
-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
- have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
- then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
-qed
-
-lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
- by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms)
-
-lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)"
- by (rule compact_rep_rev) simp
-
-lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)"
- by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms)
-
-lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"
-proof
- assume "x = abs\<cdot>y"
- then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp
- then show "rep\<cdot>x = y" by simp
-next
- assume "rep\<cdot>x = y"
- then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp
- then show "x = abs\<cdot>y" by simp
-qed
-
-end
-
-
subsection {* Casedist *}
lemma ex_one_defined_iff:
@@ -214,102 +113,6 @@
ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up
-subsection {* Take functions and finiteness *}
-
-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)
-
-text {*
- Let a ``decisive'' function be a deflation that maps every input to
- either itself or bottom. Then if a domain's take functions are all
- decisive, then all values in the domain are finite.
-*}
-
-definition
- decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
-where
- "decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)"
-
-lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d"
- unfolding decisive_def by simp
-
-lemma decisive_cases:
- assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>"
-using assms unfolding decisive_def by auto
-
-lemma decisive_bottom: "decisive \<bottom>"
- unfolding decisive_def by simp
-
-lemma decisive_ID: "decisive ID"
- unfolding decisive_def by simp
-
-lemma decisive_ssum_map:
- assumes f: "decisive f"
- assumes g: "decisive g"
- shows "decisive (ssum_map\<cdot>f\<cdot>g)"
-apply (rule decisiveI, rename_tac s)
-apply (case_tac s, simp_all)
-apply (rule_tac x=x in decisive_cases [OF f], simp_all)
-apply (rule_tac x=y in decisive_cases [OF g], simp_all)
-done
-
-lemma decisive_sprod_map:
- assumes f: "decisive f"
- assumes g: "decisive g"
- shows "decisive (sprod_map\<cdot>f\<cdot>g)"
-apply (rule decisiveI, rename_tac s)
-apply (case_tac s, simp_all)
-apply (rule_tac x=x in decisive_cases [OF f], simp_all)
-apply (rule_tac x=y in decisive_cases [OF g], simp_all)
-done
-
-lemma decisive_abs_rep:
- fixes abs rep
- assumes iso: "iso abs rep"
- assumes d: "decisive d"
- shows "decisive (abs oo d oo rep)"
-apply (rule decisiveI)
-apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
-apply (simp add: iso.rep_iso [OF iso])
-apply (simp add: iso.abs_strict [OF iso])
-done
-
-lemma lub_ID_finite:
- assumes chain: "chain d"
- assumes lub: "(\<Squnion>n. d n) = ID"
- assumes decisive: "\<And>n. decisive (d n)"
- shows "\<exists>n. d n\<cdot>x = x"
-proof -
- have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp
- have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach)
- have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>"
- using decisive unfolding decisive_def by simp
- hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}"
- by auto
- hence "finite (range (\<lambda>n. d n\<cdot>x))"
- by (rule finite_subset, simp)
- with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)"
- by (rule finite_range_imp_finch)
- then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x"
- unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
- with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
-qed
-
-
subsection {* Installing the domain package *}
lemmas con_strict_rules =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Domain_Aux.thy Mon Mar 08 15:20:40 2010 -0800
@@ -0,0 +1,263 @@
+(* Title: HOLCF/Domain_Aux.thy
+ Author: Brian Huffman
+*)
+
+header {* Domain package support *}
+
+theory Domain_Aux
+imports Ssum Sprod Fixrec
+uses
+ ("Tools/Domain/domain_take_proofs.ML")
+begin
+
+subsection {* Continuous isomorphisms *}
+
+text {* A locale for continuous isomorphisms *}
+
+locale iso =
+ fixes abs :: "'a \<rightarrow> 'b"
+ fixes rep :: "'b \<rightarrow> 'a"
+ assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"
+ assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"
+begin
+
+lemma swap: "iso rep abs"
+ by (rule iso.intro [OF rep_iso abs_iso])
+
+lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
+proof
+ assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
+ then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
+ then show "x \<sqsubseteq> y" by simp
+next
+ assume "x \<sqsubseteq> y"
+ then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
+qed
+
+lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
+ by (rule iso.abs_below [OF swap])
+
+lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
+ by (simp add: po_eq_conv abs_below)
+
+lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
+ by (rule iso.abs_eq [OF swap])
+
+lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>"
+proof -
+ have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
+ then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
+ then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
+ then show ?thesis by (rule UU_I)
+qed
+
+lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
+ by (rule iso.abs_strict [OF swap])
+
+lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>"
+proof -
+ have "x = rep\<cdot>(abs\<cdot>x)" by simp
+ also assume "abs\<cdot>x = \<bottom>"
+ also note rep_strict
+ finally show "x = \<bottom>" .
+qed
+
+lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
+ by (rule iso.abs_defin' [OF swap])
+
+lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"
+ by (erule contrapos_nn, erule abs_defin')
+
+lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
+ by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
+
+lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
+ by (auto elim: abs_defin' intro: abs_strict)
+
+lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
+ by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
+
+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
+ have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
+ then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
+qed
+
+lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
+ by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms)
+
+lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)"
+ by (rule compact_rep_rev) simp
+
+lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)"
+ by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms)
+
+lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"
+proof
+ assume "x = abs\<cdot>y"
+ then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp
+ then show "rep\<cdot>x = y" by simp
+next
+ assume "rep\<cdot>x = y"
+ then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp
+ then show "x = abs\<cdot>y" by simp
+qed
+
+end
+
+
+subsection {* Proofs about take functions *}
+
+text {*
+ This section contains lemmas that are used in a module that supports
+ the domain isomorphism package; the module contains proofs related
+ to take functions and the finiteness predicate.
+*}
+
+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>n. deflation (d n)"
+ shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
+proof (rule linorder_le_cases)
+ assume "m \<le> n"
+ with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
+ by (rule deflation_below_comp1 [OF defl defl])
+ moreover from `m \<le> n` have "min m n = m" by simp
+ ultimately show ?thesis by simp
+next
+ assume "n \<le> m"
+ with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
+ by (rule deflation_below_comp2 [OF defl defl])
+ moreover from `n \<le> m` have "min m n = n" by simp
+ ultimately show ?thesis by simp
+qed
+
+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)
+
+lemma lub_ID_take_induct:
+ assumes "chain t" and "(\<Squnion>n. t n) = ID"
+ assumes "adm P" and "\<And>n. P (t n\<cdot>x)" shows "P x"
+proof -
+ from `chain t` have "chain (\<lambda>n. t n\<cdot>x)" by simp
+ from `adm P` this `\<And>n. P (t n\<cdot>x)` have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD)
+ with `chain t` `(\<Squnion>n. t n) = ID` show "P x" by (simp add: lub_distribs)
+qed
+
+
+subsection {* Finiteness *}
+
+text {*
+ Let a ``decisive'' function be a deflation that maps every input to
+ either itself or bottom. Then if a domain's take functions are all
+ decisive, then all values in the domain are finite.
+*}
+
+definition
+ decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
+where
+ "decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)"
+
+lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d"
+ unfolding decisive_def by simp
+
+lemma decisive_cases:
+ assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>"
+using assms unfolding decisive_def by auto
+
+lemma decisive_bottom: "decisive \<bottom>"
+ unfolding decisive_def by simp
+
+lemma decisive_ID: "decisive ID"
+ unfolding decisive_def by simp
+
+lemma decisive_ssum_map:
+ assumes f: "decisive f"
+ assumes g: "decisive g"
+ shows "decisive (ssum_map\<cdot>f\<cdot>g)"
+apply (rule decisiveI, rename_tac s)
+apply (case_tac s, simp_all)
+apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+done
+
+lemma decisive_sprod_map:
+ assumes f: "decisive f"
+ assumes g: "decisive g"
+ shows "decisive (sprod_map\<cdot>f\<cdot>g)"
+apply (rule decisiveI, rename_tac s)
+apply (case_tac s, simp_all)
+apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+done
+
+lemma decisive_abs_rep:
+ fixes abs rep
+ assumes iso: "iso abs rep"
+ assumes d: "decisive d"
+ shows "decisive (abs oo d oo rep)"
+apply (rule decisiveI)
+apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
+apply (simp add: iso.rep_iso [OF iso])
+apply (simp add: iso.abs_strict [OF iso])
+done
+
+lemma lub_ID_finite:
+ assumes chain: "chain d"
+ assumes lub: "(\<Squnion>n. d n) = ID"
+ assumes decisive: "\<And>n. decisive (d n)"
+ shows "\<exists>n. d n\<cdot>x = x"
+proof -
+ have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp
+ have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach)
+ have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>"
+ using decisive unfolding decisive_def by simp
+ hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}"
+ by auto
+ hence "finite (range (\<lambda>n. d n\<cdot>x))"
+ by (rule finite_subset, simp)
+ with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)"
+ by (rule finite_range_imp_finch)
+ then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x"
+ unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
+ with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
+qed
+
+lemma lub_ID_finite_take_induct:
+ assumes "chain d" and "(\<Squnion>n. d n) = ID" and "\<And>n. decisive (d n)"
+ shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x"
+using lub_ID_finite [OF assms] by metis
+
+subsection {* ML setup *}
+
+use "Tools/Domain/domain_take_proofs.ML"
+
+end
--- a/src/HOLCF/IsaMakefile Mon Mar 08 17:37:09 2010 +0100
+++ b/src/HOLCF/IsaMakefile Mon Mar 08 15:20:40 2010 -0800
@@ -39,6 +39,7 @@
Discrete.thy \
Deflation.thy \
Domain.thy \
+ Domain_Aux.thy \
Eventual.thy \
Ffun.thy \
Fixrec.thy \
--- a/src/HOLCF/Representable.thy Mon Mar 08 17:37:09 2010 +0100
+++ b/src/HOLCF/Representable.thy Mon Mar 08 15:20:40 2010 -0800
@@ -5,51 +5,12 @@
header {* Representable Types *}
theory Representable
-imports Algebraic Universal Ssum Sprod One Fixrec
+imports Algebraic Universal Ssum Sprod One Fixrec Domain_Aux
uses
("Tools/repdef.ML")
- ("Tools/Domain/domain_take_proofs.ML")
("Tools/Domain/domain_isomorphism.ML")
begin
-subsection {* Preliminaries: Take proofs *}
-
-text {*
- This section contains lemmas that are used in a module that supports
- the domain isomorphism package; the module contains proofs related
- to take functions and the finiteness predicate.
-*}
-
-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>n. deflation (d n)"
- shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
-proof (rule linorder_le_cases)
- assume "m \<le> n"
- with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
- then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
- by (rule deflation_below_comp1 [OF defl defl])
- moreover from `m \<le> n` have "min m n = m" by simp
- ultimately show ?thesis by simp
-next
- assume "n \<le> m"
- with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
- then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
- by (rule deflation_below_comp2 [OF defl defl])
- moreover from `n \<le> m` have "min m n = n" by simp
- ultimately show ?thesis by simp
-qed
-
-use "Tools/Domain/domain_take_proofs.ML"
-
-
subsection {* Class of representable types *}
text "Overloaded embedding and projection functions between
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 08 17:37:09 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 08 15:20:40 2010 -0800
@@ -16,7 +16,8 @@
val add_axioms :
(binding * (typ * typ)) list -> theory ->
- Domain_Take_Proofs.iso_info list * theory
+ (Domain_Take_Proofs.iso_info list
+ * Domain_Take_Proofs.take_induct_info) * theory
end;
@@ -120,8 +121,13 @@
fold_map axiomatize_lub_take
(map fst dom_eqns ~~ #take_consts take_info) thy;
+ (* prove additional take theorems *)
+ val (take_info2, thy) =
+ Domain_Take_Proofs.add_lub_take_theorems
+ (map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy;
+
in
- (iso_infos, thy) (* TODO: also return take_info, lub_take_thms *)
+ ((iso_infos, take_info2), thy)
end;
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Mar 08 17:37:09 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon Mar 08 15:20:40 2010 -0800
@@ -184,7 +184,7 @@
fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
val repTs : typ list = map mk_eq_typ eqs';
val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs);
- val (iso_infos, thy) =
+ val ((iso_infos, take_info), thy) =
Domain_Axioms.add_axioms dom_eqns thy;
val ((rewss, take_rews), theorems_thy) =
@@ -192,7 +192,7 @@
|> fold_map (fn ((eq, (x,cs)), info) =>
Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
(eqs ~~ eqs' ~~ iso_infos)
- ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info;
in
theorems_thy
|> Sign.add_path (Long_Name.base_name comp_dnam)
@@ -246,7 +246,7 @@
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 (iso_infos, thy) = thy |>
+ val ((iso_infos, take_info), thy) = thy |>
Domain_Isomorphism.domain_isomorphism
(map (fn ((vs, dname, mx, _), eq) =>
(map fst vs, dname, mx, mk_eq_typ eq, NONE))
@@ -268,7 +268,7 @@
|> fold_map (fn ((eq, (x,cs)), info) =>
Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
(eqs ~~ eqs' ~~ iso_infos)
- ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info;
in
theorems_thy
|> Sign.add_path (Long_Name.base_name comp_dnam)
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 08 17:37:09 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 08 15:20:40 2010 -0800
@@ -7,8 +7,12 @@
signature DOMAIN_ISOMORPHISM =
sig
val domain_isomorphism :
- (string list * binding * mixfix * typ * (binding * binding) option) list
- -> theory -> Domain_Take_Proofs.iso_info list * theory
+ (string list * binding * mixfix * typ
+ * (binding * binding) option) list ->
+ theory ->
+ (Domain_Take_Proofs.iso_info list
+ * Domain_Take_Proofs.take_induct_info) * theory
+
val domain_isomorphism_cmd :
(string list * binding * mixfix * string * (binding * binding) option) list
-> theory -> theory
@@ -265,7 +269,8 @@
(prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
(doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
(thy: theory)
- : Domain_Take_Proofs.iso_info list * theory =
+ : (Domain_Take_Proofs.iso_info list
+ * Domain_Take_Proofs.take_induct_info) * theory =
let
val _ = Theory.requires thy "Representable" "domain isomorphisms";
@@ -644,8 +649,12 @@
fold_map prove_lub_take
(dom_binds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy;
+ (* prove additional take theorems *)
+ val (take_info2, thy) =
+ Domain_Take_Proofs.add_lub_take_theorems
+ (dom_binds ~~ iso_infos) take_info lub_take_thms thy;
in
- (iso_infos, thy)
+ ((iso_infos, take_info2), thy)
end;
val domain_isomorphism = gen_domain_isomorphism cert_typ;
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Mar 08 17:37:09 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Mar 08 15:20:40 2010 -0800
@@ -16,10 +16,9 @@
abs_inverse : thm,
rep_inverse : thm
}
-
- val define_take_functions :
- (binding * iso_info) list -> theory ->
- { take_consts : term list,
+ type take_info =
+ {
+ take_consts : term list,
take_defs : thm list,
chain_take_thms : thm list,
take_0_thms : thm list,
@@ -27,7 +26,29 @@
deflation_take_thms : thm list,
finite_consts : term list,
finite_defs : thm list
- } * theory
+ }
+ type take_induct_info =
+ {
+ 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,
+ finite_consts : term list,
+ finite_defs : thm list,
+ lub_take_thms : thm list,
+ reach_thms : thm list,
+ take_lemma_thms : thm list,
+ is_finite : bool,
+ take_induct_thms : thm list
+ }
+ val define_take_functions :
+ (binding * iso_info) list -> theory -> take_info * theory
+
+ val add_lub_take_theorems :
+ (binding * iso_info) list -> take_info -> thm list ->
+ theory -> take_induct_info * theory
val map_of_typ :
theory -> (typ * term) list -> typ -> term
@@ -52,6 +73,34 @@
rep_inverse : thm
};
+type take_info =
+ { 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,
+ finite_consts : term list,
+ finite_defs : thm list
+ };
+
+type take_induct_info =
+ {
+ 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,
+ finite_consts : term list,
+ finite_defs : thm list,
+ lub_take_thms : thm list,
+ reach_thms : thm list,
+ take_lemma_thms : thm list,
+ is_finite : bool,
+ take_induct_thms : thm list
+ };
+
val beta_ss =
HOL_basic_ss
addsimps simp_thms
@@ -168,6 +217,13 @@
((const, def_thm), thy)
end;
+fun add_qualified_def name (path, eqn) thy =
+ thy
+ |> Sign.add_path path
+ |> yield_singleton (PureThy.add_defs false)
+ (Thm.no_attributes (Binding.name name, eqn))
+ ||> Sign.parent_path;
+
fun add_qualified_thm name (path, thm) thy =
thy
|> Sign.add_path path
@@ -239,12 +295,8 @@
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;
+ add_qualified_def "take_def"
+ (Binding.name_of tbind, take_eqn) thy;
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)
@@ -388,12 +440,8 @@
(lambda n (mk_eq (mk_capply (take_const $ n, x), x))));
val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
val (finite_def_thm, thy) =
- thy
- |> Sign.add_path (Binding.name_of tbind)
- |> yield_singleton
- (PureThy.add_defs false o map Thm.no_attributes)
- (Binding.name "finite_def", finite_eqn)
- ||> Sign.parent_path;
+ add_qualified_def "finite_def"
+ (Binding.name_of tbind, finite_eqn) thy;
in ((finite_const, finite_def_thm), thy) end;
val ((finite_consts, finite_defs), thy) = thy
|> fold_map define_finite_const (dom_binds ~~ take_consts ~~ dom_eqns)
@@ -415,4 +463,174 @@
(result, thy)
end;
+fun prove_finite_take_induct
+ (spec : (binding * iso_info) list)
+ (take_info : take_info)
+ (lub_take_thms : thm list)
+ (thy : theory) =
+ let
+ val dom_binds = map fst spec;
+ val iso_infos = map snd spec;
+ val absTs = map #absT iso_infos;
+ val dnames = map Binding.name_of dom_binds;
+ val {take_consts, ...} = take_info;
+ val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info;
+ val {finite_consts, finite_defs, ...} = take_info;
+
+ val decisive_lemma =
+ let
+ fun iso_locale info =
+ @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info];
+ val iso_locale_thms = map iso_locale iso_infos;
+ val decisive_abs_rep_thms =
+ map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms;
+ val n = Free ("n", @{typ nat});
+ fun mk_decisive t =
+ Const (@{const_name decisive}, fastype_of t --> boolT) $ t;
+ fun f take_const = mk_decisive (take_const $ n);
+ val goal = mk_trp (foldr1 mk_conj (map f take_consts));
+ val rules0 = @{thm decisive_bottom} :: take_0_thms;
+ val rules1 =
+ take_Suc_thms @ decisive_abs_rep_thms
+ @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
+ val tac = EVERY [
+ rtac @{thm nat.induct} 1,
+ simp_tac (HOL_ss addsimps rules0) 1,
+ asm_simp_tac (HOL_ss addsimps rules1) 1];
+ in Goal.prove_global thy [] [] goal (K tac) end;
+ fun conjuncts 1 thm = [thm]
+ | conjuncts n thm = let
+ val thmL = thm RS @{thm conjunct1};
+ val thmR = thm RS @{thm conjunct2};
+ in thmL :: conjuncts (n-1) thmR end;
+ val decisive_thms = conjuncts (length spec) decisive_lemma;
+
+ fun prove_finite_thm (absT, finite_const) =
+ let
+ val goal = mk_trp (finite_const $ Free ("x", absT));
+ val tac =
+ EVERY [
+ rewrite_goals_tac finite_defs,
+ rtac @{thm lub_ID_finite} 1,
+ resolve_tac chain_take_thms 1,
+ resolve_tac lub_take_thms 1,
+ resolve_tac decisive_thms 1];
+ in
+ Goal.prove_global thy [] [] goal (K tac)
+ end;
+ val finite_thms =
+ map prove_finite_thm (absTs ~~ finite_consts);
+
+ fun prove_take_induct ((ch_take, lub_take), decisive) =
+ Drule.export_without_context
+ (@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]);
+ val take_induct_thms =
+ map prove_take_induct
+ (chain_take_thms ~~ lub_take_thms ~~ decisive_thms);
+
+ val thy = thy
+ |> fold (snd oo add_qualified_thm "finite")
+ (dnames ~~ finite_thms)
+ |> fold (snd oo add_qualified_thm "take_induct")
+ (dnames ~~ take_induct_thms);
+ in
+ ((finite_thms, take_induct_thms), thy)
+ end;
+
+fun add_lub_take_theorems
+ (spec : (binding * iso_info) list)
+ (take_info : take_info)
+ (lub_take_thms : thm list)
+ (thy : theory) =
+ let
+
+ (* retrieve components of spec *)
+ val dom_binds = map fst spec;
+ val iso_infos = map snd spec;
+ val absTs = map #absT iso_infos;
+ val repTs = map #repT iso_infos;
+ val dnames = map Binding.name_of dom_binds;
+ val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info;
+ val {chain_take_thms, deflation_take_thms, ...} = take_info;
+
+ (* prove take lemmas *)
+ fun prove_take_lemma ((chain_take, lub_take), dname) thy =
+ let
+ val take_lemma =
+ Drule.export_without_context
+ (@{thm lub_ID_take_lemma} OF [chain_take, lub_take]);
+ in
+ add_qualified_thm "take_lemma" (dname, take_lemma) thy
+ end;
+ val (take_lemma_thms, thy) =
+ fold_map prove_take_lemma
+ (chain_take_thms ~~ lub_take_thms ~~ dnames) thy;
+
+ (* prove reach lemmas *)
+ fun prove_reach_lemma ((chain_take, lub_take), dname) thy =
+ let
+ val thm =
+ Drule.export_without_context
+ (@{thm lub_ID_reach} OF [chain_take, lub_take]);
+ in
+ add_qualified_thm "reach" (dname, thm) thy
+ end;
+ val (reach_thms, thy) =
+ fold_map prove_reach_lemma
+ (chain_take_thms ~~ lub_take_thms ~~ dnames) thy;
+
+ (* test for finiteness of domain definitions *)
+ local
+ val types = [@{type_name ssum}, @{type_name sprod}];
+ fun finite d T = if T mem absTs then d else finite' d T
+ and finite' d (Type (c, Ts)) =
+ let val d' = d andalso c mem types;
+ in forall (finite d') Ts end
+ | finite' d _ = true;
+ in
+ val is_finite = forall (finite true) repTs;
+ end;
+
+ val ((finite_thms, take_induct_thms), thy) =
+ if is_finite
+ then
+ let
+ val ((finites, take_inducts), thy) =
+ prove_finite_take_induct spec take_info lub_take_thms thy;
+ in
+ ((SOME finites, take_inducts), thy)
+ end
+ else
+ let
+ fun prove_take_induct (chain_take, lub_take) =
+ Drule.export_without_context
+ (@{thm lub_ID_take_induct} OF [chain_take, lub_take]);
+ val take_inducts =
+ map prove_take_induct (chain_take_thms ~~ lub_take_thms);
+ val thy = fold (snd oo add_qualified_thm "take_induct")
+ (dnames ~~ take_inducts) thy;
+ in
+ ((NONE, take_inducts), thy)
+ end;
+
+ val result =
+ {
+ take_consts = #take_consts take_info,
+ take_defs = #take_defs take_info,
+ chain_take_thms = #chain_take_thms take_info,
+ take_0_thms = #take_0_thms take_info,
+ take_Suc_thms = #take_Suc_thms take_info,
+ deflation_take_thms = #deflation_take_thms take_info,
+ finite_consts = #finite_consts take_info,
+ finite_defs = #finite_defs take_info,
+ lub_take_thms = lub_take_thms,
+ reach_thms = reach_thms,
+ take_lemma_thms = take_lemma_thms,
+ is_finite = is_finite,
+ take_induct_thms = take_induct_thms
+ };
+ in
+ (result, thy)
+ end;
+
end;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 08 17:37:09 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 08 15:20:40 2010 -0800
@@ -15,7 +15,11 @@
-> Domain_Take_Proofs.iso_info
-> theory -> thm list * theory;
- val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
+ val comp_theorems :
+ bstring * Domain_Library.eq list ->
+ Domain_Take_Proofs.take_induct_info ->
+ theory -> thm list * theory
+
val quiet_mode: bool Unsynchronized.ref;
val trace_domain: bool Unsynchronized.ref;
end;
@@ -204,15 +208,14 @@
fun prove_induction
(comp_dnam, eqs : eq list)
- (take_lemmas : thm list)
- (axs_reach : thm list)
(take_rews : thm list)
+ (take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
let
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
fun dc_take dn = %%:(dn^"_take");
- val x_name = idx_name dnames "x";
+ val x_name = idx_name dnames "x";
val P_name = idx_name dnames "P";
val pg = pg' thy;
@@ -222,15 +225,15 @@
in
val axs_rep_iso = map (ga "rep_iso") dnames;
val axs_abs_iso = map (ga "abs_iso") dnames;
- val axs_chain_take = map (ga "chain_take") dnames;
- val lub_take_thms = map (ga "lub_take") dnames;
- val axs_finite_def = map (ga "finite_def") dnames;
- val take_0_thms = map (ga "take_0") dnames;
- val take_Suc_thms = map (ga "take_Suc") dnames;
val cases = map (ga "casedist" ) dnames;
val con_rews = maps (gts "con_rews" ) dnames;
end;
+ val {take_consts, ...} = take_info;
+ val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info;
+ val {lub_take_thms, finite_defs, reach_thms, ...} = take_info;
+ val {take_induct_thms, ...} = take_info;
+
fun one_con p (con, args) =
let
val P_names = map P_name (1 upto (length dnames));
@@ -281,7 +284,7 @@
in
val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
val is_emptys = map warn n__eqs;
- val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
+ val is_finite = #is_finite take_info;
val _ = if is_finite
then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
else ();
@@ -317,78 +320,32 @@
in
tacs1 @ maps cases_tacs (conss ~~ cases)
end;
- in pg'' thy [] goal tacf
- handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI)
- end;
+ in pg'' thy [] goal tacf end;
(* ----- theorems concerning finiteness and induction ----------------------- *)
val global_ctxt = ProofContext.init thy;
- val _ = trace " Proving finites, ind...";
- val (finites, ind) =
- (
+ val _ = trace " Proving ind...";
+ val ind =
if is_finite
then (* finite case *)
let
- val decisive_lemma =
- let
- val iso_locale_thms =
- map2 (fn x => fn y => @{thm iso.intro} OF [x, y])
- axs_abs_iso axs_rep_iso;
- val decisive_abs_rep_thms =
- map (fn x => @{thm decisive_abs_rep} OF [x])
- iso_locale_thms;
- val n = Free ("n", @{typ nat});
- fun mk_decisive t = %%: @{const_name decisive} $ t;
- fun f dn = mk_decisive (dc_take dn $ n);
- val goal = mk_trp (foldr1 mk_conj (map f dnames));
- val rules0 = @{thm decisive_bottom} :: take_0_thms;
- val rules1 =
- take_Suc_thms @ decisive_abs_rep_thms
- @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
- val tacs = [
- rtac @{thm nat.induct} 1,
- simp_tac (HOL_ss addsimps rules0) 1,
- asm_simp_tac (HOL_ss addsimps rules1) 1];
- in pg [] goal (K tacs) end;
- fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
- fun one_finite (dn, decisive_thm) =
+ fun concf n dn = %:(P_name n) $ %:(x_name n);
+ fun tacf {prems, context} =
let
- val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
- val tacs = [
- rtac @{thm lub_ID_finite} 1,
- resolve_tac axs_chain_take 1,
- resolve_tac lub_take_thms 1,
- rtac decisive_thm 1];
- in pg axs_finite_def goal (K tacs) end;
-
- val _ = trace " Proving finites";
- val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma);
- val _ = trace " Proving ind";
- val ind =
- let
- fun concf n dn = %:(P_name n) $ %:(x_name n);
- fun tacf {prems, context} =
- let
- fun finite_tacs (finite, fin_ind) = [
- rtac(rewrite_rule axs_finite_def finite RS exE)1,
- etac subst 1,
- rtac fin_ind 1,
- ind_prems_tac prems];
- in
- TRY (safe_tac HOL_cs) ::
- maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
- end;
- in pg'' thy [] (ind_term concf) tacf end;
- in (finites, ind) end (* let *)
+ fun finite_tacs (take_induct, fin_ind) = [
+ rtac take_induct 1,
+ rtac fin_ind 1,
+ ind_prems_tac prems];
+ in
+ TRY (safe_tac HOL_cs) ::
+ maps finite_tacs (take_induct_thms ~~ atomize global_ctxt finite_ind)
+ end;
+ in pg'' thy [] (ind_term concf) tacf end
else (* infinite case *)
let
- fun one_finite n dn =
- read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
- val finites = mapn one_finite 1 dnames;
-
val goal =
let
fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
@@ -398,33 +355,36 @@
@{thms 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;
+ let
+ val Ts = map (Type o fst) eqs;
+ val P_names = Datatype_Prop.indexify_names (map (K "P") dnames);
+ val x_names = Datatype_Prop.indexify_names (map (K "x") dnames);
+ val P_types = map (fn T => T --> HOLogic.boolT) Ts;
+ val Ps = map Free (P_names ~~ P_types);
+ val xs = map Free (x_names ~~ Ts);
+ val n = Free ("n", HOLogic.natT);
+ val goals =
+ map (fn ((P,t),x) => P $ HOLCF_Library.mk_capply (t $ n, x))
+ (Ps ~~ take_consts ~~ xs);
+ in
+ HOLogic.mk_Trueprop
+ (HOLogic.mk_all ("n", HOLogic.natT, foldr1 HOLogic.mk_conj goals))
+ end;
fun tacf {prems, context} =
let
val subtac =
EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
- val subthm = Goal.prove context [] [] subgoal' (K subtac);
+ val subthm = Goal.prove context [] [] subgoal (K subtac);
in
- map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
+ map (fn ax_reach => rtac (ax_reach RS subst) 1) reach_thms @ [
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,
+ resolve_tac chain_take_thms 1,
asm_simp_tac HOL_basic_ss 1])
]
end;
- val ind = (pg'' thy [] goal tacf
- handle ERROR _ =>
- (warning "Cannot prove infinite induction rule"; TrueI)
- );
- in (finites, ind) end
- )
- handle THM _ =>
- (warning "Induction proofs failed (THM raised)."; ([], TrueI))
- | ERROR _ =>
- (warning "Cannot prove induction rule"; ([], TrueI));
+ in pg'' thy [] goal tacf end;
val case_ns =
let
@@ -440,15 +400,11 @@
((Binding.empty, [rule]),
[Rule_Cases.case_names case_ns, Induct.induct_type dname]);
-val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
-
in thy |> Sign.add_path comp_dnam
|> snd o PureThy.add_thmss [
- ((Binding.name "finites" , finites ), []),
((Binding.name "finite_ind" , [finite_ind]), []),
((Binding.name "ind" , [ind] ), [])]
- |> (if induct_failed then I
- else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
+ |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
|> Sign.parent_path
end; (* prove_induction *)
@@ -604,7 +560,10 @@
|> Sign.parent_path
end; (* let *)
-fun comp_theorems (comp_dnam, eqs: eq list) thy =
+fun comp_theorems
+ (comp_dnam : string, eqs : eq list)
+ (take_info : Domain_Take_Proofs.take_induct_info)
+ (thy : theory) =
let
val map_tab = Domain_Take_Proofs.get_map_tab thy;
@@ -629,31 +588,7 @@
(* theorems about take *)
-local
- fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
- val axs_chain_take = map (ga "chain_take") dnames;
- val axs_lub_take = map (ga "lub_take" ) dnames;
- fun take_thms ((ax_chain_take, ax_lub_take), dname) thy =
- let
- val dnam = Long_Name.base_name dname;
- val take_lemma =
- Drule.export_without_context
- (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
- val reach =
- Drule.export_without_context
- (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
- val thy =
- thy |> Sign.add_path dnam
- |> snd o PureThy.add_thms [
- ((Binding.name "take_lemma", take_lemma), []),
- ((Binding.name "reach" , reach ), [])]
- |> Sign.parent_path;
- in ((take_lemma, reach), thy) end;
-in
- val ((take_lemmas, axs_reach), thy) =
- fold_map take_thms (axs_chain_take ~~ axs_lub_take ~~ dnames) thy
- |>> ListPair.unzip;
-end;
+val take_lemmas = #take_lemma_thms take_info;
val take_rews =
maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
@@ -661,7 +596,7 @@
(* prove induction rules, unless definition is indirect recursive *)
val thy =
if is_indirect then thy else
- prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews thy;
+ prove_induction (comp_dnam, eqs) take_rews take_info thy;
val thy =
if is_indirect then thy else
--- a/src/HOLCF/ex/Domain_ex.thy Mon Mar 08 17:37:09 2010 +0100
+++ b/src/HOLCF/ex/Domain_ex.thy Mon Mar 08 15:20:40 2010 -0800
@@ -107,7 +107,7 @@
subsection {* Generated constants and theorems *}
-domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (lazy right :: "'a tree")
+domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
lemmas tree_abs_defined_iff =
iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
@@ -174,7 +174,7 @@
text {* Rules about finiteness predicate *}
term tree_finite
thm tree.finite_def
-thm tree.finites
+thm tree.finite (* only generated for flat datatypes *)
text {* Rules about bisimulation predicate *}
term tree_bisim
@@ -196,14 +196,6 @@
-- {* Inner syntax error at "= UU" *}
*)
-text {*
- I don't know what is going on here. The failed proof has to do with
- the finiteness predicate.
-*}
-
-domain foo = Foo (lazy "bar") and bar = Bar
- -- "Cannot prove induction rule"
-
text {* Declaring class constraints on the LHS is currently broken. *}
(*
domain ('a::cpo) box = Box (lazy 'a)