--- a/src/HOL/BNF_Comp.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Mon Mar 10 23:03:51 2014 +0100
@@ -147,6 +147,9 @@
definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
+lemma id_bnf_comp_apply: "id_bnf_comp x = x"
+ unfolding id_bnf_comp_def by simp
+
bnf ID: 'a
map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
sets: "\<lambda>x. {x}"
--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy Mon Mar 10 23:03:51 2014 +0100
@@ -22,8 +22,8 @@
(? d. ft\<cdot>s=Def(Md d)) & (rt\<cdot>s=<> | ft\<cdot>(rt\<cdot>s)=Def \<bullet> & rt\<cdot>(rt\<cdot>s):A))"
by (unfold BufAC_Asm_F_def, auto)
-lemma cont_BufAC_Asm_F: "down_cont BufAC_Asm_F"
-by (auto simp add: down_cont_def BufAC_Asm_F_def3)
+lemma cont_BufAC_Asm_F: "down_continuous BufAC_Asm_F"
+by (auto simp add: down_continuous_def BufAC_Asm_F_def3)
lemma BufAC_Cmt_F_def3:
"((s,t):BufAC_Cmt_F C) = (!d x.
@@ -37,8 +37,8 @@
apply (auto intro: surjectiv_scons [symmetric])
done
-lemma cont_BufAC_Cmt_F: "down_cont BufAC_Cmt_F"
-by (auto simp add: down_cont_def BufAC_Cmt_F_def3)
+lemma cont_BufAC_Cmt_F: "down_continuous BufAC_Cmt_F"
+by (auto simp add: down_continuous_def BufAC_Cmt_F_def3)
(**** adm_BufAC_Asm ***********************************************************)
@@ -117,8 +117,8 @@
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> enat (l i) < #x -->
- (x,f\<cdot>x):down_iterate BufAC_Cmt_F i -->
- (s,f\<cdot>s):down_iterate BufAC_Cmt_F i"
+ (x,f\<cdot>x):(BufAC_Cmt_F ^^ i) top -->
+ (s,f\<cdot>s):(BufAC_Cmt_F ^^ i) top"
apply (rule_tac x="%i. 2*i" in exI)
apply (rule allI)
apply (induct_tac "i")
@@ -182,9 +182,9 @@
apply assumption
done
-lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>down_iterate BufAC_Cmt_F n)"
+lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>(BufAC_Cmt_F ^^ n) top)"
apply (unfold BufAC_Cmt_def)
-apply (subst cont_BufAC_Cmt_F [THEN INTER_down_iterate_is_gfp])
+apply (subst cont_BufAC_Cmt_F [THEN down_continuous_gfp])
apply (fast)
done
--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy Mon Mar 10 23:03:51 2014 +0100
@@ -5,7 +5,7 @@
header {* Admissibility for streams *}
theory Stream_adm
-imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Continuity"
+imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Order_Continuity"
begin
definition
@@ -93,7 +93,7 @@
lemma stream_monoP2I:
"!!X. stream_monoP F ==> !i. ? l. !x y.
- enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"
+ enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top"
apply (unfold stream_monoP_def)
apply (safe)
apply (rule_tac x="i*ia" in exI)
@@ -120,9 +120,9 @@
done
lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y.
- enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;
- down_cont F |] ==> adm (%x. x:gfp F)"
-apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *)
+ enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top;
+ down_continuous F |] ==> adm (%x. x:gfp F)"
+apply (erule down_continuous_gfp[of F, THEN ssubst])
apply (simp (no_asm))
apply (rule adm_lemmas)
apply (rule flatstream_admI)
@@ -144,7 +144,7 @@
lemma stream_antiP2I:
"!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]
- ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i"
+ ==> !i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top"
apply (unfold stream_antiP_def)
apply (rule allI)
apply (induct_tac "i")
@@ -170,10 +170,10 @@
done
lemma stream_antiP2_non_gfp_admI:
-"!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |]
+"!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; down_continuous F |]
==> adm (%u. ~ u:gfp F)"
apply (unfold adm_def)
-apply (simp add: INTER_down_iterate_is_gfp)
+apply (simp add: down_continuous_gfp)
apply (fast dest!: is_ub_thelub)
done
--- a/src/HOL/Library/Continuity.thy Mon Mar 10 23:03:15 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,297 +0,0 @@
-(* Title: HOL/Library/Continuity.thy
- Author: David von Oheimb, TU Muenchen
-*)
-
-header {* Continuity and iterations (of set transformers) *}
-
-theory Continuity
-imports Main
-begin
-
-subsection {* Continuity for complete lattices *}
-
-definition
- chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
- "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
-
-definition
- continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
- "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
-
-lemma SUP_nat_conv:
- fixes M :: "nat \<Rightarrow> 'a::complete_lattice"
- shows "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
-apply(rule order_antisym)
- apply(rule SUP_least)
- apply(case_tac n)
- apply simp
- apply (fast intro:SUP_upper le_supI2)
-apply(simp)
-apply (blast intro:SUP_least SUP_upper)
-done
-
-lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
- assumes "continuous F" shows "mono F"
-proof
- fix A B :: "'a" assume "A <= B"
- let ?C = "%i::nat. if i=0 then A else B"
- have "chain ?C" using `A <= B` by(simp add:chain_def)
- have "F B = sup (F A) (F B)"
- proof -
- have "sup A B = B" using `A <= B` by (simp add:sup_absorb2)
- hence "F B = F(SUP i. ?C i)" by (subst SUP_nat_conv) simp
- also have "\<dots> = (SUP i. F(?C i))"
- using `chain ?C` `continuous F` by(simp add:continuous_def)
- also have "\<dots> = sup (F A) (F B)" by (subst SUP_nat_conv) simp
- finally show ?thesis .
- qed
- thus "F A \<le> F B" by(subst le_iff_sup, simp)
-qed
-
-lemma continuous_lfp:
- assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)"
-proof -
- note mono = continuous_mono[OF `continuous F`]
- { fix i have "(F ^^ i) bot \<le> lfp F"
- proof (induct i)
- show "(F ^^ 0) bot \<le> lfp F" by simp
- next
- case (Suc i)
- have "(F ^^ Suc i) bot = F((F ^^ i) bot)" by simp
- also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
- also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
- finally show ?case .
- qed }
- hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_least)
- moreover have "lfp F \<le> (SUP i. (F ^^ i) bot)" (is "_ \<le> ?U")
- proof (rule lfp_lowerbound)
- have "chain(%i. (F ^^ i) bot)"
- proof -
- { fix i have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
- proof (induct i)
- case 0 show ?case by simp
- next
- case Suc thus ?case using monoD[OF mono Suc] by auto
- qed }
- thus ?thesis by(auto simp add:chain_def)
- qed
- hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
- also have "\<dots> \<le> ?U" by(fast intro:SUP_least SUP_upper)
- finally show "F ?U \<le> ?U" .
- qed
- ultimately show ?thesis by (blast intro:order_antisym)
-qed
-
-text{* The following development is just for sets but presents an up
-and a down version of chains and continuity and covers @{const gfp}. *}
-
-
-subsection "Chains"
-
-definition
- up_chain :: "(nat => 'a set) => bool" where
- "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
-
-lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
- by (simp add: up_chain_def)
-
-lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
- by (simp add: up_chain_def)
-
-lemma up_chain_less_mono:
- "up_chain F ==> x < y ==> F x \<subseteq> F y"
- apply (induct y)
- apply (blast dest: up_chainD elim: less_SucE)+
- done
-
-lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
- apply (drule le_imp_less_or_eq)
- apply (blast dest: up_chain_less_mono)
- done
-
-
-definition
- down_chain :: "(nat => 'a set) => bool" where
- "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
-
-lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
- by (simp add: down_chain_def)
-
-lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
- by (simp add: down_chain_def)
-
-lemma down_chain_less_mono:
- "down_chain F ==> x < y ==> F y \<subseteq> F x"
- apply (induct y)
- apply (blast dest: down_chainD elim: less_SucE)+
- done
-
-lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
- apply (drule le_imp_less_or_eq)
- apply (blast dest: down_chain_less_mono)
- done
-
-
-subsection "Continuity"
-
-definition
- up_cont :: "('a set => 'a set) => bool" where
- "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
-
-lemma up_contI:
- "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
-apply (unfold up_cont_def)
-apply blast
-done
-
-lemma up_contD:
- "up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)"
-apply (unfold up_cont_def)
-apply auto
-done
-
-
-lemma up_cont_mono: "up_cont f ==> mono f"
-apply (rule monoI)
-apply (drule_tac F = "\<lambda>i. if i = 0 then x else y" in up_contD)
- apply (rule up_chainI)
- apply simp
-apply (drule Un_absorb1)
-apply (auto split:split_if_asm)
-done
-
-
-definition
- down_cont :: "('a set => 'a set) => bool" where
- "down_cont f =
- (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
-
-lemma down_contI:
- "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
- down_cont f"
- apply (unfold down_cont_def)
- apply blast
- done
-
-lemma down_contD: "down_cont f ==> down_chain F ==>
- f (Inter (range F)) = Inter (f ` range F)"
- apply (unfold down_cont_def)
- apply auto
- done
-
-lemma down_cont_mono: "down_cont f ==> mono f"
-apply (rule monoI)
-apply (drule_tac F = "\<lambda>i. if i = 0 then y else x" in down_contD)
- apply (rule down_chainI)
- apply simp
-apply (drule Int_absorb1)
-apply (auto split:split_if_asm)
-done
-
-
-subsection "Iteration"
-
-definition
- up_iterate :: "('a set => 'a set) => nat => 'a set" where
- "up_iterate f n = (f ^^ n) {}"
-
-lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
- by (simp add: up_iterate_def)
-
-lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)"
- by (simp add: up_iterate_def)
-
-lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)"
- apply (rule up_chainI)
- apply (induct_tac i)
- apply simp+
- apply (erule (1) monoD)
- done
-
-lemma UNION_up_iterate_is_fp:
- "up_cont F ==>
- F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
- apply (frule up_cont_mono [THEN up_iterate_chain])
- apply (drule (1) up_contD)
- apply simp
- apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
- apply (case_tac xa)
- apply auto
- done
-
-lemma UNION_up_iterate_lowerbound:
- "mono F ==> F P = P ==> UNION UNIV (up_iterate F) \<subseteq> P"
- apply (subgoal_tac "(!!i. up_iterate F i \<subseteq> P)")
- apply fast
- apply (induct_tac i)
- prefer 2 apply (drule (1) monoD)
- apply auto
- done
-
-lemma UNION_up_iterate_is_lfp:
- "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
- apply (rule set_eq_subset [THEN iffD2])
- apply (rule conjI)
- prefer 2
- apply (drule up_cont_mono)
- apply (rule UNION_up_iterate_lowerbound)
- apply assumption
- apply (erule lfp_unfold [symmetric])
- apply (rule lfp_lowerbound)
- apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
- apply (erule UNION_up_iterate_is_fp [symmetric])
- done
-
-
-definition
- down_iterate :: "('a set => 'a set) => nat => 'a set" where
- "down_iterate f n = (f ^^ n) UNIV"
-
-lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
- by (simp add: down_iterate_def)
-
-lemma down_iterate_Suc [simp]:
- "down_iterate f (Suc i) = f (down_iterate f i)"
- by (simp add: down_iterate_def)
-
-lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)"
- apply (rule down_chainI)
- apply (induct_tac i)
- apply simp+
- apply (erule (1) monoD)
- done
-
-lemma INTER_down_iterate_is_fp:
- "down_cont F ==>
- F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
- apply (frule down_cont_mono [THEN down_iterate_chain])
- apply (drule (1) down_contD)
- apply simp
- apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
- apply (case_tac xa)
- apply auto
- done
-
-lemma INTER_down_iterate_upperbound:
- "mono F ==> F P = P ==> P \<subseteq> INTER UNIV (down_iterate F)"
- apply (subgoal_tac "(!!i. P \<subseteq> down_iterate F i)")
- apply fast
- apply (induct_tac i)
- prefer 2 apply (drule (1) monoD)
- apply auto
- done
-
-lemma INTER_down_iterate_is_gfp:
- "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
- apply (rule set_eq_subset [THEN iffD2])
- apply (rule conjI)
- apply (drule down_cont_mono)
- apply (rule INTER_down_iterate_upperbound)
- apply assumption
- apply (erule gfp_unfold [symmetric])
- apply (rule gfp_upperbound)
- apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
- apply (erule INTER_down_iterate_is_fp)
- done
-
-end
--- a/src/HOL/Library/Library.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Library/Library.thy Mon Mar 10 23:03:51 2014 +0100
@@ -7,7 +7,6 @@
BNF_Decl
Boolean_Algebra
Char_ord
- Continuity
ContNotDenum
Convex
Countable
@@ -41,6 +40,7 @@
Numeral_Type
OptionalSugar
Option_ord
+ Order_Continuity
Parallel
Permutation
Permutations
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Order_Continuity.thy Mon Mar 10 23:03:51 2014 +0100
@@ -0,0 +1,141 @@
+(* Title: HOL/Library/Order_Continuity.thy
+ Author: David von Oheimb, TU Muenchen
+*)
+
+header {* Continuity and iterations (of set transformers) *}
+
+theory Order_Continuity
+imports Main
+begin
+
+(* TODO: Generalize theory to chain-complete partial orders *)
+
+lemma SUP_nat_binary:
+ "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)"
+ apply (auto intro!: antisym SUP_least)
+ apply (rule SUP_upper2[where i=0])
+ apply simp_all
+ apply (rule SUP_upper2[where i=1])
+ apply simp_all
+ done
+
+lemma INF_nat_binary:
+ "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)"
+ apply (auto intro!: antisym INF_greatest)
+ apply (rule INF_lower2[where i=0])
+ apply simp_all
+ apply (rule INF_lower2[where i=1])
+ apply simp_all
+ done
+
+subsection {* Continuity for complete lattices *}
+
+definition
+ continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
+ "continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
+
+lemma continuousD: "continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
+ by (auto simp: continuous_def)
+
+lemma continuous_mono:
+ fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
+ assumes [simp]: "continuous F" shows "mono F"
+proof
+ fix A B :: "'a" assume [simp]: "A \<le> B"
+ have "F B = F (SUP n::nat. if n = 0 then A else B)"
+ by (simp add: sup_absorb2 SUP_nat_binary)
+ also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
+ by (auto simp: continuousD mono_def intro!: SUP_cong)
+ finally show "F A \<le> F B"
+ by (simp add: SUP_nat_binary le_iff_sup)
+qed
+
+lemma continuous_lfp:
+ assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
+proof (rule antisym)
+ note mono = continuous_mono[OF `continuous F`]
+ show "?U \<le> lfp F"
+ proof (rule SUP_least)
+ fix i show "(F ^^ i) bot \<le> lfp F"
+ proof (induct i)
+ case (Suc i)
+ have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
+ also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
+ also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
+ finally show ?case .
+ qed simp
+ qed
+ show "lfp F \<le> ?U"
+ proof (rule lfp_lowerbound)
+ have "mono (\<lambda>i::nat. (F ^^ i) bot)"
+ proof -
+ { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
+ proof (induct i)
+ case 0 show ?case by simp
+ next
+ case Suc thus ?case using monoD[OF mono Suc] by auto
+ qed }
+ thus ?thesis by (auto simp add: mono_iff_le_Suc)
+ qed
+ hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using `continuous F` by (simp add: continuous_def)
+ also have "\<dots> \<le> ?U" by (fast intro: SUP_least SUP_upper)
+ finally show "F ?U \<le> ?U" .
+ qed
+qed
+
+definition
+ down_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
+ "down_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
+
+lemma down_continuousD: "down_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
+ by (auto simp: down_continuous_def)
+
+lemma down_continuous_mono:
+ fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
+ assumes [simp]: "down_continuous F" shows "mono F"
+proof
+ fix A B :: "'a" assume [simp]: "A \<le> B"
+ have "F A = F (INF n::nat. if n = 0 then B else A)"
+ by (simp add: inf_absorb2 INF_nat_binary)
+ also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
+ by (auto simp: down_continuousD antimono_def intro!: INF_cong)
+ finally show "F A \<le> F B"
+ by (simp add: INF_nat_binary le_iff_inf inf_commute)
+qed
+
+lemma down_continuous_gfp:
+ assumes "down_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
+proof (rule antisym)
+ note mono = down_continuous_mono[OF `down_continuous F`]
+ show "gfp F \<le> ?U"
+ proof (rule INF_greatest)
+ fix i show "gfp F \<le> (F ^^ i) top"
+ proof (induct i)
+ case (Suc i)
+ have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
+ also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
+ also have "\<dots> = (F ^^ Suc i) top" by simp
+ finally show ?case .
+ qed simp
+ qed
+ show "?U \<le> gfp F"
+ proof (rule gfp_upperbound)
+ have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
+ proof -
+ { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
+ proof (induct i)
+ case 0 show ?case by simp
+ next
+ case Suc thus ?case using monoD[OF mono Suc] by auto
+ qed }
+ thus ?thesis by (auto simp add: antimono_iff_le_Suc)
+ qed
+ have "?U \<le> (INF i. (F ^^ Suc i) top)"
+ by (fast intro: INF_greatest INF_lower)
+ also have "\<dots> \<le> F ?U"
+ by (simp add: down_continuousD `down_continuous F` *)
+ finally show "?U \<le> F ?U" .
+ qed
+qed
+
+end
--- a/src/HOL/Library/RBT.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Library/RBT.thy Mon Mar 10 23:03:51 2014 +0100
@@ -36,7 +36,6 @@
subsection {* Primitive operations *}
setup_lifting type_definition_rbt
-print_theorems
lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" .
@@ -187,4 +186,14 @@
quickcheck_generator rbt predicate: is_rbt constructors: empty, insert
+subsection {* Hide implementation details *}
+
+lifting_update rbt.lifting
+lifting_forget rbt.lifting
+
+hide_const (open) impl_of empty lookup keys entries bulkload delete map fold union insert map_entry foldi
+ is_empty
+hide_fact (open) empty_def lookup_def keys_def entries_def bulkload_def delete_def map_def fold_def
+ union_def insert_def map_entry_def foldi_def is_empty_def
+
end
--- a/src/HOL/Library/RBT_Mapping.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Library/RBT_Mapping.thy Mon Mar 10 23:03:51 2014 +0100
@@ -11,42 +11,46 @@
subsection {* Implementation of mappings *}
-lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is lookup .
+context includes rbt.lifting begin
+lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is RBT.lookup .
+end
code_datatype Mapping
+context includes rbt.lifting begin
+
lemma lookup_Mapping [simp, code]:
- "Mapping.lookup (Mapping t) = lookup t"
+ "Mapping.lookup (Mapping t) = RBT.lookup t"
by (transfer fixing: t) rule
-lemma empty_Mapping [code]: "Mapping.empty = Mapping empty"
+lemma empty_Mapping [code]: "Mapping.empty = Mapping RBT.empty"
proof -
note RBT.empty.transfer[transfer_rule del]
show ?thesis by transfer simp
qed
lemma is_empty_Mapping [code]:
- "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
+ "Mapping.is_empty (Mapping t) \<longleftrightarrow> RBT.is_empty t"
unfolding is_empty_def by (transfer fixing: t) simp
lemma insert_Mapping [code]:
- "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
+ "Mapping.update k v (Mapping t) = Mapping (RBT.insert k v t)"
by (transfer fixing: t) simp
lemma delete_Mapping [code]:
- "Mapping.delete k (Mapping t) = Mapping (delete k t)"
+ "Mapping.delete k (Mapping t) = Mapping (RBT.delete k t)"
by (transfer fixing: t) simp
lemma map_entry_Mapping [code]:
- "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
- apply (transfer fixing: t) by (case_tac "lookup t k") auto
+ "Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)"
+ apply (transfer fixing: t) by (case_tac "RBT.lookup t k") auto
lemma keys_Mapping [code]:
- "Mapping.keys (Mapping t) = set (keys t)"
+ "Mapping.keys (Mapping t) = set (RBT.keys t)"
by (transfer fixing: t) (simp add: lookup_keys)
lemma ordered_keys_Mapping [code]:
- "Mapping.ordered_keys (Mapping t) = keys t"
+ "Mapping.ordered_keys (Mapping t) = RBT.keys t"
unfolding ordered_keys_def
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique)
@@ -55,7 +59,7 @@
unfolding size_def by transfer simp
lemma size_Mapping [code]:
- "Mapping.size (Mapping t) = length (keys t)"
+ "Mapping.size (Mapping t) = length (RBT.keys t)"
unfolding size_def
by (transfer fixing: t) (simp add: lookup_keys distinct_card)
@@ -63,25 +67,24 @@
notes RBT.bulkload.transfer[transfer_rule del]
begin
lemma tabulate_Mapping [code]:
- "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
+ "Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\<lambda>k. (k, f k)) ks))"
by transfer (simp add: map_of_map_restrict)
lemma bulkload_Mapping [code]:
- "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
+ "Mapping.bulkload vs = Mapping (RBT.bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
by transfer (simp add: map_of_map_restrict fun_eq_iff)
end
lemma equal_Mapping [code]:
- "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
+ "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> RBT.entries t1 = RBT.entries t2"
by (transfer fixing: t1 t2) (simp add: entries_lookup)
lemma [code nbe]:
"HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
by (fact equal_refl)
+end
-hide_const (open) impl_of lookup empty insert delete
- entries keys bulkload map_entry map fold
(*>*)
text {*
--- a/src/HOL/Library/RBT_Set.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Library/RBT_Set.thy Mon Mar 10 23:03:51 2014 +0100
@@ -19,7 +19,7 @@
section {* Definition of code datatype constructors *}
definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
- where "Set t = {x . lookup t x = Some ()}"
+ where "Set t = {x . RBT.lookup t x = Some ()}"
definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
where [simp]: "Coset t = - Set t"
@@ -146,31 +146,31 @@
lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
by (auto simp: not_Some_eq[THEN iffD1])
-lemma Set_set_keys: "Set x = dom (lookup x)"
+lemma Set_set_keys: "Set x = dom (RBT.lookup x)"
by (auto simp: Set_def)
lemma finite_Set [simp, intro!]: "finite (Set x)"
by (simp add: Set_set_keys)
-lemma set_keys: "Set t = set(keys t)"
+lemma set_keys: "Set t = set(RBT.keys t)"
by (simp add: Set_set_keys lookup_keys)
subsection {* fold and filter *}
lemma finite_fold_rbt_fold_eq:
assumes "comp_fun_commute f"
- shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
+ shows "Finite_Set.fold f A (set (RBT.entries t)) = RBT.fold (curry f) t A"
proof -
- have *: "remdups (entries t) = entries t"
+ have *: "remdups (RBT.entries t) = RBT.entries t"
using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
qed
definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b"
- where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"
+ where [code_unfold]:"fold_keys f t A = RBT.fold (\<lambda>k _ t. f k t) t A"
lemma fold_keys_def_alt:
- "fold_keys f t s = List.fold f (keys t) s"
+ "fold_keys f t s = List.fold f (RBT.keys t) s"
by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)
lemma finite_fold_fold_keys:
@@ -179,15 +179,15 @@
using assms
proof -
interpret comp_fun_commute f by fact
- have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries)
- moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto
+ have "set (RBT.keys t) = fst ` (set (RBT.entries t))" by (auto simp: fst_eq_Domain keys_entries)
+ moreover have "inj_on fst (set (RBT.entries t))" using distinct_entries distinct_map by auto
ultimately show ?thesis
by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq
comp_comp_fun_commute)
qed
definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
- "rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
+ "rbt_filter P t = RBT.fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
lemma Set_filter_rbt_filter:
"Set.filter P (Set t) = rbt_filter P t"
@@ -207,8 +207,8 @@
by (cases "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t1 True") (simp_all add: Ball_False)
qed simp
-lemma foldi_fold_conj: "foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
-unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj)
+lemma foldi_fold_conj: "RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
+unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_conj)
subsection {* foldi and Bex *}
@@ -223,8 +223,8 @@
by (cases "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t1 False") (simp_all add: Bex_True)
qed simp
-lemma foldi_fold_disj: "foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
-unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj)
+lemma foldi_fold_disj: "RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
+unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_disj)
subsection {* folding over non empty trees and selecting the minimal and maximal element *}
@@ -422,16 +422,17 @@
(** abstract **)
+context includes rbt.lifting begin
lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
is rbt_fold1_keys .
lemma fold1_keys_def_alt:
- "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
+ "fold1_keys f t = List.fold f (tl (RBT.keys t)) (hd (RBT.keys t))"
by transfer (simp add: rbt_fold1_keys_def)
lemma finite_fold1_fold1_keys:
assumes "semilattice f"
- assumes "\<not> is_empty t"
+ assumes "\<not> RBT.is_empty t"
shows "semilattice_set.F f (Set t) = fold1_keys f t"
proof -
from `semilattice f` interpret semilattice_set f by (rule semilattice_set.intro)
@@ -449,13 +450,13 @@
by transfer (simp add: rbt_min_def)
lemma r_min_eq_r_min_opt:
- assumes "\<not> (is_empty t)"
+ assumes "\<not> (RBT.is_empty t)"
shows "r_min t = r_min_opt t"
using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
lemma fold_keys_min_top_eq:
fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
- assumes "\<not> (is_empty t)"
+ assumes "\<not> (RBT.is_empty t)"
shows "fold_keys min t top = fold1_keys min t"
proof -
have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top =
@@ -487,13 +488,13 @@
by transfer (simp add: rbt_max_def)
lemma r_max_eq_r_max_opt:
- assumes "\<not> (is_empty t)"
+ assumes "\<not> (RBT.is_empty t)"
shows "r_max t = r_max_opt t"
using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
lemma fold_keys_max_bot_eq:
fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
- assumes "\<not> (is_empty t)"
+ assumes "\<not> (RBT.is_empty t)"
shows "fold_keys max t bot = fold1_keys max t"
proof -
have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot =
@@ -515,6 +516,7 @@
done
qed
+end
section {* Code equations *}
@@ -584,7 +586,7 @@
qed
lemma union_Set_Set [code]:
- "Set t1 \<union> Set t2 = Set (union t1 t2)"
+ "Set t1 \<union> Set t2 = Set (RBT.union t1 t2)"
by (auto simp add: lookup_union map_add_Some_iff Set_def)
lemma inter_Coset [code]:
@@ -592,7 +594,7 @@
by (simp add: Diff_eq [symmetric] minus_Set)
lemma inter_Coset_Coset [code]:
- "Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
+ "Coset t1 \<inter> Coset t2 = Coset (RBT.union t1 t2)"
by (auto simp add: lookup_union map_add_Some_iff Set_def)
lemma minus_Coset [code]:
@@ -611,7 +613,7 @@
qed
lemma Ball_Set [code]:
- "Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
+ "Ball (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
proof -
have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
then show ?thesis
@@ -619,7 +621,7 @@
qed
lemma Bex_Set [code]:
- "Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
+ "Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
proof -
have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
then show ?thesis
@@ -632,11 +634,11 @@
by auto
lemma subset_Coset_empty_Set_empty [code]:
- "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of
+ "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (RBT.impl_of t1, RBT.impl_of t2) of
(rbt.Empty, rbt.Empty) => False |
(_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))"
proof -
- have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
+ have *: "\<And>t. RBT.impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
show ?thesis
@@ -645,7 +647,7 @@
text {* A frequent case – avoid intermediate sets *}
lemma [code_unfold]:
- "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
+ "Set t1 \<subseteq> Set t2 \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
by (simp add: subset_code Ball_Set)
lemma card_Set [code]:
@@ -662,7 +664,7 @@
lemma the_elem_set [code]:
fixes t :: "('a :: linorder, unit) rbt"
- shows "the_elem (Set t) = (case impl_of t of
+ shows "the_elem (Set t) = (case RBT.impl_of t of
(Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
| _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))"
proof -
@@ -672,7 +674,7 @@
have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
- have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x"
+ have "RBT.impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x"
by (subst(asm) RBT_inverse[symmetric, OF *])
(auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
}
@@ -726,7 +728,7 @@
lemma Min_fin_set_fold [code]:
"Min (Set t) =
- (if is_empty t
+ (if RBT.is_empty t
then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t))
else r_min_opt t)"
proof -
@@ -742,10 +744,10 @@
lemma Inf_Set_fold:
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
- shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
+ shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
proof -
have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
- then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
+ then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
then show ?thesis
by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
@@ -767,7 +769,7 @@
lemma Max_fin_set_fold [code]:
"Max (Set t) =
- (if is_empty t
+ (if RBT.is_empty t
then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t))
else r_max_opt t)"
proof -
@@ -783,10 +785,10 @@
lemma Sup_Set_fold:
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
- shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
+ shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
proof -
have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
- then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
+ then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
then show ?thesis
by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
@@ -807,14 +809,14 @@
qed
lemma sorted_list_set[code]:
- "sorted_list_of_set (Set t) = keys t"
+ "sorted_list_of_set (Set t) = RBT.keys t"
by (auto simp add: set_keys intro: sorted_distinct_set_unique)
lemma Bleast_code [code]:
- "Bleast (Set t) P = (case filter P (keys t) of
+ "Bleast (Set t) P = (case filter P (RBT.keys t) of
x#xs \<Rightarrow> x |
[] \<Rightarrow> abort_Bleast (Set t) P)"
-proof (cases "filter P (keys t)")
+proof (cases "filter P (RBT.keys t)")
case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
next
case (Cons x ys)
@@ -831,7 +833,6 @@
thus ?thesis using Cons by (simp add: Bleast_def)
qed
-
hide_const (open) RBT_Set.Set RBT_Set.Coset
end
--- a/src/HOL/Library/bnf_decl.ML Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Library/bnf_decl.ML Mon Mar 10 23:03:51 2014 +0100
@@ -68,7 +68,7 @@
val Fwits = map2 (fn witb => fn witT =>
Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
- prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads))
+ prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
lthy;
--- a/src/HOL/Nat.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Nat.thy Mon Mar 10 23:03:51 2014 +0100
@@ -1618,6 +1618,15 @@
by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
qed (insert `n \<le> n'`, auto) -- {* trivial for @{prop "n = n'"} *}
+lemma lift_Suc_antimono_le:
+ assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
+ shows "f n \<ge> f n'"
+proof (cases "n < n'")
+ case True
+ then show ?thesis
+ by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
+qed (insert `n \<le> n'`, auto) -- {* trivial for @{prop "n = n'"} *}
+
lemma lift_Suc_mono_less:
assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
shows "f n < f n'"
@@ -1635,6 +1644,10 @@
"mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
+lemma antimono_iff_le_Suc:
+ "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
+ unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])
+
lemma mono_nat_linear_lb:
fixes f :: "nat \<Rightarrow> nat"
assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
--- a/src/HOL/Orderings.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Orderings.thy Mon Mar 10 23:03:51 2014 +0100
@@ -1010,6 +1010,28 @@
from assms show "f x \<le> f y" by (simp add: mono_def)
qed
+definition antimono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
+ "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
+
+lemma antimonoI [intro?]:
+ fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+ shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f"
+ unfolding antimono_def by iprover
+
+lemma antimonoD [dest?]:
+ fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+ shows "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
+ unfolding antimono_def by iprover
+
+lemma antimonoE:
+ fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+ assumes "antimono f"
+ assumes "x \<le> y"
+ obtains "f x \<ge> f y"
+proof
+ from assms show "f x \<ge> f y" by (simp add: antimono_def)
+qed
+
definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
"strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon Mar 10 23:03:51 2014 +0100
@@ -678,7 +678,7 @@
by (auto simp: incseq_Suc_iff le_fun_def image_iff u' intro!: real_of_ereal_positive_mono)
show "\<And>x. (\<lambda>k. u' k x) ----> f' x"
using SUP_eq u(2)
- by (intro SUP_eq_LIMSEQ[THEN iffD1]) (auto simp: u' f' incseq_mono incseq_Suc_iff le_fun_def)
+ by (intro SUP_eq_LIMSEQ[THEN iffD1]) (auto simp: u' f' incseq_Suc_iff le_fun_def)
show "bounded {integral UNIV (u' k)|k. True}"
proof (safe intro!: bounded_realI)
fix k
--- a/src/HOL/Probability/Measurable.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy Mon Mar 10 23:03:51 2014 +0100
@@ -2,9 +2,13 @@
Author: Johannes Hölzl <hoelzl@in.tum.de>
*)
theory Measurable
- imports Sigma_Algebra
+ imports
+ Sigma_Algebra
+ "~~/src/HOL/Library/Order_Continuity"
begin
+hide_const (open) Order_Continuity.continuous
+
subsection {* Measurability prover *}
lemma (in algebra) sets_Collect_finite_All:
@@ -256,6 +260,42 @@
"s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
by simp
+subsection {* Measurability for (co)inductive predicates *}
+
+lemma measurable_lfp:
+ assumes "P = lfp F"
+ assumes "Order_Continuity.continuous F"
+ assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
+ shows "pred M P"
+proof -
+ { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
+ by (induct i) (auto intro!: *) }
+ then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
+ by measurable
+ also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
+ by (auto simp add: bot_fun_def)
+ also have "\<dots> = P"
+ unfolding `P = lfp F` by (rule continuous_lfp[symmetric]) fact
+ finally show ?thesis .
+qed
+
+lemma measurable_gfp:
+ assumes "P = gfp F"
+ assumes "Order_Continuity.down_continuous F"
+ assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
+ shows "pred M P"
+proof -
+ { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
+ by (induct i) (auto intro!: *) }
+ then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
+ by measurable
+ also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
+ by (auto simp add: top_fun_def)
+ also have "\<dots> = P"
+ unfolding `P = gfp F` by (rule down_continuous_gfp[symmetric]) fact
+ finally show ?thesis .
+qed
+
hide_const (open) pred
end
--- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 10 23:03:51 2014 +0100
@@ -338,8 +338,8 @@
(maps wit_thms_of_bnf inners);
val (bnf', lthy') =
- bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
- Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
+ bnf_def const_policy (K Dont_Note) true qualify tacs wit_tac (SOME (oDs @ flat Dss))
+ Binding.empty Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
val phi =
Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def])
@@ -436,8 +436,8 @@
fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
val (bnf', lthy') =
- bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
- Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
+ bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (killedAs @ Ds))
+ Binding.empty Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -526,8 +526,8 @@
fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
val (bnf', lthy') =
- bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
- [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
+ bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
+ Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -607,8 +607,8 @@
fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
val (bnf', lthy') =
- bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
- [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
+ bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
+ Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -765,21 +765,6 @@
|> mk_Frees' "f" (map2 (curry op -->) As Bs)
||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
- val map_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#map_unfolds unfold_set);
- val set_unfoldss = #set_unfoldss unfold_set;
- val rel_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#rel_unfolds unfold_set);
-
- val expand_maps = expand_id_bnf_comp_def o
- fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
- val expand_sets =
- fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
- val expand_rels = expand_id_bnf_comp_def o
- fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
- fun unfold_maps ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: map_unfolds);
- fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
- fun unfold_rels ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: rel_unfolds);
- fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
-
val repTA = mk_T_of_bnf Ds As bnf;
val T_bind = qualify b;
val TA_params = Term.add_tfreesT repTA [];
@@ -800,12 +785,12 @@
abs_inverse = Abs_inverse', type_definition = type_definition};
val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB,
- Term.list_comb (expand_maps (mk_map_of_bnf Ds As Bs bnf), fs)), RepA));
- val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA)) o expand_maps o expand_sets)
+ Term.list_comb (mk_map_of_bnf Ds As Bs bnf, fs)), RepA));
+ val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA)))
(mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
val bnf_bd = mk_bd_of_bnf Ds As bnf;
val bnf_rel = fold_rev Term.absfree Rs' (mk_vimage2p RepA RepB $
- (Term.list_comb (expand_rels (mk_rel_of_bnf Ds As Bs bnf), Rs)));
+ (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, Rs)));
(*bd may depend only on dead type variables*)
val bd_repT = fst (dest_relT (fastype_of bnf_bd));
@@ -836,24 +821,22 @@
(bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite)
end;
- fun map_id0_tac ctxt =
- rtac (@{thm type_copy_map_id0} OF [type_definition, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;
- fun map_comp0_tac ctxt =
- rtac (@{thm type_copy_map_comp0} OF
- [type_definition, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1;
- fun map_cong0_tac ctxt =
- EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (unfold_all ctxt (map_cong0_of_bnf bnf)) ::
+ fun map_id0_tac _ =
+ rtac (@{thm type_copy_map_id0} OF [type_definition, map_id0_of_bnf bnf]) 1;
+ fun map_comp0_tac _ =
+ rtac (@{thm type_copy_map_comp0} OF [type_definition, map_comp0_of_bnf bnf]) 1;
+ fun map_cong0_tac _ =
+ EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (map_cong0_of_bnf bnf) ::
map (fn i => EVERY' [select_prem_tac live (dtac meta_spec) i, etac meta_mp,
etac (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
- fun set_map0_tac thm ctxt =
- rtac (@{thm type_copy_set_map0} OF [type_definition, unfold_all ctxt thm]) 1;
- val set_bd_tacs = map (fn thm => fn ctxt => rtac (@{thm ordLeq_ordIso_trans} OF
- [unfold_sets ctxt thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1)
- (set_bd_of_bnf bnf);
- fun le_rel_OO_tac ctxt =
- rtac (unfold_rels ctxt (le_rel_OO_of_bnf bnf) RS @{thm vimage2p_relcompp_mono}) 1;
+ fun set_map0_tac thm _ =
+ rtac (@{thm type_copy_set_map0} OF [type_definition, thm]) 1;
+ val set_bd_tacs = map (fn thm => fn _ => rtac (@{thm ordLeq_ordIso_trans} OF
+ [thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) (set_bd_of_bnf bnf);
+ fun le_rel_OO_tac _ =
+ rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1;
fun rel_OO_Grp_tac ctxt =
- (rtac (unfold_all ctxt (rel_OO_Grp_of_bnf bnf) RS @{thm vimage2p_cong} RS trans) THEN'
+ (rtac (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN'
SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
@@ -864,18 +847,40 @@
val bnf_wits = map (fn (I, t) =>
fold Term.absdummy (map (nth As) I)
- (AbsA $ Term.list_comb (expand_id_bnf_comp_def t, map Bound (0 upto length I - 1))))
+ (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
(mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
- fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
- mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
+ fun wit_tac _ = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
+ mk_simple_wit_tac (wit_thms_of_bnf bnf);
val (bnf', lthy') =
- bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME all_deads)
+ bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads)
Binding.empty Binding.empty []
((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
+
+ val unfolds = @{thm id_bnf_comp_apply} ::
+ (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
+
+ val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
+
+ val map_def = map_def_of_bnf bnf'';
+ val set_defs = set_defs_of_bnf bnf'';
+ val rel_def = rel_def_of_bnf bnf'';
+
+ val bnf_b = qualify b;
+ val def_qualify =
+ Thm.def_binding o Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
+ fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
+ val map_b = def_qualify (mk_prefix_binding mapN);
+ val rel_b = def_qualify (mk_prefix_binding relN);
+ val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)]
+ else map (fn i => def_qualify (mk_prefix_binding (mk_setN i))) (1 upto live);
+
+ val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
+ |> map (fn (b, def) => ((b, []), [([def], [])]))
+ val lthy'' = lthy' |> Local_Theory.notes notes |> snd
in
- ((bnf', (all_deads, absT_info)), lthy')
+ ((bnf'', (all_deads, absT_info)), lthy'')
end;
exception BAD_DEAD of typ * typ;
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Mar 10 23:03:51 2014 +0100
@@ -12,6 +12,7 @@
type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
val morph_bnf: morphism -> bnf -> bnf
+ val morph_bnf_defs: morphism -> bnf -> bnf
val bnf_of: Proof.context -> string -> bnf option
val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
@@ -100,16 +101,16 @@
Proof.context
val print_bnfs: Proof.context -> unit
- val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
- (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option ->
- binding -> binding -> binding list ->
+ val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool ->
+ (binding -> binding) -> (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) ->
+ typ list option -> binding -> binding -> binding list ->
(((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
string * term list *
((Proof.context -> thm list -> tactic) option * term list list) *
((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
local_theory * thm list
- val define_bnf_consts: inline_policy -> fact_policy -> typ list option ->
+ val define_bnf_consts: inline_policy -> fact_policy -> bool -> typ list option ->
binding -> binding -> binding list ->
(((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
((typ list * typ list * typ list * typ) *
@@ -121,7 +122,7 @@
(typ list -> typ list -> typ list -> term) *
(typ list -> typ list -> typ list -> term))) * local_theory
- val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
+ val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> (binding -> binding) ->
(Proof.context -> tactic) list ->
(Proof.context -> tactic) -> typ list option -> binding ->
binding -> binding list ->
@@ -434,22 +435,27 @@
axioms = axioms, defs = defs, facts = facts,
nwits = length wits, wits = wits, rel = rel};
-fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
+fun map_bnf f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16
+ (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
dead = dead, deads = deads, map = map, sets = sets, bd = bd,
axioms = axioms, defs = defs, facts = facts,
nwits = nwits, wits = wits, rel = rel}) =
- BNF {name = Morphism.binding phi name, T = Morphism.typ phi T,
- live = live, lives = List.map (Morphism.typ phi) lives,
- lives' = List.map (Morphism.typ phi) lives',
- dead = dead, deads = List.map (Morphism.typ phi) deads,
- map = Morphism.term phi map, sets = List.map (Morphism.term phi) sets,
- bd = Morphism.term phi bd,
- axioms = morph_axioms phi axioms,
- defs = morph_defs phi defs,
- facts = morph_facts phi facts,
- nwits = nwits,
- wits = List.map (morph_witness phi) wits,
- rel = Morphism.term phi rel};
+ BNF {name = f1 name, T = f2 T,
+ live = f3 live, lives = f4 lives, lives' = f5 lives', dead = f6 dead, deads = f7 deads,
+ map = f8 map, sets = f9 sets, bd = f10 bd,
+ axioms = f11 axioms, defs = f12 defs, facts = f13 facts,
+ nwits = f14 nwits, wits = f15 wits, rel = f16 rel};
+
+fun morph_bnf phi =
+ let
+ val Tphi = Morphism.typ phi;
+ val tphi = Morphism.term phi;
+ in
+ map_bnf (Morphism.binding phi) Tphi I (map Tphi) (map Tphi) I (map Tphi) tphi (map tphi) tphi
+ (morph_axioms phi) (morph_defs phi) (morph_facts phi) I (map (morph_witness phi)) tphi
+ end;
+
+fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I;
structure Data = Generic_Data
(
@@ -660,7 +666,7 @@
(* Define new BNFs *)
-fun define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
+fun define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy =
let
val live = length set_rhss;
@@ -683,8 +689,9 @@
((rhs, Drule.reflexive_thm), lthy)
else
let val b = b () in
- apfst (apsnd snd) (Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs))
- lthy)
+ apfst (apsnd snd)
+ ((if internal then Local_Theory.define_internal else Local_Theory.define)
+ ((b, NoSyn), ((Thm.def_binding b, []), rhs)) lthy)
end
end;
@@ -830,8 +837,8 @@
(mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy)
end;
-fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs
- ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
+fun prepare_def const_policy mk_fact_policy internal qualify prep_typ prep_term Ds_opt map_b rel_b
+ set_bs ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
no_defs_lthy =
let
val fact_policy = mk_fact_policy no_defs_lthy;
@@ -861,7 +868,7 @@
(bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
(bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
(mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) =
- define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
+ define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy;
val dead = length deads;
@@ -1304,7 +1311,7 @@
(bnf, Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))) lthy);
-fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
+fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
(fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
let
fun mk_wits_tac ctxt set_maps =
@@ -1324,7 +1331,7 @@
goals (map (fn tac => fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
|> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
- end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs;
+ end) oo prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs;
val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
let
@@ -1343,8 +1350,8 @@
Proof.unfolding ([[(defs, [])]])
(Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms)
(map (single o rpair []) goals @ nontriv_wit_goals) lthy)
- end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_typ Syntax.read_term NONE
- Binding.empty Binding.empty [];
+ end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
+ NONE Binding.empty Binding.empty [];
fun print_bnfs ctxt =
let
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 10 23:03:51 2014 +0100
@@ -231,7 +231,7 @@
val rel_converseps = map rel_conversep_of_bnf bnfs;
val rel_Grps = map rel_Grp_of_bnf bnfs;
val rel_OOs = map rel_OO_of_bnf bnfs;
- val rel_OO_Grps = map rel_OO_Grp_of_bnf bnfs;
+ val in_rels = map in_rel_of_bnf bnfs;
val timer = time (timer "Extracted terms & thms");
@@ -757,7 +757,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
(Logic.list_implies (prems, concl)))
- (K ((hyp_subst_tac lthy THEN' atac) 1))
+ (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' atac) 1)
|> Thm.close_derivation
end;
@@ -775,7 +775,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
(mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs)))
- (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_mapss))
+ (K (mk_bis_rel_tac m bis_def in_rels map_comps map_cong0s set_mapss))
|> Thm.close_derivation
end;
@@ -1905,7 +1905,6 @@
||>> mk_Frees "S" activephiTs
||>> mk_Frees "JR" activeJphiTs;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
- val in_rels = map in_rel_of_bnf bnfs;
fun mk_Jrel_DEADID_coinduct_thm () =
mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
@@ -2088,7 +2087,7 @@
val (Jbnf_consts, lthy) =
fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
fn T => fn lthy =>
- define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads)
+ define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads)
map_b rel_b set_bs
((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy;
@@ -2516,7 +2515,7 @@
val (Jbnfs, lthy) =
fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms =>
fn consts => fn lthy =>
- bnf_def Do_Inline (user_policy Note_Some) I tacs (wit_tac Jwit_thms) (SOME deads)
+ bnf_def Do_Inline (user_policy Note_Some) false I tacs (wit_tac Jwit_thms) (SOME deads)
map_b rel_b set_bs consts lthy
|> register_bnf (Local_Theory.full_name lthy b))
bs tacss map_bs rel_bs set_bss Jwit_thmss
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Mar 10 23:03:51 2014 +0100
@@ -13,7 +13,7 @@
val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic
val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
- val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
+ val mk_bis_rel_tac: int -> thm -> thm list -> thm list -> thm list ->
thm list list -> tactic
val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic
val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
@@ -214,38 +214,36 @@
(rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
(rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1;
-fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_map0ss =
+fun mk_bis_rel_tac m bis_def in_rels map_comp0s map_cong0s set_map0ss =
let
- val n = length rel_OO_Grps;
- val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ rel_OO_Grps);
+ val n = length in_rels;
+ val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ in_rels);
- fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) =
+ fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
- etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
- rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
- rtac @{thm relcomppI}, rtac @{thm conversepI},
- EVERY' (map (fn thm =>
- EVERY' [rtac @{thm GrpI},
- rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
- REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), atac,
- REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
- CONJ_WRAP' (fn (i, thm) =>
- if i <= m
- then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
- etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI,
- rtac @{thm case_prodI}, rtac refl]
- else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
- rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
- (1 upto (m + n) ~~ set_map0s)])
- @{thms fst_diag_id snd_diag_id})];
+ etac allE, etac allE, etac impE, atac, etac bexE,
+ REPEAT_DETERM o eresolve_tac [CollectE, conjE],
+ rtac (in_rel RS iffD2), rtac exI, rtac (Drule.rotate_prems 1 conjI),
+ CONJ_WRAP' (fn thm => EVERY' [rtac trans, rtac trans, rtac map_comp0, rtac map_cong0,
+ REPEAT_DETERM_N m o rtac thm, REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
+ atac])
+ @{thms fst_diag_id snd_diag_id},
+ rtac CollectI,
+ CONJ_WRAP' (fn (i, thm) =>
+ if i <= m
+ then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
+ etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI,
+ rtac @{thm case_prodI}, rtac refl]
+ else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
+ rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
+ (1 upto (m + n) ~~ set_map0s)];
- fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) =
+ fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
etac allE, etac allE, etac impE, atac,
- dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}),
+ dtac (in_rel RS @{thm iffD1}),
REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
- @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
- hyp_subst_tac ctxt,
+ @{thms CollectE Collect_split_in_rel_leE}),
rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 10 23:03:51 2014 +0100
@@ -1483,7 +1483,7 @@
val (Ibnf_consts, lthy) =
fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
fn T => fn lthy =>
- define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads)
+ define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads)
map_b rel_b set_bs
((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
@@ -1769,7 +1769,7 @@
val (Ibnfs, lthy) =
fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy =>
- bnf_def Do_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
+ bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
map_b rel_b set_bs consts lthy
|> register_bnf (Local_Theory.full_name lthy b))
bs tacss map_bs rel_bs set_bss
--- a/src/HOL/Topological_Spaces.thy Mon Mar 10 23:03:15 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Mon Mar 10 23:03:51 2014 +0100
@@ -1193,26 +1193,25 @@
The use of disjunction here complicates proofs considerably.
One alternative is to add a Boolean argument to indicate the direction.
Another is to develop the notions of increasing and decreasing first.*}
- "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
-
-definition
- incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
- --{*Increasing sequence*}
- "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
-
-definition
- decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
- --{*Decreasing sequence*}
- "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+ "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) \<or> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
+
+abbreviation incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
+ "incseq X \<equiv> mono X"
+
+lemma incseq_def: "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<ge> X m)"
+ unfolding mono_def ..
+
+abbreviation decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
+ "decseq X \<equiv> antimono X"
+
+lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+ unfolding antimono_def ..
definition
subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
--{*Definition of subsequence*}
"subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
-lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
- unfolding mono_def incseq_def by auto
-
lemma incseq_SucI:
"(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
using lift_Suc_mono_le[of X]