8177

1 
(* Title: HOL/IMPP/Natural.thy


2 
ID: $Id$


3 
Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM


4 
Copyright 1999 TUM


5 
*)


6 

17477

7 
header {* Natural semantics of commands *}


8 


9 
theory Natural


10 
imports Com


11 
begin

8177

12 


13 
(** Execution of commands **)


14 


15 
consts


16 
newlocs :: locals

17477

17 
setlocs :: "state => locals => state"


18 
getlocs :: "state => locals"


19 
update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900)

8177

20 
syntax (* IN Natural.thy *)

17477

21 
loc :: "state => locals" ("_<_>" [75,0] 75)

8177

22 
translations


23 
"s<X>" == "getlocs s X"


24 

23746

25 
inductive


26 
evalc :: "[com,state, state] => bool" ("<_,_>/ c> _" [0,0, 51] 51)


27 
where

17477

28 
Skip: "<SKIP,s> c> s"

8177

29 

23746

30 
 Assign: "<X :== a,s> c> s[X::=a s]"

8177

31 

23746

32 
 Local: "<c, s0[Loc Y::= a s0]> c> s1 ==>

17477

33 
<LOCAL Y := a IN c, s0> c> s1[Loc Y::=s0<Y>]"

8177

34 

23746

35 
 Semi: "[ <c0,s0> c> s1; <c1,s1> c> s2 ] ==>

17477

36 
<c0;; c1, s0> c> s2"

8177

37 

23746

38 
 IfTrue: "[ b s; <c0,s> c> s1 ] ==>

17477

39 
<IF b THEN c0 ELSE c1, s> c> s1"

8177

40 

23746

41 
 IfFalse: "[ ~b s; <c1,s> c> s1 ] ==>

17477

42 
<IF b THEN c0 ELSE c1, s> c> s1"

8177

43 

23746

44 
 WhileFalse: "~b s ==> <WHILE b DO c,s> c> s"

8177

45 

23746

46 
 WhileTrue: "[ b s0; <c,s0> c> s1; <WHILE b DO c, s1> c> s2 ] ==>

17477

47 
<WHILE b DO c, s0> c> s2"

8177

48 

23746

49 
 Body: "<the (body pn), s0> c> s1 ==>

17477

50 
<BODY pn, s0> c> s1"

8177

51 

23746

52 
 Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> c> s1 ==>

17477

53 
<X:=CALL pn(a), s0> c> (setlocs s1 (getlocs s0))


54 
[X::=s1<Res>]"

8177

55 

23746

56 
inductive


57 
evaln :: "[com,state,nat,state] => bool" ("<_,_>/ _> _" [0,0,0,51] 51)


58 
where

17477

59 
Skip: "<SKIP,s> n> s"


60 

23746

61 
 Assign: "<X :== a,s> n> s[X::=a s]"

8177

62 

23746

63 
 Local: "<c, s0[Loc Y::= a s0]> n> s1 ==>

17477

64 
<LOCAL Y := a IN c, s0> n> s1[Loc Y::=s0<Y>]"


65 

23746

66 
 Semi: "[ <c0,s0> n> s1; <c1,s1> n> s2 ] ==>

17477

67 
<c0;; c1, s0> n> s2"

8177

68 

23746

69 
 IfTrue: "[ b s; <c0,s> n> s1 ] ==>

17477

70 
<IF b THEN c0 ELSE c1, s> n> s1"

8177

71 

23746

72 
 IfFalse: "[ ~b s; <c1,s> n> s1 ] ==>

17477

73 
<IF b THEN c0 ELSE c1, s> n> s1"

8177

74 

23746

75 
 WhileFalse: "~b s ==> <WHILE b DO c,s> n> s"

17477

76 

23746

77 
 WhileTrue: "[ b s0; <c,s0> n> s1; <WHILE b DO c, s1> n> s2 ] ==>

17477

78 
<WHILE b DO c, s0> n> s2"

8177

79 

23746

