# Theory DatRef

(*  Title:       Isabelle Collections Library
Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
section ‹\isaheader{Deprecated: Data Refinement for the While-Combinator}›
theory DatRef
imports
Main
"HOL-Library.While_Combinator"
begin
text_raw ‹\label{thy:DatRef}›

text ‹
Note that this theory is deprecated. For new developments, the refinement
framework (Refine-Monadic entry of the AFP) should be used.
›

text ‹
In this theory, a data refinement framework for
non-deterministic while-loops is developed. The refinement is based on
showing simulation w.r.t. an abstraction function.
The case of deterministic while-loops is explicitely handled, to
support proper code-generation using the While-Combinator.

Note that this theory is deprecated. For new developments, the refinement
framework (Refine-Monadic entry of the AFP) should be used.
›

(* TODO-LIST and ideas
- Model nondeterministic algorithms by their step relation, and show refinement stuff for this (more general) model (c.f. dpn-pre^* formalization)
Then, the nondeterministic while-loop would be a special case.

*)

text ‹
A nondeterministic while-algorithm is described by a set of states, a
continuation condition, a step relation, a set of possible initial
states and an invariant.
›

― ‹Encapsulates a while-algorithm and its invariant›
record 'S while_algo =
― ‹Termination condition›
wa_cond :: "'S set"
― ‹Step relation (nondeterministic)›
wa_step :: "('S × 'S) set"
― ‹Initial state (nondeterministic)›
wa_initial :: "'S set"
― ‹Invariant›
wa_invar :: "'S set"

text ‹
A while-algorithm is called {\em well-defined} iff the invariant holds for
all reachable states and the accessible part of the step-relation is
well-founded.
›
― ‹Conditions that must hold for a well-defined while-algorithm›
locale while_algo =
fixes WA :: "'S while_algo"

― ‹A step must preserve the invariant›
assumes step_invar:
"⟦ s∈wa_invar WA; s∈wa_cond WA; (s,s')∈wa_step WA ⟧ ⟹ s'∈wa_invar WA"
― ‹Initial states must satisfy the invariant›
assumes initial_invar: "wa_initial WA ⊆ wa_invar WA"
― ‹The accessible part of the step relation must be well-founded›
assumes step_wf:
"wf { (s',s). s∈wa_invar WA ∧ s∈wa_cond WA ∧ (s,s')∈wa_step WA }"

text ‹
Next, a refinement relation for while-algorithms is defined.
Note that the involved while-algorithms are not required to
be well-defined. Later, some lemmas to transfer well-definedness
along refinement relations are shown.

Refinement involves a concrete algorithm, an abstract algorithm and an
abstraction function. In essence, a refinement establishes a simulation
of the concrete algorithm by the abstract algorithm w.r.t. the abstraction
function.
›

locale wa_refine =
― ‹Concrete algorithm›
fixes WAC :: "'C while_algo"
― ‹Abstract algorithm›
fixes WAA :: "'A while_algo"

― ‹Abstraction function›
fixes α :: "'C ⇒ 'A"

― ‹Condition implemented correctly: The concrete condition must be stronger
than the abstract one. Intuitively, this ensures that the concrete loop
will not run longer than the abstract one that it is simulated by.›
assumes cond_abs: "⟦ s∈wa_invar WAC; s∈wa_cond WAC ⟧ ⟹ α s ∈ wa_cond WAA"

― ‹Step implemented correctly: The abstract step relation must simulate the
concrete step relation›
assumes step_abs: "⟦ s∈wa_invar WAC; s∈wa_cond WAC; (s,s')∈wa_step WAC ⟧
⟹ (α s, α s')∈wa_step WAA"
― ‹Initial states implemented correctly: The abstractions of the concrete
initial states must be abstract initial states.›
assumes initial_abs: "α  wa_initial WAC ⊆ wa_initial WAA"
― ‹Invariant implemented correctly: The concrete invariant must be stronger
then the abstract invariant.
Note that, usually, the concrete invariant will be of the
form @{term "I_add ∩ {s. α s ∈ wa_invar WAA}"}, where @{term I_add} are
assumes invar_abs: "α  wa_invar WAC ⊆ wa_invar WAA"
begin

lemma initial_abs': "s∈wa_initial WAC ⟹ α s ∈ wa_initial WAA"
using initial_abs by auto

lemma invar_abs': "s∈wa_invar WAC ⟹ α s ∈ wa_invar WAA"
using invar_abs by auto

end

― ‹Given a concrete while-algorithm and a well-defined abstract
while-algorithm, this lemma shows refinement and
well-definedness of the concrete while-algorithm.

Assuming well-definedness of the abstract algorithm and refinement,
some proof-obligations for well-definedness of the concrete algorithm can be
discharged automatically.

For this purpose, the invariant is split into a concrete and an abstract
part. The abstract part claims that the abstraction of a state satisfies
the abstract invariant. The concrete part makes some additional claims
about a valid concrete state. Then, after having shown refinement, the
assumptions that the abstract part of the invariant is preserved, can
be discharged automatically.›
lemma wa_refine_intro:
fixes condc :: "'C set" and
stepc :: "('C×'C) set" and
initialc :: "'C set" and
fixes WAA :: "'A while_algo"
fixes α :: "'C ⇒ 'A"
assumes "while_algo WAA"

― ‹The concrete step preserves the concrete part of the invariant›
assumes step_invarc:
"!!s s'. ⟦ s∈invar_addc; s∈condc; α s ∈ wa_invar WAA; (s,s')∈stepc ⟧
― ‹The concrete initial states satisfy the concrete part of the invariant›

― ‹Condition implemented correctly›
assumes cond_abs:
"!!s. ⟦ s∈invar_addc; α s ∈ wa_invar WAA; s∈condc ⟧ ⟹ α s ∈ wa_cond WAA"
― ‹Step implemented correctly›
assumes step_abs:
"!!s s'. ⟦ s∈invar_addc; s∈condc; α s ∈ wa_invar WAA; (s,s')∈stepc ⟧
⟹ (α s, α s')∈wa_step WAA"
― ‹Initial states implemented correctly›
assumes initial_abs: "α  initialc ⊆ wa_initial WAA"

― ‹Concrete while-algorithm: The invariant is separated into a concrete and
an abstract part›
defines "WAC == ⦇
wa_cond=condc,
wa_step=stepc,
wa_initial=initialc,
wa_invar=(invar_addc ∩ {s. α s∈ wa_invar WAA}) ⦈"

shows
"while_algo WAC ∧
wa_refine WAC WAA α" (is "?T1 ∧ ?T2")
proof
interpret waa: while_algo WAA by fact
show G1: "?T1"
apply (unfold_locales)
apply safe
apply (blast intro!: step_invarc)

apply (frule (3) step_abs)
apply (frule (2) cond_abs)
apply (erule (2) waa.step_invar)

apply (erule rev_subsetD[OF _ initial_invarc])

apply (insert initial_abs waa.initial_invar) [1]
apply blast

apply (rule_tac
r="inv_image { (s',s). s∈wa_invar WAA
∧ s∈wa_cond WAA
∧ (s,s')∈wa_step WAA } α"
in wf_subset)
apply (auto simp add: cond_abs step_abs) [1]
done
show ?T2
apply (unfold_locales)
apply (auto simp add: cond_abs step_abs initial_abs WAC_def)
done
qed

― ‹After refinement has been shown, this lemma transfers
the well-definedness property up the refinement chain.
Like in @{thm [source] wa_refine_intro}, some proof-obligations can
be discharged by assuming refinement and well-definedness of the
abstract algorithm.›
lemma (in wa_refine) wa_intro:
― ‹Concrete part of the invariant›
― ‹The abstract algorithm is well-defined›
assumes "while_algo WAA"
― ‹The invariant can be split into concrete and abstract part›
assumes icf: "wa_invar WAC = addi ∩ {s. α s ∈ wa_invar WAA}"

― ‹The step-relation preserves the concrete part of the invariant›
"!!s s'. ⟦ s∈addi; s∈wa_cond WAC; α s ∈ wa_invar WAA;
(s,s')∈wa_step WAC

― ‹The initial states satisfy the concrete part of the invariant›

shows
"while_algo WAC"
proof -
interpret waa: while_algo WAA by fact
show ?thesis
apply (unfold_locales)
apply (subst icf)
apply safe
apply (simp only: icf)
apply safe

apply (frule (2) step_abs)
apply (frule (1) cond_abs)
apply (simp only: icf)
apply clarify
apply (erule (2) waa.step_invar)

apply (rule conjI)
apply (insert initial_abs waa.initial_invar) [1]
apply blast

apply (rule_tac
r="inv_image { (s',s). s∈wa_invar WAA
∧ s∈wa_cond WAA
∧ (s,s')∈wa_step WAA } α"
in wf_subset)
apply (auto simp add: cond_abs step_abs icf) [1]
done
qed

text ‹
A special case of refinement occurs, if the concrete condition implements the
abstract condition precisely. In this case, the concrete algorithm will run
as long as the abstract one that it is simulated by. This allows to
transfer properties of the result from the abstract algorithm to the
concrete one.
›

― ‹Precise refinement›
locale wa_precise_refine = wa_refine +
constrains α :: "'C ⇒ 'A"
assumes cond_precise:
"∀s. s∈wa_invar WAC ∧ α s∈wa_cond WAA ⟶ s∈wa_cond WAC"
begin
― ‹Transfer correctness property›
lemma transfer_correctness:
assumes A: "∀s. s∈wa_invar WAA ∧ s∉wa_cond WAA ⟶ P s"
shows "∀sc. sc∈wa_invar WAC ∧ sc∉wa_cond WAC ⟶ P (α sc)"
using A cond_abs invar_abs cond_precise by blast
end

text ‹Refinement as well as precise refinement is reflexive and transitive›

lemma wa_ref_refl: "wa_refine WA WA id"
by (unfold_locales) auto

lemma wa_pref_refl: "wa_precise_refine WA WA id"
by (unfold_locales) auto

lemma wa_ref_trans:
assumes "wa_refine WC WB α1"
assumes "wa_refine WB WA α2"
shows "wa_refine WC WA (α2∘α1)"
proof -
interpret r1: wa_refine WC WB α1 by fact
interpret r2: wa_refine WB WA α2 by fact

show ?thesis (* Cool, everything by auto! *)
apply unfold_locales
r1.invar_abs' r2.invar_abs'
r1.cond_abs r2.cond_abs
r1.step_abs r2.step_abs
r1.initial_abs' r2.initial_abs')
done
qed

lemma wa_pref_trans:
assumes "wa_precise_refine WC WB α1"
assumes "wa_precise_refine WB WA α2"
shows "wa_precise_refine WC WA (α2∘α1)"
proof -
interpret r1: wa_precise_refine WC WB α1 by fact
interpret r2: wa_precise_refine WB WA α2 by fact

show ?thesis
apply intro_locales
apply (rule wa_ref_trans)
apply (unfold_locales)
apply (auto simp add: r1.invar_abs' r2.invar_abs'
r1.cond_precise r2.cond_precise)
done
qed

text ‹
A well-defined while-algorithm is {\em deterministic}, iff
the step relation is a function and there is just one
initial state. Such an algorithm is suitable for direct implementation
by the while-combinator.

For deterministic while-algorithm, an own record is defined, as well as a
function that maps it to the corresponding record for non-deterministic
while algorithms. This makes sense as the step-relation may then be modeled
as a function, and the initial state may be modeled as a single state rather
than a (singleton) set of states.
›

record 'S det_while_algo =
― ‹Termination condition›
dwa_cond :: "'S ⇒ bool"
― ‹Step function›
dwa_step :: "'S ⇒ 'S"
― ‹Initial state›
dwa_initial :: "'S"
― ‹Invariant›
dwa_invar :: "'S set"

― ‹Maps the record for deterministic while-algo to the corresponding record for
the non-deterministic one›
definition "det_wa_wa DWA == ⦇
wa_cond={s. dwa_cond DWA s},
wa_step={(s,dwa_step DWA s) | s. True},
wa_initial={dwa_initial DWA},
wa_invar = dwa_invar DWA⦈"

― ‹Conditions for a deterministic while-algorithm›
locale det_while_algo =
fixes WA :: "'S det_while_algo"
― ‹The step preserves the invariant›
assumes step_invar:
"⟦ s∈dwa_invar WA; dwa_cond WA s ⟧ ⟹ dwa_step WA s ∈ dwa_invar WA"
― ‹The initial state satisfies the invariant›
assumes initial_invar: "dwa_initial WA ∈ dwa_invar WA"
― ‹The relation made up by the step-function is well-founded.›
assumes step_wf:
"wf { (dwa_step WA s,s) | s. s∈dwa_invar WA ∧ dwa_cond WA s }"

begin
lemma is_while_algo: "while_algo (det_wa_wa WA)"
apply (unfold_locales)
apply (auto simp add: det_wa_wa_def step_invar initial_invar)
apply (insert step_wf)
apply (erule_tac P=wf in back_subst)
apply auto
done

end

lemma det_while_algo_intro:
assumes "while_algo (det_wa_wa DWA)"
shows "det_while_algo DWA"
proof -
interpret while_algo "(det_wa_wa DWA)" by fact

show ?thesis using step_invar initial_invar step_wf
apply (unfold_locales)
apply (unfold det_wa_wa_def)
apply auto
apply (erule_tac P=wf in back_subst)
apply auto
done

qed

― ‹A deterministic while-algorithm is well-defined, if and only if the
corresponding non-deterministic while-algorithm is well-defined›
theorem dwa_is_wa:
"while_algo (det_wa_wa DWA) ⟷ det_while_algo DWA"
using det_while_algo_intro det_while_algo.is_while_algo by auto

definition (in det_while_algo)
"loop == (while (dwa_cond WA) (dwa_step WA) (dwa_initial WA))"

― ‹Proof rule for deterministic while loops›
lemma (in det_while_algo) while_proof:
assumes inv_imp: "⋀s. ⟦s∈dwa_invar WA; ¬ dwa_cond WA s⟧ ⟹ Q s"
shows "Q loop"
apply (unfold loop_def)
apply (rule_tac P="λx. x∈dwa_invar WA" and
r="{ (dwa_step WA s,s) | s. s∈dwa_invar WA ∧ dwa_cond WA s }"
in while_rule)
apply (simp_all add: step_invar initial_invar step_wf inv_imp)
done

― ‹This version is useful when using transferred correctness lemmas›
lemma (in det_while_algo) while_proof':
assumes inv_imp:
"∀s. s∈wa_invar (det_wa_wa WA) ∧ s∉wa_cond (det_wa_wa WA) ⟶ Q s"
shows "Q loop"
using inv_imp
`