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 = {*