Quelle Collecting.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

subsection "Collecting Semantics of Commands"

theory Collecting
imports Complete_Lattice Big_Step ACom
begin

subsubsection "The generic Step function"

notation
  sup (infixl \<open>\<squnion>\<close> 65) and
  inf (infixl \<open>\<sqinter>\<close> 70) and
  bot (\<open>\<bottom>\<close>) and
  top (\<open>\<top>\<close>)

context
  fixes f :: "vname \ aexp \ 'a \ 'a::sup"
  fixes g :: "bexp \ 'a \ 'a"
begin
fun Step :: "'a \ 'a acom \ 'a acom" where
"Step S (SKIP {Q}) = (SKIP {S})" |
"Step S (x ::= e {Q}) =
  x ::= e {f x e S}" |
"Step S (C1;; C2) = Step S C1;; Step (post C1) C2" |
"Step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
  IF b THEN {g b S} Step P1 C1 ELSE {g (Not b) S} Step P2 C2
  {post C1 \<squnion> post C2}" |
"Step S ({I} WHILE b DO {P} C {Q}) =
  {S \<squnion> post C} WHILE b DO {g b I} Step P C {g (Not b) I}"
end

lemma strip_Step[simp]: "strip(Step f g S C) = strip C"
by(induct C arbitrary: S) auto

subsubsection "Annotated commands as a complete lattice"

instantiation acom :: (order) order
begin

definition less_eq_acom :: "('a::order)acom \ 'a acom \ bool" where
"C1 \ C2 \ strip C1 = strip C2 \ (\p anno C2 p)"

definition less_acom :: "'a acom \ 'a acom \ bool" where
"less_acom x y = (x \ y \ \ y \ x)"

instance
proof (standard, goal_cases)
  case 1 show ?case by(simp add: less_acom_def)
next
  case 2 thus ?case by(auto simp: less_eq_acom_def)
next
  case 3 thus ?case by(fastforce simp: less_eq_acom_def size_annos)
next
  case 4 thus ?case
    by(fastforce simp: le_antisym less_eq_acom_def size_annos
         eq_acom_iff_strip_anno)
qed

end

lemma less_eq_acom_annos:
  "C1 \ C2 \ strip C1 = strip C2 \ list_all2 (\) (annos C1) (annos C2)"
by(auto simp add: less_eq_acom_def anno_def list_all2_conv_all_nth size_annos_same2)

lemma SKIP_le[simp]: "SKIP {S} \ c \ (\S'. c = SKIP {S'} \ S \ S')"
by (cases c) (auto simp:less_eq_acom_def anno_def)

lemma Assign_le[simp]: "x ::= e {S} \ c \ (\S'. c = x ::= e {S'} \ S \ S')"
by (cases c) (auto simp:less_eq_acom_def anno_def)

lemma Seq_le[simp]: "C1;;C2 \ C \ (\C1' C2'. C = C1';;C2' \ C1 \ C1' \ C2 \ C2')"
apply (cases C)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done

lemma If_le[simp]: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \ C \
  (\<exists>p1' p2' C1' C2' S'. C = IF b THEN {p1'} C1' ELSE {p2'} C2' {S'} \<and>
     p1 \<le> p1' \<and> p2 \<le> p2' \<and> C1 \<le> C1' \<and> C2 \<le> C2' \<and> S \<le> S')"
apply (cases C)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done

lemma While_le[simp]: "{I} WHILE b DO {p} C {P} \ W \
  (\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> C \<le> C' \<and> p \<le> p' \<and> I \<le> I' \<and> P \<le> P')"
apply (cases W)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done

lemma mono_post: "C \ C' \ post C \ post C'"
using annos_ne[of C']
by(auto simp: post_def less_eq_acom_def last_conv_nth[OF annos_ne] anno_def
     dest: size_annos_same)

definition Inf_acom :: "com \ 'a::complete_lattice acom set \ 'a acom" where
"Inf_acom c M = annotate (\p. INF C\M. anno C p) c"

global_interpretation
  Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
proof (standard, goal_cases)
  case 1 thus ?case
    by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_lower)
next
  case 2 thus ?case
    by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_greatest)
next
  case 3 thus ?case by(auto simp: Inf_acom_def)
qed

subsubsection "Collecting semantics"

definition "step = Step (\x e S. {s(x := aval e s) |s. s \ S}) (\b S. {s:S. bval b s})"

definition CS :: "com \ state set acom" where
"CS c = lfp c (step UNIV)"

