Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Misc.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/IMPP/Misc.thy
    Author:     David von Oheimb, TUM
*)

section \<open>Several examples for Hoare logic\<close>

theory Misc
imports Hoare
begin

overloading
  newlocs \<equiv> newlocs
  setlocs \<equiv> setlocs
  getlocs \<equiv> getlocs
  update \<equiv> update
begin

definition newlocs :: locals
  where "newlocs == %x. undefined"

definition setlocs :: "state => locals => state"
  where "setlocs s l' == case s of st g l => st g l'"

definition getlocs :: "state => locals"
  where "getlocs s == case s of st g l => l"

definition update  :: "state => vname => val => state"
  where "update s vn v ==
    case vn of
      Glb gn => (case s of st g l => st (g(gn:=v)) l)
    | Loc ln => (case s of st g l => st g (l(ln:=v)))"

end

subsection "state access"

lemma getlocs_def2: "getlocs (st g l) = l"
apply (unfold getlocs_def)
apply simp
done

lemma update_Loc_idem2 [simp]: "s[Loc Y::=s] = s"
apply (unfold update_def)
apply (induct_tac s)
apply (simp add: getlocs_def2)
done

lemma update_overwrt [simp]: "s[X::=x][X::=y] = s[X::=y]"
apply (unfold update_def)
apply (induct_tac X)
apply  auto
apply  (induct_tac [!] s)
apply  auto
done

lemma getlocs_Loc_update [simp]: "(s[Loc Y::=k]) = (if Y=Y' then k else s)"
apply (unfold update_def)
apply (induct_tac s)
apply (simp add: getlocs_def2)
done

lemma getlocs_Glb_update [simp]: "getlocs (s[Glb Y::=k]) = getlocs s"
apply (unfold update_def)
apply (induct_tac s)
apply (simp add: getlocs_def2)
done

lemma getlocs_setlocs [simp]: "getlocs (setlocs s l) = l"
apply (unfold setlocs_def)
apply (induct_tac s)
apply auto
apply (simp add: getlocs_def2)
done

lemma getlocs_setlocs_lemma: "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])"
apply (induct_tac Y)
apply (rule_tac [2] ext)
apply auto
done

(*unused*)
lemma classic_Local_valid:
"\v. G|={%Z s. P Z (s[Loc Y::=v]) & s = a (s[Loc Y::=v])}.
  c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}"
apply (unfold hoare_valids_def)
apply (simp (no_asm_use) add: triple_valid_def2)
apply clarsimp
apply (drule_tac x = "s" in spec)
apply (tactic "smp_tac \<^context> 1 1")
apply (drule spec)
apply (drule_tac x = "s[Loc Y::=a s]" in spec)
apply (simp (no_asm_use))
apply (erule (1) notE impE)
apply (tactic "smp_tac \<^context> 1 1")
apply simp
done

lemma classic_Local: "\v. G|-{%Z s. P Z (s[Loc Y::=v]) & s = a (s[Loc Y::=v])}.
  c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}"
apply (rule export_s)
apply (rule hoare_derivs.Local [THEN conseq1])
apply (erule spec)
apply force
done

lemma classic_Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s = d} |] ==>
  G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
apply (rule classic_Local)
apply clarsimp
apply (erule conseq12)
apply clarsimp
apply (drule sym)
apply simp
done

lemma Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s = d} |] ==>
  G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
apply (rule export_s)
apply (rule hoare_derivs.Local)
apply clarsimp
done

lemma weak_Local_indep: "[| Y'~=Y; G|-{P}. c .{%Z s. s = d} |] ==>
  G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
apply (rule weak_Local)
apply auto
done

lemma export_Local_invariant: "G|-{%Z s. Z = s}. LOCAL Y:=a IN c .{%Z s. Z = s}"
apply (rule export_s)
apply (rule_tac P' = "%Z s. s'=s & True" and Q' = "%Z s. s' = s" in conseq12)
prefer 2
apply  clarsimp
apply (rule hoare_derivs.Local)
apply clarsimp
apply (rule trueI)
done

lemma classic_Local_invariant: "G|-{%Z s. Z = s}. LOCAL Y:=a IN c .{%Z s. Z = s}"
apply (rule classic_Local)
apply clarsimp
apply (rule trueI [THEN conseq12])
apply clarsimp
done

lemma Call_invariant: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s])} ==>
  G|-{%Z s. s'=s & I Z (getlocs (s[X::=k Z])) & P Z (setlocs s newlocs[Loc Arg::=a s])}.
  X:=CALL pn (a) .{%Z s. I Z (getlocs (s[X::=k Z])) & Q Z s}"
apply (rule_tac s'1 = "s'" and
  Q' = "%Z s. I Z (getlocs (s[X::=k Z])) = I Z (getlocs (s'[X::=k Z])) & Q Z s" in
  hoare_derivs.Call [THEN conseq12])
apply  (simp (no_asm_simp) add: getlocs_setlocs_lemma)
apply force
done

end

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.