src/HOL/Hoare/Hoare.thy
author nipkow
Fri Nov 17 09:04:10 1995 +0100 (1995-11-17)
changeset 1335 5e1c0540f285
child 1374 5e407f2a3323
permissions -rw-r--r--
New directory.
Hoare logic according to Mike Gordon.
nipkow@1335
     1
(*  Title: 	HOL/Hoare/Hoare.thy
nipkow@1335
     2
    ID:         $Id$
nipkow@1335
     3
    Author: 	Norbert Galm & Tobias Nipkow
nipkow@1335
     4
    Copyright   1995 TUM
nipkow@1335
     5
nipkow@1335
     6
Sugared semantic embedding of Hoare logic.
nipkow@1335
     7
*)
nipkow@1335
     8
nipkow@1335
     9
Hoare = Arith +
nipkow@1335
    10
nipkow@1335
    11
types
nipkow@1335
    12
  'a prog			(* program syntax *)
nipkow@1335
    13
  pvar = "nat"			(* encoding of program variables ( < 26! ) *)
nipkow@1335
    14
  'a state = "pvar => 'a"	(* program state *)
nipkow@1335
    15
  'a exp ="'a state => 'a"	(* denotation of expressions *)
nipkow@1335
    16
  'a bexp = "'a state => bool"  (* denotation of boolean expressions *)
nipkow@1335
    17
  'a com = "'a state => 'a state => bool" (* denotation of programs *)
nipkow@1335
    18
nipkow@1335
    19
syntax
nipkow@1335
    20
  "@Skip"       :: "'a prog"				("SKIP")
nipkow@1335
    21
  "@Assign"	:: "[id, 'a] => 'a prog"		("_ := _")
nipkow@1335
    22
  "@Seq"	:: "['a prog, 'a prog] => 'a prog"	("_;//_" [0,1000] 999)
nipkow@1335
    23
  "@If"		:: "[bool, 'a prog, 'a prog] => 'a prog"
nipkow@1335
    24
                   ("IF _//THEN//  (_)//ELSE//  (_)//END")
nipkow@1335
    25
  "@While"	:: "[bool, bool, 'a prog] => 'a prog"
nipkow@1335
    26
                   ("WHILE _//DO {_}//  (_)//END")
nipkow@1335
    27
nipkow@1335
    28
  "@Spec"	:: "[bool, 'a prog, bool] => bool"	("{_}//_//{_}")
nipkow@1335
    29
nipkow@1335
    30
consts
nipkow@1335
    31
  (* semantics *)
nipkow@1335
    32
nipkow@1335
    33
  Skip		:: "'a com"
nipkow@1335
    34
  Assign	:: "[pvar, 'a exp] => 'a com"
nipkow@1335
    35
  Seq		:: "['a com, 'a com] => 'a com"
nipkow@1335
    36
  Cond		:: "['a bexp, 'a com, 'a com] => 'a com"
nipkow@1335
    37
  While		:: "['a bexp, 'a bexp, 'a com] => 'a com"
nipkow@1335
    38
  Iter		:: "[nat, 'a bexp, 'a com] => 'a com"
nipkow@1335
    39
nipkow@1335
    40
  Spec		:: "['a bexp, 'a com, 'a bexp] => bool"
nipkow@1335
    41
nipkow@1335
    42
defs
nipkow@1335
    43
  (* denotational semantics *)
nipkow@1335
    44
nipkow@1335
    45
  SkipDef	"Skip s s' == (s=s')"
nipkow@1335
    46
  AssignDef	"Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
nipkow@1335
    47
  SeqDef	"Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
nipkow@1335
    48
  CondDef	"Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
nipkow@1335
    49
  WhileDef	"While b inv c s s' == ? n. Iter n b c s s'"
nipkow@1335
    50
nipkow@1335
    51
  IterDef	"Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
