*** empty log message ***
authornipkow
Tue Mar 11 15:04:24 2003 +0100 (2003-03-11)
changeset 1385711d7c5a8dbb7
parent 13856 f5d08c341216
child 13858 a077513c9a07
*** empty log message ***
src/HOL/Hoare/Examples.thy
src/HOL/Hoare/ExamplesAbort.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hoare/ROOT.ML
src/HOL/Hoare/Separation.thy
src/HOL/Hoare/hoare.ML
src/HOL/Hoare/hoareAbort.ML
     1.1 --- a/src/HOL/Hoare/Examples.thy	Tue Mar 11 15:04:24 2003 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Tue Mar 11 15:04:24 2003 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  lemma Euclid_GCD: "VARS a b
     1.5   {0<A & 0<B}
     1.6   a := A; b := B;
     1.7 - WHILE  a~=b
     1.8 + WHILE  a \<noteq> b
     1.9   INV {0<a & 0<b & gcd A B = gcd a b}
    1.10   DO IF a<b THEN b := b-a ELSE a := a-b FI OD
    1.11   {a = gcd A B}"
     2.1 --- a/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 11 15:04:24 2003 +0100
     2.2 +++ b/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 11 15:04:24 2003 +0100
     2.3 @@ -1,3 +1,12 @@
     2.4 +(*  Title:      HOL/Hoare/ExamplesAbort.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +    Copyright   1998 TUM
     2.8 +
     2.9 +Some small examples for programs that may abort.
    2.10 +Currently only show the absence of abort.
    2.11 +*)
    2.12 +
    2.13  theory ExamplesAbort = HoareAbort:
    2.14  
    2.15  syntax guarded_com :: "'bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("_ \<rightarrow> _" 60)
     3.1 --- a/src/HOL/Hoare/Hoare.thy	Tue Mar 11 15:04:24 2003 +0100
     3.2 +++ b/src/HOL/Hoare/Hoare.thy	Tue Mar 11 15:04:24 2003 +0100
     3.3 @@ -60,7 +60,7 @@
     3.4  ML{*
     3.5  
     3.6  local
     3.7 -fun free a = Free(a,dummyT)
     3.8 +
     3.9  fun abs((a,T),body) =
    3.10    let val a = absfree(a, dummyT, body)
    3.11    in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
    3.12 @@ -70,9 +70,9 @@
    3.13    | mk_abstuple (x::xs) body =
    3.14        Syntax.const "split" $ abs (x, mk_abstuple xs body);
    3.15  
    3.16 -fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
    3.17 +fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
    3.18    | mk_fbody a e ((b,_)::xs) =
    3.19 -      Syntax.const "Pair" $ (if a=b then e else free b) $ mk_fbody a e xs;
    3.20 +      Syntax.const "Pair" $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;
    3.21  
    3.22  fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
    3.23  end
    3.24 @@ -193,6 +193,38 @@
    3.25  
    3.26  print_translation {* [("Valid", spec_tr')] *}
    3.27  
    3.28 +lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
    3.29 +by (auto simp:Valid_def)
    3.30 +
    3.31 +lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
    3.32 +by (auto simp:Valid_def)
    3.33 +
    3.34 +lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
    3.35 +by (auto simp:Valid_def)
    3.36 +
    3.37 +lemma CondRule:
    3.38 + "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
    3.39 +  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
    3.40 +by (auto simp:Valid_def)
    3.41 +
    3.42 +lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
    3.43 +       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
    3.44 +apply(induct n)
    3.45 + apply clarsimp
    3.46 +apply(simp (no_asm_use))
    3.47 +apply blast
    3.48 +done
    3.49 +
    3.50 +lemma WhileRule:
    3.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"
    3.52 +apply (clarsimp simp:Valid_def)
    3.53 +apply(drule iter_aux)
    3.54 +  prefer 2 apply assumption
    3.55 + apply blast
    3.56 +apply blast
    3.57 +done
    3.58 +
    3.59 +
    3.60  use "hoare.ML"
    3.61  
    3.62  method_setup vcg = {*
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Tue Mar 11 15:04:24 2003 +0100
     4.3 @@ -0,0 +1,250 @@
     4.4 +(*  Title:      HOL/Hoare/HoareAbort.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Leonor Prensa Nieto & Tobias Nipkow
     4.7 +    Copyright   2003 TUM
     4.8 +
     4.9 +Like Hoare.thy, but with an Abort statement for modelling run time errors.
    4.10 +*)
    4.11 +
    4.12 +theory HoareAbort  = Main
    4.13 +files ("hoareAbort.ML"):
    4.14 +
    4.15 +types
    4.16 +    'a bexp = "'a set"
    4.17 +    'a assn = "'a set"
    4.18 +
    4.19 +datatype
    4.20 + 'a com = Basic "'a \<Rightarrow> 'a"
    4.21 +   | Abort
    4.22 +   | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
    4.23 +   | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    4.24 +   | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
    4.25 +  
    4.26 +syntax
    4.27 +  "@assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
    4.28 +  "@annskip" :: "'a com"                    ("SKIP")
    4.29 +
    4.30 +translations
    4.31 +            "SKIP" == "Basic id"
    4.32 +
    4.33 +types 'a sem = "'a option => 'a option => bool"
    4.34 +
    4.35 +consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
    4.36 +primrec
    4.37 +"iter 0 b S = (%s s'. s ~: Some ` b & (s=s'))"
    4.38 +"iter (Suc n) b S = (%s s'. s : Some ` b & (? s''. S s s'' & iter n b S s'' s'))"
    4.39 +
    4.40 +consts Sem :: "'a com => 'a sem"
    4.41 +primrec
    4.42 +"Sem(Basic f) s s' = (case s of None \<Rightarrow> s' = None | Some t \<Rightarrow> s' = Some(f t))"
    4.43 +"Sem Abort s s' = (s' = None)"
    4.44 +"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')"
    4.45 +"Sem(IF b THEN c1 ELSE c2 FI) s s' =
    4.46 + (case s of None \<Rightarrow> s' = None
    4.47 +  | Some t \<Rightarrow> ((t : b --> Sem c1 s s') & (t ~: b --> Sem c2 s s')))"
    4.48 +"Sem(While b x c) s s' =
    4.49 + (if s = None then s' = None
    4.50 +  else EX n. iter n b (Sem c) s s')"
    4.51 +
    4.52 +constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
    4.53 +  "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
    4.54 +
    4.55 +
    4.56 +syntax
    4.57 + "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
    4.58 +                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
    4.59 +syntax ("" output)
    4.60 + "@hoare"      :: "['a assn,'a com,'a assn] => bool"
    4.61 +                 ("{_} // _ // {_}" [0,55,0] 50)
    4.62 +
    4.63 +(** parse translations **)
    4.64 +
    4.65 +ML{*
    4.66 +
    4.67 +local
    4.68 +fun free a = Free(a,dummyT)
    4.69 +fun abs((a,T),body) =
    4.70 +  let val a = absfree(a, dummyT, body)
    4.71 +  in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
    4.72 +in
    4.73 +
    4.74 +fun mk_abstuple [x] body = abs (x, body)
    4.75 +  | mk_abstuple (x::xs) body =
    4.76 +      Syntax.const "split" $ abs (x, mk_abstuple xs body);
    4.77 +
    4.78 +fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
    4.79 +  | mk_fbody a e ((b,_)::xs) =
    4.80 +      Syntax.const "Pair" $ (if a=b then e else free b) $ mk_fbody a e xs;
    4.81 +
    4.82 +fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
    4.83 +end
    4.84 +*}
    4.85 +
    4.86 +(* bexp_tr & assn_tr *)
    4.87 +(*all meta-variables for bexp except for TRUE are translated as if they
    4.88 +  were boolean expressions*)
    4.89 +ML{*
    4.90 +fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"
    4.91 +  | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b;
    4.92 +  
    4.93 +fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
    4.94 +*}
    4.95 +(* com_tr *)
    4.96 +ML{*
    4.97 +fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
    4.98 +      Syntax.const "Basic" $ mk_fexp a e xs
    4.99 +  | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
   4.100 +  | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
   4.101 +      Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
   4.102 +  | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =
   4.103 +      Syntax.const "Cond" $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
   4.104 +  | com_tr (Const ("While",_) $ b $ I $ c) xs =
   4.105 +      Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
   4.106 +  | com_tr t _ = t (* if t is just a Free/Var *)
   4.107 +*}
   4.108 +
   4.109 +(* triple_tr *)
   4.110 +ML{*
   4.111 +local
   4.112 +
   4.113 +fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
   4.114 +  | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T);
   4.115 +
   4.116 +fun vars_tr (Const ("_idts", _) $ idt $ vars) = var_tr idt :: vars_tr vars
   4.117 +  | vars_tr t = [var_tr t]
   4.118 +
   4.119 +in
   4.120 +fun hoare_vars_tr [vars, pre, prg, post] =
   4.121 +      let val xs = vars_tr vars
   4.122 +      in Syntax.const "Valid" $
   4.123 +         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
   4.124 +      end
   4.125 +  | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
   4.126 +end
   4.127 +*}
   4.128 +
   4.129 +parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
   4.130 +
   4.131 +
   4.132 +(*****************************************************************************)
   4.133 +
   4.134 +(*** print translations ***)
   4.135 +ML{*
   4.136 +fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) =
   4.137 +                            subst_bound (Syntax.free v, dest_abstuple body)
   4.138 +  | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
   4.139 +  | dest_abstuple trm = trm;
   4.140 +
   4.141 +fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
   4.142 +  | abs2list (Abs(x,T,t)) = [Free (x, T)]
   4.143 +  | abs2list _ = [];
   4.144 +
   4.145 +fun mk_ts (Const ("split",_) $ (Abs(x,_,t))) = mk_ts t
   4.146 +  | mk_ts (Abs(x,_,t)) = mk_ts t
   4.147 +  | mk_ts (Const ("Pair",_) $ a $ b) = a::(mk_ts b)
   4.148 +  | mk_ts t = [t];
   4.149 +
   4.150 +fun mk_vts (Const ("split",_) $ (Abs(x,_,t))) = 
   4.151 +           ((Syntax.free x)::(abs2list t), mk_ts t)
   4.152 +  | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
   4.153 +  | mk_vts t = raise Match;
   4.154 +  
   4.155 +fun find_ch [] i xs = (false, (Syntax.free "not_ch",Syntax.free "not_ch" ))
   4.156 +  | find_ch ((v,t)::vts) i xs = if t=(Bound i) then find_ch vts (i-1) xs
   4.157 +              else (true, (v, subst_bounds (xs,t)));
   4.158 +  
   4.159 +fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true
   4.160 +  | is_f (Abs(x,_,t)) = true
   4.161 +  | is_f t = false;
   4.162 +*}
   4.163 +
   4.164 +(* assn_tr' & bexp_tr'*)
   4.165 +ML{*  
   4.166 +fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
   4.167 +  | assn_tr' (Const ("op Int",_) $ (Const ("Collect",_) $ T1) $ 
   4.168 +                                   (Const ("Collect",_) $ T2)) =  
   4.169 +            Syntax.const "op Int" $ dest_abstuple T1 $ dest_abstuple T2
   4.170 +  | assn_tr' t = t;
   4.171 +
   4.172 +fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T 
   4.173 +  | bexp_tr' t = t;
   4.174 +*}
   4.175 +
   4.176 +(*com_tr' *)
   4.177 +ML{*
   4.178 +fun mk_assign f =
   4.179 +  let val (vs, ts) = mk_vts f;
   4.180 +      val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
   4.181 +  in if ch then Syntax.const "@assign" $ fst(which) $ snd(which)
   4.182 +     else Syntax.const "@skip" end;
   4.183 +
   4.184 +fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
   4.185 +                                           else Syntax.const "Basic" $ f
   4.186 +  | com_tr' (Const ("Seq",_) $ c1 $ c2) = Syntax.const "Seq" $
   4.187 +                                                 com_tr' c1 $ com_tr' c2
   4.188 +  | com_tr' (Const ("Cond",_) $ b $ c1 $ c2) = Syntax.const "Cond" $
   4.189 +                                           bexp_tr' b $ com_tr' c1 $ com_tr' c2
   4.190 +  | com_tr' (Const ("While",_) $ b $ I $ c) = Syntax.const "While" $
   4.191 +                                               bexp_tr' b $ assn_tr' I $ com_tr' c
   4.192 +  | com_tr' t = t;
   4.193 +
   4.194 +
   4.195 +fun spec_tr' [p, c, q] =
   4.196 +  Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
   4.197 +*}
   4.198 +
   4.199 +print_translation {* [("Valid", spec_tr')] *}
   4.200 +
   4.201 +(*** The proof rules ***)
   4.202 +
   4.203 +lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
   4.204 +by (auto simp:Valid_def)
   4.205 +
   4.206 +lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
   4.207 +by (auto simp:Valid_def)
   4.208 +
   4.209 +lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
   4.210 +by (auto simp:Valid_def)
   4.211 +
   4.212 +lemma CondRule:
   4.213 + "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
   4.214 +  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
   4.215 +by (fastsimp simp:Valid_def image_def)
   4.216 +
   4.217 +lemma iter_aux: "! s s'. Sem c s s' --> s : Some ` (I \<inter> b) --> s' : Some ` I ==>
   4.218 +       (\<And>s s'. s : Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : Some ` (I \<inter> -b))";
   4.219 +apply(unfold image_def)
   4.220 +apply(induct n)
   4.221 + apply clarsimp
   4.222 +apply(simp (no_asm_use))
   4.223 +apply blast
   4.224 +done
   4.225 +
   4.226 +lemma WhileRule:
   4.227 + "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
   4.228 +apply(simp add:Valid_def)
   4.229 +apply(simp (no_asm) add:image_def)
   4.230 +apply clarify
   4.231 +apply(drule iter_aux)
   4.232 +  prefer 2 apply assumption
   4.233 + apply blast
   4.234 +apply blast
   4.235 +done
   4.236 +
   4.237 +lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q"
   4.238 +by(auto simp:Valid_def)
   4.239 +
   4.240 +use "hoareAbort.ML"
   4.241 +
   4.242 +method_setup vcg = {*
   4.243 +  Method.no_args
   4.244 +    (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
   4.245 +  "verification condition generator"
   4.246 +
   4.247 +method_setup vcg_simp = {*
   4.248 +  Method.ctxt_args (fn ctxt =>
   4.249 +    Method.METHOD (fn facts => 
   4.250 +      hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *}
   4.251 +  "verification condition generator plus simplification"
   4.252 +
   4.253 +end
     5.1 --- a/src/HOL/Hoare/ROOT.ML	Tue Mar 11 15:04:24 2003 +0100
     5.2 +++ b/src/HOL/Hoare/ROOT.ML	Tue Mar 11 15:04:24 2003 +0100
     5.3 @@ -5,5 +5,6 @@
     5.4  *)
     5.5  
     5.6  time_use_thy "Examples";
     5.7 +time_use_thy "ExamplesAbort";
     5.8  time_use_thy "Pointers0";
     5.9  time_use_thy "Pointer_Examples";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Hoare/Separation.thy	Tue Mar 11 15:04:24 2003 +0100
     6.3 @@ -0,0 +1,90 @@
     6.4 +theory Separation = HoareAbort:
     6.5 +
     6.6 +types heap = "(nat \<Rightarrow> nat option)"
     6.7 +
     6.8 +
     6.9 +text{* The semantic definition of a few connectives: *}
    6.10 +
    6.11 +constdefs
    6.12 + R:: "heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> bool"
    6.13 +"R h h1 h2 == dom h1 \<inter> dom h2 = {} \<and> h = h1 ++ h2"
    6.14 +
    6.15 + star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
    6.16 +"star P Q == \<lambda>h. \<exists>h1 h2. R h h1 h2 \<and> P h1 \<and> Q h2"
    6.17 +
    6.18 + singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
    6.19 +"singl h x y == dom h = {x} & h x = Some y"
    6.20 +
    6.21 +lemma "VARS x y z w h
    6.22 + {star (%h. singl h x y) (%h. singl h z w) h}
    6.23 + SKIP
    6.24 + {x \<noteq> z}"
    6.25 +apply vcg
    6.26 +apply(auto simp:star_def R_def singl_def)
    6.27 +done
    6.28 +
    6.29 +text{* To suppress the heap parameter of the connectives, we assume it
    6.30 +is always called H and add/remove it upon parsing/printing. Thus
    6.31 +every pointer program needs to have a program variable H, and
    6.32 +assertions should not contain any locally bound Hs - otherwise they
    6.33 +may bind the implicit H. *}
    6.34 +
    6.35 +text{* Nice input syntax: *}
    6.36 +
    6.37 +syntax
    6.38 + "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
    6.39 + "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
    6.40 +
    6.41 +ML{*
    6.42 +fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
    6.43 +  | singl_tr ts = raise TERM ("singl_tr", ts);
    6.44 +fun star_tr [P,Q] = Syntax.const "star" $
    6.45 +      absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
    6.46 +  | star_tr ts = raise TERM ("star_tr", ts);
    6.47 +*}
    6.48 +
    6.49 +parse_translation {* [("@singl", singl_tr),("@star", star_tr)] *}
    6.50 +
    6.51 +lemma "VARS H x y z w
    6.52 + {[x\<mapsto>y] ** [z\<mapsto>w]}
    6.53 + SKIP
    6.54 + {x \<noteq> z}"
    6.55 +apply vcg
    6.56 +apply(auto simp:star_def R_def singl_def)
    6.57 +done
    6.58 +
    6.59 +text{* Nice output syntax: *}
    6.60 +
    6.61 +ML{*
    6.62 +fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
    6.63 +fun star_tr' [Abs(_,_,P),Abs(_,_,Q),_] = Syntax.const "@star" $ P $ Q
    6.64 +*}
    6.65 +
    6.66 +print_translation {* [("singl", singl_tr'),("star", star_tr')] *}
    6.67 +
    6.68 +lemma "VARS H x y z w
    6.69 + {[x\<mapsto>y] ** [z\<mapsto>w]}
    6.70 + SKIP
    6.71 + {x \<noteq> z}"
    6.72 +apply vcg
    6.73 +apply(auto simp:star_def R_def singl_def)
    6.74 +done
    6.75 +
    6.76 +
    6.77 +consts llist :: "(heap * nat)set"
    6.78 +inductive llist
    6.79 +intros
    6.80 +empty: "(%n. None, 0) : llist"
    6.81 +cons: "\<lbrakk> R h h1 h2; pto h1 p q; (h2,q):llist \<rbrakk> \<Longrightarrow> (h,p):llist"
    6.82 +
    6.83 +lemma "VARS p q h
    6.84 + {(h,p) : llist}
    6.85 + h := h(q \<mapsto> p)
    6.86 + {(h,q) : llist}"
    6.87 +apply vcg
    6.88 +apply(rule_tac "h1.0" = "%n. if n=q then Some p else None" in llist.cons)
    6.89 +prefer 3 apply assumption
    6.90 +prefer 2 apply(simp add:singl_def dom_def)
    6.91 +apply(simp add:R_def dom_def)
    6.92 +
    6.93 +
     7.1 --- a/src/HOL/Hoare/hoare.ML	Tue Mar 11 15:04:24 2003 +0100
     7.2 +++ b/src/HOL/Hoare/hoare.ML	Tue Mar 11 15:04:24 2003 +0100
     7.3 @@ -6,54 +6,11 @@
     7.4  Derivation of the proof rules and, most importantly, the VCG tactic.
     7.5  *)
     7.6  
     7.7 -(*** The proof rules ***)
     7.8 -
     7.9 -Goalw [thm "Valid_def"] "p <= q ==> Valid p (Basic id) q";
    7.10 -by (Auto_tac);
    7.11 -qed "SkipRule";
    7.12 -
    7.13 -Goalw [thm "Valid_def"] "p <= {s. (f s):q} ==> Valid p (Basic f) q";
    7.14 -by (Auto_tac);
    7.15 -qed "BasicRule";
    7.16 -
    7.17 -Goalw [thm "Valid_def"] "Valid P c1 Q ==> Valid Q c2 R ==> Valid P (c1;c2) R";
    7.18 -by (Asm_simp_tac 1);
    7.19 -by (Blast_tac 1);
    7.20 -qed "SeqRule";
    7.21 -
    7.22 -Goalw [thm "Valid_def"]
    7.23 - "p <= {s. (s:b --> s:w) & (s~:b --> s:w')} \
    7.24 -\ ==> Valid w c1 q ==> Valid w' c2 q \
    7.25 -\ ==> Valid p (Cond b c1 c2) q";
    7.26 -by (Asm_simp_tac 1);
    7.27 -by (Blast_tac 1);
    7.28 -qed "CondRule";
    7.29 -
    7.30 -Goal "! s s'. Sem c s s' --> s : I Int b --> s' : I ==> \
    7.31 -\     ! s s'. s : I --> iter n b (Sem c) s s' --> s' : I & s' ~: b";
    7.32 -by (induct_tac "n" 1);
    7.33 - by (Asm_simp_tac 1);
    7.34 -by (Simp_tac 1);
    7.35 -by (Blast_tac 1);
    7.36 -val lemma = result() RS spec RS spec RS mp RS mp;
    7.37 -
    7.38 -Goalw [thm "Valid_def"]
    7.39 - "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \
    7.40 -\ ==> Valid p (While b j c) q";
    7.41 -by (Asm_simp_tac 1);
    7.42 -by (Clarify_tac 1);
    7.43 -by (dtac lemma 1);
    7.44 -by (assume_tac 2);
    7.45 -by (Blast_tac 1);
    7.46 -by (Blast_tac 1);
    7.47 -qed "WhileRule'";
    7.48 -
    7.49 -Goal
    7.50 - "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \
    7.51 -\ ==> Valid p (While b i c) q";
    7.52 -by (rtac WhileRule' 1);
    7.53 -by (ALLGOALS assume_tac);
    7.54 -qed "WhileRule";
    7.55 +val SkipRule = thm"SkipRule";
    7.56 +val BasicRule = thm"BasicRule";
    7.57 +val SeqRule = thm"SeqRule";
    7.58 +val CondRule = thm"CondRule";
    7.59 +val WhileRule = thm"WhileRule";
    7.60  
    7.61  (*** The tactics ***)
    7.62  
    7.63 @@ -191,7 +148,8 @@
    7.64  
    7.65  (** HoareRuleTac **)
    7.66  
    7.67 -fun WlpTac Mlem tac i = rtac SeqRule i THEN  HoareRuleTac Mlem tac false (i+1)
    7.68 +fun WlpTac Mlem tac i =
    7.69 +  rtac SeqRule i THEN  HoareRuleTac Mlem tac false (i+1)
    7.70  and HoareRuleTac Mlem tac pre_cond i st = st |>
    7.71          (*abstraction over st prevents looping*)
    7.72      ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i)
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Hoare/hoareAbort.ML	Tue Mar 11 15:04:24 2003 +0100
     8.3 @@ -0,0 +1,177 @@
     8.4 +(*  Title:      HOL/Hoare/Hoare.ML
     8.5 +    ID:         $Id$
     8.6 +    Author:     Leonor Prensa Nieto & Tobias Nipkow
     8.7 +    Copyright   1998 TUM
     8.8 +
     8.9 +Derivation of the proof rules and, most importantly, the VCG tactic.
    8.10 +*)
    8.11 +
    8.12 +val SkipRule = thm"SkipRule";
    8.13 +val BasicRule = thm"BasicRule";
    8.14 +val AbortRule = thm"AbortRule";
    8.15 +val SeqRule = thm"SeqRule";
    8.16 +val CondRule = thm"CondRule";
    8.17 +val WhileRule = thm"WhileRule";
    8.18 +
    8.19 +(*** The tactics ***)
    8.20 +
    8.21 +(*****************************************************************************)
    8.22 +(** The function Mset makes the theorem                                     **)
    8.23 +(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}",        **)
    8.24 +(** where (x1,...,xn) are the variables of the particular program we are    **)
    8.25 +(** working on at the moment of the call                                    **)
    8.26 +(*****************************************************************************)
    8.27 +
    8.28 +local open HOLogic in
    8.29 +
    8.30 +(** maps (%x1 ... xn. t) to [x1,...,xn] **)
    8.31 +fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    8.32 +  | abs2list (Abs(x,T,t)) = [Free (x, T)]
    8.33 +  | abs2list _ = [];
    8.34 +
    8.35 +(** maps {(x1,...,xn). t} to [x1,...,xn] **)
    8.36 +fun mk_vars (Const ("Collect",_) $ T) = abs2list T
    8.37 +  | mk_vars _ = [];
    8.38 +
    8.39 +(** abstraction of body over a tuple formed from a list of free variables. 
    8.40 +Types are also built **)
    8.41 +fun mk_abstupleC []     body = absfree ("x", unitT, body)
    8.42 +  | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
    8.43 +                               in if w=[] then absfree (n, T, body)
    8.44 +        else let val z  = mk_abstupleC w body;
    8.45 +                 val T2 = case z of Abs(_,T,_) => T
    8.46 +                        | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    8.47 +       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) 
    8.48 +          $ absfree (n, T, z) end end;
    8.49 +
    8.50 +(** maps [x1,...,xn] to (x1,...,xn) and types**)
    8.51 +fun mk_bodyC []      = HOLogic.unit
    8.52 +  | mk_bodyC (x::xs) = if xs=[] then x 
    8.53 +               else let val (n, T) = dest_Free x ;
    8.54 +                        val z = mk_bodyC xs;
    8.55 +                        val T2 = case z of Free(_, T) => T
    8.56 +                                         | Const ("Pair", Type ("fun", [_, Type
    8.57 +                                            ("fun", [_, T])])) $ _ $ _ => T;
    8.58 +                 in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    8.59 +
    8.60 +fun dest_Goal (Const ("Goal", _) $ P) = P;
    8.61 +
    8.62 +(** maps a goal of the form:
    8.63 +        1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) 
    8.64 +fun get_vars thm = let  val c = dest_Goal (concl_of (thm));
    8.65 +                        val d = Logic.strip_assums_concl c;
    8.66 +                        val Const _ $ pre $ _ $ _ = dest_Trueprop d;
    8.67 +      in mk_vars pre end;
    8.68 +
    8.69 +
    8.70 +(** Makes Collect with type **)
    8.71 +fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
    8.72 +                      in Collect_const t $ trm end;
    8.73 +
    8.74 +fun inclt ty = Const ("op <=", [ty,ty] ---> boolT);
    8.75 +
    8.76 +(** Makes "Mset <= t" **)
    8.77 +fun Mset_incl t = let val MsetT = fastype_of t 
    8.78 +                 in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end;
    8.79 +
    8.80 +
    8.81 +fun Mset thm = let val vars = get_vars(thm);
    8.82 +                   val varsT = fastype_of (mk_bodyC vars);
    8.83 +                   val big_Collect = mk_CollectC (mk_abstupleC vars 
    8.84 +                         (Free ("P",varsT --> boolT) $ mk_bodyC vars));
    8.85 +                   val small_Collect = mk_CollectC (Abs("x",varsT,
    8.86 +                           Free ("P",varsT --> boolT) $ Bound 0));
    8.87 +                   val impl = implies $ (Mset_incl big_Collect) $ 
    8.88 +                                          (Mset_incl small_Collect);
    8.89 +   in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
    8.90 +
    8.91 +end;
    8.92 +
    8.93 +
    8.94 +(*****************************************************************************)
    8.95 +(** Simplifying:                                                            **)
    8.96 +(** Some useful lemmata, lists and simplification tactics to control which  **)
    8.97 +(** theorems are used to simplify at each moment, so that the original      **)
    8.98 +(** input does not suffer any unexpected transformation                     **)
    8.99 +(*****************************************************************************)
   8.100 +
   8.101 +Goal "-(Collect b) = {x. ~(b x)}";
   8.102 +by (Fast_tac 1);
   8.103 +qed "Compl_Collect";
   8.104 +
   8.105 +
   8.106 +(**Simp_tacs**)
   8.107 +
   8.108 +val before_set2pred_simp_tac =
   8.109 +  (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect]));
   8.110 +
   8.111 +val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
   8.112 +
   8.113 +(*****************************************************************************)
   8.114 +(** set2pred transforms sets inclusion into predicates implication,         **)
   8.115 +(** maintaining the original variable names.                                **)
   8.116 +(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
   8.117 +(** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
   8.118 +(** are first simplified by "before_set2pred_simp_tac", that returns only   **)
   8.119 +(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily           **)
   8.120 +(** transformed.                                                            **)
   8.121 +(** This transformation may solve very easy subgoals due to a ligth         **)
   8.122 +(** simplification done by (split_all_tac)                                  **)
   8.123 +(*****************************************************************************)
   8.124 +
   8.125 +fun set2pred i thm = let fun mk_string [] = ""
   8.126 +                           | mk_string (x::xs) = x^" "^mk_string xs;
   8.127 +                         val vars=get_vars(thm);
   8.128 +                         val var_string = mk_string (map (fst o dest_Free) vars);
   8.129 +      in ((before_set2pred_simp_tac i) THEN_MAYBE
   8.130 +          (EVERY [rtac subsetI i, 
   8.131 +                  rtac CollectI i,
   8.132 +                  dtac CollectD i,
   8.133 +                  (TRY(split_all_tac i)) THEN_MAYBE
   8.134 +                  ((rename_tac var_string i) THEN
   8.135 +                   (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
   8.136 +      end;
   8.137 +
   8.138 +(*****************************************************************************)
   8.139 +(** BasicSimpTac is called to simplify all verification conditions. It does **)
   8.140 +(** a light simplification by applying "mem_Collect_eq", then it calls      **)
   8.141 +(** MaxSimpTac, which solves subgoals of the form "A <= A",                 **)
   8.142 +(** and transforms any other into predicates, applying then                 **)
   8.143 +(** the tactic chosen by the user, which may solve the subgoal completely.  **)
   8.144 +(*****************************************************************************)
   8.145 +
   8.146 +fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
   8.147 +
   8.148 +fun BasicSimpTac tac =
   8.149 +  simp_tac
   8.150 +    (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc])
   8.151 +  THEN_MAYBE' MaxSimpTac tac;
   8.152 +
   8.153 +(** HoareRuleTac **)
   8.154 +
   8.155 +fun WlpTac Mlem tac i =
   8.156 +  rtac SeqRule i THEN  HoareRuleTac Mlem tac false (i+1)
   8.157 +and HoareRuleTac Mlem tac pre_cond i st = st |>
   8.158 +        (*abstraction over st prevents looping*)
   8.159 +    ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i)
   8.160 +      ORELSE
   8.161 +      (FIRST[rtac SkipRule i,
   8.162 +             rtac AbortRule i,
   8.163 +             EVERY[rtac BasicRule i,
   8.164 +                   rtac Mlem i,
   8.165 +                   split_simp_tac i],
   8.166 +             EVERY[rtac CondRule i,
   8.167 +                   HoareRuleTac Mlem tac false (i+2),
   8.168 +                   HoareRuleTac Mlem tac false (i+1)],
   8.169 +             EVERY[rtac WhileRule i,
   8.170 +                   BasicSimpTac tac (i+2),
   8.171 +                   HoareRuleTac Mlem tac true (i+1)] ] 
   8.172 +       THEN (if pre_cond then (BasicSimpTac tac i) else rtac subset_refl i) ));
   8.173 +
   8.174 +
   8.175 +(** tac:(int -> tactic) is the tactic the user chooses to solve or simplify **)
   8.176 +(** the final verification conditions                                       **)
   8.177 + 
   8.178 +fun hoare_tac tac i thm =
   8.179 +  let val Mlem = Mset(thm)
   8.180 +  in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;