(*  Title:      HOL/Hoare/Hoare.thy
    ID:         $Id$
    Author:     Leonor Prensa Nieto & Tobias Nipkow
    Copyright   1998 TUM

Sugared semantic embedding of Hoare logic.
Strictly speaking a shallow embedding (as implemented by Norbert Galm
following Mike Gordon) would suffice. Maybe the datatype com comes in useful
later.
*)

theory Hoare
imports Main
uses ("~~/src/HOL/Hoare/hoare_tac.ML")
begin


types
    'a bexp = "'a set"
    'a assn = "'a set"

datatype
 'a com = Basic "'a \<Rightarrow> 'a"
   | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
   | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
   | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)

abbreviation annskip ("SKIP") where "SKIP == Basic id"

types 'a sem = "'a => 'a => bool"

inductive Sem :: "'a com \<Rightarrow> 'a sem"
where
  "Sem (Basic f) s (f s)"
| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
| "s \<notin> b \<Longrightarrow> Sem (While b x c) s s"
| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
   Sem (While b x c) s s'"

inductive_cases [elim!]:
  "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
  "Sem (IF b THEN c1 ELSE c2 FI) s s'"

definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
  "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"



(** parse translations **)

syntax
  "_assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)

syntax
 "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
syntax ("" output)
 "_hoare"      :: "['a assn,'a com,'a assn] => bool"
                 ("{_} // _ // {_}" [0,55,0] 50)
ML {*

local

fun abs((a,T),body) =
  let val a = absfree(a, dummyT, body)
  in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
in

fun mk_abstuple [x] body = abs (x, body)
  | mk_abstuple (x::xs) body =
      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);

fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
  | mk_fbody a e ((b,_)::xs) =
      Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;

fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
end
*}

(* bexp_tr & assn_tr *)
(*all meta-variables for bexp except for TRUE are translated as if they
  were boolean expressions*)
