[STATEMENT]
lemma enc_wf_interp:
 "\<lbrakk>wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; x \<in> enc (w, I)\<rbrakk> \<Longrightarrow>
  wf_interp_for_formula (dec_word (x @- sconst (any, replicate (length I) False)),
    stream_dec (length I) (FOV \<phi>) (x @- sconst (any, replicate (length I) False))) \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; x \<in> enc (w, I)\<rbrakk> \<Longrightarrow> wf_interp_for_formula (dec_word (x @- sconst (any, replicate (length I) False)), stream_dec (length I) (FOV \<phi>) (x @- sconst (any, replicate (length I) False))) \<phi>
[PROOF STEP]
using
    stream_dec_Inl[of _ "FOV \<phi>" "length I" "stream_enc (w, I)", OF _ bspec[OF max_idx_vars]]
    stream_dec_Inr[of _ "FOV \<phi>" "length I" "stream_enc (w, I)", OF _ bspec[OF max_idx_vars]]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<in> FOV \<phi>; pre_wf_formula (length I) ?\<phi>2; ?i \<in> FOV ?\<phi>2 \<union> SOV ?\<phi>2\<rbrakk> \<Longrightarrow> \<exists>p. stream_dec (length I) (FOV \<phi>) (stream_enc (w, I)) ! ?i = Inl p
\<lbrakk>?i \<notin> FOV \<phi>; pre_wf_formula (length I) ?\<phi>2; ?i \<in> FOV ?\<phi>2 \<union> SOV ?\<phi>2\<rbrakk> \<Longrightarrow> \<exists>P. stream_dec (length I) (FOV \<phi>) (stream_enc (w, I)) ! ?i = Inr P

goal (1 subgoal):
 1. \<lbrakk>wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; x \<in> enc (w, I)\<rbrakk> \<Longrightarrow> wf_interp_for_formula (dec_word (x @- sconst (any, replicate (length I) False)), stream_dec (length I) (FOV \<phi>) (x @- sconst (any, replicate (length I) False))) \<phi>
[PROOF STEP]
by (auto split: sum.splits intro: Inr_dec_finite[OF finite_True_in_row] simp: max_idx_vars dec_word_def
    dest!: stream_dec_not_Inl stream_dec_not_Inr subsetD[OF set_cut_same] simp del: stream_enc.simps)
    (auto simp: cut_same_def in_set_zip smap2_alt shift_snth)


[STATEMENT]
lemma enc_atom_welldef: "\<forall>x a. enc_atom I x a = enc_atom I' x a \<Longrightarrow> m < length I \<Longrightarrow>
  (case (I ! m, I' ! m) of (Inl p, Inl q) \<Rightarrow> p = q | (Inr P, Inr Q) \<Rightarrow> P = Q | _ \<Rightarrow> True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl q) \<Rightarrow> p = q | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr Q) \<Rightarrow> P = Q
[PROOF STEP]
proof (induct "length I" arbitrary: I I' m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>I I' m. \<lbrakk>0 = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
 2. \<And>x I I' m. \<lbrakk>\<And>I I' m. \<lbrakk>x = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x; Suc x = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
case (Suc n I I')
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = length ?I2; \<forall>x a. enc_atom ?I2 x a = enc_atom ?I'2 x a; ?m2 < length ?I2\<rbrakk> \<Longrightarrow> case (?I2 ! ?m2, ?I'2 ! ?m2) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
Suc n = length I
\<forall>x a. enc_atom I x a = enc_atom I' x a
m < length I

goal (2 subgoals):
 1. \<And>I I' m. \<lbrakk>0 = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
 2. \<And>x I I' m. \<lbrakk>\<And>I I' m. \<lbrakk>x = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x; Suc x = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n = length ?I2; \<forall>x a. enc_atom ?I2 x a = enc_atom ?I'2 x a; ?m2 < length ?I2\<rbrakk> \<Longrightarrow> case (?I2 ! ?m2, ?I'2 ! ?m2) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
Suc n = length I
\<forall>x a. enc_atom I x a = enc_atom I' x a
m < length I
[PROOF STEP]
obtain x xs x' xs' where *: "I = x # xs" "I' = x' # xs'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = length ?I2; \<forall>x a. enc_atom ?I2 x a = enc_atom ?I'2 x a; ?m2 < length ?I2\<rbrakk> \<Longrightarrow> case (?I2 ! ?m2, ?I'2 ! ?m2) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
Suc n = length I
\<forall>x a. enc_atom I x a = enc_atom I' x a
m < length I

goal (1 subgoal):
 1. (\<And>x xs x' xs'. \<lbrakk>I = x # xs; I' = x' # xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: Suc_length_conv map_eq_Cons_conv)
[PROOF STATE]
proof (state)
this:
I = x # xs
I' = x' # xs'

goal (2 subgoals):
 1. \<And>I I' m. \<lbrakk>0 = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
 2. \<And>x I I' m. \<lbrakk>\<And>I I' m. \<lbrakk>x = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x; Suc x = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n = length ?I2; \<forall>x a. enc_atom ?I2 x a = enc_atom ?I'2 x a; ?m2 < length ?I2\<rbrakk> \<Longrightarrow> case (?I2 ! ?m2, ?I'2 ! ?m2) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
Suc n = length I
\<forall>x a. enc_atom I x a = enc_atom I' x a
m < length I
I = x # xs
I' = x' # xs'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = length ?I2; \<forall>x a. enc_atom ?I2 x a = enc_atom ?I'2 x a; ?m2 < length ?I2\<rbrakk> \<Longrightarrow> case (?I2 ! ?m2, ?I'2 ! ?m2) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
Suc n = length I
\<forall>x a. enc_atom I x a = enc_atom I' x a
m < length I
I = x # xs
I' = x' # xs'

goal (1 subgoal):
 1. case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
proof (cases m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>I I' m. \<lbrakk>n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x; Suc n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I; I = x # xs; I' = x' # xs'; m = 0\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
 2. \<And>nat. \<lbrakk>\<And>I I' m. \<lbrakk>n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x; Suc n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I; I = x # xs; I' = x' # xs'; m = Suc nat\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
m = 0

goal (2 subgoals):
 1. \<lbrakk>\<And>I I' m. \<lbrakk>n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x; Suc n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I; I = x # xs; I' = x' # xs'; m = 0\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
 2. \<And>nat. \<lbrakk>\<And>I I' m. \<lbrakk>n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x; Suc n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I; I = x # xs; I' = x' # xs'; m = Suc nat\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m = 0

goal (1 subgoal):
 1. case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
using Suc(3)
[PROOF STATE]
proof (prove)
using this:
m = 0
\<forall>x a. enc_atom I x a = enc_atom I' x a

goal (1 subgoal):
 1. case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
m = 0
\<forall>xa a. enc_atom (x # xs) xa a = enc_atom (x' # xs') xa a

goal (1 subgoal):
 1. case ((x # xs) ! m, (x' # xs') ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
by (cases x x' rule: sum.exhaust[case_product sum.exhaust]) auto
[PROOF STATE]
proof (state)
this:
case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<And>I I' m. \<lbrakk>n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x; Suc n = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I; I = x # xs; I' = x' # xs'; m = Suc nat\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x

goal (1 subgoal):
 1. \<And>I I' m. \<lbrakk>0 = length I; \<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl x) \<Rightarrow> p = x | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr x) \<Rightarrow> P = x
[PROOF STEP]
qed simp