lemma mono2_Step: fixes C1 C2 :: "'a::semilattice_sup acom"
  assumes "!!x e S1 S2. S1 \ S2 \ f x e S1 \ f x e S2"
          "!!b S1 S2. S1 \ S2 \ g b S1 \ g b S2"
  shows "C1 \ C2 \ S1 \ S2 \ Step f g S1 C1 \ Step f g S2 C2"
proof(induction S1 C1 arbitrary: C2 S2 rule: Step.induct)
  case 1 thus ?case by(auto)
next
  case 2 thus ?case by (auto simp: assms(1))
next
  case 3 thus ?case by(auto simp: mono_post)
next
  case 4 thus ?case
    by(auto simp: subset_iff assms(2))
      (metis mono_post le_supI1 le_supI2)+
next
  case 5 thus ?case
    by(auto simp: subset_iff assms(2))
      (metis mono_post le_supI1 le_supI2)+
qed

lemma mono2_step: "C1 \ C2 \ S1 \ S2 \ step S1 C1 \ step S2 C2"
unfolding step_def by(rule mono2_Step) auto

lemma mono_step: "mono (step S)"
by(blast intro: monoI mono2_step)

lemma strip_step: "strip(step S C) = strip C"
by (induction C arbitrary: S) (auto simp: step_def)

lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
apply(rule lfp_unfold[OF _  mono_step])
apply(simp add: strip_step)
done

lemma CS_unfold: "CS c = step UNIV (CS c)"
by (metis CS_def lfp_cs_unfold)

lemma strip_CS[simp]: "strip(CS c) = c"
by(simp add: CS_def index_lfp[simplified])

subsubsection "Relation to big-step semantics"

lemma asize_nz: "asize(c::com) \ 0"
by (metis length_0_conv length_annos_annotate annos_ne)

lemma post_Inf_acom:
  "\C\M. strip C = c \ post (Inf_acom c M) = \(post ` M)"
apply(subgoal_tac "\C\M. size(annos C) = asize c")
apply(simp add: post_anno_asize Inf_acom_def asize_nz neq0_conv[symmetric])
apply(simp add: size_annos)
done

lemma post_lfp: "post(lfp c f) = (\{post C|C. strip C = c \ f C \ C})"
by(auto simp add: lfp_def post_Inf_acom)

lemma big_step_post_step:
  "\ (c, s) \ t; strip C = c; s \ S; step S C \ C \ \ t \ post C"
proof(induction arbitrary: C S rule: big_step_induct)
  case Skip thus ?case by(auto simp: strip_eq_SKIP step_def post_def)
next
  case Assign thus ?case
    by(fastforce simp: strip_eq_Assign step_def post_def)
next
  case Seq thus ?case
    by(fastforce simp: strip_eq_Seq step_def post_def last_append annos_ne)
next
  case IfTrue thus ?case apply(auto simp: strip_eq_If step_def post_def)
    by (metis (lifting,full_types) mem_Collect_eq subsetD)
next
  case IfFalse thus ?case apply(auto simp: strip_eq_If step_def post_def)
    by (metis (lifting,full_types) mem_Collect_eq subsetD)
next
  case (WhileTrue b s1 c' s2 s3)
  from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
    by(auto simp: strip_eq_While)
  from WhileTrue.prems(3) \<open>C = _\<close>
  have "step P C' \ C'" "{s \ I. bval b s} \ P" "S \ I" "step (post C') C \ C"
    by (auto simp: step_def post_def)
  have "step {s \ I. bval b s} C' \ C'"
    by (rule order_trans[OF mono2_step[OF order_refl \<open>{s \<in> I. bval b s} \<le> P\<close>] \<open>step P C' \<le> C'\<close>])
  have "s1 \ {s\I. bval b s}" using \s1 \ S\ \S \ I\ \bval b s1\ by auto
  note s2_in_post_C' = WhileTrue.IH(1)[OF \strip C' = c'\ this \step {s \ I. bval b s} C' \ C'\]
  from WhileTrue.IH(2)[OF WhileTrue.prems(1) s2_in_post_C' \step (post C') C \ C\]
  show ?case .
next
  case (WhileFalse b s1 c') thus ?case
    by (force simp: strip_eq_While step_def post_def)
qed

lemma big_step_lfp: "\ (c,s) \ t; s \ S \ \ t \ post(lfp c (step S))"
by(auto simp add: post_lfp intro: big_step_post_step)

lemma big_step_CS: "(c,s) \ t \ t \ post(CS c)"
by(simp add: CS_def big_step_lfp)

end

quality100%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.