# Theory Live_True

theory Live_True
imports While_Combinator Vars Big_Step

theory Live_True
imports  Vars Big_Step
begin

subsection

fun L ::  where
|
|
|
|

lemma L_mono:
proof-
have  for X Y
proof(induction c arbitrary: X Y)
case (While b c)
show ?case
proof(simp, rule lfp_mono)
fix Z show
using While by auto
qed
next
case If thus ?case by(auto simp: subset_iff)
qed auto
thus ?thesis by(rule monoI)
qed

lemma mono_union_L:

by (metis (no_types) L_mono mono_def order_eq_iff set_eq_subset sup_mono)

lemma L_While_unfold:

by(metis lfp_unfold[OF mono_union_L] L.simps(5))

lemma L_While_pfp:
using L_While_unfold by blast

lemma L_While_vars:
using L_While_unfold by blast

lemma L_While_X:
using L_While_unfold by blast

text
declare L.simps(5)[simp del]

subsection

theorem L_correct:

proof (induction arbitrary: X t rule: big_step_induct)
case Skip then show ?case by auto
next
case Assign then show ?case
by (auto simp: ball_Un)
next
case (Seq c1 s1 s2 c2 s3 X t1)
from Seq.IH(1) Seq.prems obtain t2 where
t12:  and s2t2:
by simp blast
from Seq.IH(2)[OF s2t2] obtain t3 where
t23:  and s3t3:
by auto
show ?case using t12 t23 s3t3 by auto
next
case (IfTrue b s c1 s' c2)
hence  and  by auto
from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have  by simp
from IfTrue.IH[OF ] obtain t' where
by auto
thus ?case using  by auto
next
case (IfFalse b s c2 s' c1)
hence   by auto
from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have  by simp
from IfFalse.IH[OF ] obtain t' where
by auto
thus ?case using  by auto
next
case (WhileFalse b s c)
hence
by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
thus ?case using WhileFalse.prems L_While_X[of X b c] by auto
next
case (WhileTrue b s1 c s2 s3 X t1)
let ?w =
from  WhileTrue.prems have
by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
have  using  L_While_pfp WhileTrue.prems
by (blast)
from WhileTrue.IH(1)[OF this] obtain t2 where
by auto
from WhileTrue.IH(2)[OF this(2)] obtain t3 where
by auto
with   show ?case by auto
qed

subsection

lemma L_subset_vars:
proof(induction c arbitrary: X)
case (While b c)
have
using While.IH[of ]
by (auto intro!: lfp_lowerbound)
thus ?case by (simp add: L.simps(5))
qed auto

text

lemma L_While: fixes b c X
assumes  defines
shows  (is )
proof -
let ?V =
have
proof(rule lfp_while[where C = ])
next
fix Y show
unfolding f_def using L_subset_vars[of c] by blast
next
show  using  by simp
qed
thus ?thesis by (simp add: f_def L.simps(5))
qed

lemma L_While_let:

lemma L_While_set:
by(rule L_While_let, simp)

text
lemmas [code] = L.simps(1-4) L_While_set
text

text
lemma
by eval

subsection

text

fun iter ::  where
|

text

fun Lb ::  where
|
|
|
|

text
lemma
by eval

lemma lfp_subset_iter:

proof(induction n arbitrary: A)
case 0 thus ?case by simp
next
case Suc thus ?case by simp (metis lfp_lowerbound)
qed

lemma
proof(induction c arbitrary: X)
case (While b c)
let ?f  =
let ?fb =
show ?case
proof (simp add: L.simps(5), rule lfp_subset_iter[OF mono_union_L])
show  using While.IH by blast
show
by (metis (full_types) L.simps(5) L_subset_vars rvars.simps(5))
qed
next
case Seq thus ?case by simp (metis (full_types) L_mono monoD subset_trans)
qed auto

end