1476

1 
(* Title: HOL/Hoare/Hoare.thy

1335

2 
ID: $Id$

1476

3 
Author: Norbert Galm & Tobias Nipkow

1335

4 
Copyright 1995 TUM


5 


6 
Sugared semantic embedding of Hoare logic.


7 
*)


8 


9 
Hoare = Arith +


10 


11 
types

1476

12 
'a prog (* program syntax *)


13 
pvar = nat (* encoding of program variables ( < 26! ) *)


14 
'a state = pvar => 'a (* program state *)


15 
'a exp = 'a state => 'a (* denotation of expressions *)


16 
'a bexp = 'a state => bool (* denotation of boolean expressions *)

1384

17 
'a com = 'a state => 'a state => bool (* denotation of programs *)

1335

18 


19 
syntax

1476

20 
"@Skip" :: 'a prog ("SKIP")


21 
"@Assign" :: [id, 'a] => 'a prog ("_ := _")


22 
"@Seq" :: ['a prog, 'a prog] => 'a prog ("_;//_" [0,1000] 999)


23 
"@If" :: [bool, 'a prog, 'a prog] => 'a prog

1335

24 
("IF _//THEN// (_)//ELSE// (_)//END")

1476

25 
"@While" :: [bool, bool, 'a prog] => 'a prog

1335

26 
("WHILE _//DO {_}// (_)//END")


27 

1476

28 
"@Spec" :: [bool, 'a prog, bool] => bool ("{_}//_//{_}")

1335

29 

1558

30 
constdefs


31 
(* denotational semantics *)

1335

32 

1476

33 
Skip :: 'a com

1558

34 
"Skip s s' == (s=s')"


35 

1476

36 
Assign :: [pvar, 'a exp] => 'a com

1558

37 
"Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"


38 

1476

39 
Seq :: ['a com, 'a com] => 'a com

1558

40 
"Seq c c' s s' == ? s''. c s s'' & c' s'' s'"


41 

1476

42 
Cond :: ['a bexp, 'a com, 'a com] => 'a com

1558

43 
"Cond b c c' s s' == (b(s) > c s s') & (~b s > c' s s')"


44 

1476

45 
While :: ['a bexp, 'a bexp, 'a com] => 'a com

1558

46 
"While b inv c s s' == ? n. Iter n b c s s'"


47 

1476

48 
Iter :: [nat, 'a bexp, 'a com] => 'a com

1824

49 
"Iter n b c == nat_rec (%s s'.~b(s) & (s=s'))


50 
(%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s') n"

1335

51 

1476

52 
Spec :: ['a bexp, 'a com, 'a bexp] => bool

1558

53 
"Spec p c q == !s s'. c s s' > p s > q s'"

1335

54 


55 
end


56 


57 
ML


58 


59 


60 
(*** term manipulation ***)


61 


62 
(* name_in_term:bool (name:string,trm:term) bestimmt, ob in trm der Name name als Konstante,


63 
freie Var., schemeVariable oder als Name fuer eine LambdaAbstraktion vorkommt *)


64 

1476

65 
fun name_in_term (name,Const (s,t)) =(name=s)


66 
 name_in_term (name,Free (s,t)) =(name=s)


67 
 name_in_term (name,Var ((s,i),t)) =(name=s ^ makestring i)


68 
 name_in_term (name,Abs (s,t,trm)) =(name=s) orelse (name_in_term (name,trm))


69 
 name_in_term (name,trm1 $ trm2) =(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))


70 
 name_in_term (_,_) =false;

1335

71 


72 
(* variant_name:string (name:string,trm:term) liefert einen von name abgewandelten Namen (durch Anhaengen


73 
von genuegend vielen "_"), der nicht in trm vorkommt. Im Gegensatz zu variant_abs beruecktsichtigt es


74 
auch Namen von schemeVariablen und von LambdaAbstraktionen in trm *)


75 

1476

76 
fun variant_name (name,trm) =if name_in_term (name,trm)


77 
then variant_name (name ^ "_",trm)


78 
else name;

1335

79 


80 
(* subst_term:term (von:term,nach:term,trm:term) liefert den Term, der aus


81 
trm entsteht, wenn alle Teilterme, die gleich von sind, durch nach ersetzt


82 
wurden *)


83 

1476

84 
fun subst_term (von,nach,Abs (s,t,trm)) =if von=Abs (s,t,trm)


85 
then nach


86 
else Abs (s,t,subst_term (von,nach,trm))


87 
 subst_term (von,nach,trm1 $ trm2) =if von=trm1 $ trm2


88 
then nach


89 
else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)


90 
 subst_term (von,nach,trm) =if von=trm


91 
then nach


92 
else trm;

1335

93 


94 


95 
(* Translation between program vars ("a"  "z") and their encoding as


96 
natural numbers: "a" <==> 0, "b" <==> Suc(0), ..., "z" <==> 25 *)


97 

1476

98 
fun is_pvarID s = size s=1 andalso "a"<=s andalso s<="z";

1335

99 


100 
fun pvarID2pvar s =


101 
let fun rest2pvar (i,arg) =


102 
if i=0 then arg else rest2pvar(i1, Syntax.const "Suc" $ arg)


103 
in rest2pvar(ord s  ord "a", Syntax.const "0") end;


104 

1476

105 
fun pvar2pvarID trm =


106 
let


107 
fun rest2pvarID (Const("0",_),i) =chr (i + ord "a")


108 
 rest2pvarID (Const("Suc",_) $ trm,i) =rest2pvarID (trm,i+1)


109 
in


110 
rest2pvarID (trm,0)


111 
end;

1335

112 


113 


114 
(*** parse translations: syntax > semantics ***)


115 


116 
(* term_tr:term (name:string,trm:term) ersetzt in trm alle freien Variablen, die eine pvarID


117 
darstellen, durch name $ pvarID2pvar(pvarID). Beispiel:


118 
bei name="s" und dem Term "a=b & a=X" wird der Term "s(0)=s(Suc(0)) & s(0)=X" geliefert *)


119 


120 
fun term_tr (name,Free (s,t)) = if is_pvarID s

1476

121 
then Syntax.free name $ pvarID2pvar s


122 
else Free (s,t)

1335

123 
 term_tr (name,Abs (s,t,trm)) = Abs (s,t,term_tr (name,trm))

1476

124 
 term_tr (name,trm1 $ trm2) = term_tr (name,trm1) $ term_tr (name,trm2)

1335

125 
 term_tr (name,trm) = trm;


126 


127 
fun bool_tr B =


128 
let val name = variant_name("s",B)


129 
in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,B))) end;


130 


131 
fun exp_tr E =


132 
let val name = variant_name("s",E)


133 
in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,E))) end;