ML{*
fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;

fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
*}
(* com_tr *)
ML{*
fun com_tr (Const(@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
      Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
  | com_tr t _ = t (* if t is just a Free/Var *)
*}

(* triple_tr *)    (* FIXME does not handle "_idtdummy" *)
ML{*
local

fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
  | var_tr(Const (@{syntax_const "_constrain"}, _) $ (Free (a,_)) $ T) = (a,T);

fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
  | vars_tr t = [var_tr t]

in
fun hoare_vars_tr [vars, pre, prg, post] =
      let val xs = vars_tr vars
      in Syntax.const @{const_syntax Valid} $
         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
      end
  | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
end
*}

parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *}


(*****************************************************************************)

(*** print translations ***)
ML{*
fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
                            subst_bound (Syntax.free v, dest_abstuple body)
  | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
  | dest_abstuple trm = trm;

fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
  | abs2list (Abs(x,T,t)) = [Free (x, T)]
  | abs2list _ = [];

fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
  | mk_ts (Abs(x,_,t)) = mk_ts t
  | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
  | mk_ts t = [t];

fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
           ((Syntax.free x)::(abs2list t), mk_ts t)
  | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
  | mk_vts t = raise Match;

fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
  | find_ch ((v,t)::vts) i xs =
      if t = Bound i then find_ch vts (i-1) xs
      else (true, (v, subst_bounds (xs, t)));

fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
  | is_f (Abs(x,_,t)) = true
  | is_f t = false;
*}

(* assn_tr' & bexp_tr'*)
ML{*
fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
  | assn_tr' (Const (@{const_syntax inter}, _) $
        (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) =
      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
  | assn_tr' t = t;

fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
  | bexp_tr' t = t;
*}

(*com_tr' *)
ML{*
fun mk_assign f =
  let val (vs, ts) = mk_vts f;
      val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
  in
    if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
    else Syntax.const @{const_syntax annskip}
  end;

fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
      if is_f f then mk_assign f
      else Syntax.const @{const_syntax Basic} $ f
  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
  | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
  | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
  | com_tr' t = t;

fun spec_tr' [p, c, q] =
  Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
*}

<<<<<<< local
<<<<<<< local
text {*
 The following specification of syntax and translations is for
 Isabelle experts only; feel free to ignore it.

 While the first part is still a somewhat intelligible specification
 of the concrete syntactic representation of our Hoare language, the
 actual ``ML drivers'' is quite involved.  Just note that the we
 re-use the basic quote/antiquote translations as already defined in
 Isabelle/Pure (see \verb,Syntax.quote_tr, and
 \verb,Syntax.quote_tr',).
*}

syntax
  "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)
  "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_" [1000] 1000)
  "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
        ("_[_'/\<acute>_]" [1000] 999)
  "_Assert"      :: "'a => 'a set"           ("(.{_}.)" [0] 1000)
  "_Assign"      :: "idt => 'b => 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
  "_Cond"        :: "'a bexp => 'a com => 'a com => 'a com"
        ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
  "_While_inv"   :: "'a bexp => 'a assn => 'a com => 'a com"
        ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
  "_While"       :: "'a bexp => 'a com => 'a com"
        ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)

syntax (xsymbols)
  "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)

translations
  ".{b}."                   => "Collect .(b)."
  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
  "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
  "WHILE b INV i DO c OD"   => "While .{b}. i c"

parse_translation {*
  let
    fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
      | quote_tr ts = raise TERM ("quote_tr", ts);
  in [("_quote", quote_tr)] end
*}

text {*
 As usual in Isabelle syntax translations, the part for printing is
 more complicated --- we cannot express parts as macro rules as above.
 Don't look here, unless you have to do similar things for yourself.
*}

print_translation {*
  let
    fun quote_tr' f (t :: ts) =
          Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
      | quote_tr' _ _ = raise Match;

    val assert_tr' = quote_tr' (Syntax.const "_Assert");

    fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
          quote_tr' (Syntax.const name) (t :: ts)
      | bexp_tr' _ _ = raise Match;

    fun upd_tr' (x_upd, T) =
      (case try (unsuffix RecordPackage.updateN) x_upd of
        SOME x => (x, if T = dummyT then T else Term.domain_type T)
      | NONE => raise Match);

    fun update_name_tr' (Free x) = Free (upd_tr' x)
      | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
          c $ Free (upd_tr' x)
      | update_name_tr' (Const x) = Const (upd_tr' x)
      | update_name_tr' _ = raise Match;

    fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
      | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
      | K_tr' _ = raise Match;

    fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
          quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
            (Abs (x, dummyT, K_tr' k) :: ts)
      | assign_tr' _ = raise Match;
  in
    [("Collect", assert_tr'), ("Basic", assign_tr'),
      ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]
  end
*}

subsection {* Rules for single-step proof \label{sec:hoare-isar} *}

text {*
 We are now ready to introduce a set of Hoare rules to be used in
 single-step structured proofs in Isabelle/Isar.  We refer to the
 concrete syntax introduce above.

 \medskip Assertions of Hoare Logic may be manipulated in
 calculational proofs, with the inclusion expressed in terms of sets
 or predicates.  Reversed order is supported as well.
*}

lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"
  by (unfold Valid_def) blast
lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q"
  by (unfold Valid_def) blast

lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'"
  by (unfold Valid_def) blast
lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'"
  by (unfold Valid_def) blast

lemma [trans]:
    "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"
  by (simp add: Valid_def)
lemma [trans]:
    "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"
  by (simp add: Valid_def)

lemma [trans]:
    "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."
  by (simp add: Valid_def)
lemma [trans]:
    "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."
  by (simp add: Valid_def)


text {*
 Identity and basic assignments.\footnote{The $\idt{hoare}$ method
 introduced in \S\ref{sec:hoare-vcg} is able to provide proper
 instances for any number of basic assignments, without producing
 additional verification conditions.}
*}

lemma skip [intro?]: "|- P SKIP P"
proof -
  have "|- {s. id s : P} SKIP P" by (rule basic)
  thus ?thesis by simp
qed

lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"
  by (rule basic)

text {*
 Note that above formulation of assignment corresponds to our
 preferred way to model state spaces, using (extensible) record types
 in HOL \cite{Naraschewski-Wenzel:1998:HOOL}.  For any record field
 $x$, Isabelle/HOL provides a functions $x$ (selector) and
 $\idt{x{\dsh}update}$ (update).  Above, there is only a place-holder
 appearing for the latter kind of function: due to concrete syntax
 \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due
 to the external nature of HOL record fields, we could not even state
 a general theorem relating selector and update functions (if this
 were required here); this would only work for any particular instance
 of record fields introduced so far.}
*}

text {*
 Sequential composition --- normalizing with associativity achieves
 proper of chunks of code verified separately.
*}

lemmas [trans, intro?] = seq

lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"
  by (auto simp add: Valid_def)

text {*
 Conditional statements.
*}

lemmas [trans, intro?] = cond

lemma [trans, intro?]:
  "|- .{\<acute>P & \<acute>b}. c1 Q
      ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
      ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
    by (rule cond) (simp_all add: Valid_def)

text {*
 While statements --- with optional invariant.
*}

lemma [intro?]:
    "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"
  by (rule while)

lemma [intro?]:
    "|- (P Int b) c P ==> |- P (While b arbitrary c) (P Int -b)"
  by (rule while)


lemma [intro?]:
  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
    ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
  by (simp add: while Collect_conj_eq Collect_neg_eq)

lemma [intro?]:
  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
    ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
  by (simp add: while Collect_conj_eq Collect_neg_eq)


subsection {* Verification conditions \label{sec:hoare-vcg} *}
=======
print_translation {* [("Valid", spec_tr')] *}
>>>>>>> other
=======
print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
>>>>>>> other

lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp:Valid_def)

lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
by (auto simp:Valid_def)

lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
by (auto simp:Valid_def)

lemma CondRule:
 "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
by (auto simp:Valid_def)

lemma While_aux:
  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
  shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
    s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
  using assms
  by (induct "WHILE b INV {i} DO c OD" s s') auto

lemma WhileRule:
 "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
apply (clarsimp simp:Valid_def)
apply(drule While_aux)
  apply assumption
 apply blast
apply blast
done


lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}"
  by blast

lemmas AbortRule = SkipRule  -- "dummy version"
use "~~/src/HOL/Hoare/hoare_tac.ML"

method_setup vcg = {*
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
  "verification condition generator"

method_setup vcg_simp = {*
  Scan.succeed (fn ctxt =>
    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *}
  "verification condition generator plus simplification"

end