src/HOL/IMPP/Misc.thy

modernized header uniformly as section;

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

section {* Several examples for Hoare logic *}

theory Misc
imports Hoare
begin

defs
  newlocs_def: "newlocs       == %x. undefined"
  setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
  getlocs_def: "getlocs s     == case s of st g l => l"
   update_def: "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)))"


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<Y>] = 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])<Y'> = (if Y=Y' then k else s<Y'>)"
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<Y> = 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<Y>" in spec)
apply (tactic "smp_tac 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 1 1")
apply simp
done

lemma classic_Local: "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = 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<Y'> = 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<Y'> = 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<Y'> = 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<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
apply (rule export_s)
apply (rule_tac P' = "%Z s. s'=s & True" and Q' = "%Z s. s'<Y> = s<Y>" 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<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
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<Res>])} ==>  
  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