# HG changeset patch # User wenzelm # Date 1258224978 -3600 # Node ID 1a97dcd8dc6a8a8eef9b469a46fdb2fa0718a236 # Parent 3222fa0528466d77f5905bdfa0a9523027c910e2 moved old SList, LList, LFilter to AFP/Lazy-Lists-II; diff -r 3222fa052846 -r 1a97dcd8dc6a src/HOL/Induct/LFilter.thy --- a/src/HOL/Induct/LFilter.thy Sat Nov 14 18:45:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,271 +0,0 @@ -(* Title: HOL/LList.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge -*) - -header {*The "filter" functional for coinductive lists - --defined by a combination of induction and coinduction*} - -theory LFilter imports LList begin - -inductive_set - findRel :: "('a => bool) => ('a llist * 'a llist)set" - for p :: "'a => bool" - where - found: "p x ==> (LCons x l, LCons x l) \ findRel p" - | seek: "[| ~p x; (l,l') \ findRel p |] ==> (LCons x l, l') \ findRel p" - -declare findRel.intros [intro] - -definition - find :: "['a => bool, 'a llist] => 'a llist" where - "find p l = (SOME l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p)))" - -definition - lfilter :: "['a => bool, 'a llist] => 'a llist" where - "lfilter p l = llist_corec l (%l. case find p l of - LNil => None - | LCons y z => Some(y,z))" - - -subsection {* @{text findRel}: basic laws *} - -inductive_cases - findRel_LConsE [elim!]: "(LCons x l, l'') \ findRel p" - - -lemma findRel_functional [rule_format]: - "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'" -by (erule findRel.induct, auto) - -lemma findRel_imp_LCons [rule_format]: - "(l,l'): findRel p ==> \x l''. l' = LCons x l'' & p x" -by (erule findRel.induct, auto) - -lemma findRel_LNil [elim!]: "(LNil,l): findRel p ==> R" -by (blast elim: findRel.cases) - - -subsection {* Properties of @{text "Domain (findRel p)"} *} - -lemma LCons_Domain_findRel [simp]: - "LCons x l \ Domain(findRel p) = (p x | l \ Domain(findRel p))" -by auto - -lemma Domain_findRel_iff: - "(l \ Domain (findRel p)) = (\x l'. (l, LCons x l') \ findRel p & p x)" -by (blast dest: findRel_imp_LCons) - -lemma Domain_findRel_mono: - "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)" -apply clarify -apply (erule findRel.induct, blast+) -done - - -subsection {* @{text find}: basic equations *} - -lemma find_LNil [simp]: "find p LNil = LNil" -by (unfold find_def, blast) - -lemma findRel_imp_find [simp]: "(l,l') \ findRel p ==> find p l = l'" -apply (unfold find_def) -apply (blast dest: findRel_functional) -done - -lemma find_LCons_found: "p x ==> find p (LCons x l) = LCons x l" -by (blast intro: findRel_imp_find) - -lemma diverge_find_LNil [simp]: "l ~: Domain(findRel p) ==> find p l = LNil" -by (unfold find_def, blast) - -lemma find_LCons_seek: "~ (p x) ==> find p (LCons x l) = find p l" -apply (case_tac "LCons x l \ Domain (findRel p) ") - apply auto -apply (blast intro: findRel_imp_find) -done - -lemma find_LCons [simp]: - "find p (LCons x l) = (if p x then LCons x l else find p l)" -by (simp add: find_LCons_seek find_LCons_found) - - - -subsection {* @{text lfilter}: basic equations *} - -lemma lfilter_LNil [simp]: "lfilter p LNil = LNil" -by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) - -lemma diverge_lfilter_LNil [simp]: - "l ~: Domain(findRel p) ==> lfilter p l = LNil" -by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) - -lemma lfilter_LCons_found: - "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)" -by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) - -lemma findRel_imp_lfilter [simp]: - "(l, LCons x l') \ findRel p ==> lfilter p l = LCons x (lfilter p l')" -by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) - -lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l" -apply (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) -apply (case_tac "LCons x l \ Domain (findRel p) ") - apply (simp add: Domain_findRel_iff, auto) -done - -lemma lfilter_LCons [simp]: - "lfilter p (LCons x l) = - (if p x then LCons x (lfilter p l) else lfilter p l)" -by (simp add: lfilter_LCons_found lfilter_LCons_seek) - -declare llistD_Fun_LNil_I [intro!] llistD_Fun_LCons_I [intro!] - - -lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" -apply (auto iff: Domain_findRel_iff) -done - -lemma lfilter_eq_LCons [rule_format]: - "lfilter p l = LCons x l' --> - (\l''. l' = lfilter p l'' & (l, LCons x l'') \ findRel p)" -apply (subst lfilter_def [THEN def_llist_corec]) -apply (case_tac "l \ Domain (findRel p) ") - apply (auto iff: Domain_findRel_iff) -done - - -lemma lfilter_cases: "lfilter p l = LNil | - (\y l'. lfilter p l = LCons y (lfilter p l') & p y)" -apply (case_tac "l \ Domain (findRel p) ") -apply (auto iff: Domain_findRel_iff) -done - - -subsection {* @{text lfilter}: simple facts by coinduction *} - -lemma lfilter_K_True: "lfilter (%x. True) l = l" -by (rule_tac l = "l" in llist_fun_equalityI, simp_all) - -lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l" -apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) -apply safe -txt{*Cases: @{text "p x"} is true or false*} -apply (rule lfilter_cases [THEN disjE]) - apply (erule ssubst, auto) -done - - -subsection {* Numerous lemmas required to prove @{text lfilter_conj} *} - -lemma findRel_conj_lemma [rule_format]: - "(l,l') \ findRel q - ==> l' = LCons x l'' --> p x --> (l,l') \ findRel (%x. p x & q x)" -by (erule findRel.induct, auto) - -lemmas findRel_conj = findRel_conj_lemma [OF _ refl] - -lemma findRel_not_conj_Domain [rule_format]: - "(l,l'') \ findRel (%x. p x & q x) - ==> (l, LCons x l') \ findRel q --> ~ p x --> - l' \ Domain (findRel (%x. p x & q x))" -by (erule findRel.induct, auto) - -lemma findRel_conj2 [rule_format]: - "(l,lxx) \ findRel q - ==> lxx = LCons x lx --> (lx,lz) \ findRel(%x. p x & q x) --> ~ p x - --> (l,lz) \ findRel (%x. p x & q x)" -by (erule findRel.induct, auto) - -lemma findRel_lfilter_Domain_conj [rule_format]: - "(lx,ly) \ findRel p - ==> \l. lx = lfilter q l --> l \ Domain (findRel(%x. p x & q x))" -apply (erule findRel.induct) - apply (blast dest!: sym [THEN lfilter_eq_LCons] intro: findRel_conj, auto) -apply (drule sym [THEN lfilter_eq_LCons], auto) -apply (drule spec) -apply (drule refl [THEN rev_mp]) -apply (blast intro: findRel_conj2) -done - - -lemma findRel_conj_lfilter [rule_format]: - "(l,l'') \ findRel(%x. p x & q x) - ==> l'' = LCons y l' --> - (lfilter q l, LCons y (lfilter q l')) \ findRel p" -by (erule findRel.induct, auto) - -lemma lfilter_conj_lemma: - "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l) - \ llistD_Fun (range (%u. (lfilter p (lfilter q u), - lfilter (%x. p x & q x) u)))" -apply (case_tac "l \ Domain (findRel q)") - apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))") - prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono]) - txt{*There are no @{text qs} in @{text l}: both lists are @{text LNil}*} - apply (simp_all add: Domain_findRel_iff, clarify) -txt{*case @{text "q x"}*} -apply (case_tac "p x") - apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter]) - txt{*case @{text "q x"} and @{text "~(p x)"} *} -apply (case_tac "l' \ Domain (findRel (%x. p x & q x))") - txt{*subcase: there is no @{text "p & q"} in @{text l'} and therefore none in @{text l}*} - apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))") - prefer 3 apply (blast intro: findRel_not_conj_Domain) - apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ") - prefer 3 apply (blast intro: findRel_lfilter_Domain_conj) - txt{* {\dots} and therefore too, no @{text p} in @{text "lfilter q l'"}. - Both results are @{text LNil}*} - apply (simp_all add: Domain_findRel_iff, clarify) -txt{*subcase: there is a @{text "p & q"} in @{text l'} and therefore also one in @{text l} *} -apply (subgoal_tac " (l, LCons xa l'a) \ findRel (%x. p x & q x) ") - prefer 2 apply (blast intro: findRel_conj2) -apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) \ findRel p") - apply simp -apply (blast intro: findRel_conj_lfilter) -done - - -lemma lfilter_conj: "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l" -apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) -apply (blast intro: lfilter_conj_lemma rev_subsetD [OF _ llistD_Fun_mono]) -done - - -subsection {* Numerous lemmas required to prove ??: - @{text "lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)"} - *} - -lemma findRel_lmap_Domain: - "(l,l') \ findRel(%x. p (f x)) ==> lmap f l \ Domain(findRel p)" -by (erule findRel.induct, auto) - -lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' --> - (\y l''. x = f y & l' = lmap f l'' & l = LCons y l'')" -apply (subst lmap_def [THEN def_llist_corec]) -apply (rule_tac l = "l" in llistE, auto) -done - - -lemma lmap_LCons_findRel_lemma [rule_format]: - "(lx,ly) \ findRel p - ==> \l. lmap f l = lx --> ly = LCons x l' --> - (\y l''. x = f y & l' = lmap f l'' & - (l, LCons y l'') \ findRel(%x. p(f x)))" -apply (erule findRel.induct, simp_all) -apply (blast dest!: lmap_eq_LCons)+ -done - -lemmas lmap_LCons_findRel = lmap_LCons_findRel_lemma [OF _ refl refl] - -lemma lfilter_lmap: "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)" -apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) -apply safe -apply (case_tac "lmap f l \ Domain (findRel p)") - apply (simp add: Domain_findRel_iff, clarify) - apply (frule lmap_LCons_findRel, force) -apply (subgoal_tac "l ~: Domain (findRel (%x. p (f x)))", simp) -apply (blast intro: findRel_lmap_Domain) -done - -end diff -r 3222fa052846 -r 1a97dcd8dc6a src/HOL/Induct/LList.thy --- a/src/HOL/Induct/LList.thy Sat Nov 14 18:45:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,912 +0,0 @@ -(* Title: HOL/Induct/LList.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - -Shares NIL, CONS, List_case with List.thy - -Still needs flatten function -- hard because it need -bounds on the amount of lookahead required. - -Could try (but would it work for the gfp analogue of term?) - LListD_Fun_def "LListD_Fun(A) == (%Z. Id_on({Numb(0)}) <++> Id_on(A) <**> Z)" - -A nice but complex example would be [ML for the Working Programmer, page 176] - from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1)))) - -Previous definition of llistD_Fun was explicit: - llistD_Fun_def - "llistD_Fun(r) == - {(LNil,LNil)} Un - (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)" -*) - -header {*Definition of type llist by a greatest fixed point*} - -theory LList imports SList begin - -coinductive_set - llist :: "'a item set => 'a item set" - for A :: "'a item set" - where - NIL_I: "NIL \ llist(A)" - | CONS_I: "[| a \ A; M \ llist(A) |] ==> CONS a M \ llist(A)" - -coinductive_set - LListD :: "('a item * 'a item)set => ('a item * 'a item)set" - for r :: "('a item * 'a item)set" - where - NIL_I: "(NIL, NIL) \ LListD(r)" - | CONS_I: "[| (a,b) \ r; (M,N) \ LListD(r) |] - ==> (CONS a M, CONS b N) \ LListD(r)" - - -typedef (LList) - 'a llist = "llist(range Leaf) :: 'a item set" - by (blast intro: llist.NIL_I) - -definition - list_Fun :: "['a item set, 'a item set] => 'a item set" where - --{*Now used exclusively for abbreviating the coinduction rule*} - "list_Fun A X = {z. z = NIL | (\M a. z = CONS a M & a \ A & M \ X)}" - -definition - LListD_Fun :: - "[('a item * 'a item)set, ('a item * 'a item)set] => - ('a item * 'a item)set" where - "LListD_Fun r X = - {z. z = (NIL, NIL) | - (\M N a b. z = (CONS a M, CONS b N) & (a, b) \ r & (M, N) \ X)}" - -definition - LNil :: "'a llist" where - --{*abstract constructor*} - "LNil = Abs_LList NIL" - -definition - LCons :: "['a, 'a llist] => 'a llist" where - --{*abstract constructor*} - "LCons x xs = Abs_LList(CONS (Leaf x) (Rep_LList xs))" - -definition - llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b" where - "llist_case c d l = - List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)" - -definition - LList_corec_fun :: "[nat, 'a=> ('b item * 'a) option, 'a] => 'b item" where - "LList_corec_fun k f == - nat_rec (%x. {}) - (%j r x. case f x of None => NIL - | Some(z,w) => CONS z (r w)) - k" - -definition - LList_corec :: "['a, 'a => ('b item * 'a) option] => 'b item" where - "LList_corec a f = (\k. LList_corec_fun k f a)" - -definition - llist_corec :: "['a, 'a => ('b * 'a) option] => 'b llist" where - "llist_corec a f = - Abs_LList(LList_corec a - (%z. case f z of None => None - | Some(v,w) => Some(Leaf(v), w)))" - -definition - llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set" where - "llistD_Fun(r) = - prod_fun Abs_LList Abs_LList ` - LListD_Fun (Id_on(range Leaf)) - (prod_fun Rep_LList Rep_LList ` r)" - - - -text{* The case syntax for type @{text "'a llist"} *} -syntax (* FIXME proper case syntax!? *) - LNil :: logic - LCons :: logic -translations - "case p of LNil => a | LCons x l => b" == "CONST llist_case a (%x l. b) p" - - -subsubsection{* Sample function definitions. Item-based ones start with @{text L} *} - -definition - Lmap :: "('a item => 'b item) => ('a item => 'b item)" where - "Lmap f M = LList_corec M (List_case None (%x M'. Some((f(x), M'))))" - -definition - lmap :: "('a=>'b) => ('a llist => 'b llist)" where - "lmap f l = llist_corec l (%z. case z of LNil => None - | LCons y z => Some(f(y), z))" - -definition - iterates :: "['a => 'a, 'a] => 'a llist" where - "iterates f a = llist_corec a (%x. Some((x, f(x))))" - -definition - Lconst :: "'a item => 'a item" where - "Lconst(M) == lfp(%N. CONS M N)" - -definition - Lappend :: "['a item, 'a item] => 'a item" where - "Lappend M N = LList_corec (M,N) - (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2))))) - (%M1 M2 N. Some((M1, (M2,N))))))" - -definition - lappend :: "['a llist, 'a llist] => 'a llist" where - "lappend l n = llist_corec (l,n) - (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2))))) - (%l1 l2 n. Some((l1, (l2,n))))))" - - -text{*Append generates its result by applying f, where - f((NIL,NIL)) = None - f((NIL, CONS N1 N2)) = Some((N1, (NIL,N2)) - f((CONS M1 M2, N)) = Some((M1, (M2,N)) -*} - -text{* -SHOULD @{text LListD_Fun_CONS_I}, etc., be equations (for rewriting)? -*} - -lemmas UN1_I = UNIV_I [THEN UN_I, standard] - -subsubsection{* Simplification *} - -declare option.split [split] - -text{*This justifies using llist in other recursive type definitions*} -lemma llist_mono: - assumes subset: "A \ B" - shows "llist A \ llist B" -proof - fix x - assume "x \ llist A" - then show "x \ llist B" - proof coinduct - case llist - then show ?case using subset - by cases blast+ - qed -qed - - -lemma llist_unfold: "llist(A) = usum {Numb(0)} (uprod A (llist A))" - by (fast intro!: llist.intros [unfolded NIL_def CONS_def] - elim: llist.cases [unfolded NIL_def CONS_def]) - - -subsection{* Type checking by coinduction *} - -text {* - {\dots} using @{text list_Fun} THE COINDUCTIVE DEFINITION PACKAGE - COULD DO THIS! -*} - -lemma llist_coinduct: - "[| M \ X; X \ list_Fun A (X Un llist(A)) |] ==> M \ llist(A)" -apply (simp add: list_Fun_def) -apply (erule llist.coinduct) -apply (blast intro: elim:); -done - -lemma list_Fun_NIL_I [iff]: "NIL \ list_Fun A X" -by (simp add: list_Fun_def NIL_def) - -lemma list_Fun_CONS_I [intro!,simp]: - "[| M \ A; N \ X |] ==> CONS M N \ list_Fun A X" -by (simp add: list_Fun_def CONS_def) - - -text{*Utilise the ``strong'' part, i.e. @{text "gfp(f)"}*} -lemma list_Fun_llist_I: "M \ llist(A) ==> M \ list_Fun A (X Un llist(A))" -apply (unfold list_Fun_def) -apply (erule llist.cases) -apply auto -done - -subsection{* @{text LList_corec} satisfies the desired recurion equation *} - -text{*A continuity result?*} -lemma CONS_UN1: "CONS M (\x. f(x)) = (\x. CONS M (f x))" -apply (simp add: CONS_def In1_UN1 Scons_UN1_y) -done - -lemma CONS_mono: "[| M\M'; N\N' |] ==> CONS M N \ CONS M' N'" -apply (simp add: CONS_def In1_mono Scons_mono) -done - -declare LList_corec_fun_def [THEN def_nat_rec_0, simp] - LList_corec_fun_def [THEN def_nat_rec_Suc, simp] - - -subsubsection{* The directions of the equality are proved separately *} - -lemma LList_corec_subset1: - "LList_corec a f \ - (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))" -apply (unfold LList_corec_def) -apply (rule UN_least) -apply (case_tac k) -apply (simp_all (no_asm_simp)) -apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+ -done - -lemma LList_corec_subset2: - "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) \ - LList_corec a f" -apply (simp add: LList_corec_def) -apply (simp add: CONS_UN1, safe) -apply (rule_tac a="Suc(?k)" in UN_I, simp, simp)+ -done - -text{*the recursion equation for @{text LList_corec} -- NOT SUITABLE FOR REWRITING!*} -lemma LList_corec: - "LList_corec a f = - (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))" -by (rule equalityI LList_corec_subset1 LList_corec_subset2)+ - -text{*definitional version of same*} -lemma def_LList_corec: - "[| !!x. h(x) = LList_corec x f |] - ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))" -by (simp add: LList_corec) - -text{*A typical use of co-induction to show membership in the @{text gfp}. - Bisimulation is @{text "range(%x. LList_corec x f)"} *} -lemma LList_corec_type: "LList_corec a f \ llist UNIV" -apply (rule_tac X = "range (%x. LList_corec x ?g)" in llist_coinduct) -apply (rule rangeI, safe) -apply (subst LList_corec, simp) -done - - -subsection{* @{text llist} equality as a @{text gfp}; the bisimulation principle *} - -text{*This theorem is actually used, unlike the many similar ones in ZF*} -lemma LListD_unfold: "LListD r = dsum (Id_on {Numb 0}) (dprod r (LListD r))" - by (fast intro!: LListD.intros [unfolded NIL_def CONS_def] - elim: LListD.cases [unfolded NIL_def CONS_def]) - -lemma LListD_implies_ntrunc_equality [rule_format]: - "\M N. (M,N) \ LListD(Id_on A) --> ntrunc k M = ntrunc k N" -apply (induct_tac "k" rule: nat_less_induct) -apply (safe del: equalityI) -apply (erule LListD.cases) -apply (safe del: equalityI) -apply (case_tac "n", simp) -apply (rename_tac "n'") -apply (case_tac "n'") -apply (simp_all add: CONS_def less_Suc_eq) -done - -text{*The domain of the @{text LListD} relation*} -lemma Domain_LListD: - "Domain (LListD(Id_on A)) \ llist(A)" -apply (rule subsetI) -apply (erule llist.coinduct) -apply (simp add: NIL_def CONS_def) -apply (drule_tac P = "%x. xa \ Domain x" in LListD_unfold [THEN subst], auto) -done - -text{*This inclusion justifies the use of coinduction to show @{text "M = N"}*} -lemma LListD_subset_Id_on: "LListD(Id_on A) \ Id_on(llist(A))" -apply (rule subsetI) -apply (rule_tac p = x in PairE, safe) -apply (rule Id_on_eqI) -apply (rule LListD_implies_ntrunc_equality [THEN ntrunc_equality], assumption) -apply (erule DomainI [THEN Domain_LListD [THEN subsetD]]) -done - - -subsubsection{* Coinduction, using @{text LListD_Fun} *} - -text {* THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! *} - -lemma LListD_Fun_mono: "A\B ==> LListD_Fun r A \ LListD_Fun r B" -apply (simp add: LListD_Fun_def) -apply (assumption | rule basic_monos)+ -done - -lemma LListD_coinduct: - "[| M \ X; X \ LListD_Fun r (X Un LListD(r)) |] ==> M \ LListD(r)" -apply (cases M) -apply (simp add: LListD_Fun_def) -apply (erule LListD.coinduct) -apply (auto ); -done - -lemma LListD_Fun_NIL_I: "(NIL,NIL) \ LListD_Fun r s" -by (simp add: LListD_Fun_def NIL_def) - -lemma LListD_Fun_CONS_I: - "[| x\A; (M,N):s |] ==> (CONS x M, CONS x N) \ LListD_Fun (Id_on A) s" -by (simp add: LListD_Fun_def CONS_def, blast) - -text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*} -lemma LListD_Fun_LListD_I: - "M \ LListD(r) ==> M \ LListD_Fun r (X Un LListD(r))" -apply (cases M) -apply (simp add: LListD_Fun_def) -apply (erule LListD.cases) -apply auto -done - - -text{*This converse inclusion helps to strengthen @{text LList_equalityI}*} -lemma Id_on_subset_LListD: "Id_on(llist(A)) \ LListD(Id_on A)" -apply (rule subsetI) -apply (erule LListD_coinduct) -apply (rule subsetI) -apply (erule Id_onE) -apply (erule ssubst) -apply (erule llist.cases) -apply (simp_all add: Id_onI LListD_Fun_NIL_I LListD_Fun_CONS_I) -done - -lemma LListD_eq_Id_on: "LListD(Id_on A) = Id_on(llist(A))" -apply (rule equalityI LListD_subset_Id_on Id_on_subset_LListD)+ -done - -lemma LListD_Fun_Id_on_I: "M \ llist(A) ==> (M,M) \ LListD_Fun (Id_on A) (X Un Id_on(llist(A)))" -apply (rule LListD_eq_Id_on [THEN subst]) -apply (rule LListD_Fun_LListD_I) -apply (simp add: LListD_eq_Id_on Id_onI) -done - - -subsubsection{* To show two LLists are equal, exhibit a bisimulation! - [also admits true equality] - Replace @{text A} by some particular set, like @{text "{x. True}"}??? *} -lemma LList_equalityI: - "[| (M,N) \ r; r \ LListD_Fun (Id_on A) (r Un Id_on(llist(A))) |] - ==> M=N" -apply (rule LListD_subset_Id_on [THEN subsetD, THEN Id_onE]) -apply (erule LListD_coinduct) -apply (simp add: LListD_eq_Id_on, safe) -done - - -subsection{* Finality of @{text "llist(A)"}: Uniqueness of functions defined by corecursion *} - -text{*We must remove @{text Pair_eq} because it may turn an instance of reflexivity - @{text "(h1 b, h2 b) = (h1 ?x17, h2 ?x17)"} into a conjunction! - (or strengthen the Solver?) -*} -declare Pair_eq [simp del] - -text{*abstract proof using a bisimulation*} -lemma LList_corec_unique: - "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w)); - !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |] - ==> h1=h2" -apply (rule ext) -txt{*next step avoids an unknown (and flexflex pair) in simplification*} -apply (rule_tac A = UNIV and r = "range(%u. (h1 u, h2 u))" - in LList_equalityI) -apply (rule rangeI, safe) -apply (simp add: LListD_Fun_NIL_I UNIV_I [THEN LListD_Fun_CONS_I]) -done - -lemma equals_LList_corec: - "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |] - ==> h = (%x. LList_corec x f)" -by (simp add: LList_corec_unique LList_corec) - - -subsubsection{*Obsolete proof of @{text LList_corec_unique}: - complete induction, not coinduction *} - -lemma ntrunc_one_CONS [simp]: "ntrunc (Suc 0) (CONS M N) = {}" -by (simp add: CONS_def ntrunc_one_In1) - -lemma ntrunc_CONS [simp]: - "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)" -by (simp add: CONS_def) - - -lemma - assumes prem1: - "!!x. h1 x = (case f x of None => NIL | Some(z,w) => CONS z (h1 w))" - and prem2: - "!!x. h2 x = (case f x of None => NIL | Some(z,w) => CONS z (h2 w))" - shows "h1=h2" -apply (rule ntrunc_equality [THEN ext]) -apply (rule_tac x = x in spec) -apply (induct_tac "k" rule: nat_less_induct) -apply (rename_tac "n") -apply (rule allI) -apply (subst prem1) -apply (subst prem2, simp) -apply (intro strip) -apply (case_tac "n") -apply (rename_tac [2] "m") -apply (case_tac [2] "m", simp_all) -done - - -subsection{*Lconst: defined directly by @{text lfp} *} - -text{*But it could be defined by corecursion.*} - -lemma Lconst_fun_mono: "mono(CONS(M))" -apply (rule monoI subset_refl CONS_mono)+ -apply assumption -done - -text{* @{text "Lconst(M) = CONS M (Lconst M)"} *} -lemmas Lconst = Lconst_fun_mono [THEN Lconst_def [THEN def_lfp_unfold]] - -text{*A typical use of co-induction to show membership in the gfp. - The containing set is simply the singleton @{text "{Lconst(M)}"}. *} -lemma Lconst_type: "M\A ==> Lconst(M): llist(A)" -apply (rule singletonI [THEN llist_coinduct], safe) -apply (rule_tac P = "%u. u \ ?A" in Lconst [THEN ssubst]) -apply (assumption | rule list_Fun_CONS_I singletonI UnI1)+ -done - -lemma Lconst_eq_LList_corec: "Lconst(M) = LList_corec M (%x. Some(x,x))" -apply (rule equals_LList_corec [THEN fun_cong], simp) -apply (rule Lconst) -done - -text{*Thus we could have used gfp in the definition of Lconst*} -lemma gfp_Lconst_eq_LList_corec: "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))" -apply (rule equals_LList_corec [THEN fun_cong], simp) -apply (rule Lconst_fun_mono [THEN gfp_unfold]) -done - - -subsection{* Isomorphisms *} - -lemma LListI: "x \ llist (range Leaf) ==> x \ LList" -by (simp add: LList_def) - -lemma LListD: "x \ LList ==> x \ llist (range Leaf)" -by (simp add: LList_def) - - -subsubsection{* Distinctness of constructors *} - -lemma LCons_not_LNil [iff]: "~ LCons x xs = LNil" -apply (simp add: LNil_def LCons_def) -apply (subst Abs_LList_inject) -apply (rule llist.intros CONS_not_NIL rangeI LListI Rep_LList [THEN LListD])+ -done - -lemmas LNil_not_LCons [iff] = LCons_not_LNil [THEN not_sym, standard] - - -subsubsection{* llist constructors *} - -lemma Rep_LList_LNil: "Rep_LList LNil = NIL" -apply (simp add: LNil_def) -apply (rule llist.NIL_I [THEN LListI, THEN Abs_LList_inverse]) -done - -lemma Rep_LList_LCons: "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)" -apply (simp add: LCons_def) -apply (rule llist.CONS_I [THEN LListI, THEN Abs_LList_inverse] - rangeI Rep_LList [THEN LListD])+ -done - -subsubsection{* Injectiveness of @{text CONS} and @{text LCons} *} - -lemma CONS_CONS_eq2: "(CONS M N=CONS M' N') = (M=M' & N=N')" -apply (simp add: CONS_def) -done - -lemmas CONS_inject = CONS_CONS_eq [THEN iffD1, THEN conjE, standard] - - -text{*For reasoning about abstract llist constructors*} - -declare Rep_LList [THEN LListD, intro] LListI [intro] -declare llist.intros [intro] - -lemma LCons_LCons_eq [iff]: "(LCons x xs=LCons y ys) = (x=y & xs=ys)" -apply (simp add: LCons_def) -apply (subst Abs_LList_inject) -apply (auto simp add: Rep_LList_inject) -done - -lemma CONS_D2: "CONS M N \ llist(A) ==> M \ A & N \ llist(A)" -apply (erule llist.cases) -apply (erule CONS_neq_NIL, fast) -done - - -subsection{* Reasoning about @{text "llist(A)"} *} - -text{*A special case of @{text list_equality} for functions over lazy lists*} -lemma LList_fun_equalityI: - "[| M \ llist(A); g(NIL): llist(A); - f(NIL)=g(NIL); - !!x l. [| x\A; l \ llist(A) |] ==> - (f(CONS x l),g(CONS x l)) \ - LListD_Fun (Id_on A) ((%u.(f(u),g(u)))`llist(A) Un - Id_on(llist(A))) - |] ==> f(M) = g(M)" -apply (rule LList_equalityI) -apply (erule imageI) -apply (rule image_subsetI) -apply (erule_tac a=x in llist.cases) -apply (erule ssubst, erule ssubst, erule LListD_Fun_Id_on_I, blast) -done - - -subsection{* The functional @{text Lmap} *} - -lemma Lmap_NIL [simp]: "Lmap f NIL = NIL" -by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp) - -lemma Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)" -by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp) - - - -text{*Another type-checking proof by coinduction*} -lemma Lmap_type: - "[| M \ llist(A); !!x. x\A ==> f(x):B |] ==> Lmap f M \ llist(B)" -apply (erule imageI [THEN llist_coinduct], safe) -apply (erule llist.cases, simp_all) -done - -text{*This type checking rule synthesises a sufficiently large set for @{text f}*} -lemma Lmap_type2: "M \ llist(A) ==> Lmap f M \ llist(f`A)" -apply (erule Lmap_type) -apply (erule imageI) -done - -subsubsection{* Two easy results about @{text Lmap} *} - -lemma Lmap_compose: "M \ llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)" -apply (simp add: o_def) -apply (drule imageI) -apply (erule LList_equalityI, safe) -apply (erule llist.cases, simp_all) -apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ f])+ -apply assumption -done - -lemma Lmap_ident: "M \ llist(A) ==> Lmap (%x. x) M = M" -apply (drule imageI) -apply (erule LList_equalityI, safe) -apply (erule llist.cases, simp_all) -apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ "%x. x"])+ -apply assumption -done - - -subsection{* @{text Lappend} -- its two arguments cause some complications! *} - -lemma Lappend_NIL_NIL [simp]: "Lappend NIL NIL = NIL" -apply (simp add: Lappend_def) -apply (rule LList_corec [THEN trans], simp) -done - -lemma Lappend_NIL_CONS [simp]: - "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')" -apply (simp add: Lappend_def) -apply (rule LList_corec [THEN trans], simp) -done - -lemma Lappend_CONS [simp]: - "Lappend (CONS M M') N = CONS M (Lappend M' N)" -apply (simp add: Lappend_def) -apply (rule LList_corec [THEN trans], simp) -done - -declare llist.intros [simp] LListD_Fun_CONS_I [simp] - range_eqI [simp] image_eqI [simp] - - -lemma Lappend_NIL [simp]: "M \ llist(A) ==> Lappend NIL M = M" -by (erule LList_fun_equalityI, simp_all) - -lemma Lappend_NIL2: "M \ llist(A) ==> Lappend M NIL = M" -by (erule LList_fun_equalityI, simp_all) - - -subsubsection{* Alternative type-checking proofs for @{text Lappend} *} - -text{*weak co-induction: bisimulation and case analysis on both variables*} -lemma Lappend_type: "[| M \ llist(A); N \ llist(A) |] ==> Lappend M N \ llist(A)" -apply (rule_tac X = "\u\llist (A) . \v \ llist (A) . {Lappend u v}" in llist_coinduct) -apply fast -apply safe -apply (erule_tac a = u in llist.cases) -apply (erule_tac a = v in llist.cases, simp_all, blast) -done - -text{*strong co-induction: bisimulation and case analysis on one variable*} -lemma Lappend_type': "[| M \ llist(A); N \ llist(A) |] ==> Lappend M N \ llist(A)" -apply (rule_tac X = "(%u. Lappend u N) `llist (A)" in llist_coinduct) -apply (erule imageI) -apply (rule image_subsetI) -apply (erule_tac a = x in llist.cases) -apply (simp add: list_Fun_llist_I, simp) -done - -subsection{* Lazy lists as the type @{text "'a llist"} -- strongly typed versions of above *} - -subsubsection{* @{text llist_case}: case analysis for @{text "'a llist"} *} - -declare LListI [THEN Abs_LList_inverse, simp] -declare Rep_LList_inverse [simp] -declare Rep_LList [THEN LListD, simp] -declare rangeI [simp] inj_Leaf [simp] - -lemma llist_case_LNil [simp]: "llist_case c d LNil = c" -by (simp add: llist_case_def LNil_def) - -lemma llist_case_LCons [simp]: "llist_case c d (LCons M N) = d M N" -by (simp add: llist_case_def LCons_def) - - -text{*Elimination is case analysis, not induction.*} -lemma llistE: "[| l=LNil ==> P; !!x l'. l=LCons x l' ==> P |] ==> P" -apply (rule Rep_LList [THEN LListD, THEN llist.cases]) - apply (simp add: Rep_LList_LNil [symmetric] Rep_LList_inject, blast) -apply (erule LListI [THEN Rep_LList_cases], clarify) -apply (simp add: Rep_LList_LCons [symmetric] Rep_LList_inject, blast) -done - -subsubsection{* @{text llist_corec}: corecursion for @{text "'a llist"} *} - -text{*Lemma for the proof of @{text llist_corec}*} -lemma LList_corec_type2: - "LList_corec a - (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) - \ llist(range Leaf)" -apply (rule_tac X = "range (%x. LList_corec x ?g)" in llist_coinduct) -apply (rule rangeI, safe) -apply (subst LList_corec, force) -done - -lemma llist_corec [nitpick_simp]: - "llist_corec a f = - (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))" -apply (unfold llist_corec_def LNil_def LCons_def) -apply (subst LList_corec) -apply (case_tac "f a") -apply (simp add: LList_corec_type2) -apply (force simp add: LList_corec_type2) -done - -text{*definitional version of same*} -lemma def_llist_corec: - "[| !!x. h(x) = llist_corec x f |] ==> - h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))" -by (simp add: llist_corec) - -subsection{* Proofs about type @{text "'a llist"} functions *} - -subsection{* Deriving @{text llist_equalityI} -- @{text llist} equality is a bisimulation *} - -lemma LListD_Fun_subset_Times_llist: - "r \ (llist A) <*> (llist A) - ==> LListD_Fun (Id_on A) r \ (llist A) <*> (llist A)" -by (auto simp add: LListD_Fun_def) - -lemma subset_Times_llist: - "prod_fun Rep_LList Rep_LList ` r \ - (llist(range Leaf)) <*> (llist(range Leaf))" -by (blast intro: Rep_LList [THEN LListD]) - -lemma prod_fun_lemma: - "r \ (llist(range Leaf)) <*> (llist(range Leaf)) - ==> prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r \ r" -apply safe -apply (erule subsetD [THEN SigmaE2], assumption) -apply (simp add: LListI [THEN Abs_LList_inverse]) -done - -lemma prod_fun_range_eq_Id_on: - "prod_fun Rep_LList Rep_LList ` range(%x. (x, x)) = - Id_on(llist(range Leaf))" -apply (rule equalityI, blast) -apply (fast elim: LListI [THEN Abs_LList_inverse, THEN subst]) -done - -text{*Used with @{text lfilter}*} -lemma llistD_Fun_mono: - "A\B ==> llistD_Fun A \ llistD_Fun B" -apply (simp add: llistD_Fun_def prod_fun_def, auto) -apply (rule image_eqI) - prefer 2 apply (blast intro: rev_subsetD [OF _ LListD_Fun_mono], force) -done - -subsubsection{* To show two llists are equal, exhibit a bisimulation! - [also admits true equality] *} -lemma llist_equalityI: - "[| (l1,l2) \ r; r \ llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2" -apply (simp add: llistD_Fun_def) -apply (rule Rep_LList_inject [THEN iffD1]) -apply (rule_tac r = "prod_fun Rep_LList Rep_LList `r" and A = "range (Leaf)" in LList_equalityI) -apply (erule prod_fun_imageI) -apply (erule image_mono [THEN subset_trans]) -apply (rule image_compose [THEN subst]) -apply (rule prod_fun_compose [THEN subst]) -apply (subst image_Un) -apply (subst prod_fun_range_eq_Id_on) -apply (rule LListD_Fun_subset_Times_llist [THEN prod_fun_lemma]) -apply (rule subset_Times_llist [THEN Un_least]) -apply (rule Id_on_subset_Times) -done - -subsubsection{* Rules to prove the 2nd premise of @{text llist_equalityI} *} -lemma llistD_Fun_LNil_I [simp]: "(LNil,LNil) \ llistD_Fun(r)" -apply (simp add: llistD_Fun_def LNil_def) -apply (rule LListD_Fun_NIL_I [THEN prod_fun_imageI]) -done - -lemma llistD_Fun_LCons_I [simp]: - "(l1,l2):r ==> (LCons x l1, LCons x l2) \ llistD_Fun(r)" -apply (simp add: llistD_Fun_def LCons_def) -apply (rule rangeI [THEN LListD_Fun_CONS_I, THEN prod_fun_imageI]) -apply (erule prod_fun_imageI) -done - -text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*} -lemma llistD_Fun_range_I: "(l,l) \ llistD_Fun(r Un range(%x.(x,x)))" -apply (simp add: llistD_Fun_def) -apply (rule Rep_LList_inverse [THEN subst]) -apply (rule prod_fun_imageI) -apply (subst image_Un) -apply (subst prod_fun_range_eq_Id_on) -apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_Id_on_I]) -done - -text{*A special case of @{text list_equality} for functions over lazy lists*} -lemma llist_fun_equalityI: - "[| f(LNil)=g(LNil); - !!x l. (f(LCons x l),g(LCons x l)) - \ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) - |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)" -apply (rule_tac r = "range (%u. (f (u),g (u)))" in llist_equalityI) -apply (rule rangeI, clarify) -apply (rule_tac l = u in llistE) -apply (simp_all add: llistD_Fun_range_I) -done - - -subsection{* The functional @{text lmap} *} - -lemma lmap_LNil [simp, nitpick_simp]: "lmap f LNil = LNil" -by (rule lmap_def [THEN def_llist_corec, THEN trans], simp) - -lemma lmap_LCons [simp, nitpick_simp]: -"lmap f (LCons M N) = LCons (f M) (lmap f N)" -by (rule lmap_def [THEN def_llist_corec, THEN trans], simp) - - -subsubsection{* Two easy results about @{text lmap} *} - -lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)" -by (rule_tac l = l in llist_fun_equalityI, simp_all) - -lemma lmap_ident [simp]: "lmap (%x. x) l = l" -by (rule_tac l = l in llist_fun_equalityI, simp_all) - - -subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *} - -lemma iterates [nitpick_simp]: "iterates f x = LCons x (iterates f (f x))" -by (rule iterates_def [THEN def_llist_corec, THEN trans], simp) - -lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)" -apply (rule_tac r = "range (%u. (lmap f (iterates f u),iterates f (f u)))" in llist_equalityI) -apply (rule rangeI, safe) -apply (rule_tac x1 = "f (u)" in iterates [THEN ssubst]) -apply (rule_tac x1 = u in iterates [THEN ssubst], simp) -done - -lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))" -apply (subst lmap_iterates) -apply (rule iterates) -done - -subsection{* A rather complex proof about iterates -- cf Andy Pitts *} - -subsubsection{* Two lemmas about @{text "natrec n x (%m. g)"}, which is essentially - @{text "(g^n)(x)"} *} - -lemma fun_power_lmap: "nat_rec (LCons b l) (%m. lmap(f)) n = - LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)" -by (induct_tac "n", simp_all) - -lemma fun_power_Suc: "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)" -by (induct_tac "n", simp_all) - -lemmas Pair_cong = refl [THEN cong, THEN cong, of concl: Pair] - - -text{*The bisimulation consists of @{text "{(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}"} - for all @{text u} and all @{text "n::nat"}.*} -lemma iterates_equality: - "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)" -apply (rule ext) -apply (rule_tac - r = "\u. range (%n. (nat_rec (h u) (%m y. lmap f y) n, - nat_rec (iterates f u) (%m y. lmap f y) n))" - in llist_equalityI) -apply (rule UN1_I range_eqI Pair_cong nat_rec_0 [symmetric])+ -apply clarify -apply (subst iterates, atomize) -apply (drule_tac x=u in spec) -apply (erule ssubst) -apply (subst fun_power_lmap) -apply (subst fun_power_lmap) -apply (rule llistD_Fun_LCons_I) -apply (rule lmap_iterates [THEN subst]) -apply (subst fun_power_Suc) -apply (subst fun_power_Suc, blast) -done - - -subsection{* @{text lappend} -- its two arguments cause some complications! *} - -lemma lappend_LNil_LNil [simp, nitpick_simp]: "lappend LNil LNil = LNil" -apply (simp add: lappend_def) -apply (rule llist_corec [THEN trans], simp) -done - -lemma lappend_LNil_LCons [simp, nitpick_simp]: - "lappend LNil (LCons l l') = LCons l (lappend LNil l')" -apply (simp add: lappend_def) -apply (rule llist_corec [THEN trans], simp) -done - -lemma lappend_LCons [simp, nitpick_simp]: - "lappend (LCons l l') N = LCons l (lappend l' N)" -apply (simp add: lappend_def) -apply (rule llist_corec [THEN trans], simp) -done - -lemma lappend_LNil [simp]: "lappend LNil l = l" -by (rule_tac l = l in llist_fun_equalityI, simp_all) - -lemma lappend_LNil2 [simp]: "lappend l LNil = l" -by (rule_tac l = l in llist_fun_equalityI, simp_all) - - -text{*The infinite first argument blocks the second*} -lemma lappend_iterates [simp]: "lappend (iterates f x) N = iterates f x" -apply (rule_tac r = "range (%u. (lappend (iterates f u) N,iterates f u))" - in llist_equalityI) - apply (rule rangeI, safe) -apply (subst (1 2) iterates) -apply simp -done - -subsubsection{* Two proofs that @{text lmap} distributes over lappend *} - -text{*Long proof requiring case analysis on both both arguments*} -lemma lmap_lappend_distrib: - "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)" -apply (rule_tac r = "\n. range (%l. (lmap f (lappend l n), - lappend (lmap f l) (lmap f n)))" - in llist_equalityI) -apply (rule UN1_I) -apply (rule rangeI, safe) -apply (rule_tac l = l in llistE) -apply (rule_tac l = n in llistE, simp_all) -apply (blast intro: llistD_Fun_LCons_I) -done - -text{*Shorter proof of theorem above using @{text llist_equalityI} as strong coinduction*} -lemma lmap_lappend_distrib': - "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)" -by (rule_tac l = l in llist_fun_equalityI, auto) - -text{*Without strong coinduction, three case analyses might be needed*} -lemma lappend_assoc': "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)" -by (rule_tac l = l1 in llist_fun_equalityI, auto) - -setup {* - Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case} - (map dest_Const [@{term LNil}, @{term LCons}]) -*} - -end diff -r 3222fa052846 -r 1a97dcd8dc6a src/HOL/Induct/README.html --- a/src/HOL/Induct/README.html Sat Nov 14 18:45:24 2009 +0100 +++ b/src/HOL/Induct/README.html Sat Nov 14 19:56:18 2009 +0100 @@ -32,9 +32,6 @@ HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz">paper available). -
  • LFilter is an inductive/corecursive formalization of the -filter functional for infinite streams. -
  • Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. diff -r 3222fa052846 -r 1a97dcd8dc6a src/HOL/Induct/ROOT.ML --- a/src/HOL/Induct/ROOT.ML Sat Nov 14 18:45:24 2009 +0100 +++ b/src/HOL/Induct/ROOT.ML Sat Nov 14 19:56:18 2009 +0100 @@ -2,5 +2,4 @@ use_thys ["Common_Patterns"]; use_thys ["QuoDataType", "QuoNestedDataType", "Term", - "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", - "SList", "LFilter", "Com"]; + "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"]; diff -r 3222fa052846 -r 1a97dcd8dc6a src/HOL/Induct/SList.thy --- a/src/HOL/Induct/SList.thy Sat Nov 14 18:45:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1037 +0,0 @@ -(* Title: SList.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: B. Wolff, University of Bremen - -Enriched theory of lists; mutual indirect recursive data-types. - -Definition of type 'a list (strict lists) by a least fixed point - -We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z) -and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z) - -so that list can serve as a "functor" for defining other recursive types. - -This enables the conservative construction of mutual recursive data-types -such as - -datatype 'a m = Node 'a * ('a m) list - -Tidied by lcp. Still needs removal of nat_rec. -*) - -header {* Extended List Theory (old) *} - -theory SList -imports Sexp -begin - -(*Hilbert_Choice is needed for the function "inv"*) - -(* *********************************************************************** *) -(* *) -(* Building up data type *) -(* *) -(* *********************************************************************** *) - - -(* Defining the Concrete Constructors *) -definition - NIL :: "'a item" where - "NIL = In0(Numb(0))" - -definition - CONS :: "['a item, 'a item] => 'a item" where - "CONS M N = In1(Scons M N)" - -inductive_set - list :: "'a item set => 'a item set" - for A :: "'a item set" - where - NIL_I: "NIL: list A" - | CONS_I: "[| a: A; M: list A |] ==> CONS a M : list A" - - -typedef (List) - 'a list = "list(range Leaf) :: 'a item set" - by (blast intro: list.NIL_I) - -abbreviation "Case == Datatype.Case" -abbreviation "Split == Datatype.Split" - -definition - List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b" where - "List_case c d = Case(%x. c)(Split(d))" - -definition - List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b" where - "List_rec M c d = wfrec (pred_sexp^+) - (%g. List_case c (%x y. d x y (g y))) M" - - -(* *********************************************************************** *) -(* *) -(* Abstracting data type *) -(* *) -(* *********************************************************************** *) - -(*Declaring the abstract list constructors*) - -no_translations - "[x, xs]" == "x#[xs]" - "[x]" == "x#[]" -no_notation - Nil ("[]") and - Cons (infixr "#" 65) - -definition - Nil :: "'a list" ("[]") where - "Nil = Abs_List(NIL)" - -definition - "Cons" :: "['a, 'a list] => 'a list" (infixr "#" 65) where - "x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))" - -definition - (* list Recursion -- the trancl is Essential; see list.ML *) - list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b" where - "list_rec l c d = - List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)" - -definition - list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b" where - "list_case a f xs = list_rec xs a (%x xs r. f x xs)" - -(* list Enumeration *) -translations - "[x, xs]" == "x#[xs]" - "[x]" == "x#[]" - - "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)" - - -(* *********************************************************************** *) -(* *) -(* Generalized Map Functionals *) -(* *) -(* *********************************************************************** *) - - -(* Generalized Map Functionals *) - -definition - Rep_map :: "('b => 'a item) => ('b list => 'a item)" where - "Rep_map f xs = list_rec xs NIL(%x l r. CONS(f x) r)" - -definition - Abs_map :: "('a item => 'b) => 'a item => 'b list" where - "Abs_map g M = List_rec M Nil (%N L r. g(N)#r)" - - -(**** Function definitions ****) - -definition - null :: "'a list => bool" where - "null xs = list_rec xs True (%x xs r. False)" - -definition - hd :: "'a list => 'a" where - "hd xs = list_rec xs (@x. True) (%x xs r. x)" - -definition - tl :: "'a list => 'a list" where - "tl xs = list_rec xs (@xs. True) (%x xs r. xs)" - -definition - (* a total version of tl: *) - ttl :: "'a list => 'a list" where - "ttl xs = list_rec xs [] (%x xs r. xs)" - -no_notation member (infixl "mem" 55) - -definition - member :: "['a, 'a list] => bool" (infixl "mem" 55) where - "x mem xs = list_rec xs False (%y ys r. if y=x then True else r)" - -definition - list_all :: "('a => bool) => ('a list => bool)" where - "list_all P xs = list_rec xs True(%x l r. P(x) & r)" - -definition - map :: "('a=>'b) => ('a list => 'b list)" where - "map f xs = list_rec xs [] (%x l r. f(x)#r)" - -no_notation append (infixr "@" 65) - -definition - append :: "['a list, 'a list] => 'a list" (infixr "@" 65) where - "xs@ys = list_rec xs ys (%x l r. x#r)" - -definition - filter :: "['a => bool, 'a list] => 'a list" where - "filter P xs = list_rec xs [] (%x xs r. if P(x)then x#r else r)" - -definition - foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b" where - "foldl f a xs = list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)" - -definition - foldr :: "[['a,'b] => 'b, 'b, 'a list] => 'b" where - "foldr f a xs = list_rec xs a (%x xs r. (f x r))" - -definition - length :: "'a list => nat" where - "length xs = list_rec xs 0 (%x xs r. Suc r)" - -definition - drop :: "['a list,nat] => 'a list" where - "drop t n = (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)" - -definition - copy :: "['a, nat] => 'a list" where (* make list of n copies of x *) - "copy t = nat_rec [] (%m xs. t # xs)" - -definition - flat :: "'a list list => 'a list" where - "flat = foldr (op @) []" - -definition - nth :: "[nat, 'a list] => 'a" where - "nth = nat_rec hd (%m r xs. r(tl xs))" - -definition - rev :: "'a list => 'a list" where - "rev xs = list_rec xs [] (%x xs xsa. xsa @ [x])" - -(* miscellaneous definitions *) -definition - zipWith :: "['a * 'b => 'c, 'a list * 'b list] => 'c list" where - "zipWith f S = (list_rec (fst S) (%T.[]) - (%x xs r. %T. if null T then [] - else f(x,hd T) # r(tl T)))(snd(S))" - -definition - zip :: "'a list * 'b list => ('a*'b) list" where - "zip = zipWith (%s. s)" - -definition - unzip :: "('a*'b) list => ('a list * 'b list)" where - "unzip = foldr(% (a,b)(c,d).(a#c,b#d))([],[])" - - -consts take :: "['a list,nat] => 'a list" -primrec - take_0: "take xs 0 = []" - take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs" - -consts enum :: "[nat,nat] => nat list" -primrec - enum_0: "enum i 0 = []" - enum_Suc: "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])" - - -no_translations - "[x\xs . P]" == "filter (%x. P) xs" - -syntax - (* Special syntax for list_all and filter *) - "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10) - -translations - "[x\xs. P]" == "CONST filter(%x. P) xs" - "Alls x:xs. P" == "CONST list_all(%x. P)xs" - - -lemma ListI: "x : list (range Leaf) ==> x : List" -by (simp add: List_def) - -lemma ListD: "x : List ==> x : list (range Leaf)" -by (simp add: List_def) - -lemma list_unfold: "list(A) = usum {Numb(0)} (uprod A (list(A)))" - by (fast intro!: list.intros [unfolded NIL_def CONS_def] - elim: list.cases [unfolded NIL_def CONS_def]) - -(*This justifies using list in other recursive type definitions*) -lemma list_mono: "A<=B ==> list(A) <= list(B)" -apply (rule subsetI) -apply (erule list.induct) -apply (auto intro!: list.intros) -done - -(*Type checking -- list creates well-founded sets*) -lemma list_sexp: "list(sexp) <= sexp" -apply (rule subsetI) -apply (erule list.induct) -apply (unfold NIL_def CONS_def) -apply (auto intro: sexp.intros sexp_In0I sexp_In1I) -done - -(* A <= sexp ==> list(A) <= sexp *) -lemmas list_subset_sexp = subset_trans [OF list_mono list_sexp] - - -(*Induction for the type 'a list *) -lemma list_induct: - "[| P(Nil); - !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)" -apply (unfold Nil_def Cons_def) -apply (rule Rep_List_inverse [THEN subst]) -(*types force good instantiation*) -apply (rule Rep_List [unfolded List_def, THEN list.induct], simp) -apply (erule Abs_List_inverse [unfolded List_def, THEN subst], blast) -done - - -(*** Isomorphisms ***) - -lemma inj_on_Abs_list: "inj_on Abs_List (list(range Leaf))" -apply (rule inj_on_inverseI) -apply (erule Abs_List_inverse [unfolded List_def]) -done - -(** Distinctness of constructors **) - -lemma CONS_not_NIL [iff]: "CONS M N ~= NIL" -by (simp add: NIL_def CONS_def) - -lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym] -lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE, standard] -lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL] - -lemma Cons_not_Nil [iff]: "x # xs ~= Nil" -apply (unfold Nil_def Cons_def) -apply (rule CONS_not_NIL [THEN inj_on_Abs_list [THEN inj_on_contraD]]) -apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def]) -done - -lemmas Nil_not_Cons [iff] = Cons_not_Nil [THEN not_sym, standard] -lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE, standard] -lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil] - -(** Injectiveness of CONS and Cons **) - -lemma CONS_CONS_eq [iff]: "(CONS K M)=(CONS L N) = (K=L & M=N)" -by (simp add: CONS_def) - -(*For reasoning about abstract list constructors*) -declare Rep_List [THEN ListD, intro] ListI [intro] -declare list.intros [intro,simp] -declare Leaf_inject [dest!] - -lemma Cons_Cons_eq [iff]: "(x#xs=y#ys) = (x=y & xs=ys)" -apply (simp add: Cons_def) -apply (subst Abs_List_inject) -apply (auto simp add: Rep_List_inject) -done - -lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard] - -lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)" - by (induct L == "CONS M N" set: list) auto - -lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp" -apply (simp add: CONS_def In1_def) -apply (fast dest!: Scons_D) -done - - -(*Reasoning about constructors and their freeness*) - - -lemma not_CONS_self: "N: list(A) ==> !M. N ~= CONS M N" -apply (erule list.induct) apply simp_all done - -lemma not_Cons_self2: "\x. l ~= x#l" -by (induct l rule: list_induct) simp_all - - -lemma neq_Nil_conv2: "(xs ~= []) = (\y ys. xs = y#ys)" -by (induct xs rule: list_induct) auto - -(** Conversion rules for List_case: case analysis operator **) - -lemma List_case_NIL [simp]: "List_case c h NIL = c" -by (simp add: List_case_def NIL_def) - -lemma List_case_CONS [simp]: "List_case c h (CONS M N) = h M N" -by (simp add: List_case_def CONS_def) - - -(*** List_rec -- by wf recursion on pred_sexp ***) - -(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not - hold if pred_sexp^+ were changed to pred_sexp. *) - -lemma List_rec_unfold_lemma: - "(%M. List_rec M c d) == - wfrec (pred_sexp^+) (%g. List_case c (%x y. d x y (g y)))" -by (simp add: List_rec_def) - -lemmas List_rec_unfold = - def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl], - standard] - - -(** pred_sexp lemmas **) - -lemma pred_sexp_CONS_I1: - "[| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+" -by (simp add: CONS_def In1_def) - -lemma pred_sexp_CONS_I2: - "[| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+" -by (simp add: CONS_def In1_def) - -lemma pred_sexp_CONS_D: - "(CONS M1 M2, N) : pred_sexp^+ ==> - (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+" -apply (frule pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD]) -apply (blast dest!: sexp_CONS_D intro: pred_sexp_CONS_I1 pred_sexp_CONS_I2 - trans_trancl [THEN transD]) -done - - -(** Conversion rules for List_rec **) - -lemma List_rec_NIL [simp]: "List_rec NIL c h = c" -apply (rule List_rec_unfold [THEN trans]) -apply (simp add: List_case_NIL) -done - -lemma List_rec_CONS [simp]: - "[| M: sexp; N: sexp |] - ==> List_rec (CONS M N) c h = h M N (List_rec N c h)" -apply (rule List_rec_unfold [THEN trans]) -apply (simp add: pred_sexp_CONS_I2) -done - - -(*** list_rec -- by List_rec ***) - -lemmas Rep_List_in_sexp = - subsetD [OF range_Leaf_subset_sexp [THEN list_subset_sexp] - Rep_List [THEN ListD]] - - -lemma list_rec_Nil [simp]: "list_rec Nil c h = c" -by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Nil_def) - - -lemma list_rec_Cons [simp]: "list_rec (a#l) c h = h a l (list_rec l c h)" -by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Cons_def - Rep_List_inverse Rep_List [THEN ListD] inj_Leaf Rep_List_in_sexp) - - -(*Type checking. Useful?*) -lemma List_rec_type: - "[| M: list(A); - A<=sexp; - c: C(NIL); - !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h x y r: C(CONS x y) - |] ==> List_rec M c h : C(M :: 'a item)" -apply (erule list.induct, simp) -apply (insert list_subset_sexp) -apply (subst List_rec_CONS, blast+) -done - - - -(** Generalized map functionals **) - -lemma Rep_map_Nil [simp]: "Rep_map f Nil = NIL" -by (simp add: Rep_map_def) - -lemma Rep_map_Cons [simp]: - "Rep_map f(x#xs) = CONS(f x)(Rep_map f xs)" -by (simp add: Rep_map_def) - -lemma Rep_map_type: "(!!x. f(x): A) ==> Rep_map f xs: list(A)" -apply (simp add: Rep_map_def) -apply (rule list_induct, auto) -done - -lemma Abs_map_NIL [simp]: "Abs_map g NIL = Nil" -by (simp add: Abs_map_def) - -lemma Abs_map_CONS [simp]: - "[| M: sexp; N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N" -by (simp add: Abs_map_def) - -(*Eases the use of primitive recursion.*) -lemma def_list_rec_NilCons: - "[| !!xs. f(xs) = list_rec xs c h |] - ==> f [] = c & f(x#xs) = h x xs (f xs)" -by simp - - - -lemma Abs_map_inverse: - "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |] - ==> Rep_map f (Abs_map g M) = M" -apply (erule list.induct, simp_all) -apply (insert list_subset_sexp) -apply (subst Abs_map_CONS, blast) -apply blast -apply simp -done - -(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*) - -(** list_case **) - -(* setting up rewrite sets *) - -text{*Better to have a single theorem with a conjunctive conclusion.*} -declare def_list_rec_NilCons [OF list_case_def, simp] - -(** list_case **) - -lemma expand_list_case: - "P(list_case a f xs) = ((xs=[] --> P a ) & (!y ys. xs=y#ys --> P(f y ys)))" -by (induct xs rule: list_induct) simp_all - - -(**** Function definitions ****) - -declare def_list_rec_NilCons [OF null_def, simp] -declare def_list_rec_NilCons [OF hd_def, simp] -declare def_list_rec_NilCons [OF tl_def, simp] -declare def_list_rec_NilCons [OF ttl_def, simp] -declare def_list_rec_NilCons [OF append_def, simp] -declare def_list_rec_NilCons [OF member_def, simp] -declare def_list_rec_NilCons [OF map_def, simp] -declare def_list_rec_NilCons [OF filter_def, simp] -declare def_list_rec_NilCons [OF list_all_def, simp] - - -(** nth **) - -lemma def_nat_rec_0_eta: - "[| !!n. f = nat_rec c h |] ==> f(0) = c" -by simp - -lemma def_nat_rec_Suc_eta: - "[| !!n. f = nat_rec c h |] ==> f(Suc(n)) = h n (f n)" -by simp - -declare def_nat_rec_0_eta [OF nth_def, simp] -declare def_nat_rec_Suc_eta [OF nth_def, simp] - - -(** length **) - -lemma length_Nil [simp]: "length([]) = 0" -by (simp add: length_def) - -lemma length_Cons [simp]: "length(a#xs) = Suc(length(xs))" -by (simp add: length_def) - - -(** @ - append **) - -lemma append_assoc [simp]: "(xs@ys)@zs = xs@(ys@zs)" -by (induct xs rule: list_induct) simp_all - -lemma append_Nil2 [simp]: "xs @ [] = xs" -by (induct xs rule: list_induct) simp_all - -(** mem **) - -lemma mem_append [simp]: "x mem (xs@ys) = (x mem xs | x mem ys)" -by (induct xs rule: list_induct) simp_all - -lemma mem_filter [simp]: "x mem [x\xs. P x ] = (x mem xs & P(x))" -by (induct xs rule: list_induct) simp_all - -(** list_all **) - -lemma list_all_True [simp]: "(Alls x:xs. True) = True" -by (induct xs rule: list_induct) simp_all - -lemma list_all_conj [simp]: - "list_all p (xs@ys) = ((list_all p xs) & (list_all p ys))" -by (induct xs rule: list_induct) simp_all - -lemma list_all_mem_conv: "(Alls x:xs. P(x)) = (!x. x mem xs --> P(x))" -apply (induct xs rule: list_induct) -apply simp_all -apply blast -done - -lemma nat_case_dist : "(! n. P n) = (P 0 & (! n. P (Suc n)))" -apply auto -apply (induct_tac n) -apply auto -done - - -lemma alls_P_eq_P_nth: "(Alls u:A. P u) = (!n. n < length A --> P(nth n A))" -apply (induct_tac A rule: list_induct) -apply simp_all -apply (rule trans) -apply (rule_tac [2] nat_case_dist [symmetric], simp_all) -done - - -lemma list_all_imp: - "[| !x. P x --> Q x; (Alls x:xs. P(x)) |] ==> (Alls x:xs. Q(x))" -by (simp add: list_all_mem_conv) - - -(** The functional "map" and the generalized functionals **) - -lemma Abs_Rep_map: - "(!!x. f(x): sexp) ==> - Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs" -apply (induct xs rule: list_induct) -apply (simp_all add: Rep_map_type list_sexp [THEN subsetD]) -done - - -(** Additional mapping lemmas **) - -lemma map_ident [simp]: "map(%x. x)(xs) = xs" -by (induct xs rule: list_induct) simp_all - -lemma map_append [simp]: "map f (xs@ys) = map f xs @ map f ys" -by (induct xs rule: list_induct) simp_all - -lemma map_compose: "map(f o g)(xs) = map f (map g xs)" -apply (simp add: o_def) -apply (induct xs rule: list_induct) -apply simp_all -done - - -lemma mem_map_aux1 [rule_format]: - "x mem (map f q) --> (\y. y mem q & x = f y)" -by (induct q rule: list_induct) auto - -lemma mem_map_aux2 [rule_format]: - "(\y. y mem q & x = f y) --> x mem (map f q)" -by (induct q rule: list_induct) auto - -lemma mem_map: "x mem (map f q) = (\y. y mem q & x = f y)" -apply (rule iffI) -apply (erule mem_map_aux1) -apply (erule mem_map_aux2) -done - -lemma hd_append [rule_format]: "A ~= [] --> hd(A @ B) = hd(A)" -by (induct A rule: list_induct) auto - -lemma tl_append [rule_format]: "A ~= [] --> tl(A @ B) = tl(A) @ B" -by (induct A rule: list_induct) auto - - -(** take **) - -lemma take_Suc1 [simp]: "take [] (Suc x) = []" -by simp - -lemma take_Suc2 [simp]: "take(a#xs)(Suc x) = a#take xs x" -by simp - - -(** drop **) - -lemma drop_0 [simp]: "drop xs 0 = xs" -by (simp add: drop_def) - -lemma drop_Suc1 [simp]: "drop [] (Suc x) = []" -apply (induct x) -apply (simp_all add: drop_def) -done - -lemma drop_Suc2 [simp]: "drop(a#xs)(Suc x) = drop xs x" -by (simp add: drop_def) - - -(** copy **) - -lemma copy_0 [simp]: "copy x 0 = []" -by (simp add: copy_def) - -lemma copy_Suc [simp]: "copy x (Suc y) = x # copy x y" -by (simp add: copy_def) - - -(** fold **) - -lemma foldl_Nil [simp]: "foldl f a [] = a" -by (simp add: foldl_def) - -lemma foldl_Cons [simp]: "foldl f a(x#xs) = foldl f (f a x) xs" -by (simp add: foldl_def) - -lemma foldr_Nil [simp]: "foldr f a [] = a" -by (simp add: foldr_def) - -lemma foldr_Cons [simp]: "foldr f z(x#xs) = f x (foldr f z xs)" -by (simp add: foldr_def) - - -(** flat **) - -lemma flat_Nil [simp]: "flat [] = []" -by (simp add: flat_def) - -lemma flat_Cons [simp]: "flat (x # xs) = x @ flat xs" -by (simp add: flat_def) - -(** rev **) - -lemma rev_Nil [simp]: "rev [] = []" -by (simp add: rev_def) - -lemma rev_Cons [simp]: "rev (x # xs) = rev xs @ [x]" -by (simp add: rev_def) - - -(** zip **) - -lemma zipWith_Cons_Cons [simp]: - "zipWith f (a#as,b#bs) = f(a,b) # zipWith f (as,bs)" -by (simp add: zipWith_def) - -lemma zipWith_Nil_Nil [simp]: "zipWith f ([],[]) = []" -by (simp add: zipWith_def) - - -lemma zipWith_Cons_Nil [simp]: "zipWith f (x,[]) = []" -by (induct x rule: list_induct) (simp_all add: zipWith_def) - - -lemma zipWith_Nil_Cons [simp]: "zipWith f ([],x) = []" -by (simp add: zipWith_def) - -lemma unzip_Nil [simp]: "unzip [] = ([],[])" -by (simp add: unzip_def) - - - -(** SOME LIST THEOREMS **) - -(* SQUIGGOL LEMMAS *) - -lemma map_compose_ext: "map(f o g) = ((map f) o (map g))" -apply (simp add: o_def) -apply (rule ext) -apply (simp add: map_compose [symmetric] o_def) -done - -lemma map_flat: "map f (flat S) = flat(map (map f) S)" -by (induct S rule: list_induct) simp_all - -lemma list_all_map_eq: "(Alls u:xs. f(u) = g(u)) --> map f xs = map g xs" -by (induct xs rule: list_induct) simp_all - -lemma filter_map_d: "filter p (map f xs) = map f (filter(p o f)(xs))" -by (induct xs rule: list_induct) simp_all - -lemma filter_compose: "filter p (filter q xs) = filter(%x. p x & q x) xs" -by (induct xs rule: list_induct) simp_all - -(* "filter(p, filter(q,xs)) = filter(q, filter(p,xs))", - "filter(p, filter(p,xs)) = filter(p,xs)" BIRD's thms.*) - -lemma filter_append [rule_format, simp]: - "\B. filter p (A @ B) = (filter p A @ filter p B)" -by (induct A rule: list_induct) simp_all - - -(* inits(xs) == map(fst,splits(xs)), - - splits([]) = [] - splits(a # xs) = <[],xs> @ map(%x. , splits(xs)) - (x @ y = z) = mem splits(z) - x mem xs & y mem ys = mem diag(xs,ys) *) - -lemma length_append: "length(xs@ys) = length(xs)+length(ys)" -by (induct xs rule: list_induct) simp_all - -lemma length_map: "length(map f xs) = length(xs)" -by (induct xs rule: list_induct) simp_all - - -lemma take_Nil [simp]: "take [] n = []" -by (induct n) simp_all - -lemma take_take_eq [simp]: "\n. take (take xs n) n = take xs n" -apply (induct xs rule: list_induct) -apply simp_all -apply (rule allI) -apply (induct_tac n) -apply auto -done - -lemma take_take_Suc_eq1 [rule_format]: - "\n. take (take xs(Suc(n+m))) n = take xs n" -apply (induct_tac xs rule: list_induct) -apply simp_all -apply (rule allI) -apply (induct_tac n) -apply auto -done - -declare take_Suc [simp del] - -lemma take_take_1: "take (take xs (n+m)) n = take xs n" -apply (induct m) -apply (simp_all add: take_take_Suc_eq1) -done - -lemma take_take_Suc_eq2 [rule_format]: - "\n. take (take xs n)(Suc(n+m)) = take xs n" -apply (induct_tac xs rule: list_induct) -apply simp_all -apply (rule allI) -apply (induct_tac n) -apply auto -done - -lemma take_take_2: "take(take xs n)(n+m) = take xs n" -apply (induct m) -apply (simp_all add: take_take_Suc_eq2) -done - -(* length(take(xs,n)) = min(n, length(xs)) *) -(* length(drop(xs,n)) = length(xs) - n *) - -lemma drop_Nil [simp]: "drop [] n = []" -by (induct n) auto - -lemma drop_drop [rule_format]: "\xs. drop (drop xs m) n = drop xs(m+n)" -apply (induct_tac m) -apply auto -apply (induct_tac xs rule: list_induct) -apply auto -done - -lemma take_drop [rule_format]: "\xs. (take xs n) @ (drop xs n) = xs" -apply (induct_tac n) -apply auto -apply (induct_tac xs rule: list_induct) -apply auto -done - -lemma copy_copy: "copy x n @ copy x m = copy x (n+m)" -by (induct n) auto - -lemma length_copy: "length(copy x n) = n" -by (induct n) auto - -lemma length_take [rule_format, simp]: - "\xs. length(take xs n) = min (length xs) n" -apply (induct n) - apply auto -apply (induct_tac xs rule: list_induct) - apply auto -done - -lemma length_take_drop: "length(take A k) + length(drop A k) = length(A)" -by (simp only: length_append [symmetric] take_drop) - -lemma take_append [rule_format]: "\A. length(A) = n --> take(A@B) n = A" -apply (induct n) -apply (rule allI) -apply (rule_tac [2] allI) -apply (induct_tac A rule: list_induct) -apply (induct_tac [3] A rule: list_induct, simp_all) -done - -lemma take_append2 [rule_format]: - "\A. length(A) = n --> take(A@B) (n+k) = A @ take B k" -apply (induct n) -apply (rule allI) -apply (rule_tac [2] allI) -apply (induct_tac A rule: list_induct) -apply (induct_tac [3] A rule: list_induct, simp_all) -done - -lemma take_map [rule_format]: "\n. take (map f A) n = map f (take A n)" -apply (induct A rule: list_induct) -apply simp_all -apply (rule allI) -apply (induct_tac n) -apply simp_all -done - -lemma drop_append [rule_format]: "\A. length(A) = n --> drop(A@B)n = B" -apply (induct n) -apply (rule allI) -apply (rule_tac [2] allI) -apply (induct_tac A rule: list_induct) -apply (induct_tac [3] A rule: list_induct) -apply simp_all -done - -lemma drop_append2 [rule_format]: - "\A. length(A) = n --> drop(A@B)(n+k) = drop B k" -apply (induct n) -apply (rule allI) -apply (rule_tac [2] allI) -apply (induct_tac A rule: list_induct) -apply (induct_tac [3] A rule: list_induct) -apply simp_all -done - - -lemma drop_all [rule_format]: "\A. length(A) = n --> drop A n = []" -apply (induct n) -apply (rule allI) -apply (rule_tac [2] allI) -apply (induct_tac A rule: list_induct) -apply (induct_tac [3] A rule: list_induct) -apply auto -done - -lemma drop_map [rule_format]: "\n. drop (map f A) n = map f (drop A n)" -apply (induct A rule: list_induct) -apply simp_all -apply (rule allI) -apply (induct_tac n) -apply simp_all -done - -lemma take_all [rule_format]: "\A. length(A) = n --> take A n = A" -apply (induct n) -apply (rule allI) -apply (rule_tac [2] allI) -apply (induct_tac A rule: list_induct) -apply (induct_tac [3] A rule: list_induct) -apply auto -done - -lemma foldl_single: "foldl f a [b] = f a b" -by simp_all - -lemma foldl_append [simp]: - "\a. foldl f a (A @ B) = foldl f (foldl f a A) B" -by (induct A rule: list_induct) simp_all - -lemma foldl_map: - "\e. foldl f e (map g S) = foldl (%x y. f x (g y)) e S" -by (induct S rule: list_induct) simp_all - -lemma foldl_neutr_distr [rule_format]: - assumes r_neutr: "\a. f a e = a" - and r_neutl: "\a. f e a = a" - and assoc: "\a b c. f a (f b c) = f(f a b) c" - shows "\y. f y (foldl f e A) = foldl f y A" -apply (induct A rule: list_induct) -apply (simp_all add: r_neutr r_neutl, clarify) -apply (erule all_dupE) -apply (rule trans) -prefer 2 apply assumption -apply (simp (no_asm_use) add: assoc [THEN spec, THEN spec, THEN spec, THEN sym]) -apply simp -done - -lemma foldl_append_sym: -"[| !a. f a e = a; !a. f e a = a; - !a b c. f a (f b c) = f(f a b) c |] - ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)" -apply (rule trans) -apply (rule foldl_append) -apply (rule sym) -apply (rule foldl_neutr_distr, auto) -done - -lemma foldr_append [rule_format, simp]: - "\a. foldr f a (A @ B) = foldr f (foldr f a B) A" -by (induct A rule: list_induct) simp_all - - -lemma foldr_map: "\e. foldr f e (map g S) = foldr (f o g) e S" -by (induct S rule: list_induct) (simp_all add: o_def) - -lemma foldr_Un_eq_UN: "foldr op Un {} S = (UN X: {t. t mem S}.X)" -by (induct S rule: list_induct) auto - -lemma foldr_neutr_distr: - "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |] - ==> foldr f y S = f (foldr f e S) y" -by (induct S rule: list_induct) auto - -lemma foldr_append2: - "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |] - ==> foldr f e (A @ B) = f (foldr f e A) (foldr f e B)" -apply auto -apply (rule foldr_neutr_distr) -apply auto -done - -lemma foldr_flat: - "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |] ==> - foldr f e (flat S) = (foldr f e)(map (foldr f e) S)" -apply (induct S rule: list_induct) -apply (simp_all del: foldr_append add: foldr_append2) -done - - -lemma list_all_map: "(Alls x:map f xs .P(x)) = (Alls x:xs.(P o f)(x))" -by (induct xs rule: list_induct) auto - -lemma list_all_and: - "(Alls x:xs. P(x)&Q(x)) = ((Alls x:xs. P(x))&(Alls x:xs. Q(x)))" -by (induct xs rule: list_induct) auto - - -lemma nth_map [rule_format]: - "\i. i < length(A) --> nth i (map f A) = f(nth i A)" -apply (induct A rule: list_induct) -apply simp_all -apply (rule allI) -apply (induct_tac i) -apply auto -done - -lemma nth_app_cancel_right [rule_format]: - "\i. i < length(A) --> nth i(A@B) = nth i A" -apply (induct A rule: list_induct) -apply simp_all -apply (rule allI) -apply (induct_tac i) -apply simp_all -done - -lemma nth_app_cancel_left [rule_format]: - "\n. n = length(A) --> nth(n+i)(A@B) = nth i B" -by (induct A rule: list_induct) simp_all - - -(** flat **) - -lemma flat_append [simp]: "flat(xs@ys) = flat(xs) @ flat(ys)" -by (induct xs rule: list_induct) auto - -lemma filter_flat: "filter p (flat S) = flat(map (filter p) S)" -by (induct S rule: list_induct) auto - - -(** rev **) - -lemma rev_append [simp]: "rev(xs@ys) = rev(ys) @ rev(xs)" -by (induct xs rule: list_induct) auto - -lemma rev_rev_ident [simp]: "rev(rev l) = l" -by (induct l rule: list_induct) auto - -lemma rev_flat: "rev(flat ls) = flat (map rev (rev ls))" -by (induct ls rule: list_induct) auto - -lemma rev_map_distrib: "rev(map f l) = map f (rev l)" -by (induct l rule: list_induct) auto - -lemma foldl_rev: "foldl f b (rev l) = foldr (%x y. f y x) b l" -by (induct l rule: list_induct) auto - -lemma foldr_rev: "foldr f b (rev l) = foldl (%x y. f y x) b l" -apply (rule sym) -apply (rule trans) -apply (rule_tac [2] foldl_rev) -apply simp -done - -end diff -r 3222fa052846 -r 1a97dcd8dc6a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Nov 14 18:45:24 2009 +0100 +++ b/src/HOL/IsaMakefile Sat Nov 14 19:56:18 2009 +0100 @@ -430,12 +430,11 @@ HOL-Induct: HOL $(LOG)/HOL-Induct.gz -$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \ - Induct/LFilter.thy Induct/LList.thy Induct/Ordinals.thy \ - Induct/PropLog.thy Induct/QuoNestedDataType.thy \ - Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \ - Induct/Sigma_Algebra.thy Induct/SList.thy Induct/ABexp.thy \ - Induct/Term.thy Induct/Tree.thy Induct/document/root.tex +$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \ + Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy \ + Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \ + Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/Term.thy \ + Induct/Tree.thy Induct/document/root.tex @$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct