Theory Listn

(*  Title:      HOL/MicroJava/DFA/Listn.thy
    Author:     Tobias Nipkow
    Copyright   2000 TUM
*)

section ‹Fixed Length Lists›

theory Listn
imports Err
begin

definition 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 (case_prod 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 (#) 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). (⋃{list n A |n. n <= m}, le r, sup f)"

lemmas [simp] = set_update_subsetI

lemma 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 simp
done

lemma Cons_notle_Nil [iff]: 
  "~ x#xs <=[r] []"
apply (unfold lesub_def Listn.le_def)
apply simp
done


lemma Cons_le_Cons [iff]:
  "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)"
apply (unfold lesub_def Listn.le_def)
apply simp
done

lemma 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 blast
done  

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)
done


lemma 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)
done

lemma 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)
done

lemma 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 clarify
apply simp
apply (blast intro: order_trans)
done

lemma 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 blast
apply clarify
apply simp
apply (blast intro: order_antisym)
done

lemma 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)
done


lemma 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 auto
done  

lemma le_list_appendI:
  "⋀b c d. a <=[r] b ⟹ c <=[r] d ⟹ a@c <=[r] b@d"
apply (induct a)
 apply simp
apply (case_tac b)
apply auto
done

lemma 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)
  done

lemma listI:
  "⟦ length xs = n; set xs <= A ⟧ ⟹ xs ∈ list n A"
apply (unfold list_def)
apply blast
done

lemma listE_length [simp]:
   "xs ∈ list n A ⟹ length xs = n"
apply (unfold list_def)
apply blast
done 

lemma less_lengthI:
  "⟦ xs ∈ list n A; p < n ⟧ ⟹ p < length xs"
  by simp

lemma listE_set [simp]:
  "xs ∈ list n A ⟹ set xs <= A"
apply (unfold list_def)
apply blast
done 

lemma list_0 [simp]:
  "list 0 A = {[]}"
apply (unfold list_def)
apply auto
done 

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 auto
done 

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 simp
apply (simp add: in_list_Suc_iff)
apply blast
done


lemma nth_in [rule_format, simp]:
  "∀i n. length xs = n ⟶ set xs <= A ⟶ i < n ⟶ (xs!i) ∈ A"
apply (induct "xs")
 apply simp
apply (simp add: nth_Cons split: nat.split)
done

lemma listE_nth_in:
  "⟦ xs ∈ list n A; i < n ⟧ ⟹ (xs!i) ∈ A"
  by auto


lemma listn_Cons_Suc [elim!]:
  "l#xs ∈ list n A ⟹ (⋀n'. n = Suc n' ⟹ l ∈ A ⟹ xs ∈ list n' A ⟹ P) ⟹ P"
  by (cases n) auto

lemma 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 blast
qed


lemma listt_update_in_list [simp, intro!]:
  "⟦ xs ∈ list n A; x∈ A ⟧ ⟹ xs[i := x] ∈ list n A"
apply (unfold list_def)
apply simp
done 

lemma plus_list_Nil [simp]:
  "[] +[f] xs = []"
apply (unfold plussub_def map2_def)
apply simp
done 

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 simp
apply clarify
apply (simp (no_asm_simp) split: list.split)
done

lemma 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 simp
apply clarify
apply (case_tac xs)
 apply simp
apply (force simp add: nth_Cons split: list.split nat.split)
done


lemma (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)
done

lemma (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)
done

lemma (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)
done

lemma (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 simp
apply (simp add: in_list_Suc_iff)
apply clarify
apply (simp add: nth_Cons split: nat.split)
done

lemma 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 (rename_tac m n)
 apply (case_tac "m=n")
  apply simp
 apply (fast intro!: equals0I dest: not_sym)
apply (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 clarify
apply (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 blast
apply (erule_tac x = "{a. ∃xs. size xs = k ∧ a#xs ∈ M}" in allE)
apply (erule impE)
 apply blast
apply (thin_tac "∃x xs. P x xs" for P)
apply clarify
apply (rename_tac maxA xs)
apply (erule_tac x = "{ys. size ys = size xs ∧ maxA#ys ∈ M}" in allE)
apply (erule impE)
 apply blast
apply clarify
apply (thin_tac "m ∈ M")
  apply (thin_tac "maxA#xs ∈ M")
apply (rule bexI)
 prefer 2
 apply assumption
apply clarify
apply simp
apply blast
done

lemma closed_listI:
  "closed S f ⟹ closed (list n S) (map2 f)"
apply (unfold closed_def)
apply (induct n)
 apply simp
apply clarify
apply (simp add: in_list_Suc_iff)
apply clarify
apply simp
done


lemma 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 ?thesis
apply (unfold Listn.sl_def)
apply (simp (no_asm) only: semilat_Def split_conv)
apply (rule conjI)
 apply simp
apply (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)
done
qed

lemma 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 simp
apply clarify
apply (simp add: in_list_Suc_iff)
apply clarify
apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)
apply force
done 

lemma lem: "⋀x xs. x +_(#) 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 simp
apply clarify
apply (simp add: in_list_Suc_iff)
apply clarify
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
apply (force simp add: semilat_le_err_OK1)
done

lemma 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 simp
apply clarify
apply (simp add: in_list_Suc_iff)
apply clarify
apply (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 clarify
apply (rotate_tac -3)
apply (erule thin_rl)
apply (erule thin_rl)
apply force
done

lemma 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 simp
apply clarify
apply (simp add: in_list_Suc_iff)
apply clarify
apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)
apply clarify
apply (rule conjI)
 apply (blast intro: lift2_le_ub)
apply blast
done 

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 simp
apply clarify
apply (simp add: in_list_Suc_iff)
apply clarify
apply (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 simp
apply clarify
apply (simp add: in_list_Suc_iff)
apply clarify
apply (simp add: plussub_def closed_err_lift2_conv)
done

lemma 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 simp
apply (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 simp
apply (fastforce intro!: err_semilat_UnionI err_semilat_sup
                dest: lesub_list_impl_same_size 
                simp add: plussub_def Listn.sup_def)
done

end