Theory Idempotence
section "Idempotence of the auxiliary type system meant for loop bodies"
theory Idempotence
imports Definitions
begin
text ‹
\null
As in my previous paper \<^cite>‹"Noce24"›, the purpose of this section is to prove that the auxiliary
type system @{const [names_short] noninterf.ctyping1} used to simulate the execution of loop bodies
is idempotent, namely that if its output for a given input is the pair formed by @{typ "state set"}
@{term B} and @{typ "vname set"} @{term Y}, then the output is the same if @{term B} and @{term Y}
are fed back into the type system (lemma @{text ctyping1_idem}).
›
subsection "Local context proofs"
context noninterf
begin
abbreviation ctyping1_idem_lhs where
"ctyping1_idem_lhs s t t' ys ys' x ≡
if [y←ys'. fst y = x] = []
then if [y←ys. fst y = x] = []
then s x
else case snd (last [y←ys. fst y = x]) of None ⇒ t x | Some i ⇒ i
else case snd (last [y←ys'. fst y = x]) of None ⇒ t' x | Some i ⇒ i"
abbreviation ctyping1_idem_rhs where
"ctyping1_idem_rhs f s t x ≡
if f x = []
then s x
else case snd (last (f x)) of None ⇒ t x | Some i ⇒ i"
abbreviation ctyping1_idem_pred where
"ctyping1_idem_pred s t t' ys ys' A (S :: state_upd list set) ≡ ∃f s'.
(∃t''. ctyping1_idem_lhs s t t' ys ys' = ctyping1_idem_rhs f s' t'') ∧
(∀x. (f x = [] ⟷ [y←ys @ ys'. fst y = x] = []) ∧
(f x ≠ [] ⟶ last (f x) = last [y←ys @ ys'. fst y = x])) ∧
(∃ys''. f = (λx. [y←ys''. fst y = x]) ∧ ys'' ∈ S) ∧ s' ∈ A"
lemma ctyping1_merge_aux_no_nil:
"ws ∈ A ⨆ B ⟹ ws ≠ []"
by (erule ctyping1_merge_aux.cases, simp_all)
lemma ctyping1_merge_aux_empty_lhs:
"{} ⨆ B = {[(ys, False)] | ys. ys ∈ B}"
by (rule equalityI, clarify, erule ctyping1_merge_aux.induct, auto)
lemma ctyping1_merge_aux_empty_rhs:
"A ⨆ {} = {[(xs, True)] | xs. xs ∈ A}"
by (rule equalityI, clarify, erule ctyping1_merge_aux.induct, auto)
lemma ctyping1_merge_empty_lhs:
"{} ⊔ B = B"
by (force simp: ctyping1_merge_def ctyping1_merge_aux_empty_lhs)
lemma ctyping1_merge_empty_rhs:
"A ⊔ {} = A"
by (force simp: ctyping1_merge_def ctyping1_merge_aux_empty_rhs)
lemma ctyping1_aux_nonempty:
"⊢ c ≠ {}"
by (induction c, auto simp: Let_def ctyping1_merge_def
ctyping1_merge_append_def ctyping1_append_def, fastforce)
lemma ctyping1_merge_idem_fst:
assumes
A: "⋀ys ys'. ys ∈ ⊢ c⇩1 ⟹ ys' ∈ ⊢ c⇩1 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1)" and
B: "⋀ys ys'. ys ∈ ⊢ c⇩2 ⟹ ys' ∈ ⊢ c⇩2 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩2)" and
C: "s ∈ A" and
D: "ys ∈ ⊢ c⇩1 ⊔ ⊢ c⇩2" and
E: "ys' ∈ ⊢ c⇩1 ⊔ ⊢ c⇩2"
shows "ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1 ⊔ ⊢ c⇩2)"
proof -
obtain ws where "ws ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2" and "ys = concat (map fst ws)"
using D by (auto simp: ctyping1_merge_def)
thus ?thesis
proof (induction ws arbitrary: ys rule: list.induct,
blast dest: ctyping1_merge_aux_no_nil)
fix w ws ys
assume
F: "⋀xs. ws ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2 ⟹ xs = concat (map fst ws) ⟹
ctyping1_idem_pred s t t' xs ys' A (⊢ c⇩1 ⊔ ⊢ c⇩2)" and
G: "w # ws ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2"
assume "ys = concat (map fst (w # ws))"
hence H: "ys = fst w @ concat (map fst ws)"
(is "ys = ?x @ ?xs")
by simp
have "ctyping1_idem_pred s t t' ?xs ys' A (⊢ c⇩1 ⊔ ⊢ c⇩2)"
proof (cases ws)
case Nil
show ?thesis
apply (rule exI [of _ "λx. [y←ys'. fst y = x]"])
apply (rule exI [of _ s])
apply (rule conjI)
apply (rule exI [of _ t'])
by (auto simp: C E Nil)
next
case Cons
have "ws ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2"
using G by (rule ctyping1_merge_aux.cases, simp_all add: Cons)
thus ?thesis
using F by simp
qed
then obtain f and s' and t'' and ys'' where
I: "ctyping1_idem_lhs s t t' ?xs ys' =
ctyping1_idem_rhs f s' t''" and
J: "∀x. (f x = [] ⟷ [y←?xs @ ys'. fst y = x] = []) ∧
(f x ≠ [] ⟶ last (f x) = last [y←?xs @ ys'. fst y = x])" and
K: "f = (λx. [y←ys''. fst y = x])" and
L: "ys'' ∈ ⊢ c⇩1 ⊔ ⊢ c⇩2" and
M: "s' ∈ A"
by auto
obtain ws'' where
N: "ws'' ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2" and
O: "ys'' = concat (map fst ws'')"
using L by (auto simp: ctyping1_merge_def)
show "ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1 ⊔ ⊢ c⇩2)"
proof (cases "w ∈ set ws''")
assume P: "w ∈ set ws''"
show ?thesis
apply (rule exI [of _ f])
apply (rule exI [of _ s'])
apply (rule conjI)
apply (rule exI [of _ t''])
apply (rule ext)
subgoal for x
proof (cases "[y←ys'. fst y = x]", cases "[y←ys. fst y = x] = []")
case Cons
thus "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs f s' t'' x"
by (insert fun_cong [OF I, of x], simp)
next
case Nil
moreover case True
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs f s' t'' x"
using H by (insert fun_cong [OF I, of x], simp)
next
case Nil
case False
hence "[y←?x. fst y = x] ≠ [] ∨ [y←?xs. fst y = x] ≠ []"
using H by simp
moreover {
assume "[y←?x. fst y = x] ≠ []"
hence "[y←ys''. fst y = x] ≠ []"
using O and P by (auto simp: filter_concat)
hence "[y←?xs. fst y = x] ≠ []"
using J and K and Nil by simp
}
ultimately have Q: "[y←?xs. fst y = x] ≠ []" ..
hence "(case snd (last [y←?xs. fst y = x]) of
None ⇒ t x | Some i ⇒ i) = ctyping1_idem_rhs f s' t'' x"
using Nil by (insert fun_cong [OF I, of x], simp)
moreover have "last [y←?xs. fst y = x] = last [y←ys. fst y = x]"
using H and Q by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs f s' t'' x"
using Nil and False by simp
qed
apply (rule conjI)
subgoal
proof -
show "∀x. (f x = [] ⟷ [y←ys @ ys'. fst y = x] = []) ∧
(f x ≠ [] ⟶ last (f x) = last [y←ys @ ys'. fst y = x])"
(is "∀x. ?P x ∧ ?Q x")
proof
fix x
have "?P x"
proof
assume Q: "f x = []"
hence "[y←?xs @ ys'. fst y = x] = []"
using J by simp
moreover have "[y←?x. fst y = x] = []"
using K and O and P and Q by (simp add: filter_concat)
ultimately show "[y←ys @ ys'. fst y = x] = []"
using H by simp
qed (insert H J, simp)
moreover have "?Q x"
using J and H by simp
ultimately show "?P x ∧ ?Q x" ..
qed
qed
by (insert K L M, blast)
next
assume P: "w ∉ set ws''"
let ?y = "fst (hd ws'')"
show ?thesis
proof (cases "snd w = snd (hd ws'')")
assume Q: "snd w = snd (hd ws'')"
hence "snd w ∧ snd (hd ws'') ∨ ¬ snd w ∧ ¬ snd (hd ws'')"
(is "?P ∨ ?Q")
by simp
moreover {
assume ?P
have "?x ∈ ⊢ c⇩1"
using G by (rule ctyping1_merge_aux.cases, insert `?P`, simp_all)
moreover have "?y ∈ ⊢ c⇩1"
using N by (rule ctyping1_merge_aux.cases, insert `?P`, simp_all)
ultimately have "ctyping1_idem_pred s t t' ?x ?y A (⊢ c⇩1)"
using A by simp
}
moreover {
assume ?Q
have "?x ∈ ⊢ c⇩2"
using G by (rule ctyping1_merge_aux.cases, insert `?Q`, simp_all)
moreover have "?y ∈ ⊢ c⇩2"
using N by (rule ctyping1_merge_aux.cases, insert `?Q`, simp_all)
ultimately have "ctyping1_idem_pred s t t' ?x ?y A (⊢ c⇩2)"
using B by simp
}
ultimately obtain f⇩0 and s⇩0 and t⇩0 and ys⇩0 where
R: "ctyping1_idem_lhs s t t' ?x ?y =
ctyping1_idem_rhs f⇩0 s⇩0 t⇩0" and
S: "∀x. (f⇩0 x = [] ⟷ [y←?x @ ?y. fst y = x] = []) ∧
(f⇩0 x ≠ [] ⟶ last (f⇩0 x) = last [y←?x @ ?y. fst y = x])" and
T: "f⇩0 = (λx. [y←ys⇩0. fst y = x])" and
U: "ys⇩0 ∈ ⊢ c⇩1 ∧ snd w ∨ ys⇩0 ∈ ⊢ c⇩2 ∧ ¬ snd w"
by auto
from U obtain w⇩0 where
V: "[w⇩0] ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2" and
W: "ys⇩0 = fst w⇩0" and
X: "snd w⇩0 = snd w"
by fastforce
show ?thesis
proof (cases "w⇩0 ∈ set ws''")
assume Y: "w⇩0 ∈ set ws''"
show ?thesis
apply (rule exI [of _ f])
apply (rule exI [of _ s'])
apply (rule conjI)
apply (rule exI [of _ t''])
apply (rule ext)
subgoal for x
proof (cases "[y←ys'. fst y = x]", cases "[y←ys. fst y = x] = []")
case Cons
thus "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs f s' t'' x"
by (insert fun_cong [OF I, of x], simp)
next
case Nil
moreover case True
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs f s' t'' x"
using H by (insert fun_cong [OF I, of x], simp)
next
case Nil
case False
hence "[y←?x. fst y = x] ≠ [] ∨ [y←?xs. fst y = x] ≠ []"
using H by simp
moreover {
assume "[y←?x. fst y = x] ≠ []"
hence "[y←ys⇩0. fst y = x] ≠ []"
using S and T by simp
hence "[y←ys''. fst y = x] ≠ []"
using O and W and Y by (auto simp: filter_concat)
hence "[y←?xs. fst y = x] ≠ []"
using J and K and Nil by simp
}
ultimately have Z: "[y←?xs. fst y = x] ≠ []" ..
hence "(case snd (last [y←?xs. fst y = x]) of
None ⇒ t x | Some i ⇒ i) = ctyping1_idem_rhs f s' t'' x"
using Nil by (insert fun_cong [OF I, of x], simp)
moreover have "last [y←?xs. fst y = x] = last [y←ys. fst y = x]"
using H and Z by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs f s' t'' x"
using Nil and False by simp
qed
apply (rule conjI)
subgoal
proof -
show "∀x. (f x = [] ⟷ [y←ys @ ys'. fst y = x] = []) ∧
(f x ≠ [] ⟶ last (f x) = last [y←ys @ ys'. fst y = x])"
(is "∀x. ?P x ∧ ?Q x")
proof
fix x
have "?P x"
proof
assume Z: "f x = []"
hence "[y←?xs @ ys'. fst y = x] = []"
using J by simp
moreover have "[y←ys''. fst y = x] = []"
using K and Z by simp
hence "[y←ys⇩0. fst y = x] = []"
using O and W and Y by (simp add: filter_concat)
hence "[y←?x. fst y = x] = []"
using S and T by simp
ultimately show "[y←ys @ ys'. fst y = x] = []"
using H by simp
qed (insert H J, simp)
moreover have "?Q x"
using J and H by simp
ultimately show "?P x ∧ ?Q x" ..
qed
qed
by (insert K L M, blast)
next
assume Y: "w⇩0 ∉ set ws''"
let ?ws = "w⇩0 # tl ws''"
{
assume Z: "tl ws'' ≠ []"
have "tl ws'' ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2"
using N by (rule ctyping1_merge_aux.cases, insert Z, simp_all)
moreover have "snd (hd (tl ws'')) = (¬ snd w)"
using N by (rule ctyping1_merge_aux.cases, insert Q Z, simp_all)
moreover have "w⇩0 ∉ set (tl ws'')"
using Y by (cases ws'', simp_all)
ultimately have "?ws ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2"
by (cases w⇩0, insert U W X, auto)
}
hence Z: "?ws ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2"
by (cases "tl ws''", insert V, simp_all)
let ?ys = "concat (map fst (tl ws''))"
let ?f = "λx. [y←concat (map fst ?ws). fst y = x]"
let ?t = "λx. if f x = [] then t⇩0 x else t'' x"
have AA: "ws'' = hd ws'' # tl ws''"
by (insert ctyping1_merge_aux_no_nil [OF N], simp)
have AB: "ys'' = ?y @ ?ys"
using O by (subst (asm) AA, simp)
have AC: "∀x. [y←?ys. fst y = x] ≠ [] ⟶
last (?f x) = last (f x)"
using K and O by (subst (asm) AA, simp)
have AD: "∀x. [y←?ys. fst y = x] = [] ∧ [y←?y. fst y = x] ≠ [] ⟶
last (?f x) = last (f x)"
(is "∀x. ?P x ∧ ?Q x ⟶ _")
proof clarify
fix x
assume "?P x" and "?Q x"
moreover from this and S and T have
"last [y←ys⇩0. fst y = x] = last [y←?x @ ?y. fst y = x]"
by simp
ultimately show "last (?f x) = last (f x)"
using K and W and AB by simp
qed
show ?thesis
apply (rule exI [of _ ?f])
apply (rule exI [of _ s'])
apply (rule conjI)
apply (rule exI [of _ ?t])
apply (rule ext)
subgoal for x
proof (cases "[y←ys'. fst y = x]", cases "[y←?xs. fst y = x] = []")
case Cons
hence AE:
"(case snd (last [y←ys'. fst y = x]) of
None ⇒ t' x | Some i ⇒ i) =
(case snd (last (f x)) of None ⇒ ?t x | Some i ⇒ i)"
using J by (insert fun_cong [OF I, of x], simp)
show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s' ?t x"
proof (cases "[y←?ys. fst y = x] ≠ []")
case True
thus ?thesis
using AC and AE and Cons by simp
next
case False
moreover have "[y←ys''. fst y = x] ≠ []"
using J and K and Cons by simp
ultimately have "[y←?y. fst y = x] ≠ []"
using AB by simp
moreover from this have "?f x ≠ []"
using S and T and W by simp
ultimately show ?thesis
using AD and AE and Cons and False by simp
qed
next
case Nil
moreover case False
ultimately have
"(case snd (last [y←ys. fst y = x]) of
None ⇒ t x | Some i ⇒ i) =
(case snd (last (f x)) of None ⇒ ?t x | Some i ⇒ i)"
using J and H by (insert fun_cong [OF I, of x], simp)
moreover have
AE: "[y←?y. fst y = x] ≠ [] ∨ [y←?ys. fst y = x] ≠ []"
(is "_ ∨ ?P")
using J and K and AB and False by auto
hence "?f x ≠ []"
using S and T and W by (cases ?P, simp_all)
moreover have "last (?f x) = last (f x)"
using AC and AD and AE by blast
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s' ?t x"
using H and Nil and False by auto
next
case Nil
moreover case True
ultimately have AE: "f x = []"
using J by simp
hence AF: "[y←?y @ ?ys. fst y = x] = []"
using K and AB by simp
show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s' ?t x"
proof (cases "[y←?x. fst y = x] = []")
assume AG: "[y←?x. fst y = x] = []"
moreover from J and AE have "s x = s' x"
by (insert fun_cong [OF I, of x], simp)
moreover have "[y←ys⇩0. fst y = x] = []"
using S and T and AF and AG by simp
hence "?f x = []"
using W and AF by simp
ultimately show ?thesis
using H and Nil and True by simp
next
assume AG: "[y←?x. fst y = x] ≠ []"
moreover from this and S and AE and AF have
"(case snd (last [y←?x. fst y = x]) of
None ⇒ t x | Some i ⇒ i) =
(case snd (last (f⇩0 x)) of None ⇒ ?t x | Some i ⇒ i)"
by (insert fun_cong [OF R, of x], simp)
moreover have "[y←ys⇩0. fst y = x] ≠ []"
using S and T and AG by simp
hence "?f x ≠ []"
using W by simp
moreover have "last (?f x) = last (f⇩0 x)"
using T and W and AF by simp
ultimately show ?thesis
using H and Nil and True by auto
qed
qed
apply (rule conjI)
subgoal
proof -
show "∀x. (?f x = [] ⟷ [y←ys @ ys'. fst y = x] = []) ∧
(?f x ≠ [] ⟶ last (?f x) = last [y←ys @ ys'. fst y = x])"
(is "∀x. ?P x ∧ ?Q x")
proof
fix x
have AE: "?P x"
proof
assume AF: "?f x = []"
hence "[y←?x @ ?y. fst y = x] = []"
using S and T and W by simp
moreover from this and J and K and AB and AF have
"[y←?xs @ ys'. fst y = x] = []"
by auto
ultimately show "[y←ys @ ys'. fst y = x] = []"
using H by simp
next
assume "[y←ys @ ys'. fst y = x] = []"
hence "[y←?x @ ?y @ ?ys. fst y = x] = []"
using H and J and K and AB by simp
moreover from this have "[y←ys⇩0. fst y = x] = []"
using S and T by simp
ultimately show "?f x = []"
using W by simp
qed
moreover have "?Q x"
proof (clarify, cases "[y←?y @ ?ys. fst y = x]")
case Nil
hence "last (?f x) = last (f⇩0 x)"
using T and W by simp
moreover assume "?f x ≠ []"
hence "[y←ys @ ys'. fst y = x] ≠ []"
using AE by blast
hence "[y←?x @ ?y @ ?ys. fst y = x] ≠ []"
using H and J and K and AB by simp
ultimately have "last (?f x) = last [y←?x. fst y = x]"
using S and Nil by simp
moreover have "[y←?xs @ ys'. fst y = x] = []"
using J and K and AB and Nil by simp
ultimately show
"last (?f x) = last [y←ys @ ys'. fst y = x]"
using H by simp
next
case Cons
hence "[y←?y. fst y = x] ≠ [] ∨
[y←?ys. fst y = x] ≠ []"
by auto
hence "last (?f x) = last (f x)"
using AC and AD by blast
moreover have "f x ≠ []"
using K and AB and Cons by simp
ultimately show
"last (?f x) = last [y←ys @ ys'. fst y = x]"
using H and J by simp
qed
ultimately show "?P x ∧ ?Q x" ..
qed
qed
by (rule conjI, rule exI [of _ "concat (map fst ?ws)"],
insert M Z, auto simp only: ctyping1_merge_def)
qed
next
assume "snd w ≠ snd (hd ws'')"
hence "snd w ∧ ¬ snd (hd ws'') ∨ ¬ snd w ∧ snd (hd ws'')"
(is "?P ∨ ?Q")
by simp
moreover {
assume ?P
moreover have "?x ∈ ⊢ c⇩1"
using G by (rule ctyping1_merge_aux.cases, insert `?P`, simp_all)
moreover have "(?x, True) ∉ set ws''"
using P and `?P` by (cases w, simp)
ultimately have "w # ws'' ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2"
using N by (cases w, auto)
}
moreover {
assume ?Q
moreover have "?x ∈ ⊢ c⇩2"
using G by (rule ctyping1_merge_aux.cases, insert `?Q`, simp_all)
moreover have "(?x, False) ∉ set ws''"
using P and `?Q` by (cases w, simp)
ultimately have "w # ws'' ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2"
using N by (cases w, auto)
}
ultimately have Q: "w # ws'' ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2"
(is "?ws ∈ _") ..
let ?f = "λx. [y←concat (map fst ?ws). fst y = x]"
let ?t = "λx. if f x = [] then t x else t'' x"
show ?thesis
apply (rule exI [of _ ?f])
apply (rule exI [of _ s'])
apply (rule conjI)
apply (rule exI [of _ ?t])
apply (rule ext)
subgoal for x
proof (cases "[y←ys'. fst y = x]", cases "[y←?xs. fst y = x] = []")
case Cons
moreover from this have
"(case snd (last [y←ys'. fst y = x]) of
None ⇒ t' x | Some i ⇒ i) =
(case snd (last (f x)) of None ⇒ ?t x | Some i ⇒ i)"
using J by (insert fun_cong [OF I, of x], simp)
moreover have "?f x ≠ []"
using J and K and O and Cons by simp
moreover have "f x ≠ []"
using J and Cons by simp
hence "last (?f x) = last (f x)"
using K and O by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s' ?t x"
by auto
next
case Nil
moreover case False
ultimately have
"(case snd (last [y←ys. fst y = x]) of
None ⇒ t x | Some i ⇒ i) =
(case snd (last (f x)) of None ⇒ ?t x | Some i ⇒ i)"
using J and H by (insert fun_cong [OF I, of x], simp)
moreover have "?f x ≠ []"
using J and K and O and False by simp
moreover have "f x ≠ []"
using J and False by simp
hence "last (?f x) = last (f x)"
using K and O by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s' ?t x"
using H and Nil and False by auto
next
case Nil
moreover case True
ultimately have R: "f x = []"
using J by simp
show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s' ?t x"
proof (cases "[y←?x. fst y = x] = []")
assume "[y←?x. fst y = x] = []"
moreover have "[y←ys''. fst y = x] = []"
using K and R by simp
ultimately have "?f x = []"
using O by simp
moreover from J and R have "s x = s' x"
by (insert fun_cong [OF I, of x], simp)
ultimately show ?thesis
using H and Nil and True by simp
next
assume "[y←?x. fst y = x] ≠ []"
moreover have "last [y←ys. fst y = x] = last [y←?x. fst y = x]"
using H and True by simp
moreover have "last (?f x) = last [y←?x. fst y = x]"
using K and O and R by simp
ultimately show ?thesis
using H and R and Nil by simp
qed
qed
apply (rule conjI)
subgoal
proof -
show "∀x. (?f x = [] ⟷ [y←ys @ ys'. fst y = x] = []) ∧
(?f x ≠ [] ⟶ last (?f x) = last [y←ys @ ys'. fst y = x])"
(is "∀x. ?P x ∧ ?Q x")
proof
fix x
have "?P x"
proof
assume "?f x = []"
hence "[y←?x @ ys''. fst y = x] = []"
using O by simp
moreover from this have "[y←?xs @ ys'. fst y = x] = []"
using J and K by simp
ultimately show "[y←ys @ ys'. fst y = x] = []"
using H by simp
next
assume "[y←ys @ ys'. fst y = x] = []"
hence "[y←?x @ ?xs @ ys'. fst y = x] = []"
using H by simp
moreover from this have "[y←ys''. fst y = x] = []"
using J and K by simp
ultimately show "?f x = []"
using O by simp
qed
moreover have "?Q x"
proof (clarify, cases "[y←ys''. fst y = x]")
case Nil
hence "last (?f x) = last [y←?x. fst y = x]"
using O by simp
moreover have "[y←?xs @ ys'. fst y = x] = []"
using J and K and Nil by simp
hence
"last [y←ys @ ys'. fst y = x] = last [y←?x. fst y = x]"
using H by simp
ultimately show
"last (?f x) = last [y←ys @ ys'. fst y = x]"
by simp
next
case Cons
hence "last (?f x) = last (f x)"
using K and O by simp
moreover have R: "f x ≠ []"
using K and Cons by simp
hence "last [y←?xs @ ys'. fst y = x] = last (f x)"
using J by simp
moreover have "[y←?xs @ ys'. fst y = x] ≠ []"
using J and R by simp
ultimately show
"last (?f x) = last [y←ys @ ys'. fst y = x]"
using H by simp
qed
ultimately show "?P x ∧ ?Q x" ..
qed
qed
by (rule conjI, rule exI [of _ "concat (map fst ?ws)"],
insert M Q, auto simp only: ctyping1_merge_def)
qed
qed
qed
qed
lemma ctyping1_merge_append_idem_fst:
assumes
A: "⋀ys ys'. ys ∈ ⊢ c⇩1 ⟹ ys' ∈ ⊢ c⇩1 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1)" and
B: "⋀ys ys'. ys ∈ ⊢ c⇩2 ⟹ ys' ∈ ⊢ c⇩2 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩2)" and
C: "s ∈ A" and
D: "ys ∈ ⊢ c⇩1 ⊔⇩@ ⊢ c⇩2" and
E: "ys' ∈ ⊢ c⇩1 ⊔⇩@ ⊢ c⇩2"
shows "ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1 ⊔⇩@ ⊢ c⇩2)"
apply (subst ctyping1_merge_append_def)
apply (split if_split)
apply (rule conjI)
subgoal
proof
assume F: "card (⊢ c⇩2) = Suc 0"
with D obtain ys⇩1 and ys⇩2 where
G: "ys = ys⇩1 @ ys⇩2" and
H: "ys⇩1 ∈ ⊢ c⇩1" and
I: "ys⇩2 ∈ ⊢ c⇩2"
by (auto simp: ctyping1_merge_append_def ctyping1_append_def)
from E and F obtain ys⇩1' and ys⇩2' where
J: "ys' = ys⇩1' @ ys⇩2'" and
K: "ys⇩1' ∈ ⊢ c⇩1" and
L: "ys⇩2' ∈ ⊢ c⇩2"
by (auto simp: ctyping1_merge_append_def ctyping1_append_def)
have M: "ys⇩2' = ys⇩2"
using F and I and L by (fastforce simp: card_1_singleton_iff)
obtain f and s' and t'' and ys⇩1'' where
N: "ctyping1_idem_lhs s t t' ys⇩1 ys⇩1' =
ctyping1_idem_rhs f s' t''" and
O: "∀x. (f x = [] ⟷ [y←ys⇩1 @ ys⇩1'. fst y = x] = []) ∧
(f x ≠ [] ⟶ last (f x) = last [y←ys⇩1 @ ys⇩1'. fst y = x])" and
P: "f = (λx. [y←ys⇩1''. fst y = x])" and
Q: "ys⇩1'' ∈ ⊢ c⇩1" and
R: "s' ∈ A"
using A [OF H K] by auto
let ?f = "λx. [y←ys⇩1'' @ ys⇩2. fst y = x]"
let ?t = "λx. if [y←ys⇩2. fst y = x] = [] then t'' x else t' x"
show "ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1 @ ⊢ c⇩2)"
apply (rule exI [of _ ?f])
apply (rule exI [of _ s'])
apply (rule conjI)
apply (rule exI [of _ ?t])
apply (rule ext)
subgoal for x
proof (cases "[y←ys⇩2. fst y = x]", cases "f x = []")
case Nil
moreover case True
ultimately have "s x = s' x"
using O by (insert fun_cong [OF N, of x], simp)
moreover have "[y←ys'. fst y = x] = []"
using J and M and O and Nil and True by simp
moreover have "[y←ys. fst y = x] = []"
using G and O and Nil and True by simp
moreover have "?f x = []"
using P and Nil and True by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s' ?t x"
by simp
next
case Nil
moreover from this have
"[y←ys'. fst y = x] = [y←ys⇩1'. fst y = x]"
using J and M by simp
moreover have "[y←ys. fst y = x] = [y←ys⇩1. fst y = x]"
using G and Nil by simp
moreover case False
moreover from this have "?f x ≠ []"
using P by simp
moreover have "last (?f x) = last (f x)"
using P and Nil by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s' ?t x"
by (insert fun_cong [OF N, of x], auto)
next
case Cons
moreover from this have "[y←ys'. fst y = x] ≠ []"
using J and M by simp
moreover have
"last [y←ys'. fst y = x] = last [y←ys⇩2. fst y = x]"
using J and M and Cons by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s' ?t x"
by simp
qed
apply (rule conjI)
subgoal
proof -
show "∀x. (?f x = [] ⟷ [y←ys @ ys'. fst y = x] = []) ∧
(?f x ≠ [] ⟶ last (?f x) = last [y←ys @ ys'. fst y = x])"
(is "∀x. ?P x ∧ ?Q x")
proof
fix x
have "?P x"
using G and J and M and O and P by auto
moreover have "?Q x"
proof (clarify, cases "[y←ys⇩2. fst y = x]")
case Nil
moreover assume "?f x ≠ []"
ultimately have
"last (?f x) = last [y←ys⇩1 @ ys⇩1'. fst y = x]"
using O and P by simp
thus "last (?f x) = last [y←ys @ ys'. fst y = x]"
using G and J and M and Nil by simp
next
case Cons
thus "last (?f x) = last [y←ys @ ys'. fst y = x]"
using J and M by simp
qed
ultimately show "?P x ∧ ?Q x" ..
qed
qed
by (rule conjI, rule exI [of _ "ys⇩1'' @ ys⇩2"],
insert I Q R, auto simp: ctyping1_append_def)
qed
subgoal
proof
assume F: "card (⊢ c⇩2) ≠ Suc 0"
with D obtain ws and xs where
G: "ys = ws @ xs" and
H: "ws ∈ ⊢ c⇩1 ⊔ ⊢ c⇩2" and
I: "xs ∈ ⊢ c⇩2"
by (auto simp: ctyping1_merge_append_def ctyping1_append_def)
from E and F obtain ws' and xs' where
J: "ys' = ws' @ xs'" and
K: "ws' ∈ ⊢ c⇩1 ⊔ ⊢ c⇩2" and
L: "xs' ∈ ⊢ c⇩2"
by (auto simp: ctyping1_merge_append_def ctyping1_append_def)
from I have "[(xs, False)] ∈ ⊢ c⇩1 ⨆ ⊢ c⇩2" ..
hence M: "xs ∈ ⊢ c⇩1 ⊔ ⊢ c⇩2"
by (force simp: ctyping1_merge_def)
obtain f and s' and r and zs where
N: "ctyping1_idem_lhs s t t' ws xs =
ctyping1_idem_rhs f s' r" and
O: "∀x. (f x = [] ⟷ [y←ws @ xs. fst y = x] = []) ∧
(f x ≠ [] ⟶ last (f x) = last [y←ws @ xs. fst y = x])" and
P: "f = (λx. [y←zs. fst y = x])" and
Q: "zs ∈ ⊢ c⇩1 ⊔ ⊢ c⇩2" and
R: "s' ∈ A"
using ctyping1_merge_idem_fst [OF A B C H M] by auto
obtain f' and s'' and r' and zs' where
S: "ctyping1_idem_lhs s t t' zs ws' =
ctyping1_idem_rhs f' s'' r'" and
T: "∀x. (f' x = [] ⟷ [y←zs @ ws'. fst y = x] = []) ∧
(f' x ≠ [] ⟶ last (f' x) = last [y←zs @ ws'. fst y = x])" and
U: "f' = (λx. [y←zs'. fst y = x])" and
V: "zs' ∈ ⊢ c⇩1 ⊔ ⊢ c⇩2" and
W: "s'' ∈ A"
using ctyping1_merge_idem_fst [OF A B C Q K] by auto
let ?f = "λx. [y←zs' @ xs'. fst y = x]"
let ?t = "λx. if [y←xs'. fst y = x] = [] then r' x else t' x"
show "ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1 ⊔ ⊢ c⇩2 @ ⊢ c⇩2)"
apply (rule exI [of _ ?f])
apply (rule exI [of _ s''])
apply (rule conjI)
apply (rule exI [of _ ?t])
apply (rule ext)
subgoal for x
proof (cases "[y←xs'. fst y = x]", cases "f' x = []")
case Nil
moreover case True
hence "s x = s'' x"
using T by (insert fun_cong [OF S, of x], simp)
moreover have "[y←ys'. fst y = x] = []"
using J and T and Nil and True by simp
moreover have "[y←zs. fst y = x] = []"
using T and True by simp
hence "[y←ys. fst y = x] = []"
using G and O and P by simp
moreover have "?f x = []"
using U and Nil and True by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s'' ?t x"
by simp
next
case Nil
moreover from this have
X: "[y←ys'. fst y = x] = [y←ws'. fst y = x]"
using J by simp
moreover case False
moreover have
"[y←zs. fst y = x] ≠ [] ∧ [y←ys. fst y = x] ≠ [] ∧
last [y←ys. fst y = x] = last [y←zs. fst y = x]"
(is "?P ∧ ?Q ∧ ?R") if
a: "[y←ys'. fst y = x] = []"
proof -
have ?P
using T and X and False and a by simp
moreover from this have ?Q
using G and O and P by simp
moreover have ?R
using G and O and P and `?P` by simp
ultimately show ?thesis
by simp
qed
moreover have "?f x ≠ []"
using U and False by simp
moreover have "last (?f x) = last (f' x)"
using U and Nil by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s'' ?t x"
by (insert fun_cong [OF S, of x], auto)
next
case Cons
moreover from this have "[y←ys'. fst y = x] ≠ []"
using J by simp
moreover have
"last [y←ys'. fst y = x] = last [y←xs'. fst y = x]"
using J and Cons by simp
ultimately show "ctyping1_idem_lhs s t t' ys ys' x =
ctyping1_idem_rhs ?f s'' ?t x"
by simp
qed
apply (rule conjI)
subgoal
proof -
show "∀x. (?f x = [] ⟷ [y←ys @ ys'. fst y = x] = []) ∧
(?f x ≠ [] ⟶ last (?f x) = last [y←ys @ ys'. fst y = x])"
(is "∀x. ?P x ∧ ?Q x")
proof
fix x
have "?P x"
proof
assume "[y←zs' @ xs'. fst y = x] = []"
moreover from this have "[y←zs @ ws'. fst y = x] = []"
using T and U by simp
moreover from this have "[y←ws @ xs. fst y = x] = []"
using O and P by simp
ultimately show "[y←ys @ ys'. fst y = x] = []"
using G and J by simp
next
assume "[y←ys @ ys'. fst y = x] = []"
hence "[y←ws @ xs @ ws' @ xs'. fst y = x] = []"
using G and J by simp
moreover from this have "[y←zs. fst y = x] = []"
using O and P by simp
ultimately show "[y←zs' @ xs'. fst y = x] = []"
using T and U by simp
qed
moreover have "?Q x"
proof (clarify, cases "[y←xs'. fst y = x]")
case Nil
moreover assume "?f x ≠ []"
ultimately have X: "f' x ≠ []"
using U by simp
hence Y: "last (?f x) = last [y←zs @ ws'. fst y = x]"
using T and U and Nil by simp
show "last (?f x) = last [y←ys @ ys'. fst y = x]"
proof (cases "[y←ws'. fst y = x] = []")
case True
moreover from this have "f x ≠ []"
using P and T and X by simp
ultimately have
"last (?f x) = last [y←ws @ xs. fst y = x]"
using O and P and Y by simp
thus ?thesis
using G and J and Nil and True by simp
next
case False
thus ?thesis
using J and Y and Nil by simp
qed
qed (simp add: J)
ultimately show "?P x ∧ ?Q x" ..
qed
qed
by (rule conjI, rule exI [of _ "zs' @ xs'"],
insert L V W, auto simp: ctyping1_append_def)
qed
done
lemma ctyping1_aux_idem_fst:
"⟦s ∈ A; ys ∈ ⊢ c; ys' ∈ ⊢ c⟧ ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c)"
proof (induction c arbitrary: ys ys')
fix c⇩1 c⇩2 ys ys'
show
"⟦⋀ys ys'. s ∈ A ⟹ ys ∈ ⊢ c⇩1 ⟹ ys' ∈ ⊢ c⇩1 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1);
⋀ys ys'. s ∈ A ⟹ ys ∈ ⊢ c⇩2 ⟹ ys' ∈ ⊢ c⇩2 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩2);
s ∈ A; ys ∈ ⊢ c⇩1;; c⇩2; ys' ∈ ⊢ c⇩1;; c⇩2⟧ ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1;; c⇩2)"
by (simp, rule ctyping1_merge_append_idem_fst [simplified])
next
fix c⇩1 c⇩2 ys ys'
show
"⟦⋀ys ys'. s ∈ A ⟹ ys ∈ ⊢ c⇩1 ⟹ ys' ∈ ⊢ c⇩1 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1);
⋀ys ys'. s ∈ A ⟹ ys ∈ ⊢ c⇩2 ⟹ ys' ∈ ⊢ c⇩2 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩2);
s ∈ A; ys ∈ ⊢ c⇩1 OR c⇩2; ys' ∈ ⊢ c⇩1 OR c⇩2⟧ ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1 OR c⇩2)"
by (simp, rule ctyping1_merge_idem_fst [simplified])
next
fix b c⇩1 c⇩2 ys ys'
assume
A: "⋀ys ys'. s ∈ A ⟹ ys ∈ ⊢ c⇩1 ⟹ ys' ∈ ⊢ c⇩1 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩1)" and
B: "⋀ys ys'. s ∈ A ⟹ ys ∈ ⊢ c⇩2 ⟹ ys' ∈ ⊢ c⇩2 ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c⇩2)" and
C: "s ∈ A" and
D: "ys ∈ ⊢ IF b THEN c⇩1 ELSE c⇩2" and
E: "ys' ∈ ⊢ IF b THEN c⇩1 ELSE c⇩2"
show "ctyping1_idem_pred s t t' ys ys' A (⊢ IF b THEN c⇩1 ELSE c⇩2)"
proof (cases "⊢ b")
case None
show ?thesis
by (insert A B C D E None, simp,
rule ctyping1_merge_idem_fst [simplified])
next
case (Some v)
show ?thesis
proof (cases v)
case True
thus ?thesis
by (insert A C D E Some, simp add: ctyping1_merge_empty_rhs)
next
case False
thus ?thesis
by (insert B C D E Some, simp add: ctyping1_merge_empty_lhs)
qed
qed
next
fix b c ys ys'
assume
A: "⋀ys ys'. s ∈ A ⟹ ys ∈ ⊢ c ⟹ ys' ∈ ⊢ c ⟹
ctyping1_idem_pred s t t' ys ys' A (⊢ c)" and
B: "s ∈ A" and
C: "ys ∈ ⊢ WHILE b DO c" and
D: "ys' ∈ ⊢ WHILE b DO c"
have E: "ctyping1_idem_pred s t t' ys ys' A (⊢ WHILE b DO c)" if
a: "ys ∈ ⊢ c" and
b: "ys' ∈ ⊢ c" and
c: "⊢ b ∈ {Some True, None}"
proof -
have "ctyping1_idem_pred s t t' ys ys' A (⊢ c)"
using A and B and a and b by simp
then obtain f and s' and t'' and ys'' where
E: "ctyping1_idem_lhs s t t' ys ys' =
ctyping1_idem_rhs f s' t''" and
F: "∀x. (f x = [] ⟷ [y←ys @ ys'. fst y = x] = []) ∧
(f x ≠ [] ⟶ last (f x) = last [y←ys @ ys'. fst y = x])" and
G: "f = (λx. [y←ys''. fst y = x])" and
H: "ys'' ∈ ⊢ c" and
I: "s' ∈ A"
by auto
show ?thesis
by (rule exI [of _ f], insert E F G H I c, force)
qed
show "ctyping1_idem_pred s t t' ys ys' A (⊢ WHILE b DO c)"
proof (cases "⊢ b")
case None
show ?thesis
proof (cases ys')
case Nil
show ?thesis
proof (cases "ys = []")
case True
thus ?thesis
by (insert B None Nil, force)
next
case False
thus ?thesis
by (insert B C None Nil, force)
qed
next
case Cons
show ?thesis
proof (cases "ys = []")
case True
show ?thesis
apply (insert B D None Cons True)
apply (rule exI [of _ "λx. [y←ys'. fst y = x]"])
apply (rule exI [of _ s])
apply (rule conjI)
apply fastforce
apply (rule conjI)
apply fastforce
apply (rule conjI)
apply (rule exI [of _ ys'])
by simp_all
next
case False
hence "ys ∈ ⊢ c ∧ ys' ∈ ⊢ c"
using C and D and None and Cons by simp
thus ?thesis
using None by (blast intro: E)
qed
qed
next
case (Some v)
show ?thesis
proof (cases v)
case True
hence "ys ∈ ⊢ c ∧ ys' ∈ ⊢ c"
using C and D and Some by simp
thus ?thesis
using Some and True by (fastforce intro: E)
next
case False
hence "ys = [] ∧ ys' = []"
using C and D and Some by simp
thus ?thesis
by (insert B Some False, simp)
qed
qed
qed fastforce+
lemma ctyping1_idem_fst_1:
"⟦s ∈ A; ys ∈ ⊢ c; ys' ∈ ⊢ c⟧ ⟹ ∃f s'.
(∃t''. ctyping1_idem_lhs s t t' ys ys' = ctyping1_idem_rhs f s' t'') ∧
(∃ys''. f = (λx. [y←ys''. fst y = x]) ∧ ys'' ∈ ⊢ c) ∧ s' ∈ A"
apply (drule ctyping1_aux_idem_fst [where ys' = ys'], assumption+)
apply clarify
apply (rule exI, (rule conjI)?)+
apply assumption
by blast
lemma ctyping1_idem_fst_2:
"⟦s ∈ A; ys ∈ ⊢ c⟧ ⟹ ∃f s'.
(∃t'.
(λx. if [y←ys. fst y = x] = []
then s x
else case snd (last [y←ys. fst y = x]) of None ⇒ t x | Some i ⇒ i) =
(λx. if f x = []
then s' x
else case snd (last (f x)) of None ⇒ t' x | Some i ⇒ i)) ∧
(∃ys'. f = (λx. [y←ys'. fst y = x]) ∧ ys' ∈ ⊢ c) ∧
(∃f' s''.
(∃t''. s' = (λx. if f' x = []
then s'' x
else case snd (last (f' x)) of None ⇒ t'' x | Some i ⇒ i)) ∧
(∃ys''. f' = (λx. [y←ys''. fst y = x]) ∧ ys'' ∈ ⊢ c) ∧ s'' ∈ A)"
(is "⟦_; _⟧ ⟹ ∃_ _. (∃_. ?f = _) ∧ _")
by (rule exI, rule exI [of _ ?f], fastforce)
lemma ctyping1_idem_fst:
"⊢ c (⊆ A, X) = (B, Y) ⟹ case ⊢ c (⊆ B, Y) of (B', Y') ⇒ B' = B"
by (auto intro: ctyping1_idem_fst_1 ctyping1_idem_fst_2 simp: ctyping1_def)
lemma ctyping1_idem_snd_1:
assumes
A: "A ≠ {}" and
B: "∀r f s.
(∀t. r ≠ (λx. if f x = [] then s x else case snd (last (f x)) of
None ⇒ t x | Some i ⇒ i)) ∨
(∀ys. f = (λx. [y←ys. fst y = x]) ⟶ ys ∉ ⊢ c) ∨ s ∉ A"
(is "∀r f s. (∀t. r ≠ ?r f s t) ∨ _")
shows "UNIV = S"
proof -
obtain s where C: "s ∈ A"
using A by blast
obtain ys where D: "ys ∈ ⊢ c"
by (insert ctyping1_aux_nonempty, blast)
let ?f = "λx. [y←ys. fst y = x]"
show ?thesis
using B [rule_format, of "?r ?f s (λx. 0)" ?f s] and C and D by auto
qed
lemma ctyping1_idem_snd_2:
"{x. ∀f.
(f x = [] ⟶ (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ⟶
(∀f.
(f x = [] ⟶ (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ⟶
x ∈ X) ∧
(f x ≠ [] ⟶ (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ⟶
(∃i. snd (last (f x)) = Some i)))) ∧
(f x ≠ [] ⟶ (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ⟶
(∃i. snd (last (f x)) = Some i))} =
{x. ∀f.
(f x = [] ⟶ (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ⟶
x ∈ X) ∧
(f x ≠ [] ⟶ (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ⟶
(∃i. snd (last (f x)) = Some i))}"
by (rule equalityI, force+)
lemma ctyping1_idem_snd:
"⊢ c (⊆ A, X) = (B, Y) ⟹ case ⊢ c (⊆ B, Y) of (B', Y') ⇒ Y' = Y"
by (clarsimp simp: ctyping1_def ctyping1_idem_snd_1 ctyping1_idem_snd_2)
lemma ctyping1_idem:
"⊢ c (⊆ A, X) = (B, Y) ⟹ ⊢ c (⊆ B, Y) = (B, Y)"
by (frule ctyping1_idem_fst, drule ctyping1_idem_snd, auto)
end
end