# Theory Abstract_Completeness.Abstract_Completeness

```(*<*)
(* An abstract completeness theorem *)
theory Abstract_Completeness
imports
Collections.Locale_Code
"HOL-Library.Countable_Set"
"HOL-Library.FSet"
"HOL-Library.Code_Target_Nat"
"HOL-Library.Linear_Temporal_Logic_on_Streams"
begin
(*>*)

section‹General Tree Concepts›

codatatype 'a tree = Node (root: 'a) (cont: "'a tree fset")

inductive tfinite where
tfinite: "(⋀ t'. t' |∈| cont t ⟹ tfinite t') ⟹ tfinite t"

(*<*)(* Infinite paths in trees. *)(*>*)
coinductive ipath where
ipath: "⟦root t = shd steps; t' |∈| cont t; ipath t' (stl steps)⟧ ⟹ ipath t steps"

(*<*)(* Finite trees have no infinite paths. *)
lemma ftree_no_ipath: "tfinite t ⟹ ¬ ipath t steps"
by (induct t arbitrary: steps rule: tfinite.induct) (auto elim: ipath.cases)
(*>*)

primcorec konig where
"shd (konig t) = root t"
| "stl (konig t) = konig (SOME t'. t' |∈| cont t ∧ ¬ tfinite t')"

lemma Konig: "¬ tfinite t ⟹ ipath t (konig t)"
by (coinduction arbitrary: t) (metis (lifting) tfinite.simps konig.simps someI_ex)

section‹Rule Systems›

(*<*)(* A step consists of a pair (s,r) such that the rule r is taken in state s. *)(*>*)
type_synonym ('state, 'rule) step = "'state × 'rule"
(*<*)(* A derivation tree is a tree of steps: *)(*>*)
type_synonym ('state, 'rule) dtree = "('state, 'rule) step tree"

locale RuleSystem_Defs =
fixes eff :: "'rule ⇒ 'state ⇒ 'state fset ⇒ bool"
(* The countable set of rules is initially provided as a stream: *)
and rules :: "'rule stream"
begin

abbreviation "R ≡ sset rules"

lemma countable_R: "countable R" by (metis countableI_type countable_image sset_range)
lemma NE_R: "R ≠ {}" by (metis UNIV_witness all_not_in_conv empty_is_image sset_range)

definition "enabled r s ≡ ∃ sl. eff r s sl"
definition "pickEff r s ≡ if enabled r s then (SOME sl. eff r s sl) else the None"

lemma pickEff: "enabled r s ⟹ eff r s (pickEff r s)"
by (metis enabled_def pickEff_def tfl_some)

abbreviation "effStep step ≡ eff (snd step) (fst step)"
abbreviation "enabledAtStep r step ≡ enabled r (fst step)"
abbreviation "takenAtStep r step ≡ snd step = r"

text ‹Saturation is a very strong notion of fairness:
If a rule is enabled at some point, it will eventually be taken.›
definition "saturated r ≡ alw (holds (enabledAtStep r) impl ev (holds (takenAtStep r)))"
definition "Saturated steps ≡ ∀ r ∈ R. saturated r steps"

(*<*)(* Well-formed derivation trees *)(*>*)
coinductive wf where
wf: "⟦snd (root t) ∈ R; effStep (root t) (fimage (fst o root) (cont t));
⋀t'. t' |∈| cont t ⟹ wf t'⟧ ⟹ wf t"

(*<*)(* Escape paths *)(*>*)
coinductive epath where
epath: "⟦snd (shd steps) ∈ R; fst (shd (stl steps)) |∈| sl; effStep (shd steps) sl;
epath (stl steps)⟧ ⟹ epath steps"

lemma wf_ipath_epath:
assumes "wf t" "ipath t steps"
shows "epath steps"
proof -
have *: "⋀t st. ipath t st ⟹ root t = shd st" by (auto elim: ipath.cases)
show ?thesis using assms
proof (coinduction arbitrary: t steps)
case epath
then show ?case by (cases rule: wf.cases[case_product ipath.cases]) (metis * o_apply fimageI)
qed
qed

definition "fair rs ≡ sset rs ⊆ R ∧ (∀ r ∈ R. alw (ev (holds ((=) r))) rs)"

lemma fair_stl: "fair rs ⟹ fair (stl rs)"
unfolding fair_def by (metis alw.simps subsetD stl_sset subsetI)

lemma sdrop_fair: "fair rs ⟹ fair (sdrop m rs)"
using alw_sdrop unfolding fair_def by (metis alw.coinduct alw_nxt fair_def fair_stl)

section‹A Fair Enumeration of the Rules›

(*<*)(* The fair enumeration of rules *)(*>*)
definition "fenum ≡ flat (smap (λn. stake n rules) (fromN 1))"

lemma sset_fenum: "sset fenum = R"
unfolding fenum_def by (subst sset_flat)
(auto simp: stream.set_map in_set_conv_nth sset_range[of rules],
metis atLeast_Suc_greaterThan greaterThan_0 lessI range_eqI stake_nth)

lemma fair_fenum: "fair fenum"
proof -
{ fix r assume "r ∈ R"
then obtain m where r: "r = rules !! m" unfolding sset_range by blast
{ fix n :: nat and rs let ?fenum = "λn. flat (smap (λn. stake n rules) (fromN n))"
assume "n > 0"
hence "alw (ev (holds ((=) r))) (rs @- ?fenum n)"
proof (coinduction arbitrary: n rs)
case alw
show ?case
proof (rule exI[of _ "rs @- ?fenum n"], safe)
show "∃n' rs'. stl (rs @- ?fenum n) = rs' @- ?fenum n' ∧ n' > 0"
proof(cases rs)
case Nil thus ?thesis unfolding alw by (intro exI) auto
qed (auto simp: alw intro: exI[of _ n])
next
show "ev (holds ((=) r)) (rs @- flat (smap (λn. stake n rules) (fromN n)))"
using alw r unfolding ev_holds_sset
by (cases "m < n") (force simp: stream.set_map in_set_conv_nth)+
qed
qed
}
}
thus "fair fenum" unfolding fair_def sset_fenum
by (metis fenum_def alw_shift le_less zero_less_one)
qed

definition "trim rs s = sdrop_while (λr. Not (enabled r s)) rs"

(*<*)(* The fair tree associated to a stream of rules and a state *)(*>*)
primcorec mkTree where
"root (mkTree rs s) = (s, (shd (trim rs s)))"
| "cont (mkTree rs s) = fimage (mkTree (stl (trim rs s))) (pickEff (shd (trim rs s)) s)"

(*<*)(* More efficient code equation for mkTree *)(*>*)
lemma mkTree_unfold[code]: "mkTree rs s =
(case trim rs s of SCons r s' ⇒ Node (s, r) (fimage (mkTree s') (pickEff r s)))"
by (subst mkTree.ctr) (simp split: stream.splits)

end

locale RuleSystem = RuleSystem_Defs eff rules
for eff :: "'rule ⇒ 'state ⇒ 'state fset ⇒ bool" and rules :: "'rule stream" +
fixes S :: "'state set"
assumes eff_S: "⋀ s r sl s'. ⟦s ∈ S; r ∈ R; eff r s sl; s' |∈| sl⟧ ⟹ s' ∈ S"
and enabled_R: "⋀ s. s ∈ S ⟹ ∃ r ∈ R. ∃ sl. eff r s sl"
begin

(*<*)(* The minimum waiting time in a stream for the enabled rules in a given state: *)(*>*)
definition "minWait rs s ≡ LEAST n. enabled (shd (sdrop n rs)) s"

lemma trim_alt:
assumes s: "s ∈ S" and rs: "fair rs"
shows "trim rs s = sdrop (minWait rs s) rs"
proof (unfold trim_def minWait_def sdrop_simps, rule sdrop_while_sdrop_LEAST[unfolded o_def])
from enabled_R[OF s] obtain r sl where r: "r ∈ R" and sl: "eff r s sl" by blast
from bspec[OF conjunct2[OF rs[unfolded fair_def]] r] obtain m where "r = rs !! m"
by atomize_elim (erule alw.cases, auto simp only: ev_holds_sset sset_range)
with r sl show "∃n. enabled (rs !! n) s" unfolding enabled_def by auto
qed

lemma minWait_ex:
assumes s: "s ∈ S" and rs: "fair rs"
shows "∃ n. enabled (shd (sdrop n rs)) s"
proof -
obtain r where r: "r ∈ R" and e: "enabled r s" using enabled_R s unfolding enabled_def by blast
then obtain n where "shd (sdrop n rs) = r" using sdrop_fair[OF rs]
by (metis (full_types) alw_nxt holds.simps sdrop.simps(1) fair_def sdrop_wait)
thus ?thesis using r e by auto
qed

lemma assumes "s ∈ S" and "fair rs"
shows trim_in_R: "shd (trim rs s) ∈ R"
and trim_enabled: "enabled (shd (trim rs s)) s"
and trim_fair: "fair (trim rs s)"
unfolding trim_alt[OF assms] minWait_def
using LeastI_ex[OF minWait_ex[OF assms]] sdrop_fair[OF assms(2)]
conjunct1[OF assms(2)[unfolded fair_def]] by simp_all (metis subsetD snth_sset)

lemma minWait_least: "⟦enabled (shd (sdrop n rs)) s⟧ ⟹ minWait rs s ≤ n"
unfolding minWait_def by (intro Least_le conjI)

lemma in_cont_mkTree:
assumes s: "s ∈ S" and rs: "fair rs" and t': "t' |∈| cont (mkTree rs s)"
shows "∃ sl' s'. s' ∈ S ∧ eff (shd (trim rs s)) s sl' ∧
s' |∈| sl' ∧ t' = mkTree (stl (trim rs s)) s'"
proof -
define sl' where "sl' = pickEff (shd (trim rs s)) s"
obtain s' where s': "s' |∈| sl'" and "t' = mkTree (stl (trim rs s)) s'"
using t' unfolding sl'_def by auto
moreover have 1: "enabled (shd (trim rs s)) s" using trim_enabled[OF s rs] .
moreover with trim_in_R pickEff eff_S s rs s'[unfolded sl'_def] have "s' ∈ S" by blast
ultimately show ?thesis unfolding sl'_def using pickEff by blast
qed

lemma ipath_mkTree_sdrop:
assumes s: "s ∈ S" and rs: "fair rs" and i: "ipath (mkTree rs s) steps"
shows "∃ n s'. s' ∈ S ∧ ipath (mkTree (sdrop n rs) s') (sdrop m steps)"
using s rs i proof (induct m arbitrary: steps rs)
case (Suc m)
then obtain n s' where s': "s' ∈ S"
and ip: "ipath (mkTree (sdrop n rs) s') (sdrop m steps)" (is "ipath ?t _") by blast
from ip obtain t' where r: "root ?t = shd (sdrop m steps)" and t': "t' |∈| cont ?t"
and i: "ipath t' (sdrop (Suc m) steps)" by (cases, simp)
from in_cont_mkTree[OF s' sdrop_fair[OF Suc.prems(2)] t'] obtain sl'' s'' where
e: "eff (shd (trim (sdrop n rs) s')) s' sl''" and
s'': "s'' |∈| sl''" and t'_def: "t' = mkTree (stl (trim (sdrop n rs) s')) s''" by blast
have "shd (trim (sdrop n rs) s') ∈ R" by (metis sdrop_fair Suc.prems(2) trim_in_R s')
thus ?case using i s'' e s' unfolding sdrop_stl t'_def sdrop_add add.commute[of n]
trim_alt[OF s' sdrop_fair[OF Suc.prems(2)]]
by (intro exI[of _ "minWait (sdrop n rs) s' + Suc n"] exI[of _ s'']) (simp add: eff_S)
qed (auto intro!: exI[of _ 0] exI[of _ s])

lemma wf_mkTree:
assumes s: "s ∈ S" and "fair rs"
shows "wf (mkTree rs s)"
using assms proof (coinduction arbitrary: rs s)
case (wf rs s) let ?t = "mkTree rs s"
have "snd (root ?t) ∈ R" using trim_in_R[OF wf] by simp
moreover have "fst ∘ root ∘ mkTree (stl (trim rs s)) = id" by auto
hence "effStep (root ?t) (fimage (fst ∘ root) (cont ?t))"
using trim_enabled[OF wf] by (simp add: pickEff)
ultimately show ?case using fair_stl[OF trim_fair[OF wf]] in_cont_mkTree[OF wf]
by (auto intro!: exI[of _ "stl (trim rs s)"])
qed

(*<*)(* The position of a rule in a rule stream *)(*>*)
definition "pos rs r ≡ LEAST n. shd (sdrop n rs) = r"

lemma pos: "⟦fair rs; r ∈ R⟧ ⟹ shd (sdrop (pos rs r) rs) = r"
unfolding pos_def
by (rule LeastI_ex) (metis (full_types) alw.cases fair_def holds.simps sdrop_wait)

lemma pos_least: "shd (sdrop n rs) = r ⟹ pos rs r ≤ n"
unfolding pos_def by (metis (full_types) Least_le)

lemma minWait_le_pos: "⟦fair rs; r ∈ R; enabled r s⟧ ⟹ minWait rs s ≤ pos rs r"
by (auto simp del: sdrop_simps intro: minWait_least simp: pos)

lemma stake_pos_minWait:
assumes rs: "fair rs" and m: "minWait rs s < pos rs r" and r: "r ∈ R" and s: "s ∈ S"
shows "pos (stl (trim rs s)) r = pos rs r - Suc (minWait rs s)"
proof -
have "pos rs r - Suc (minWait rs s) + minWait rs s = pos rs r - Suc 0" using m by auto
moreover have "shd (stl (sdrop (pos rs r - Suc 0) rs)) = shd (sdrop (pos rs r) rs)"
by (metis Suc_pred gr_implies_not0 m neq0_conv sdrop.simps(2) sdrop_stl)
ultimately have "pos (stl (trim rs s)) r ≤ pos rs r - Suc (minWait rs s)"
using pos[OF rs r] by (auto simp: add.commute trim_alt[OF s rs] intro: pos_least)
moreover
have "pos rs r ≤ pos (stl (trim rs s)) r + Suc (minWait rs s)"
using pos[OF sdrop_fair[OF fair_stl[OF rs]] r, of "minWait rs s"]
by (auto simp: trim_alt[OF s rs] add.commute intro: pos_least)
hence "pos rs r - Suc (minWait rs s) ≤ pos (stl (trim rs s)) r" by linarith
ultimately show ?thesis by simp
qed

lemma ipath_mkTree_ev:
assumes s: "s ∈ S" and rs: "fair rs"
and i: "ipath (mkTree rs s) steps" and r: "r ∈ R"
and alw: "alw (holds (enabledAtStep r)) steps"
shows "ev (holds (takenAtStep r)) steps"
using s rs i alw proof (induction "pos rs r" arbitrary: rs s steps rule: less_induct)
case (less rs s steps) note s = ‹s ∈ S› and trim_def' = trim_alt[OF s ‹fair rs›]
let ?t = "mkTree rs s"
from less(4,3) s in_cont_mkTree obtain t' :: "('state, 'rule) step tree" and s' where
rt: "root ?t = shd steps" and i: "ipath (mkTree (stl (trim rs s)) s') (stl steps)" and
s': "s' ∈ S" by cases fast
show ?case
proof(cases "pos rs r = minWait rs s")
case True
with pos[OF less.prems(2) r] rt[symmetric] show ?thesis by (auto simp: trim_def' ev.base)
next
case False
have e: "enabled r s" using less.prems(4) rt  by (subst (asm) alw_nxt, cases steps) auto
with False r less.prems(2) have 2: "minWait rs s < pos rs r" using minWait_le_pos by force
let ?m1 = "pos rs r - Suc (minWait rs s)"
have "Suc ?m1 ≤ pos rs r" using 2 by auto
moreover have "?m1 = pos (stl (trim rs s)) r" using e ‹fair rs› 2 r s
by (auto intro: stake_pos_minWait[symmetric])
moreover have "fair (stl (trim rs s))" "alw (holds (enabledAtStep r)) (stl steps)"
using less.prems by (metis fair_stl trim_fair, metis alw.simps)
ultimately show "?thesis" by (auto intro: ev.step[OF less.hyps[OF _ s' _ i]])
qed
qed

section‹Persistent rules›

definition
"per r ≡
∀s r1 sl' s'. s ∈ S ∧ enabled r s ∧ r1 ∈ R - {r} ∧ eff r1 s sl' ∧ s' |∈| sl' ⟶ enabled r s'"

lemma per_alw:
assumes p: "per r" and e: "epath steps ∧ fst (shd steps) ∈ S"
shows "alw (holds (enabledAtStep r) impl
(holds (takenAtStep r) or nxt (holds (enabledAtStep r)))) steps"
using e proof coinduct
case (alw steps)
moreover
{ let ?s = "fst (shd steps)"  let ?r1 = "snd (shd steps)"
let ?s' = "fst (shd (stl steps))"
assume "?s ∈ S" and "enabled r ?s" and "?r1 ≠ r"
moreover have "?r1 ∈ R" using alw by (auto elim: epath.cases)
moreover obtain sl' where "eff ?r1 ?s sl' ∧ ?s' |∈| sl'" using alw by (auto elim: epath.cases)
ultimately have "enabled r ?s'" using p unfolding per_def by blast
}
ultimately show ?case by (auto intro: eff_S elim: epath.cases)
qed

end ― ‹context RuleSystem›

(*<*) (* Rule-persistent rule system *) (*>*)
locale PersistentRuleSystem = RuleSystem eff rules S
for eff :: "'rule ⇒ 'state ⇒ 'state fset ⇒ bool" and rules :: "'rule stream" and S +
assumes per: "⋀ r. r ∈ R ⟹ per r"
begin

lemma ipath_mkTree_saturated:
assumes s: "s ∈ S" and rs: "fair rs"
and i: "ipath (mkTree rs s) steps" and r: "r ∈ R"
shows "saturated r steps"
unfolding saturated_def using s rs i proof (coinduction arbitrary: rs s steps)
case (alw rs s steps)
show ?case
proof (intro exI[of _ steps], safe)
assume "holds (enabledAtStep r) steps"
hence "alw (holds (enabledAtStep r)) steps ∨ ev (holds (takenAtStep r)) steps"
by (rule variance[OF _ per_alw[OF per[OF r]]])
(metis wf_ipath_epath wf_mkTree alw mkTree.simps(1) ipath.simps fst_conv)
thus "ev (holds (takenAtStep r)) steps" by (metis ipath_mkTree_ev[OF alw r])
next
from alw show "∃rs' s' steps'.
stl steps = steps' ∧ s' ∈ S ∧ fair rs' ∧ ipath (mkTree rs' s') steps'"
using ipath_mkTree_sdrop[where m=1, simplified] trim_in_R sdrop_fair by fast
qed
qed

theorem ipath_mkTree_Saturated:
assumes "s ∈ S" and "fair rs" and "ipath (mkTree rs s) steps"
shows "Saturated steps"
unfolding Saturated_def using ipath_mkTree_saturated[OF assms] by blast

theorem epath_completeness_Saturated:
assumes "s ∈ S"
shows
"(∃ t. fst (root t) = s ∧ wf t ∧ tfinite t) ∨
(∃ steps. fst (shd steps) = s ∧ epath steps ∧ Saturated steps)" (is "?A ∨ ?B")
proof -
{ assume "¬ ?A"
with assms have "¬ tfinite (mkTree fenum s)" using wf_mkTree fair_fenum by auto
then obtain steps where "ipath (mkTree fenum s) steps" using Konig by blast
with assms have "fst (shd steps) = s ∧ epath steps ∧ Saturated steps"
by (metis wf_ipath_epath ipath.simps ipath_mkTree_Saturated
wf_mkTree fair_fenum mkTree.simps(1) fst_conv)
hence ?B by blast
}
thus ?thesis by blast
qed

end ― ‹context PersistentRuleSystem›

section‹Code generation›

(* Here we assume a deterministic effect eff': *)

locale RuleSystem_Code =
fixes eff' :: "'rule ⇒ 'state ⇒ 'state fset option"
and rules :: "'rule stream" ― ‹countably many rules›
begin

definition "eff r s sl ≡ eff' r s = Some sl"

end (* context RuleSystem_Code *)

definition [code del]: "effG eff' r s sl ≡ RuleSystem_Code.eff eff' r s sl"

sublocale RuleSystem_Code < RuleSystem_Defs
where eff = "effG eff'" and rules = rules .

context RuleSystem_Code
begin

lemma enabled_eff': "enabled r s ⟷ eff' r s ≠ None"
unfolding enabled_def effG_def eff_def by auto

lemma pickEff_the[code]: "pickEff r s = the (eff' r s)"
unfolding pickEff_def enabled_def effG_def eff_def by auto

lemmas [code_unfold] = trim_def enabled_eff' pickEff_the

(*<*)
end (* context RuleSystem_Code *)
(*>*)

setup Locale_Code.open_block
interpretation i: RuleSystem_Code eff' rules for eff' and rules .
declare [[lc_delete "RuleSystem_Defs.mkTree (effG ?eff')"]]
declare [[lc_delete RuleSystem_Defs.trim]]
declare [[lc_delete RuleSystem_Defs.enabled]]
declare [[lc_delete RuleSystem_Defs.pickEff]]
declare [[lc_add "RuleSystem_Defs.mkTree (effG ?eff')" i.mkTree_unfold]]
setup Locale_Code.close_block

code_printing
constant the ⇀ (Haskell) "fromJust"
| constant Option.is_none ⇀ (Haskell) "isNothing"

export_code mkTree_effG_uu in Haskell module_name Tree (*file "."*)

(*<*)
end
(*>*)
```