80 
 Body: "<the (body pn), s0>  n> s1 ==>

17477

81 
<BODY pn, s0> Suc n> s1"

8177

82 

23746

83 
 Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> n> s1 ==>

17477

84 
<X:=CALL pn(a), s0> n> (setlocs s1 (getlocs s0))


85 
[X::=s1<Res>]"

8177

86 


87 

17477

88 
inductive_cases evalc_elim_cases:


89 
"<SKIP,s> c> t" "<X:==a,s> c> t" "<LOCAL Y:=a IN c,s> c> t"


90 
"<c1;;c2,s> c> t" "<IF b THEN c1 ELSE c2,s> c> t"


91 
"<BODY P,s> c> s1" "<X:=CALL P(a),s> c> s1"

8177

92 

17477

93 
inductive_cases evaln_elim_cases:


94 
"<SKIP,s> n> t" "<X:==a,s> n> t" "<LOCAL Y:=a IN c,s> n> t"


95 
"<c1;;c2,s> n> t" "<IF b THEN c1 ELSE c2,s> n> t"


96 
"<BODY P,s> n> s1" "<X:=CALL P(a),s> n> s1"


97 


98 
inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> c> t"


99 
inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> n> t"


100 

19803

101 
declare evalc.intros [intro]


102 
declare evaln.intros [intro]


103 


104 
declare evalc_elim_cases [elim!]


105 
declare evaln_elim_cases [elim!]


106 


107 
(* evaluation of com is deterministic *)


108 
lemma com_det [rule_format (no_asm)]: "<c,s> c> t ==> (!u. <c,s> c> u > u=t)"


109 
apply (erule evalc.induct)


110 
apply (erule_tac [8] V = "<?c,s1> c> s2" in thin_rl)


111 
(*blast_tac needs Unify.search_bound := 40*)


112 
apply (best elim: evalc_WHILE_case)+


113 
done


114 


115 
lemma evaln_evalc: "<c,s> n> t ==> <c,s> c> t"


116 
apply (erule evaln.induct)


117 
apply (tactic {* ALLGOALS (resolve_tac (thms "evalc.intros") THEN_ALL_NEW atac) *})


118 
done


119 


120 
lemma Suc_le_D_lemma: "[ Suc n <= m'; (!!m. n <= m ==> P (Suc m)) ] ==> P m'"


121 
apply (frule Suc_le_D)


122 
apply blast


123 
done


124 


125 
lemma evaln_nonstrict [rule_format]: "<c,s> n> t ==> !m. n<=m > <c,s> m> t"


126 
apply (erule evaln.induct)


127 
apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac (thm "Suc_le_D_lemma"), REPEAT o smp_tac 1]) *})


128 
apply (tactic {* ALLGOALS (resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})


129 
done


130 


131 
lemma evaln_Suc: "<c,s> n> s' ==> <c,s> Suc n> s'"


132 
apply (erule evaln_nonstrict)


133 
apply auto


134 
done


135 


136 
lemma evaln_max2: "[ <c1,s1> n1> t1; <c2,s2> n2> t2 ] ==>


137 
? n. <c1,s1> n > t1 & <c2,s2> n > t2"


138 
apply (cut_tac m = "n1" and n = "n2" in nat_le_linear)


139 
apply (blast dest: evaln_nonstrict)


140 
done


141 


142 
lemma evalc_evaln: "<c,s> c> t ==> ? n. <c,s> n> t"


143 
apply (erule evalc.induct)


144 
apply (tactic {* ALLGOALS (REPEAT o etac exE) *})


145 
apply (tactic {* TRYALL (EVERY'[datac (thm "evaln_max2") 1, REPEAT o eresolve_tac [exE, conjE]]) *})


146 
apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})


147 
done


148 


149 
lemma eval_eq: "<c,s> c> t = (? n. <c,s> n> t)"


150 
apply (fast elim: evalc_evaln evaln_evalc)


151 
done

17477

152 

8177

153 
end