134 

1476

135 
fun prog_tr (Const ("@Skip",_)) = Syntax.const "Skip"

1335

136 
 prog_tr (Const ("@Assign",_) $ Free (V,_) $ E) =


137 
if is_pvarID V


138 
then Syntax.const "Assign" $ pvarID2pvar V $ exp_tr E


139 
else error("Not a valid program variable: " ^ quote V)

1476

140 
 prog_tr (Const ("@Seq",_) $ C $ C') =

1335

141 
Syntax.const "Seq" $ prog_tr C $ prog_tr C'


142 
 prog_tr (Const ("@If",_) $ B $ C $ C') =


143 
Syntax.const "Cond" $ bool_tr B $ prog_tr C $ prog_tr C'


144 
 prog_tr (Const ("@While",_) $ B $ INV $ C) =


145 
Syntax.const "While" $ bool_tr B $ bool_tr INV $ prog_tr C;


146 


147 
fun spec_tr [P,C,Q] = Syntax.const "Spec" $ bool_tr P $ prog_tr C $ bool_tr Q;


148 


149 
val parse_translation = [("@Spec",spec_tr)];


150 


151 


152 
(*** print translations: semantics > syntax ***)


153 


154 
(* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch


155 
entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:

1476

156 
bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)

1335

157 

1476

158 
fun term_tr' (name,Free (s,t) $ trm) =if name=s


159 
then Syntax.free (pvar2pvarID trm)


160 
else Free (s,t) $ term_tr' (name,trm)


161 
 term_tr' (name,Abs (s,t,trm)) =Abs (s,t,term_tr' (name,trm))


162 
 term_tr' (name,trm1 $ trm2) =term_tr' (name,trm1) $ term_tr' (name,trm2)


163 
 term_tr' (name,trm) =trm;

1335

164 

1476

165 
fun bexp_tr' (Abs(_,_,b)) =term_tr' (variant_abs ("s",dummyT,b));

1335

166 

1476

167 
fun exp_tr' (Abs(_,_,e)) =term_tr' (variant_abs ("s",dummyT,e));

1335

168 

1476

169 
fun com_tr' (Const ("Skip",_)) =Syntax.const "@Skip"


170 
 com_tr' (Const ("Assign",_) $ v $ e) =Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e


171 
 com_tr' (Const ("Seq",_) $ c $ c') =Syntax.const "@Seq" $ com_tr' c $ com_tr' c'


172 
 com_tr' (Const ("Cond",_) $ b $ c $ c') =Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'


173 
 com_tr' (Const ("While",_) $ b $ inv $ c) =Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;

1335

174 

1476

175 
fun spec_tr' [p,c,q] =Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;

1335

176 

1476

177 
val print_translation =[("Spec",spec_tr')];
