removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
1.1 --- a/NEWS Sat Mar 13 16:44:12 2010 +0100
1.2 +++ b/NEWS Sat Mar 13 17:19:12 2010 +0100
1.3 @@ -89,6 +89,9 @@
1.4 contain multiple interpretations of local typedefs (with different
1.5 non-emptiness proofs), even in a global theory context.
1.6
1.7 +* Theory Library/Coinductive_List has been removed -- superceded by
1.8 +AFP/thys/Coinductive.
1.9 +
1.10 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
1.11 Min, Max from theory Finite_Set. INCOMPATIBILITY.
1.12
2.1 --- a/src/HOL/IsaMakefile Sat Mar 13 16:44:12 2010 +0100
2.2 +++ b/src/HOL/IsaMakefile Sat Mar 13 17:19:12 2010 +0100
2.3 @@ -394,30 +394,28 @@
2.4 Library/Inner_Product.thy Library/Kleene_Algebra.thy \
2.5 Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
2.6 Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy \
2.7 - Library/State_Monad.thy Library/Multiset.thy \
2.8 - Library/Permutation.thy Library/Quotient_Type.thy \
2.9 - Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \
2.10 - Library/README.html Library/Continuity.thy \
2.11 - Library/Order_Relation.thy Library/Nested_Environment.thy \
2.12 - Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \
2.13 - Library/Library/document/root.tex Library/Library/document/root.bib \
2.14 + Library/State_Monad.thy Library/Multiset.thy Library/Permutation.thy \
2.15 + Library/Quotient_Type.thy Library/Quicksort.thy \
2.16 + Library/Nat_Infinity.thy Library/Word.thy Library/README.html \
2.17 + Library/Continuity.thy Library/Order_Relation.thy \
2.18 + Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy \
2.19 + Library/Library/ROOT.ML Library/Library/document/root.tex \
2.20 + Library/Library/document/root.bib \
2.21 Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
2.22 Library/Product_ord.thy Library/Char_nat.thy Library/Table.thy \
2.23 Library/Sublist_Order.thy Library/List_lexord.thy \
2.24 - Library/Coinductive_List.thy Library/AssocList.thy \
2.25 - Library/Formal_Power_Series.thy Library/Binomial.thy \
2.26 - Library/Eval_Witness.thy Library/Code_Char.thy \
2.27 + Library/AssocList.thy Library/Formal_Power_Series.thy \
2.28 + Library/Binomial.thy Library/Eval_Witness.thy Library/Code_Char.thy \
2.29 Library/Code_Char_chr.thy Library/Code_Integer.thy \
2.30 Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \
2.31 Library/Boolean_Algebra.thy Library/Countable.thy \
2.32 Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy \
2.33 Library/Poly_Deriv.thy Library/Polynomial.thy Library/Preorder.thy \
2.34 Library/Product_plus.thy Library/Product_Vector.thy Library/Tree.thy \
2.35 - Library/Enum.thy Library/Float.thy Library/Quotient_List.thy \
2.36 - Library/Quotient_Option.thy Library/Quotient_Product.thy \
2.37 - Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \
2.38 - Library/Nat_Bijection.thy \
2.39 - $(SRC)/Tools/float.ML \
2.40 + Library/Enum.thy Library/Float.thy Library/Quotient_List.thy \
2.41 + Library/Quotient_Option.thy Library/Quotient_Product.thy \
2.42 + Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \
2.43 + Library/Nat_Bijection.thy $(SRC)/Tools/float.ML \
2.44 $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \
2.45 Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \
2.46 Library/OptionalSugar.thy Library/SML_Quickcheck.thy
3.1 --- a/src/HOL/Library/Coinductive_List.thy Sat Mar 13 16:44:12 2010 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,856 +0,0 @@
3.4 -(* Title: HOL/Library/Coinductive_Lists.thy
3.5 - Author: Lawrence C Paulson and Makarius
3.6 -*)
3.7 -
3.8 -header {* Potentially infinite lists as greatest fixed-point *}
3.9 -
3.10 -theory Coinductive_List
3.11 -imports List Main
3.12 -begin
3.13 -
3.14 -subsection {* List constructors over the datatype universe *}
3.15 -
3.16 -definition "NIL = Datatype.In0 (Datatype.Numb 0)"
3.17 -definition "CONS M N = Datatype.In1 (Datatype.Scons M N)"
3.18 -
3.19 -lemma CONS_not_NIL [iff]: "CONS M N \<noteq> NIL"
3.20 - and NIL_not_CONS [iff]: "NIL \<noteq> CONS M N"
3.21 - and CONS_inject [iff]: "(CONS K M) = (CONS L N) = (K = L \<and> M = N)"
3.22 - by (simp_all add: NIL_def CONS_def)
3.23 -
3.24 -lemma CONS_mono: "M \<subseteq> M' \<Longrightarrow> N \<subseteq> N' \<Longrightarrow> CONS M N \<subseteq> CONS M' N'"
3.25 - by (simp add: CONS_def In1_mono Scons_mono)
3.26 -
3.27 -lemma CONS_UN1: "CONS M (\<Union>x. f x) = (\<Union>x. CONS M (f x))"
3.28 - -- {* A continuity result? *}
3.29 - by (simp add: CONS_def In1_UN1 Scons_UN1_y)
3.30 -
3.31 -definition "List_case c h = Datatype.Case (\<lambda>_. c) (Datatype.Split h)"
3.32 -
3.33 -lemma List_case_NIL [simp]: "List_case c h NIL = c"
3.34 - and List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
3.35 - by (simp_all add: List_case_def NIL_def CONS_def)
3.36 -
3.37 -
3.38 -subsection {* Corecursive lists *}
3.39 -
3.40 -coinductive_set LList for A
3.41 -where NIL [intro]: "NIL \<in> LList A"
3.42 - | CONS [intro]: "a \<in> A \<Longrightarrow> M \<in> LList A \<Longrightarrow> CONS a M \<in> LList A"
3.43 -
3.44 -lemma LList_mono:
3.45 - assumes subset: "A \<subseteq> B"
3.46 - shows "LList A \<subseteq> LList B"
3.47 - -- {* This justifies using @{text LList} in other recursive type definitions. *}
3.48 -proof
3.49 - fix x
3.50 - assume "x \<in> LList A"
3.51 - then show "x \<in> LList B"
3.52 - proof coinduct
3.53 - case LList
3.54 - then show ?case using subset
3.55 - by cases blast+
3.56 - qed
3.57 -qed
3.58 -
3.59 -primrec
3.60 - LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
3.61 - 'a \<Rightarrow> 'b Datatype.item" where
3.62 - "LList_corec_aux 0 f x = {}"
3.63 - | "LList_corec_aux (Suc k) f x =
3.64 - (case f x of
3.65 - None \<Rightarrow> NIL
3.66 - | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
3.67 -
3.68 -definition "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
3.69 -
3.70 -text {*
3.71 - Note: the subsequent recursion equation for @{text LList_corec} may
3.72 - be used with the Simplifier, provided it operates in a non-strict
3.73 - fashion for case expressions (i.e.\ the usual @{text case}
3.74 - congruence rule needs to be present).
3.75 -*}
3.76 -
3.77 -lemma LList_corec:
3.78 - "LList_corec a f =
3.79 - (case f a of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (LList_corec w f))"
3.80 - (is "?lhs = ?rhs")
3.81 -proof
3.82 - show "?lhs \<subseteq> ?rhs"
3.83 - apply (unfold LList_corec_def)
3.84 - apply (rule UN_least)
3.85 - apply (case_tac k)
3.86 - apply (simp_all (no_asm_simp) split: option.splits)
3.87 - apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+
3.88 - done
3.89 - show "?rhs \<subseteq> ?lhs"
3.90 - apply (simp add: LList_corec_def split: option.splits)
3.91 - apply (simp add: CONS_UN1)
3.92 - apply safe
3.93 - apply (rule_tac a = "Suc ?k" in UN_I, simp, simp)+
3.94 - done
3.95 -qed
3.96 -
3.97 -lemma LList_corec_type: "LList_corec a f \<in> LList UNIV"
3.98 -proof -
3.99 - have "\<exists>x. LList_corec a f = LList_corec x f" by blast
3.100 - then show ?thesis
3.101 - proof coinduct
3.102 - case (LList L)
3.103 - then obtain x where L: "L = LList_corec x f" by blast
3.104 - show ?case
3.105 - proof (cases "f x")
3.106 - case None
3.107 - then have "LList_corec x f = NIL"
3.108 - by (simp add: LList_corec)
3.109 - with L have ?NIL by simp
3.110 - then show ?thesis ..
3.111 - next
3.112 - case (Some p)
3.113 - then have "LList_corec x f = CONS (fst p) (LList_corec (snd p) f)"
3.114 - by (simp add: LList_corec split: prod.split)
3.115 - with L have ?CONS by auto
3.116 - then show ?thesis ..
3.117 - qed
3.118 - qed
3.119 -qed
3.120 -
3.121 -
3.122 -subsection {* Abstract type definition *}
3.123 -
3.124 -typedef 'a llist = "LList (range Datatype.Leaf) :: 'a Datatype.item set"
3.125 -proof
3.126 - show "NIL \<in> ?llist" ..
3.127 -qed
3.128 -
3.129 -lemma NIL_type: "NIL \<in> llist"
3.130 - unfolding llist_def by (rule LList.NIL)
3.131 -
3.132 -lemma CONS_type: "a \<in> range Datatype.Leaf \<Longrightarrow>
3.133 - M \<in> llist \<Longrightarrow> CONS a M \<in> llist"
3.134 - unfolding llist_def by (rule LList.CONS)
3.135 -
3.136 -lemma llistI: "x \<in> LList (range Datatype.Leaf) \<Longrightarrow> x \<in> llist"
3.137 - by (simp add: llist_def)
3.138 -
3.139 -lemma llistD: "x \<in> llist \<Longrightarrow> x \<in> LList (range Datatype.Leaf)"
3.140 - by (simp add: llist_def)
3.141 -
3.142 -lemma Rep_llist_UNIV: "Rep_llist x \<in> LList UNIV"
3.143 -proof -
3.144 - have "Rep_llist x \<in> llist" by (rule Rep_llist)
3.145 - then have "Rep_llist x \<in> LList (range Datatype.Leaf)"
3.146 - by (simp add: llist_def)
3.147 - also have "\<dots> \<subseteq> LList UNIV" by (rule LList_mono) simp
3.148 - finally show ?thesis .
3.149 -qed
3.150 -
3.151 -definition "LNil = Abs_llist NIL"
3.152 -definition "LCons x xs = Abs_llist (CONS (Datatype.Leaf x) (Rep_llist xs))"
3.153 -
3.154 -code_datatype LNil LCons
3.155 -
3.156 -lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
3.157 - apply (simp add: LNil_def LCons_def)
3.158 - apply (subst Abs_llist_inject)
3.159 - apply (auto intro: NIL_type CONS_type Rep_llist)
3.160 - done
3.161 -
3.162 -lemma LNil_not_LCons [iff]: "LNil \<noteq> LCons x xs"
3.163 - by (rule LCons_not_LNil [symmetric])
3.164 -
3.165 -lemma LCons_inject [iff]: "(LCons x xs = LCons y ys) = (x = y \<and> xs = ys)"
3.166 - apply (simp add: LCons_def)
3.167 - apply (subst Abs_llist_inject)
3.168 - apply (auto simp add: Rep_llist_inject intro: CONS_type Rep_llist)
3.169 - done
3.170 -
3.171 -lemma Rep_llist_LNil: "Rep_llist LNil = NIL"
3.172 - by (simp add: LNil_def add: Abs_llist_inverse NIL_type)
3.173 -
3.174 -lemma Rep_llist_LCons: "Rep_llist (LCons x l) =
3.175 - CONS (Datatype.Leaf x) (Rep_llist l)"
3.176 - by (simp add: LCons_def Abs_llist_inverse CONS_type Rep_llist)
3.177 -
3.178 -lemma llist_cases [cases type: llist]:
3.179 - obtains
3.180 - (LNil) "l = LNil"
3.181 - | (LCons) x l' where "l = LCons x l'"
3.182 -proof (cases l)
3.183 - case (Abs_llist L)
3.184 - from `L \<in> llist` have "L \<in> LList (range Datatype.Leaf)" by (rule llistD)
3.185 - then show ?thesis
3.186 - proof cases
3.187 - case NIL
3.188 - with Abs_llist have "l = LNil" by (simp add: LNil_def)
3.189 - with LNil show ?thesis .
3.190 - next
3.191 - case (CONS a K)
3.192 - then have "K \<in> llist" by (blast intro: llistI)
3.193 - then obtain l' where "K = Rep_llist l'" by cases
3.194 - with CONS and Abs_llist obtain x where "l = LCons x l'"
3.195 - by (auto simp add: LCons_def Abs_llist_inject)
3.196 - with LCons show ?thesis .
3.197 - qed
3.198 -qed
3.199 -
3.200 -
3.201 -definition
3.202 - [code del]: "llist_case c d l =
3.203 - List_case c (\<lambda>x y. d (inv Datatype.Leaf x) (Abs_llist y)) (Rep_llist l)"
3.204 -
3.205 -
3.206 -syntax (* FIXME? *)
3.207 - LNil :: logic
3.208 - LCons :: logic
3.209 -translations
3.210 - "case p of XCONST LNil \<Rightarrow> a | XCONST LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
3.211 -
3.212 -lemma llist_case_LNil [simp, code]: "llist_case c d LNil = c"
3.213 - by (simp add: llist_case_def LNil_def
3.214 - NIL_type Abs_llist_inverse)
3.215 -
3.216 -lemma llist_case_LCons [simp, code]: "llist_case c d (LCons M N) = d M N"
3.217 - by (simp add: llist_case_def LCons_def
3.218 - CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
3.219 -
3.220 -lemma llist_case_cert:
3.221 - assumes "CASE \<equiv> llist_case c d"
3.222 - shows "(CASE LNil \<equiv> c) &&& (CASE (LCons M N) \<equiv> d M N)"
3.223 - using assms by simp_all
3.224 -
3.225 -setup {*
3.226 - Code.add_case @{thm llist_case_cert}
3.227 -*}
3.228 -
3.229 -definition
3.230 - [code del]: "llist_corec a f =
3.231 - Abs_llist (LList_corec a
3.232 - (\<lambda>z.
3.233 - case f z of None \<Rightarrow> None
3.234 - | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)))"
3.235 -
3.236 -lemma LList_corec_type2:
3.237 - "LList_corec a
3.238 - (\<lambda>z. case f z of None \<Rightarrow> None
3.239 - | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)) \<in> llist"
3.240 - (is "?corec a \<in> _")
3.241 -proof (unfold llist_def)
3.242 - let "LList_corec a ?g" = "?corec a"
3.243 - have "\<exists>x. ?corec a = ?corec x" by blast
3.244 - then show "?corec a \<in> LList (range Datatype.Leaf)"
3.245 - proof coinduct
3.246 - case (LList L)
3.247 - then obtain x where L: "L = ?corec x" by blast
3.248 - show ?case
3.249 - proof (cases "f x")
3.250 - case None
3.251 - then have "?corec x = NIL"
3.252 - by (simp add: LList_corec)
3.253 - with L have ?NIL by simp
3.254 - then show ?thesis ..
3.255 - next
3.256 - case (Some p)
3.257 - then have "?corec x =
3.258 - CONS (Datatype.Leaf (fst p)) (?corec (snd p))"
3.259 - by (simp add: LList_corec split: prod.split)
3.260 - with L have ?CONS by auto
3.261 - then show ?thesis ..
3.262 - qed
3.263 - qed
3.264 -qed
3.265 -
3.266 -lemma llist_corec [code, nitpick_simp]:
3.267 - "llist_corec a f =
3.268 - (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
3.269 -proof (cases "f a")
3.270 - case None
3.271 - then show ?thesis
3.272 - by (simp add: llist_corec_def LList_corec LNil_def)
3.273 -next
3.274 - case (Some p)
3.275 -
3.276 - let "?corec a" = "llist_corec a f"
3.277 - let "?rep_corec a" =
3.278 - "LList_corec a
3.279 - (\<lambda>z. case f z of None \<Rightarrow> None
3.280 - | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w))"
3.281 -
3.282 - have "?corec a = Abs_llist (?rep_corec a)"
3.283 - by (simp only: llist_corec_def)
3.284 - also from Some have "?rep_corec a =
3.285 - CONS (Datatype.Leaf (fst p)) (?rep_corec (snd p))"
3.286 - by (simp add: LList_corec split: prod.split)
3.287 - also have "?rep_corec (snd p) = Rep_llist (?corec (snd p))"
3.288 - by (simp only: llist_corec_def Abs_llist_inverse LList_corec_type2)
3.289 - finally have "?corec a = LCons (fst p) (?corec (snd p))"
3.290 - by (simp only: LCons_def)
3.291 - with Some show ?thesis by (simp split: prod.split)
3.292 -qed
3.293 -
3.294 -
3.295 -subsection {* Equality as greatest fixed-point -- the bisimulation principle *}
3.296 -
3.297 -coinductive_set EqLList for r
3.298 -where EqNIL: "(NIL, NIL) \<in> EqLList r"
3.299 - | EqCONS: "(a, b) \<in> r \<Longrightarrow> (M, N) \<in> EqLList r \<Longrightarrow>
3.300 - (CONS a M, CONS b N) \<in> EqLList r"
3.301 -
3.302 -lemma EqLList_unfold:
3.303 - "EqLList r = dsum (Id_on {Datatype.Numb 0}) (dprod r (EqLList r))"
3.304 - by (fast intro!: EqLList.intros [unfolded NIL_def CONS_def]
3.305 - elim: EqLList.cases [unfolded NIL_def CONS_def])
3.306 -
3.307 -lemma EqLList_implies_ntrunc_equality:
3.308 - "(M, N) \<in> EqLList (Id_on A) \<Longrightarrow> ntrunc k M = ntrunc k N"
3.309 - apply (induct k arbitrary: M N rule: nat_less_induct)
3.310 - apply (erule EqLList.cases)
3.311 - apply (safe del: equalityI)
3.312 - apply (case_tac n)
3.313 - apply simp
3.314 - apply (rename_tac n')
3.315 - apply (case_tac n')
3.316 - apply (simp_all add: CONS_def less_Suc_eq)
3.317 - done
3.318 -
3.319 -lemma Domain_EqLList: "Domain (EqLList (Id_on A)) \<subseteq> LList A"
3.320 - apply (rule subsetI)
3.321 - apply (erule LList.coinduct)
3.322 - apply (subst (asm) EqLList_unfold)
3.323 - apply (auto simp add: NIL_def CONS_def)
3.324 - done
3.325 -
3.326 -lemma EqLList_Id_on: "EqLList (Id_on A) = Id_on (LList A)"
3.327 - (is "?lhs = ?rhs")
3.328 -proof
3.329 - show "?lhs \<subseteq> ?rhs"
3.330 - apply (rule subsetI)
3.331 - apply (rule_tac p = x in PairE)
3.332 - apply clarify
3.333 - apply (rule Id_on_eqI)
3.334 - apply (rule EqLList_implies_ntrunc_equality [THEN ntrunc_equality],
3.335 - assumption)
3.336 - apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]])
3.337 - done
3.338 - {
3.339 - fix M N assume "(M, N) \<in> Id_on (LList A)"
3.340 - then have "(M, N) \<in> EqLList (Id_on A)"
3.341 - proof coinduct
3.342 - case (EqLList M N)
3.343 - then obtain L where L: "L \<in> LList A" and MN: "M = L" "N = L" by blast
3.344 - from L show ?case
3.345 - proof cases
3.346 - case NIL with MN have ?EqNIL by simp
3.347 - then show ?thesis ..
3.348 - next
3.349 - case CONS with MN have ?EqCONS by (simp add: Id_onI)
3.350 - then show ?thesis ..
3.351 - qed
3.352 - qed
3.353 - }
3.354 - then show "?rhs \<subseteq> ?lhs" by auto
3.355 -qed
3.356 -
3.357 -lemma EqLList_Id_on_iff [iff]: "(p \<in> EqLList (Id_on A)) = (p \<in> Id_on (LList A))"
3.358 - by (simp only: EqLList_Id_on)
3.359 -
3.360 -
3.361 -text {*
3.362 - To show two LLists are equal, exhibit a bisimulation! (Also admits
3.363 - true equality.)
3.364 -*}
3.365 -
3.366 -lemma LList_equalityI
3.367 - [consumes 1, case_names EqLList, case_conclusion EqLList EqNIL EqCONS]:
3.368 - assumes r: "(M, N) \<in> r"
3.369 - and step: "\<And>M N. (M, N) \<in> r \<Longrightarrow>
3.370 - M = NIL \<and> N = NIL \<or>
3.371 - (\<exists>a b M' N'.
3.372 - M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> Id_on A \<and>
3.373 - ((M', N') \<in> r \<or> (M', N') \<in> EqLList (Id_on A)))"
3.374 - shows "M = N"
3.375 -proof -
3.376 - from r have "(M, N) \<in> EqLList (Id_on A)"
3.377 - proof coinduct
3.378 - case EqLList
3.379 - then show ?case by (rule step)
3.380 - qed
3.381 - then show ?thesis by auto
3.382 -qed
3.383 -
3.384 -lemma LList_fun_equalityI
3.385 - [consumes 1, case_names NIL_type NIL CONS, case_conclusion CONS EqNIL EqCONS]:
3.386 - assumes M: "M \<in> LList A"
3.387 - and fun_NIL: "g NIL \<in> LList A" "f NIL = g NIL"
3.388 - and fun_CONS: "\<And>x l. x \<in> A \<Longrightarrow> l \<in> LList A \<Longrightarrow>
3.389 - (f (CONS x l), g (CONS x l)) = (NIL, NIL) \<or>
3.390 - (\<exists>M N a b.
3.391 - (f (CONS x l), g (CONS x l)) = (CONS a M, CONS b N) \<and>
3.392 - (a, b) \<in> Id_on A \<and>
3.393 - (M, N) \<in> {(f u, g u) | u. u \<in> LList A} \<union> Id_on (LList A))"
3.394 - (is "\<And>x l. _ \<Longrightarrow> _ \<Longrightarrow> ?fun_CONS x l")
3.395 - shows "f M = g M"
3.396 -proof -
3.397 - let ?bisim = "{(f L, g L) | L. L \<in> LList A}"
3.398 - have "(f M, g M) \<in> ?bisim" using M by blast
3.399 - then show ?thesis
3.400 - proof (coinduct taking: A rule: LList_equalityI)
3.401 - case (EqLList M N)
3.402 - then obtain L where MN: "M = f L" "N = g L" and L: "L \<in> LList A" by blast
3.403 - from L show ?case
3.404 - proof (cases L)
3.405 - case NIL
3.406 - with fun_NIL and MN have "(M, N) \<in> Id_on (LList A)" by auto
3.407 - then have "(M, N) \<in> EqLList (Id_on A)" ..
3.408 - then show ?thesis by cases simp_all
3.409 - next
3.410 - case (CONS a K)
3.411 - from fun_CONS and `a \<in> A` `K \<in> LList A`
3.412 - have "?fun_CONS a K" (is "?NIL \<or> ?CONS") .
3.413 - then show ?thesis
3.414 - proof
3.415 - assume ?NIL
3.416 - with MN CONS have "(M, N) \<in> Id_on (LList A)" by auto
3.417 - then have "(M, N) \<in> EqLList (Id_on A)" ..
3.418 - then show ?thesis by cases simp_all
3.419 - next
3.420 - assume ?CONS
3.421 - with CONS obtain a b M' N' where
3.422 - fg: "(f L, g L) = (CONS a M', CONS b N')"
3.423 - and ab: "(a, b) \<in> Id_on A"
3.424 - and M'N': "(M', N') \<in> ?bisim \<union> Id_on (LList A)"
3.425 - by blast
3.426 - from M'N' show ?thesis
3.427 - proof
3.428 - assume "(M', N') \<in> ?bisim"
3.429 - with MN fg ab show ?thesis by simp
3.430 - next
3.431 - assume "(M', N') \<in> Id_on (LList A)"
3.432 - then have "(M', N') \<in> EqLList (Id_on A)" ..
3.433 - with MN fg ab show ?thesis by simp
3.434 - qed
3.435 - qed
3.436 - qed
3.437 - qed
3.438 -qed
3.439 -
3.440 -text {*
3.441 - Finality of @{text "llist A"}: Uniqueness of functions defined by corecursion.
3.442 -*}
3.443 -
3.444 -lemma equals_LList_corec:
3.445 - assumes h: "\<And>x. h x =
3.446 - (case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h w))"
3.447 - shows "h x = (\<lambda>x. LList_corec x f) x"
3.448 -proof -
3.449 - def h' \<equiv> "\<lambda>x. LList_corec x f"
3.450 - then have h': "\<And>x. h' x =
3.451 - (case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h' w))"
3.452 - unfolding h'_def by (simp add: LList_corec)
3.453 - have "(h x, h' x) \<in> {(h u, h' u) | u. True}" by blast
3.454 - then show "h x = h' x"
3.455 - proof (coinduct taking: UNIV rule: LList_equalityI)
3.456 - case (EqLList M N)
3.457 - then obtain x where MN: "M = h x" "N = h' x" by blast
3.458 - show ?case
3.459 - proof (cases "f x")
3.460 - case None
3.461 - with h h' MN have ?EqNIL by simp
3.462 - then show ?thesis ..
3.463 - next
3.464 - case (Some p)
3.465 - with h h' MN have "M = CONS (fst p) (h (snd p))"
3.466 - and "N = CONS (fst p) (h' (snd p))"
3.467 - by (simp_all split: prod.split)
3.468 - then have ?EqCONS by (auto iff: Id_on_iff)
3.469 - then show ?thesis ..
3.470 - qed
3.471 - qed
3.472 -qed
3.473 -
3.474 -
3.475 -lemma llist_equalityI
3.476 - [consumes 1, case_names Eqllist, case_conclusion Eqllist EqLNil EqLCons]:
3.477 - assumes r: "(l1, l2) \<in> r"
3.478 - and step: "\<And>q. q \<in> r \<Longrightarrow>
3.479 - q = (LNil, LNil) \<or>
3.480 - (\<exists>l1 l2 a b.
3.481 - q = (LCons a l1, LCons b l2) \<and> a = b \<and>
3.482 - ((l1, l2) \<in> r \<or> l1 = l2))"
3.483 - (is "\<And>q. _ \<Longrightarrow> ?EqLNil q \<or> ?EqLCons q")
3.484 - shows "l1 = l2"
3.485 -proof -
3.486 - def M \<equiv> "Rep_llist l1" and N \<equiv> "Rep_llist l2"
3.487 - with r have "(M, N) \<in> {(Rep_llist l1, Rep_llist l2) | l1 l2. (l1, l2) \<in> r}"
3.488 - by blast
3.489 - then have "M = N"
3.490 - proof (coinduct taking: UNIV rule: LList_equalityI)
3.491 - case (EqLList M N)
3.492 - then obtain l1 l2 where
3.493 - MN: "M = Rep_llist l1" "N = Rep_llist l2" and r: "(l1, l2) \<in> r"
3.494 - by auto
3.495 - from step [OF r] show ?case
3.496 - proof
3.497 - assume "?EqLNil (l1, l2)"
3.498 - with MN have ?EqNIL by (simp add: Rep_llist_LNil)
3.499 - then show ?thesis ..
3.500 - next
3.501 - assume "?EqLCons (l1, l2)"
3.502 - with MN have ?EqCONS
3.503 - by (force simp add: Rep_llist_LCons EqLList_Id_on intro: Rep_llist_UNIV)
3.504 - then show ?thesis ..
3.505 - qed
3.506 - qed
3.507 - then show ?thesis by (simp add: M_def N_def Rep_llist_inject)
3.508 -qed
3.509 -
3.510 -lemma llist_fun_equalityI
3.511 - [case_names LNil LCons, case_conclusion LCons EqLNil EqLCons]:
3.512 - assumes fun_LNil: "f LNil = g LNil"
3.513 - and fun_LCons: "\<And>x l.
3.514 - (f (LCons x l), g (LCons x l)) = (LNil, LNil) \<or>
3.515 - (\<exists>l1 l2 a b.
3.516 - (f (LCons x l), g (LCons x l)) = (LCons a l1, LCons b l2) \<and>
3.517 - a = b \<and> ((l1, l2) \<in> {(f u, g u) | u. True} \<or> l1 = l2))"
3.518 - (is "\<And>x l. ?fun_LCons x l")
3.519 - shows "f l = g l"
3.520 -proof -
3.521 - have "(f l, g l) \<in> {(f l, g l) | l. True}" by blast
3.522 - then show ?thesis
3.523 - proof (coinduct rule: llist_equalityI)
3.524 - case (Eqllist q)
3.525 - then obtain l where q: "q = (f l, g l)" by blast
3.526 - show ?case
3.527 - proof (cases l)
3.528 - case LNil
3.529 - with fun_LNil and q have "q = (g LNil, g LNil)" by simp
3.530 - then show ?thesis by (cases "g LNil") simp_all
3.531 - next
3.532 - case (LCons x l')
3.533 - with `?fun_LCons x l'` q LCons show ?thesis by blast
3.534 - qed
3.535 - qed
3.536 -qed
3.537 -
3.538 -
3.539 -subsection {* Derived operations -- both on the set and abstract type *}
3.540 -
3.541 -subsubsection {* @{text Lconst} *}
3.542 -
3.543 -definition "Lconst M \<equiv> lfp (\<lambda>N. CONS M N)"
3.544 -
3.545 -lemma Lconst_fun_mono: "mono (CONS M)"
3.546 - by (simp add: monoI CONS_mono)
3.547 -
3.548 -lemma Lconst: "Lconst M = CONS M (Lconst M)"
3.549 - by (rule Lconst_def [THEN def_lfp_unfold]) (rule Lconst_fun_mono)
3.550 -
3.551 -lemma Lconst_type:
3.552 - assumes "M \<in> A"
3.553 - shows "Lconst M \<in> LList A"
3.554 -proof -
3.555 - have "Lconst M \<in> {Lconst (id M)}" by simp
3.556 - then show ?thesis
3.557 - proof coinduct
3.558 - case (LList N)
3.559 - then have "N = Lconst M" by simp
3.560 - also have "\<dots> = CONS M (Lconst M)" by (rule Lconst)
3.561 - finally have ?CONS using `M \<in> A` by simp
3.562 - then show ?case ..
3.563 - qed
3.564 -qed
3.565 -
3.566 -lemma Lconst_eq_LList_corec: "Lconst M = LList_corec M (\<lambda>x. Some (x, x))"
3.567 - apply (rule equals_LList_corec)
3.568 - apply simp
3.569 - apply (rule Lconst)
3.570 - done
3.571 -
3.572 -lemma gfp_Lconst_eq_LList_corec:
3.573 - "gfp (\<lambda>N. CONS M N) = LList_corec M (\<lambda>x. Some(x, x))"
3.574 - apply (rule equals_LList_corec)
3.575 - apply simp
3.576 - apply (rule Lconst_fun_mono [THEN gfp_unfold])
3.577 - done
3.578 -
3.579 -
3.580 -subsubsection {* @{text Lmap} and @{text lmap} *}
3.581 -
3.582 -definition
3.583 - "Lmap f M = LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
3.584 -definition
3.585 - "lmap f l = llist_corec l
3.586 - (\<lambda>z.
3.587 - case z of LNil \<Rightarrow> None
3.588 - | LCons y z \<Rightarrow> Some (f y, z))"
3.589 -
3.590 -lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
3.591 - and Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"
3.592 - by (simp_all add: Lmap_def LList_corec)
3.593 -
3.594 -lemma Lmap_type:
3.595 - assumes M: "M \<in> LList A"
3.596 - and f: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> B"
3.597 - shows "Lmap f M \<in> LList B"
3.598 -proof -
3.599 - from M have "Lmap f M \<in> {Lmap f N | N. N \<in> LList A}" by blast
3.600 - then show ?thesis
3.601 - proof coinduct
3.602 - case (LList L)
3.603 - then obtain N where L: "L = Lmap f N" and N: "N \<in> LList A" by blast
3.604 - from N show ?case
3.605 - proof cases
3.606 - case NIL
3.607 - with L have ?NIL by simp
3.608 - then show ?thesis ..
3.609 - next
3.610 - case (CONS K a)
3.611 - with f L have ?CONS by auto
3.612 - then show ?thesis ..
3.613 - qed
3.614 - qed
3.615 -qed
3.616 -
3.617 -lemma Lmap_compose:
3.618 - assumes M: "M \<in> LList A"
3.619 - shows "Lmap (f o g) M = Lmap f (Lmap g M)" (is "?lhs M = ?rhs M")
3.620 -proof -
3.621 - have "(?lhs M, ?rhs M) \<in> {(?lhs N, ?rhs N) | N. N \<in> LList A}"
3.622 - using M by blast
3.623 - then show ?thesis
3.624 - proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
3.625 - case (EqLList L M)
3.626 - then obtain N where LM: "L = ?lhs N" "M = ?rhs N" and N: "N \<in> LList A" by blast
3.627 - from N show ?case
3.628 - proof cases
3.629 - case NIL
3.630 - with LM have ?EqNIL by simp
3.631 - then show ?thesis ..
3.632 - next
3.633 - case CONS
3.634 - with LM have ?EqCONS by auto
3.635 - then show ?thesis ..
3.636 - qed
3.637 - qed
3.638 -qed
3.639 -
3.640 -lemma Lmap_ident:
3.641 - assumes M: "M \<in> LList A"
3.642 - shows "Lmap (\<lambda>x. x) M = M" (is "?lmap M = _")
3.643 -proof -
3.644 - have "(?lmap M, M) \<in> {(?lmap N, N) | N. N \<in> LList A}" using M by blast
3.645 - then show ?thesis
3.646 - proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
3.647 - case (EqLList L M)
3.648 - then obtain N where LM: "L = ?lmap N" "M = N" and N: "N \<in> LList A" by blast
3.649 - from N show ?case
3.650 - proof cases
3.651 - case NIL
3.652 - with LM have ?EqNIL by simp
3.653 - then show ?thesis ..
3.654 - next
3.655 - case CONS
3.656 - with LM have ?EqCONS by auto
3.657 - then show ?thesis ..
3.658 - qed
3.659 - qed
3.660 -qed
3.661 -
3.662 -lemma lmap_LNil [simp, nitpick_simp]: "lmap f LNil = LNil"
3.663 - and lmap_LCons [simp, nitpick_simp]:
3.664 - "lmap f (LCons M N) = LCons (f M) (lmap f N)"
3.665 - by (simp_all add: lmap_def llist_corec)
3.666 -
3.667 -lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
3.668 - by (coinduct l rule: llist_fun_equalityI) auto
3.669 -
3.670 -lemma lmap_ident [simp]: "lmap (\<lambda>x. x) l = l"
3.671 - by (coinduct l rule: llist_fun_equalityI) auto
3.672 -
3.673 -
3.674 -
3.675 -subsubsection {* @{text Lappend} *}
3.676 -
3.677 -definition
3.678 - "Lappend M N = LList_corec (M, N)
3.679 - (split (List_case
3.680 - (List_case None (\<lambda>N1 N2. Some (N1, (NIL, N2))))
3.681 - (\<lambda>M1 M2 N. Some (M1, (M2, N)))))"
3.682 -definition
3.683 - "lappend l n = llist_corec (l, n)
3.684 - (split (llist_case
3.685 - (llist_case None (\<lambda>n1 n2. Some (n1, (LNil, n2))))
3.686 - (\<lambda>l1 l2 n. Some (l1, (l2, n)))))"
3.687 -
3.688 -lemma Lappend_NIL_NIL [simp]:
3.689 - "Lappend NIL NIL = NIL"
3.690 - and Lappend_NIL_CONS [simp]:
3.691 - "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"
3.692 - and Lappend_CONS [simp]:
3.693 - "Lappend (CONS M M') N = CONS M (Lappend M' N)"
3.694 - by (simp_all add: Lappend_def LList_corec)
3.695 -
3.696 -lemma Lappend_NIL [simp]: "M \<in> LList A \<Longrightarrow> Lappend NIL M = M"
3.697 - by (erule LList_fun_equalityI) auto
3.698 -
3.699 -lemma Lappend_NIL2: "M \<in> LList A \<Longrightarrow> Lappend M NIL = M"
3.700 - by (erule LList_fun_equalityI) auto
3.701 -
3.702 -lemma Lappend_type:
3.703 - assumes M: "M \<in> LList A" and N: "N \<in> LList A"
3.704 - shows "Lappend M N \<in> LList A"
3.705 -proof -
3.706 - have "Lappend M N \<in> {Lappend u v | u v. u \<in> LList A \<and> v \<in> LList A}"
3.707 - using M N by blast
3.708 - then show ?thesis
3.709 - proof coinduct
3.710 - case (LList L)
3.711 - then obtain M N where L: "L = Lappend M N"
3.712 - and M: "M \<in> LList A" and N: "N \<in> LList A"
3.713 - by blast
3.714 - from M show ?case
3.715 - proof cases
3.716 - case NIL
3.717 - from N show ?thesis
3.718 - proof cases
3.719 - case NIL
3.720 - with L and `M = NIL` have ?NIL by simp
3.721 - then show ?thesis ..
3.722 - next
3.723 - case CONS
3.724 - with L and `M = NIL` have ?CONS by simp
3.725 - then show ?thesis ..
3.726 - qed
3.727 - next
3.728 - case CONS
3.729 - with L N have ?CONS by auto
3.730 - then show ?thesis ..
3.731 - qed
3.732 - qed
3.733 -qed
3.734 -
3.735 -lemma lappend_LNil_LNil [simp, nitpick_simp]: "lappend LNil LNil = LNil"
3.736 - and lappend_LNil_LCons [simp, nitpick_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
3.737 - and lappend_LCons [simp, nitpick_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
3.738 - by (simp_all add: lappend_def llist_corec)
3.739 -
3.740 -lemma lappend_LNil1 [simp]: "lappend LNil l = l"
3.741 - by (coinduct l rule: llist_fun_equalityI) auto
3.742 -
3.743 -lemma lappend_LNil2 [simp]: "lappend l LNil = l"
3.744 - by (coinduct l rule: llist_fun_equalityI) auto
3.745 -
3.746 -lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
3.747 - by (coinduct l1 rule: llist_fun_equalityI) auto
3.748 -
3.749 -lemma lmap_lappend_distrib: "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
3.750 - by (coinduct l rule: llist_fun_equalityI) auto
3.751 -
3.752 -
3.753 -subsection{* iterates *}
3.754 -
3.755 -text {* @{text llist_fun_equalityI} cannot be used here! *}
3.756 -
3.757 -definition
3.758 - iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
3.759 - "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
3.760 -
3.761 -lemma iterates [nitpick_simp]: "iterates f x = LCons x (iterates f (f x))"
3.762 - apply (unfold iterates_def)
3.763 - apply (subst llist_corec)
3.764 - apply simp
3.765 - done
3.766 -
3.767 -lemma lmap_iterates: "lmap f (iterates f x) = iterates f (f x)"
3.768 -proof -
3.769 - have "(lmap f (iterates f x), iterates f (f x)) \<in>
3.770 - {(lmap f (iterates f u), iterates f (f u)) | u. True}" by blast
3.771 - then show ?thesis
3.772 - proof (coinduct rule: llist_equalityI)
3.773 - case (Eqllist q)
3.774 - then obtain x where q: "q = (lmap f (iterates f x), iterates f (f x))"
3.775 - by blast
3.776 - also have "iterates f (f x) = LCons (f x) (iterates f (f (f x)))"
3.777 - by (subst iterates) rule
3.778 - also have "iterates f x = LCons x (iterates f (f x))"
3.779 - by (subst iterates) rule
3.780 - finally have ?EqLCons by auto
3.781 - then show ?case ..
3.782 - qed
3.783 -qed
3.784 -
3.785 -lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
3.786 - by (subst lmap_iterates) (rule iterates)
3.787 -
3.788 -
3.789 -subsection{* A rather complex proof about iterates -- cf.\ Andy Pitts *}
3.790 -
3.791 -lemma funpow_lmap:
3.792 - fixes f :: "'a \<Rightarrow> 'a"
3.793 - shows "(lmap f ^^ n) (LCons b l) = LCons ((f ^^ n) b) ((lmap f ^^ n) l)"
3.794 - by (induct n) simp_all
3.795 -
3.796 -
3.797 -lemma iterates_equality:
3.798 - assumes h: "\<And>x. h x = LCons x (lmap f (h x))"
3.799 - shows "h = iterates f"
3.800 -proof
3.801 - fix x
3.802 - have "(h x, iterates f x) \<in>
3.803 - {((lmap f ^^ n) (h u), (lmap f ^^ n) (iterates f u)) | u n. True}"
3.804 - proof -
3.805 - have "(h x, iterates f x) = ((lmap f ^^ 0) (h x), (lmap f ^^ 0) (iterates f x))"
3.806 - by simp
3.807 - then show ?thesis by blast
3.808 - qed
3.809 - then show "h x = iterates f x"
3.810 - proof (coinduct rule: llist_equalityI)
3.811 - case (Eqllist q)
3.812 - then obtain u n where "q = ((lmap f ^^ n) (h u), (lmap f ^^ n) (iterates f u))"
3.813 - (is "_ = (?q1, ?q2)")
3.814 - by auto
3.815 - also have "?q1 = LCons ((f ^^ n) u) ((lmap f ^^ Suc n) (h u))"
3.816 - proof -
3.817 - have "?q1 = (lmap f ^^ n) (LCons u (lmap f (h u)))"
3.818 - by (subst h) rule
3.819 - also have "\<dots> = LCons ((f ^^ n) u) ((lmap f ^^ n) (lmap f (h u)))"
3.820 - by (rule funpow_lmap)
3.821 - also have "(lmap f ^^ n) (lmap f (h u)) = (lmap f ^^ Suc n) (h u)"
3.822 - by (simp add: funpow_swap1)
3.823 - finally show ?thesis .
3.824 - qed
3.825 - also have "?q2 = LCons ((f ^^ n) u) ((lmap f ^^ Suc n) (iterates f u))"
3.826 - proof -
3.827 - have "?q2 = (lmap f ^^ n) (LCons u (iterates f (f u)))"
3.828 - by (subst iterates) rule
3.829 - also have "\<dots> = LCons ((f ^^ n) u) ((lmap f ^^ n) (iterates f (f u)))"
3.830 - by (rule funpow_lmap)
3.831 - also have "(lmap f ^^ n) (iterates f (f u)) = (lmap f ^^ Suc n) (iterates f u)"
3.832 - by (simp add: lmap_iterates funpow_swap1)
3.833 - finally show ?thesis .
3.834 - qed
3.835 - finally have ?EqLCons by (auto simp del: funpow.simps)
3.836 - then show ?case ..
3.837 - qed
3.838 -qed
3.839 -
3.840 -lemma lappend_iterates: "lappend (iterates f x) l = iterates f x"
3.841 -proof -
3.842 - have "(lappend (iterates f x) l, iterates f x) \<in>
3.843 - {(lappend (iterates f u) l, iterates f u) | u. True}" by blast
3.844 - then show ?thesis
3.845 - proof (coinduct rule: llist_equalityI)
3.846 - case (Eqllist q)
3.847 - then obtain x where "q = (lappend (iterates f x) l, iterates f x)" by blast
3.848 - also have "iterates f x = LCons x (iterates f (f x))" by (rule iterates)
3.849 - finally have ?EqLCons by auto
3.850 - then show ?case ..
3.851 - qed
3.852 -qed
3.853 -
3.854 -setup {*
3.855 - Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
3.856 - (map dest_Const [@{term LNil}, @{term LCons}])
3.857 -*}
3.858 -
3.859 -end
4.1 --- a/src/HOL/Library/Library.thy Sat Mar 13 16:44:12 2010 +0100
4.2 +++ b/src/HOL/Library/Library.thy Sat Mar 13 17:19:12 2010 +0100
4.3 @@ -10,7 +10,6 @@
4.4 Char_ord
4.5 Code_Char_chr
4.6 Code_Integer
4.7 - Coinductive_List
4.8 Continuity
4.9 ContNotDenum
4.10 Countable