# Theory While_Combinator

theory While_Combinator
imports Main

section

theory While_Combinator
imports Main
begin

subsection

definition while_option ::  where

theorem while_option_unfold[code]:

proof cases
assume
show ?thesis
proof (cases )
case True
then obtain k where 1:  ..
with  obtain l where  by (cases k) auto
with 1 have  by (auto simp: funpow_swap1)
then have 2:  ..
from 1
have
by (rule Least_Suc) (simp add: )
also have
finally
show ?thesis
using True 2  by (simp add: funpow_swap1 while_option_def)
next
case False
then have  by blast
then have
with False   show ?thesis by (simp add: while_option_def)
qed
next
assume [simp]:
have least:
by (rule Least_equality) auto
moreover
have  by (rule exI[of _ ]) auto
ultimately show ?thesis unfolding while_option_def by auto
qed

lemma while_option_stop2:

by (metis (lifting) LeastI_ex)

lemma while_option_stop:
by(metis while_option_stop2)

theorem while_option_rule:
assumes step:
and result:
and init:
shows
proof -
define k where
from assms have t:
by (simp add: while_option_def k_def split: if_splits)
have 1:
by (auto simp: k_def dest: not_less_Least)

{ fix i assume  then have
by (induct i) (auto simp: init step 1) }
thus  by (auto simp: t)
qed

lemma funpow_commute:

by (induct k arbitrary: s) auto

