# Theory Listn

Up to index of Isabelle/HOL/HOL-MicroJava-skip_proofs

theory Listn
imports Err
`(*  Title:      HOL/MicroJava/DFA/Listn.thy    Author:     Tobias Nipkow    Copyright   2000 TUM*)header {* \isaheader{Fixed Length Lists} *}theory Listnimports Errbegindefinition list :: "nat => 'a set => 'a list set" where"list n A == {xs. length xs = n & set xs <= A}"definition le :: "'a ord => ('a list)ord" where"le r == list_all2 (%x y. x <=_r y)"abbreviation  lesublist_syntax :: "'a list => 'a ord => 'a list => bool"       ("(_ /<=[_] _)" [50, 0, 51] 50)  where "x <=[r] y == x <=_(le r) y"abbreviation  lesssublist_syntax :: "'a list => 'a ord => 'a list => bool"       ("(_ /<[_] _)" [50, 0, 51] 50)  where "x <[r] y == x <_(le r) y"definition map2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list" where"map2 f == (%xs ys. map (split f) (zip xs ys))"abbreviation  plussublist_syntax :: "'a list => ('a => 'b => 'c) => 'b list => 'c list"       ("(_ /+[_] _)" [65, 0, 66] 65)  where "x +[f] y == x +_(map2 f) y"primrec coalesce :: "'a err list => 'a list err" where  "coalesce [] = OK[]"| "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"definition sl :: "nat => 'a sl => 'a list sl" where"sl n == %(A,r,f). (list n A, le r, map2 f)"definition sup :: "('a => 'b => 'c err) => 'a list => 'b list => 'c list err" where"sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"definition upto_esl :: "nat => 'a esl => 'a list esl" where"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"lemmas [simp] = set_update_subsetIlemma unfold_lesub_list:  "xs <=[r] ys == Listn.le r xs ys"  by (simp add: lesub_def)lemma Nil_le_conv [iff]:  "([] <=[r] ys) = (ys = [])"apply (unfold lesub_def Listn.le_def)apply simpdonelemma Cons_notle_Nil [iff]:   "~ x#xs <=[r] []"apply (unfold lesub_def Listn.le_def)apply simpdonelemma Cons_le_Cons [iff]:  "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)"apply (unfold lesub_def Listn.le_def)apply simpdonelemma Cons_less_Conss [simp]:  "order r ==>   x#xs <_(Listn.le r) y#ys =   (x <_r y & xs <=[r] ys  |  x = y & xs <_(Listn.le r) ys)"apply (unfold lesssub_def)apply blastdone  lemma list_update_le_cong:  "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";apply (unfold unfold_lesub_list)apply (unfold Listn.le_def)apply (simp add: list_all2_conv_all_nth nth_list_update)donelemma le_listD:  "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p"apply (unfold Listn.le_def lesub_def)apply (simp add: list_all2_conv_all_nth)donelemma le_list_refl:  "!x. x <=_r x ==> xs <=[r] xs"apply (unfold unfold_lesub_list)apply (simp add: Listn.le_def list_all2_conv_all_nth)donelemma le_list_trans:  "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs"apply (unfold unfold_lesub_list)apply (simp add: Listn.le_def list_all2_conv_all_nth)apply clarifyapply simpapply (blast intro: order_trans)donelemma le_list_antisym:  "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys"apply (unfold unfold_lesub_list)apply (simp add: Listn.le_def list_all2_conv_all_nth)apply (rule nth_equalityI) apply blastapply clarifyapply simpapply (blast intro: order_antisym)donelemma order_listI [simp, intro!]:  "order r ==> order(Listn.le r)"apply (subst Semilat.order_def)apply (blast intro: le_list_refl le_list_trans le_list_antisym             dest: order_refl)donelemma lesub_list_impl_same_size [simp]:  "xs <=[r] ys ==> size ys = size xs"  apply (unfold Listn.le_def lesub_def)apply (simp add: list_all2_conv_all_nth)done lemma lesssub_list_impl_same_size:  "xs <_(Listn.le r) ys ==> size ys = size xs"apply (unfold lesssub_def)apply autodone  lemma le_list_appendI:  "!!b c d. a <=[r] b ==> c <=[r] d ==> a@c <=[r] b@d"apply (induct a) apply simpapply (case_tac b)apply autodonelemma le_listI:  "length a = length b ==> (!!n. n < length a ==> a!n <=_r b!n) ==> a <=[r] b"  apply (unfold lesub_def Listn.le_def)  apply (simp add: list_all2_conv_all_nth)  donelemma listI:  "[| length xs = n; set xs <= A |] ==> xs : list n A"apply (unfold list_def)apply blastdonelemma listE_length [simp]:   "xs : list n A ==> length xs = n"apply (unfold list_def)apply blastdone lemma less_lengthI:  "[| xs : list n A; p < n |] ==> p < length xs"  by simplemma listE_set [simp]:  "xs : list n A ==> set xs <= A"apply (unfold list_def)apply blastdone lemma list_0 [simp]:  "list 0 A = {[]}"apply (unfold list_def)apply autodone lemma in_list_Suc_iff:   "(xs : list (Suc n) A) = (∃y∈ A. ∃ys∈ list n A. xs = y#ys)"apply (unfold list_def)apply (case_tac "xs")apply autodone lemma Cons_in_list_Suc [iff]:  "(x#xs : list (Suc n) A) = (x∈ A & xs : list n A)";apply (simp add: in_list_Suc_iff)done lemma list_not_empty:  "∃a. a∈ A ==> ∃xs. xs : list n A";apply (induct "n") apply simpapply (simp add: in_list_Suc_iff)apply blastdonelemma nth_in [rule_format, simp]:  "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A"apply (induct "xs") apply simpapply (simp add: nth_Cons split: nat.split)donelemma listE_nth_in:  "[| xs : list n A; i < n |] ==> (xs!i) : A"  by autolemma listn_Cons_Suc [elim!]:  "l#xs ∈ list n A ==> (!!n'. n = Suc n' ==> l ∈ A ==> xs ∈ list n' A ==> P) ==> P"  by (cases n) autolemma listn_appendE [elim!]:  "a@b ∈ list n A ==> (!!n1 n2. n=n1+n2 ==> a ∈ list n1 A ==> b ∈ list n2 A ==> P) ==> P" proof -  have "!!n. a@b ∈ list n A ==> ∃n1 n2. n=n1+n2 ∧ a ∈ list n1 A ∧ b ∈ list n2 A"    (is "!!n. ?list a n ==> ∃n1 n2. ?P a n n1 n2")  proof (induct a)    fix n assume "?list [] n"    hence "?P [] n 0 n" by simp    thus "∃n1 n2. ?P [] n n1 n2" by fast  next    fix n l ls    assume "?list (l#ls) n"    then obtain n' where n: "n = Suc n'" "l ∈ A" and list_n': "ls@b ∈ list n' A" by fastforce    assume "!!n. ls @ b ∈ list n A ==> ∃n1 n2. n = n1 + n2 ∧ ls ∈ list n1 A ∧ b ∈ list n2 A"    hence "∃n1 n2. n' = n1 + n2 ∧ ls ∈ list n1 A ∧ b ∈ list n2 A" by this (rule list_n')    then obtain n1 n2 where "n' = n1 + n2" "ls ∈ list n1 A" "b ∈ list n2 A" by fast    with n have "?P (l#ls) n (n1+1) n2" by simp    thus "∃n1 n2. ?P (l#ls) n n1 n2" by fastforce  qed  moreover  assume "a@b ∈ list n A" "!!n1 n2. n=n1+n2 ==> a ∈ list n1 A ==> b ∈ list n2 A ==> P"  ultimately  show ?thesis by blastqedlemma listt_update_in_list [simp, intro!]:  "[| xs : list n A; x∈ A |] ==> xs[i := x] : list n A"apply (unfold list_def)apply simpdone lemma plus_list_Nil [simp]:  "[] +[f] xs = []"apply (unfold plussub_def map2_def)apply simpdone lemma plus_list_Cons [simp]:  "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))"  by (simp add: plussub_def map2_def split: list.split)lemma length_plus_list [rule_format, simp]:  "!ys. length(xs +[f] ys) = min(length xs) (length ys)"apply (induct xs) apply simpapply clarifyapply (simp (no_asm_simp) split: list.split)donelemma nth_plus_list [rule_format, simp]:  "!xs ys i. length xs = n --> length ys = n --> i<n -->   (xs +[f] ys)!i = (xs!i) +_f (ys!i)"apply (induct n) apply simpapply clarifyapply (case_tac xs) apply simpapply (force simp add: nth_Cons split: list.split nat.split)donelemma (in Semilat) plus_list_ub1 [rule_format]: "[| set xs <= A; set ys <= A; size xs = size ys |]   ==> xs <=[r] xs +[f] ys"apply (unfold unfold_lesub_list)apply (simp add: Listn.le_def list_all2_conv_all_nth)donelemma (in Semilat) plus_list_ub2: "[|set xs <= A; set ys <= A; size xs = size ys |]  ==> ys <=[r] xs +[f] ys"apply (unfold unfold_lesub_list)apply (simp add: Listn.le_def list_all2_conv_all_nth)donelemma (in Semilat) plus_list_lub [rule_format]:shows "!xs ys zs. set xs <= A --> set ys <= A --> set zs <= A   --> size xs = n & size ys = n -->   xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs"apply (unfold unfold_lesub_list)apply (simp add: Listn.le_def list_all2_conv_all_nth)donelemma (in Semilat) list_update_incr [rule_format]: "x∈ A ==> set xs <= A -->   (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])"apply (unfold unfold_lesub_list)apply (simp add: Listn.le_def list_all2_conv_all_nth)apply (induct xs) apply simpapply (simp add: in_list_Suc_iff)apply clarifyapply (simp add: nth_Cons split: nat.split)donelemma acc_le_listI [intro!]:  "[| order r; acc r |] ==> acc(Listn.le r)"apply (unfold acc_def)apply (subgoal_tac "wf(UN n. {(ys,xs). size xs = n ∧ size ys = n ∧ xs <_(Listn.le r) ys})") apply (erule wf_subset) apply (blast intro: lesssub_list_impl_same_size)apply (rule wf_UN) prefer 2 apply clarify apply (rename_tac m n) apply (case_tac "m=n")  apply simp apply (fast intro!: equals0I dest: not_sym)apply clarifyapply (rename_tac n)apply (induct_tac n) apply (simp add: lesssub_def cong: conj_cong)apply (rename_tac k)apply (simp add: wf_eq_minimal)apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)apply clarifyapply (rename_tac M m)apply (case_tac "∃x xs. size xs = k ∧ x#xs ∈ M") prefer 2 apply (erule thin_rl) apply (erule thin_rl) apply blastapply (erule_tac x = "{a. ∃xs. size xs = k ∧ a#xs:M}" in allE)apply (erule impE) apply blastapply (thin_tac "∃x xs. ?P x xs")apply clarifyapply (rename_tac maxA xs)apply (erule_tac x = "{ys. size ys = size xs ∧ maxA#ys ∈ M}" in allE)apply (erule impE) apply blastapply clarifyapply (thin_tac "m ∈ M")apply (thin_tac "maxA#xs ∈ M")apply (rule bexI) prefer 2 apply assumptionapply clarifyapply simpapply blastdonelemma closed_listI:  "closed S f ==> closed (list n S) (map2 f)"apply (unfold closed_def)apply (induct n) apply simpapply clarifyapply (simp add: in_list_Suc_iff)apply clarifyapply simpdonelemma Listn_sl_aux:assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))"proof -  interpret Semilat A r f using assms by (rule Semilat.intro)show ?thesisapply (unfold Listn.sl_def)apply (simp (no_asm) only: semilat_Def split_conv)apply (rule conjI) apply simpapply (rule conjI) apply (simp only: closedI closed_listI)apply (simp (no_asm) only: list_def)apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)doneqedlemma Listn_sl: "!!L. semilat L ==> semilat (Listn.sl n L)" by(simp add: Listn_sl_aux split_tupled_all)lemma coalesce_in_err_list [rule_format]:  "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"apply (induct n) apply simpapply clarifyapply (simp add: in_list_Suc_iff)apply clarifyapply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)apply forcedone lemma lem: "!!x xs. x +_(op #) xs = x#xs"  by (simp add: plussub_def)lemma coalesce_eq_OK1_D [rule_format]:  "semilat(err A, Err.le r, lift2 f) ==>   !xs. xs : list n A --> (!ys. ys : list n A -->   (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"apply (induct n)  apply simpapply clarifyapply (simp add: in_list_Suc_iff)apply clarifyapply (simp split: err.split_asm add: lem Err.sup_def lift2_def)apply (force simp add: semilat_le_err_OK1)donelemma coalesce_eq_OK2_D [rule_format]:  "semilat(err A, Err.le r, lift2 f) ==>   !xs. xs : list n A --> (!ys. ys : list n A -->   (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"apply (induct n) apply simpapply clarifyapply (simp add: in_list_Suc_iff)apply clarifyapply (simp split: err.split_asm add: lem Err.sup_def lift2_def)apply (force simp add: semilat_le_err_OK2)done lemma lift2_le_ub:  "[| semilat(err A, Err.le r, lift2 f); x∈ A; y∈ A; x +_f y = OK z;       u∈ A; x <=_r u; y <=_r u |] ==> z <=_r u"apply (unfold semilat_Def plussub_def err_def)apply (simp add: lift2_def)apply clarifyapply (rotate_tac -3)apply (erule thin_rl)apply (erule thin_rl)apply forcedonelemma coalesce_eq_OK_ub_D [rule_format]:  "semilat(err A, Err.le r, lift2 f) ==>   !xs. xs : list n A --> (!ys. ys : list n A -->   (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us            & us : list n A --> zs <=[r] us))"apply (induct n) apply simpapply clarifyapply (simp add: in_list_Suc_iff)apply clarifyapply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)apply clarifyapply (rule conjI) apply (blast intro: lift2_le_ub)apply blastdone lemma lift2_eq_ErrD:  "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x∈ A; y∈ A |]   ==> ~(∃u∈ A. x <=_r u & y <=_r u)"  by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])lemma coalesce_eq_Err_D [rule_format]:  "[| semilat(err A, Err.le r, lift2 f) |]   ==> !xs. xs∈ list n A --> (!ys. ys∈ list n A -->       coalesce (xs +[f] ys) = Err -->       ~(∃zs∈ list n A. xs <=[r] zs & ys <=[r] zs))"apply (induct n) apply simpapply clarifyapply (simp add: in_list_Suc_iff)apply clarifyapply (simp split: err.split_asm add: lem Err.sup_def lift2_def) apply (blast dest: lift2_eq_ErrD)done lemma closed_err_lift2_conv:  "closed (err A) (lift2 f) = (∀x∈ A. ∀y∈ A. x +_f y : err A)"apply (unfold closed_def)apply (simp add: err_def)done lemma closed_map2_list [rule_format]:  "closed (err A) (lift2 f) ==>   ∀xs. xs : list n A --> (∀ys. ys : list n A -->   map2 f xs ys : list n (err A))"apply (unfold map2_def)apply (induct n) apply simpapply clarifyapply (simp add: in_list_Suc_iff)apply clarifyapply (simp add: plussub_def closed_err_lift2_conv)donelemma closed_lift2_sup:  "closed (err A) (lift2 f) ==>   closed (err (list n A)) (lift2 (sup f))"  by (fastforce  simp add: closed_def plussub_def sup_def lift2_def                          coalesce_in_err_list closed_map2_list                split: err.split)lemma err_semilat_sup:  "err_semilat (A,r,f) ==>   err_semilat (list n A, Listn.le r, sup f)"apply (unfold Err.sl_def)apply (simp only: split_conv)apply (simp (no_asm) only: semilat_Def plussub_def)apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)apply (rule conjI) apply (drule Semilat.orderI [OF Semilat.intro]) apply simpapply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D)done lemma err_semilat_upto_esl:  "!!L. err_semilat L ==> err_semilat(upto_esl m L)"apply (unfold Listn.upto_esl_def)apply (simp (no_asm_simp) only: split_tupled_all)apply simpapply (fastforce intro!: err_semilat_UnionI err_semilat_sup                dest: lesub_list_impl_same_size                 simp add: plussub_def Listn.sup_def)doneend`