nipkow@1335
    52
		           (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
nipkow@1335
    53
nipkow@1335
    54
  SpecDef	"Spec p c q == !s s'. c s s' --> p s --> q s'"
nipkow@1335
    55
nipkow@1335
    56
end
nipkow@1335
    57
nipkow@1335
    58
ML
nipkow@1335
    59
nipkow@1335
    60
nipkow@1335
    61
(*** term manipulation ***)
nipkow@1335
    62
nipkow@1335
    63
(* name_in_term:bool (name:string,trm:term) bestimmt, ob in trm der Name name als Konstante,
nipkow@1335
    64
   freie Var., scheme-Variable oder als Name fuer eine Lambda-Abstraktion vorkommt *)
nipkow@1335
    65
nipkow@1335
    66
fun name_in_term (name,Const (s,t))	=(name=s)
nipkow@1335
    67
  | name_in_term (name,Free (s,t))	=(name=s)
nipkow@1335
    68
  | name_in_term (name,Var ((s,i),t))	=(name=s ^ makestring i)
nipkow@1335
    69
  | name_in_term (name,Abs (s,t,trm))	=(name=s) orelse (name_in_term (name,trm))
nipkow@1335
    70
  | name_in_term (name,trm1 $ trm2)	=(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
nipkow@1335
    71
  | name_in_term (_,_)			=false;
nipkow@1335
    72
nipkow@1335
    73
(* variant_name:string (name:string,trm:term) liefert einen von name abgewandelten Namen (durch Anhaengen
nipkow@1335
    74
   von genuegend vielen "_"), der nicht in trm vorkommt. Im Gegensatz zu variant_abs beruecktsichtigt es
nipkow@1335
    75
   auch Namen von scheme-Variablen und von Lambda-Abstraktionen in trm *)
nipkow@1335
    76
nipkow@1335
    77
fun variant_name (name,trm)	=if name_in_term (name,trm)
nipkow@1335
    78
					then variant_name (name ^ "_",trm)
nipkow@1335
    79
					else name;
nipkow@1335
    80
nipkow@1335
    81
(* subst_term:term (von:term,nach:term,trm:term) liefert den Term, der aus
nipkow@1335
    82
trm entsteht, wenn alle Teilterme, die gleich von sind, durch nach ersetzt
nipkow@1335
    83
wurden *)
nipkow@1335
    84
nipkow@1335
    85
fun subst_term (von,nach,Abs (s,t,trm))	=if von=Abs (s,t,trm)
nipkow@1335
    86
						then nach
nipkow@1335
    87
						else Abs (s,t,subst_term (von,nach,trm))
nipkow@1335
    88
  | subst_term (von,nach,trm1 $ trm2)	=if von=trm1 $ trm2
nipkow@1335
    89
						then nach
nipkow@1335
    90
						else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)
nipkow@1335
    91
  | subst_term (von,nach,trm)		=if von=trm
nipkow@1335
    92
						then nach
nipkow@1335
    93
						else trm;
nipkow@1335
    94
nipkow@1335
    95
nipkow@1335
    96
(* Translation between program vars ("a" - "z") and their encoding as
nipkow@1335
    97
   natural numbers: "a" <==> 0, "b" <==> Suc(0), ..., "z" <==> 25 *)
nipkow@1335
    98
nipkow@1335
    99
fun is_pvarID s	= size s=1 andalso "a"<=s andalso s<="z";
nipkow@1335
   100
nipkow@1335
   101
fun pvarID2pvar s =
nipkow@1335
   102
  let fun rest2pvar (i,arg) =
nipkow@1335
   103
            if i=0 then arg else rest2pvar(i-1, Syntax.const "Suc" $ arg)
nipkow@1335
   104
  in rest2pvar(ord s - ord "a", Syntax.const "0") end;
nipkow@1335
   105
nipkow@1335
   106
fun pvar2pvarID trm	=
nipkow@1335
   107
	let
nipkow@1335
   108
		fun rest2pvarID (Const("0",_),i)		=chr (i + ord "a")
nipkow@1335
   109
		  | rest2pvarID (Const("Suc",_) $ trm,i)	=rest2pvarID (trm,i+1)
nipkow@1335
   110
	in
nipkow@1335
   111
		rest2pvarID (trm,0)
nipkow@1335
   112
	end;
nipkow@1335
   113
nipkow@1335
   114
nipkow@1335
   115
(*** parse translations: syntax -> semantics ***)
nipkow@1335
   116
nipkow@1335
   117
(* term_tr:term (name:string,trm:term) ersetzt in trm alle freien Variablen, die eine pvarID
nipkow@1335
   118
   darstellen, durch name $ pvarID2pvar(pvarID). Beispiel:
nipkow@1335
   119
   bei name="s" und dem Term "a=b & a=X" wird der Term "s(0)=s(Suc(0)) & s(0)=X" geliefert *)
nipkow@1335
   120
nipkow@1335
   121
fun term_tr (name,Free (s,t)) = if is_pvarID s
nipkow@1335
   122
				then Syntax.free name $ pvarID2pvar s
nipkow@1335
   123
				else Free (s,t)
nipkow@1335
   124
  | term_tr (name,Abs (s,t,trm)) = Abs (s,t,term_tr (name,trm))
nipkow@1335
   125
  | term_tr (name,trm1 $ trm2)	= term_tr (name,trm1) $ term_tr (name,trm2)
nipkow@1335
   126
  | term_tr (name,trm) = trm;
nipkow@1335
   127
nipkow@1335
   128
fun bool_tr B =
nipkow@1335
   129
  let val name = variant_name("s",B)
nipkow@1335
   130
  in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,B))) end;
