src/HOL/Hoare/Hoare.thy
 changeset 13857 11d7c5a8dbb7 parent 13764 3e180bf68496 child 15032 02aed07e01bf
```     1.1 --- a/src/HOL/Hoare/Hoare.thy	Tue Mar 11 15:04:24 2003 +0100
1.2 +++ b/src/HOL/Hoare/Hoare.thy	Tue Mar 11 15:04:24 2003 +0100
1.3 @@ -60,7 +60,7 @@
1.4  ML{*
1.5
1.6  local
1.7 -fun free a = Free(a,dummyT)
1.8 +
1.9  fun abs((a,T),body) =
1.10    let val a = absfree(a, dummyT, body)
1.11    in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) \$ a \$ T end
1.12 @@ -70,9 +70,9 @@
1.13    | mk_abstuple (x::xs) body =
1.14        Syntax.const "split" \$ abs (x, mk_abstuple xs body);
1.15
1.16 -fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
1.17 +fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
1.18    | mk_fbody a e ((b,_)::xs) =
1.19 -      Syntax.const "Pair" \$ (if a=b then e else free b) \$ mk_fbody a e xs;
1.20 +      Syntax.const "Pair" \$ (if a=b then e else Syntax.free b) \$ mk_fbody a e xs;
1.21
1.22  fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
1.23  end
1.24 @@ -193,6 +193,38 @@
1.25
1.26  print_translation {* [("Valid", spec_tr')] *}
1.27
1.28 +lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
1.29 +by (auto simp:Valid_def)
1.30 +
1.31 +lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
1.32 +by (auto simp:Valid_def)
1.33 +
1.34 +lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
1.35 +by (auto simp:Valid_def)
1.36 +
1.37 +lemma CondRule:
1.38 + "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
1.39 +  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
1.40 +by (auto simp:Valid_def)
1.41 +
1.42 +lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
1.43 +       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
1.44 +apply(induct n)
1.45 + apply clarsimp
1.46 +apply(simp (no_asm_use))
1.47 +apply blast
1.48 +done
1.49 +
1.50 +lemma WhileRule:
1.51 + "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
1.52 +apply (clarsimp simp:Valid_def)
1.53 +apply(drule iter_aux)
1.54 +  prefer 2 apply assumption
1.55 + apply blast
1.56 +apply blast
1.57 +done
1.58 +
1.59 +
1.60  use "hoare.ML"
1.61
1.62  method_setup vcg = {*
```