added Library/Nat_Infinity.thy and Library/Continuity.thy
authoroheimb
Thu May 31 17:06:00 2001 +0200 (2001-05-31)
changeset 11351c5c403d30c77
parent 11350 4c55b020d6ee
child 11352 140d55f5836d
added Library/Nat_Infinity.thy and Library/Continuity.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Nat_Infinity.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Continuity.thy	Thu May 31 17:06:00 2001 +0200
     1.3 @@ -0,0 +1,219 @@
     1.4 +(*  Title:      HOL/Library/Continuity.thy
     1.5 +    ID:         $$
     1.6 +    Author: 	David von Oheimb, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +*)
    1.10 +
    1.11 +header {*
    1.12 +  \title{Continuity and interations (of set transformers)}
    1.13 +  \author{David von Oheimb}
    1.14 +*}
    1.15 +
    1.16 +theory Continuity = Relation_Power:
    1.17 +
    1.18 +
    1.19 +subsection "Chains"
    1.20 +
    1.21 +constdefs
    1.22 +  up_chain      :: "(nat => 'a set) => bool"
    1.23 + "up_chain F      == !i. F i <= F (Suc i)"
    1.24 +
    1.25 +lemma up_chainI: "(!!i. F i <= F (Suc i)) ==> up_chain F"
    1.26 +by (simp add: up_chain_def);
    1.27 +
    1.28 +lemma up_chainD: "up_chain F ==> F i <= F (Suc i)"
    1.29 +by (simp add: up_chain_def);
    1.30 +
    1.31 +lemma up_chain_less_mono [rule_format]: "up_chain F ==> x < y --> F x <= F y"
    1.32 +apply (induct_tac y)
    1.33 +apply (blast dest: up_chainD elim: less_SucE)+
    1.34 +done
    1.35 +
    1.36 +lemma up_chain_mono: "up_chain F ==> x <= y ==> F x <= F y"
    1.37 +apply (drule le_imp_less_or_eq)
    1.38 +apply (blast dest: up_chain_less_mono)
    1.39 +done
    1.40 +
    1.41 +
    1.42 +constdefs
    1.43 +  down_chain      :: "(nat => 'a set) => bool"
    1.44 + "down_chain F == !i. F (Suc i) <= F i"
    1.45 +
    1.46 +lemma down_chainI: "(!!i. F (Suc i) <= F i) ==> down_chain F"
    1.47 +by (simp add: down_chain_def);
    1.48 +
    1.49 +lemma down_chainD: "down_chain F ==> F (Suc i) <= F i"
    1.50 +by (simp add: down_chain_def);
    1.51 +
    1.52 +lemma down_chain_less_mono[rule_format]: "down_chain F ==> x < y --> F y <= F x"
    1.53 +apply (induct_tac y)
    1.54 +apply (blast dest: down_chainD elim: less_SucE)+
    1.55 +done
    1.56 +
    1.57 +lemma down_chain_mono: "down_chain F ==> x <= y ==> F y <= F x"
    1.58 +apply (drule le_imp_less_or_eq)
    1.59 +apply (blast dest: down_chain_less_mono)
    1.60 +done
    1.61 +
    1.62 +
    1.63 +subsection "Continuity"
    1.64 +
    1.65 +constdefs
    1.66 +  up_cont :: "('a set => 'a set) => bool"
    1.67 + "up_cont f == !F. up_chain F --> f (Union (range F)) = Union (f`(range F))"
    1.68 +
    1.69 +lemma up_contI: 
    1.70 + "(!!F. up_chain F ==> f (Union (range F)) = Union (f`(range F))) ==> up_cont f"
    1.71 +apply (unfold up_cont_def)
    1.72 +by blast
    1.73 +
    1.74 +lemma up_contD: 
    1.75 +  "[| up_cont f; up_chain F |] ==> f (Union (range F)) = Union (f`(range F))"
    1.76 +apply (unfold up_cont_def)
    1.77 +by auto
    1.78 +
    1.79 +
    1.80 +lemma up_cont_mono: "up_cont f ==> mono f"
    1.81 +apply (rule monoI)
    1.82 +apply (drule_tac F = "%i. if i = 0 then A else B" in up_contD)
    1.83 +apply  (rule up_chainI)
    1.84 +apply  simp+
    1.85 +apply (drule Un_absorb1)
    1.86 +apply auto
    1.87 +done
    1.88 +
    1.89 +
    1.90 +constdefs
    1.91 +  down_cont :: "('a set => 'a set) => bool"
    1.92 + "down_cont f == !F. down_chain F --> f (Inter (range F)) = Inter (f`(range F))"
    1.93 +
    1.94 +lemma down_contI: 
    1.95 + "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f`(range F))) ==> 
    1.96 +  down_cont f"
    1.97 +apply (unfold down_cont_def)
    1.98 +by blast
    1.99 +
   1.100 +lemma down_contD: "[| down_cont f; down_chain F |] ==> 
   1.101 +  f (Inter (range F)) = Inter (f`(range F))"
   1.102 +apply (unfold down_cont_def)
   1.103 +by auto
   1.104 +
   1.105 +lemma down_cont_mono: "down_cont f ==> mono f"
   1.106 +apply (rule monoI)
   1.107 +apply (drule_tac F = "%i. if i = 0 then B else A" in down_contD)
   1.108 +apply  (rule down_chainI)
   1.109 +apply  simp+
   1.110 +apply (drule Int_absorb1)
   1.111 +apply auto
   1.112 +done
   1.113 +
   1.114 +
   1.115 +subsection "Iteration"
   1.116 +
   1.117 +constdefs
   1.118 +
   1.119 +  up_iterate :: "('a set => 'a set) => nat => 'a set"
   1.120 + "up_iterate f n == (f^n) {}"
   1.121 +
   1.122 +lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
   1.123 +by (simp add: up_iterate_def)
   1.124 +
   1.125 +lemma up_iterate_Suc [simp]: 
   1.126 +  "up_iterate f (Suc i) = f (up_iterate f i)"
   1.127 +by (simp add: up_iterate_def)
   1.128 +
   1.129 +lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)"
   1.130 +apply (rule up_chainI)
   1.131 +apply (induct_tac i)
   1.132 +apply simp+
   1.133 +apply (erule (1) monoD)
   1.134 +done
   1.135 +
   1.136 +lemma UNION_up_iterate_is_fp: 
   1.137 +"up_cont F ==> F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
   1.138 +apply (frule up_cont_mono [THEN up_iterate_chain])
   1.139 +apply (drule (1) up_contD)
   1.140 +apply simp
   1.141 +apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
   1.142 +apply (case_tac "xa")
   1.143 +apply auto
   1.144 +done
   1.145 +
   1.146 +lemma UNION_up_iterate_lowerbound: 
   1.147 +"[| mono F; F P = P |] ==> UNION UNIV (up_iterate F) <= P"
   1.148 +apply (subgoal_tac "(!!i. up_iterate F i <= P)")
   1.149 +apply  fast
   1.150 +apply (induct_tac "i")
   1.151 +prefer 2 apply (drule (1) monoD)
   1.152 +apply auto
   1.153 +done
   1.154 +
   1.155 +lemma UNION_up_iterate_is_lfp: 
   1.156 +  "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
   1.157 +apply (rule set_eq_subset [THEN iffD2])
   1.158 +apply (rule conjI)
   1.159 +prefer 2
   1.160 +apply  (drule up_cont_mono)
   1.161 +apply  (rule UNION_up_iterate_lowerbound)
   1.162 +apply   assumption
   1.163 +apply  (erule lfp_unfold [symmetric])
   1.164 +apply (rule lfp_lowerbound)
   1.165 +apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   1.166 +apply (erule UNION_up_iterate_is_fp [symmetric])
   1.167 +done
   1.168 +
   1.169 +
   1.170 +constdefs
   1.171 +
   1.172 +  down_iterate :: "('a set => 'a set) => nat => 'a set"
   1.173 + "down_iterate f n == (f^n) UNIV"
   1.174 +
   1.175 +lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   1.176 +by (simp add: down_iterate_def)
   1.177 +
   1.178 +lemma down_iterate_Suc [simp]: 
   1.179 +  "down_iterate f (Suc i) = f (down_iterate f i)"
   1.180 +by (simp add: down_iterate_def)
   1.181 +
   1.182 +lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)"
   1.183 +apply (rule down_chainI)
   1.184 +apply (induct_tac i)
   1.185 +apply simp+
   1.186 +apply (erule (1) monoD)
   1.187 +done
   1.188 +
   1.189 +lemma INTER_down_iterate_is_fp: 
   1.190 +"down_cont F ==> 
   1.191 + F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
   1.192 +apply (frule down_cont_mono [THEN down_iterate_chain])
   1.193 +apply (drule (1) down_contD)
   1.194 +apply simp
   1.195 +apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
   1.196 +apply (case_tac "xa")
   1.197 +apply auto
   1.198 +done
   1.199 +
   1.200 +lemma INTER_down_iterate_upperbound: 
   1.201 +"[| mono F; F P = P |] ==> P <= INTER UNIV (down_iterate F)"
   1.202 +apply (subgoal_tac "(!!i. P <= down_iterate F i)")
   1.203 +apply  fast
   1.204 +apply (induct_tac "i")
   1.205 +prefer 2 apply (drule (1) monoD)
   1.206 +apply auto
   1.207 +done
   1.208 +
   1.209 +lemma INTER_down_iterate_is_gfp: 
   1.210 +  "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
   1.211 +apply (rule set_eq_subset [THEN iffD2])
   1.212 +apply (rule conjI)
   1.213 +apply  (drule down_cont_mono)
   1.214 +apply  (rule INTER_down_iterate_upperbound)
   1.215 +apply   assumption
   1.216 +apply  (erule gfp_unfold [symmetric])
   1.217 +apply (rule gfp_upperbound)
   1.218 +apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   1.219 +apply (erule INTER_down_iterate_is_fp)
   1.220 +done
   1.221 +
   1.222 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Thu May 31 17:06:00 2001 +0200
     2.3 @@ -0,0 +1,216 @@
     2.4 +(*  Title: 	HOL/Library/Nat_Infinity.thy
     2.5 +    ID:         $ $
     2.6 +    Author: 	David von Oheimb, TU Muenchen
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8 +
     2.9 +*)
    2.10 +
    2.11 +header {*
    2.12 +  \title{Natural numbers with infinity}
    2.13 +  \author{David von Oheimb}
    2.14 +*}
    2.15 +
    2.16 +theory Nat_Infinity = Datatype:
    2.17 +
    2.18 +subsection "Definitions"
    2.19 +
    2.20 +text {*
    2.21 + We extend the standard natural numbers by a special value indicating infinity.
    2.22 + This includes extending the ordering relations @{term "op <"} and 
    2.23 + @{term "op <="}.
    2.24 +*}
    2.25 +
    2.26 +datatype inat = Fin nat | Infty
    2.27 +
    2.28 +instance inat :: ord ..
    2.29 +instance inat :: zero ..
    2.30 +
    2.31 +consts
    2.32 +
    2.33 +  iSuc	:: "inat => inat"
    2.34 +
    2.35 +syntax (xsymbols)
    2.36 +
    2.37 +  Infty		:: inat					("\<infinity>")
    2.38 +
    2.39 +defs
    2.40 +
    2.41 +  iZero_def:	"0      == Fin 0"
    2.42 +  iSuc_def:	"iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
    2.43 +  iless_def:	"m < n  == case m of Fin m1 => (case n of Fin n1 => m1 < n1 
    2.44 +						             | \<infinity> => True)
    2.45 +				   | \<infinity>  => False "
    2.46 +  ile_def:	"(m::inat) <= n == \<not>(n<m)"
    2.47 +
    2.48 +lemmas inat_defs = iZero_def iSuc_def iless_def ile_def
    2.49 +lemmas inat_splits = inat.split inat.split_asm
    2.50 +
    2.51 +
    2.52 +text {* Below is a not quite complete set of theorems. Use
    2.53 +@{text "apply(simp add:inat_defs split:inat_splits, arith?)"}
    2.54 +to prove new theorems or solve arithmetic subgoals involving @{typ inat} 
    2.55 +on the fly.
    2.56 +*}
    2.57 +
    2.58 +subsection "Constructors"
    2.59 +
    2.60 +lemma Fin_0: "Fin 0 = 0"
    2.61 +by(simp add:inat_defs split:inat_splits, arith?)
    2.62 +
    2.63 +lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    2.64 +by(simp add:inat_defs split:inat_splits, arith?)
    2.65 +
    2.66 +lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    2.67 +by(simp add:inat_defs split:inat_splits, arith?)
    2.68 +
    2.69 +lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
    2.70 +by(simp add:inat_defs split:inat_splits, arith?)
    2.71 +
    2.72 +lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
    2.73 +by(simp add:inat_defs split:inat_splits, arith?)
    2.74 +
    2.75 +lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
    2.76 +by(simp add:inat_defs split:inat_splits, arith?)
    2.77 +
    2.78 +lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
    2.79 +by(simp add:inat_defs split:inat_splits, arith?)
    2.80 +
    2.81 +
    2.82 +subsection "Ordering relations"
    2.83 +
    2.84 +lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
    2.85 +by(simp add:inat_defs split:inat_splits, arith?)
    2.86 +
    2.87 +lemma iless_linear: "m < n | m = n | n < (m::inat)"
    2.88 +by(simp add:inat_defs split:inat_splits, arith?)
    2.89 +
    2.90 +lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
    2.91 +by(simp add:inat_defs split:inat_splits, arith?)
    2.92 +
    2.93 +lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
    2.94 +by(simp add:inat_defs split:inat_splits, arith?)
    2.95 +
    2.96 +lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
    2.97 +by(simp add:inat_defs split:inat_splits, arith?)
    2.98 +
    2.99 +lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
   2.100 +by(simp add:inat_defs split:inat_splits, arith?)
   2.101 +
   2.102 +lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
   2.103 +by(simp add:inat_defs split:inat_splits, arith?)
   2.104 +
   2.105 +lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)"
   2.106 +by(simp add:inat_defs split:inat_splits, arith?)
   2.107 +
   2.108 +lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
   2.109 +by(simp add:inat_defs split:inat_splits, arith?)
   2.110 +
   2.111 +lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   2.112 +by(simp add:inat_defs split:inat_splits, arith?)
   2.113 +
   2.114 +lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
   2.115 +by(simp add:inat_defs split:inat_splits, arith?)
   2.116 +
   2.117 +lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
   2.118 +by(simp add:inat_defs split:inat_splits, arith?)
   2.119 +
   2.120 +lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)"
   2.121 +by(simp add:inat_defs split:inat_splits, arith?)
   2.122 +
   2.123 +
   2.124 +(* ----------------------------------------------------------------------- *)
   2.125 +
   2.126 +lemma ile_def2: "m <= n = (m < n | m = (n::inat))"
   2.127 +by(simp add:inat_defs split:inat_splits, arith?)
   2.128 +
   2.129 +lemma ile_refl [simp]: "n <= (n::inat)"
   2.130 +by(simp add:inat_defs split:inat_splits, arith?)
   2.131 +
   2.132 +lemma ile_trans: "i <= j ==> j <= k ==> i <= (k::inat)"
   2.133 +by(simp add:inat_defs split:inat_splits, arith?)
   2.134 +
   2.135 +lemma ile_iless_trans: "i <= j ==> j < k ==> i < (k::inat)"
   2.136 +by(simp add:inat_defs split:inat_splits, arith?)
   2.137 +
   2.138 +lemma iless_ile_trans: "i < j ==> j <= k ==> i < (k::inat)"
   2.139 +by(simp add:inat_defs split:inat_splits, arith?)
   2.140 +
   2.141 +lemma Infty_ub [simp]: "n <= \<infinity>"
   2.142 +by(simp add:inat_defs split:inat_splits, arith?)
   2.143 +
   2.144 +lemma i0_lb [simp]: "(0::inat) <= n"
   2.145 +by(simp add:inat_defs split:inat_splits, arith?)
   2.146 +
   2.147 +lemma Infty_ileE [elim!]: "\<infinity> <= Fin m ==> R"
   2.148 +by(simp add:inat_defs split:inat_splits, arith?)
   2.149 +
   2.150 +lemma Fin_ile_mono [simp]: "(Fin n <= Fin m) = (n <= m)"
   2.151 +by(simp add:inat_defs split:inat_splits, arith?)
   2.152 +
   2.153 +lemma ilessI1: "n <= m ==> n \<noteq> m ==> n < (m::inat)"
   2.154 +by(simp add:inat_defs split:inat_splits, arith?)
   2.155 +
   2.156 +lemma ileI1: "m < n ==> iSuc m <= n"
   2.157 +by(simp add:inat_defs split:inat_splits, arith?)
   2.158 +
   2.159 +lemma Suc_ile_eq: "Fin (Suc m) <= n = (Fin m < n)"
   2.160 +by(simp add:inat_defs split:inat_splits, arith?)
   2.161 +
   2.162 +lemma iSuc_ile_mono [simp]: "iSuc n <= iSuc m = (n <= m)"
   2.163 +by(simp add:inat_defs split:inat_splits, arith?)
   2.164 +
   2.165 +lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m <= n)"
   2.166 +by(simp add:inat_defs split:inat_splits, arith?)
   2.167 +
   2.168 +lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n <= 0"
   2.169 +by(simp add:inat_defs split:inat_splits, arith?)
   2.170 +
   2.171 +lemma ile_iSuc [simp]: "n <= iSuc n"
   2.172 +by(simp add:inat_defs split:inat_splits, arith?)
   2.173 +
   2.174 +lemma Fin_ile: "n <= Fin m ==> \<exists>k. n = Fin k"
   2.175 +by(simp add:inat_defs split:inat_splits, arith?)
   2.176 +
   2.177 +lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   2.178 +apply (induct_tac "k")
   2.179 +apply  (simp (no_asm) only: Fin_0)
   2.180 +apply  (fast intro: ile_iless_trans i0_lb)
   2.181 +apply (erule exE)
   2.182 +apply (drule spec)
   2.183 +apply (erule exE)
   2.184 +apply (drule ileI1)
   2.185 +apply (rule iSuc_Fin [THEN subst])
   2.186 +apply (rule exI)
   2.187 +apply (erule (1) ile_iless_trans)
   2.188 +done
   2.189 +
   2.190 +ML {*
   2.191 +val Fin_0 = thm "Fin_0";
   2.192 +val Suc_ile_eq = thm "Suc_ile_eq";
   2.193 +val iSuc_Fin = thm "iSuc_Fin";
   2.194 +val iSuc_Infty = thm "iSuc_Infty";
   2.195 +val iSuc_mono = thm "iSuc_mono";
   2.196 +val iSuc_ile_mono = thm "iSuc_ile_mono";
   2.197 +val not_iSuc_ilei0=thm "not_iSuc_ilei0";
   2.198 +val iSuc_inject = thm "iSuc_inject";
   2.199 +val i0_iless_iSuc = thm "i0_iless_iSuc";
   2.200 +val i0_eq = thm "i0_eq";
   2.201 +val i0_lb = thm "i0_lb";
   2.202 +val ile_def = thm "ile_def";
   2.203 +val ile_refl = thm "ile_refl";
   2.204 +val Infty_ub = thm "Infty_ub";
   2.205 +val ilessI1 = thm "ilessI1";
   2.206 +val ile_iless_trans = thm "ile_iless_trans";
   2.207 +val ile_trans = thm "ile_trans";
   2.208 +val ileI1 = thm "ileI1";
   2.209 +val ile_iSuc = thm "ile_iSuc";
   2.210 +val Fin_iless_Infty = thm "Fin_iless_Infty";
   2.211 +val Fin_ile_mono = thm "Fin_ile_mono";
   2.212 +val chain_incr = thm "chain_incr";
   2.213 +val Infty_eq = thm "Infty_eq";
   2.214 +*}
   2.215 +
   2.216 +end
   2.217 +
   2.218 +
   2.219 +