nipkow@1335
   131
nipkow@1335
   132
fun exp_tr E =
nipkow@1335
   133
  let val name = variant_name("s",E)
nipkow@1335
   134
  in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,E))) end;
nipkow@1335
   135
nipkow@1335
   136
fun prog_tr (Const ("@Skip",_))	= Syntax.const "Skip"
nipkow@1335
   137
  | prog_tr (Const ("@Assign",_) $ Free (V,_) $ E) =
nipkow@1335
   138
      if is_pvarID V
nipkow@1335
   139
      then Syntax.const "Assign" $ pvarID2pvar V $ exp_tr E
nipkow@1335
   140
      else error("Not a valid program variable: " ^ quote V)
nipkow@1335
   141
  | prog_tr (Const ("@Seq",_) $ C $ C')	=
nipkow@1335
   142
      Syntax.const "Seq" $ prog_tr C $ prog_tr C'
nipkow@1335
   143
  | prog_tr (Const ("@If",_) $ B $ C $ C') =
nipkow@1335
   144
      Syntax.const "Cond" $ bool_tr B $ prog_tr C $ prog_tr C'
nipkow@1335
   145
  | prog_tr (Const ("@While",_) $ B $ INV $ C) =
nipkow@1335
   146
      Syntax.const "While" $ bool_tr B $ bool_tr INV $ prog_tr C;
nipkow@1335
   147
nipkow@1335
   148
fun spec_tr [P,C,Q] = Syntax.const "Spec" $ bool_tr P $ prog_tr C $ bool_tr Q;
nipkow@1335
   149
nipkow@1335
   150
val parse_translation = [("@Spec",spec_tr)];
nipkow@1335
   151
nipkow@1335
   152
nipkow@1335
   153
(*** print translations: semantics -> syntax ***)
nipkow@1335
   154
nipkow@1335
   155
(* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch
nipkow@1335
   156
   entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:
nipkow@1335
   157
	bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)
nipkow@1335
   158
nipkow@1335
   159
fun term_tr' (name,Free (s,t) $ trm)	=if name=s
nipkow@1335
   160
						then Syntax.free (pvar2pvarID trm)
nipkow@1335
   161
						else Free (s,t) $ term_tr' (name,trm)
nipkow@1335
   162
  | term_tr' (name,Abs (s,t,trm))	=Abs (s,t,term_tr' (name,trm))
nipkow@1335
   163
  | term_tr' (name,trm1 $ trm2)		=term_tr' (name,trm1) $ term_tr' (name,trm2)
nipkow@1335
   164
  | term_tr' (name,trm)			=trm;
nipkow@1335
   165
nipkow@1335
   166
fun bexp_tr' (Abs(_,_,b))	=term_tr' (variant_abs ("s",dummyT,b));
nipkow@1335
   167
nipkow@1335
   168
fun exp_tr' (Abs(_,_,e))	=term_tr' (variant_abs ("s",dummyT,e));
nipkow@1335
   169
nipkow@1335
   170
fun com_tr' (Const ("Skip",_))			=Syntax.const "@Skip"
nipkow@1335
   171
  | com_tr' (Const ("Assign",_) $ v $ e)		=Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e
nipkow@1335
   172
  | com_tr' (Const ("Seq",_) $ c $ c')		=Syntax.const "@Seq" $ com_tr' c $ com_tr' c'
nipkow@1335
   173
  | com_tr' (Const ("Cond",_) $ b $ c $ c')		=Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'
nipkow@1335
   174
  | com_tr' (Const ("While",_) $ b $ inv $ c)	=Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;
nipkow@1335
   175
nipkow@1335
   176
fun spec_tr' [p,c,q]		=Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
nipkow@1335
   177
nipkow@1335
   178
val print_translation	=[("Spec",spec_tr')];