lemma while_option_commute_invariant:
assumes Invariant:
assumes TestCommute:
assumes BodyCommute:
assumes Initial:
shows
unfolding while_option_def
proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
fix k
assume
with Initial show
proof (induction k arbitrary: s)
case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
next
case (Suc k) thus ?case
proof (cases )
assume
with Suc.IH[of ] Suc.prems show ?thesis
by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
next
assume
with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
qed
qed
next
fix k
assume
with Initial show
proof (induction k arbitrary: s)
case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
next
case (Suc k) thus ?case
proof (cases )
assume
with Suc.IH[of ] Suc.prems show ?thesis
by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
next
assume
with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
qed
qed
next
fix k
assume k:
have *:
(is )
proof (cases ?k')
case 0
have
unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
hence  by (auto simp: TestCommute Initial)
hence  by (intro Least_equality) auto
with 0 show ?thesis by auto
next
case (Suc k')
have
unfolding Suc[symmetric] by (rule LeastI) (rule k)
moreover
{ fix k assume
hence  unfolding Suc by simp
hence  by (rule iffD1[OF not_not, OF not_less_Least])
}
note b' = this
{ fix k assume
hence
and
and
by (induct k) (auto simp: b' assms)
with
have
and
and
by (auto simp: b')
}
note b = this(1) and body = this(2) and inv = this(3)
hence k':  by auto
ultimately show ?thesis unfolding Suc using b
proof (intro Least_equality[symmetric], goal_cases)
case 1
hence Test:
by (auto simp: BodyCommute inv b)
have  by (auto simp: Invariant inv b)
with Test show ?case by (auto simp: TestCommute)
next
case 2
thus ?case by (metis not_less_eq_eq)
qed
qed
have  unfolding *
proof (rule funpow_commute, clarify)
fix k assume
hence TestTrue:  by (auto dest: not_less_Least)
from  have
proof (induct k)
case 0 thus ?case by (auto simp: assms)
next
case (Suc h)
hence  by auto
with Suc show ?case
by (auto, metis (lifting, no_types) Invariant Suc_lessD not_less_Least)
qed
with TestTrue show
by (metis BodyCommute)
qed
thus  by blast
qed

lemma while_option_commute:
assumes
shows
by(rule while_option_commute_invariant[where P = ])

subsection

definition while ::
where

lemma while_unfold [code]:

unfolding while_def by (subst while_option_unfold) simp

lemma def_while_unfold:
assumes fdef:
shows
unfolding fdef by (fact while_unfold)

text

theorem while_rule_lemma:
assumes invariant:
and terminate:
and wf:
shows
using wf
apply (induct s)
apply simp
apply (subst while_unfold)
done

theorem while_rule:

apply (rule while_rule_lemma)
prefer 4 apply assumption
apply blast
apply blast
apply (erule wf_subset)
apply blast
done

text

theorem wf_while_option_Some:
assumes
and  and
shows
using assms(1,3)
proof (induction s)
case less thus ?case using assms(2)
by (subst while_option_unfold) simp
qed

lemma wf_rel_while_option_Some:
assumes wf:
assumes smaller:
assumes inv:
assumes init:
shows
proof -
from smaller have  by auto
with wf have  by (auto simp: wf_subset)
with inv init show ?thesis by (auto simp: wf_while_option_Some)
qed

theorem measure_while_option_Some: fixes f ::
shows
by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])

text

lemma while_option_finite_subset_Some: fixes C ::
assumes  and  and
shows
proof(rule measure_while_option_Some[where
f=  and P=  and s= ])
fix A assume A:
show
(is )
proof
show ?L by(metis A(1) assms(2) monoD[OF ])
show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
qed
qed simp

lemma lfp_the_while_option:
assumes  and  and
shows
proof-
obtain P where
using while_option_finite_subset_Some[OF assms] by blast
with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
show ?thesis by auto
qed

lemma lfp_while:
assumes  and  and
shows
unfolding while_def using assms by (rule lfp_the_while_option) blast

lemma wf_finite_less:
assumes
shows
by (rule wf_measure[where f=, THEN wf_subset])
(fastforce simp: less_eq assms intro: psubset_card_mono)

lemma wf_finite_greater:
assumes
shows
by (rule wf_measure[where f=, THEN wf_subset])
(fastforce simp: less_eq assms intro: psubset_card_mono)

lemma while_option_finite_increasing_Some:
fixes f ::
assumes  and  and
shows
by (rule wf_rel_while_option_Some[where R= and P= and s=])
(auto simp: assms monoD intro: wf_finite_greater[where C=, simplified])

lemma lfp_the_while_option_lattice:
fixes f ::
assumes  and
shows
proof -
obtain P where
using while_option_finite_increasing_Some[OF assms, where s=bot] by simp blast
with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
show ?thesis by auto
qed

lemma lfp_while_lattice:
fixes f ::
assumes  and
shows
unfolding while_def using assms by (rule lfp_the_while_option_lattice)

lemma while_option_finite_decreasing_Some:
fixes f ::
assumes  and  and
shows
by (rule wf_rel_while_option_Some[where R= and P= and s=])
(auto simp add: assms monoD intro: wf_finite_less[where C=, simplified])

lemma gfp_the_while_option_lattice:
fixes f ::
assumes  and
shows
proof -
obtain P where
using while_option_finite_decreasing_Some[OF assms, where s=top] by simp blast
with while_option_stop2[OF this] gfp_Kleene_iter[OF assms(1)]
show ?thesis by auto
qed

lemma gfp_while_lattice:
fixes f ::
assumes  and
shows
unfolding while_def using assms by (rule gfp_the_while_option_lattice)

text

context
fixes p ::
and f ::
and x :: 'a
begin

qualified fun rtrancl_while_test ::
where

qualified fun rtrancl_while_step ::
where

definition rtrancl_while ::
where

qualified fun rtrancl_while_invariant ::
where

qualified lemma rtrancl_while_invariant:
assumes inv:  and test:
shows
proof (cases st)
fix ws Z assume st:
with test obtain h t where   by (cases ws) auto
with inv st show ?thesis by (auto intro: rtrancl.rtrancl_into_rtrancl)
qed

lemma rtrancl_while_Some: assumes
shows
proof -
have  by simp
with rtrancl_while_invariant have I:
by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
{ assume
hence ?thesis using I
by (auto simp del:Image_Collect_case_prod dest: Image_closed_trancl)
} moreover
{ assume
hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
}
ultimately show ?thesis by simp
qed

lemma rtrancl_while_finite_Some:
assumes  (is )
shows
proof -
let ?R =
have  by (blast intro: wf_mlex)
then show ?thesis unfolding rtrancl_while_def
proof (rule wf_rel_while_option_Some[of ?R rtrancl_while_invariant])
fix st assume *:
hence I:
by (blast intro: rtrancl_while_invariant)
show
proof (cases st)
fix ws Z let ?ws =  and ?Z =
assume st:
with * obtain h t where ws:   by (cases ws) auto
{ assume
then obtain z where  by fastforce
with st ws I have    by auto
with assms have  by (blast intro: psubset_card_mono)
with st ws have ?thesis unfolding mlex_prod_def by simp
}
moreover
{ assume
with st ws have    by (auto simp: filter_empty_conv)
with st ws have ?thesis unfolding mlex_prod_def by simp
}
ultimately show ?thesis by blast
qed