1(* Title: HOL/IMPP/Natural.thy 2 Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM 3*) 4 5section \<open>Natural semantics of commands\<close> 6 7theory Natural 8imports Com 9begin 10 11(** Execution of commands **) 12 13consts 14 newlocs :: locals 15 setlocs :: "state => locals => state" 16 getlocs :: "state => locals" 17 update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900) 18 19abbreviation 20 loc :: "state => locals" ("_<_>" [75,0] 75) where 21 "s<X> == getlocs s X" 22 23inductive 24 evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51) 25 where 26 Skip: "<SKIP,s> -c-> s" 27 28 | Assign: "<X :== a,s> -c-> s[X::=a s]" 29 30 | Local: "<c, s0[Loc Y::= a s0]> -c-> s1 ==> 31 <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]" 32 33 | Semi: "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==> 34 <c0;; c1, s0> -c-> s2" 35 36 | IfTrue: "[| b s; <c0,s> -c-> s1 |] ==> 37 <IF b THEN c0 ELSE c1, s> -c-> s1" 38 39 | IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==> 40 <IF b THEN c0 ELSE c1, s> -c-> s1" 41 42 | WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s" 43 44 | WhileTrue: "[| b s0; <c,s0> -c-> s1; <WHILE b DO c, s1> -c-> s2 |] ==> 45 <WHILE b DO c, s0> -c-> s2" 46 47 | Body: "<the (body pn), s0> -c-> s1 ==> 48 <BODY pn, s0> -c-> s1" 49 50 | Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==> 51 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0)) 52 [X::=s1<Res>]" 53 54inductive 55 evaln :: "[com,state,nat,state] => bool" ("<_,_>/ -_-> _" [0,0,0,51] 51) 56 where 57 Skip: "<SKIP,s> -n-> s" 58 59 | Assign: "<X :== a,s> -n-> s[X::=a s]" 60 61 | Local: "<c, s0[Loc Y::= a s0]> -n-> s1 ==> 62 <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]" 63 64 | Semi: "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==> 65 <c0;; c1, s0> -n-> s2" 66 67 | IfTrue: "[| b s; <c0,s> -n-> s1 |] ==> 68 <IF b THEN c0 ELSE c1, s> -n-> s1" 69 70 | IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==> 71 <IF b THEN c0 ELSE c1, s> -n-> s1" 72 73 | WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s" 74 75 | WhileTrue: "[| b s0; <c,s0> -n-> s1; <WHILE b DO c, s1> -n-> s2 |] ==> 76 <WHILE b DO c, s0> -n-> s2" 77 78 | Body: "<the (body pn), s0> - n-> s1 ==> 79 <BODY pn, s0> -Suc n-> s1" 80 81 | Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==> 82 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0)) 83 [X::=s1<Res>]" 84 85 86inductive_cases evalc_elim_cases: 87 "<SKIP,s> -c-> t" "<X:==a,s> -c-> t" "<LOCAL Y:=a IN c,s> -c-> t" 88 "<c1;;c2,s> -c-> t" "<IF b THEN c1 ELSE c2,s> -c-> t" 89 "<BODY P,s> -c-> s1" "<X:=CALL P(a),s> -c-> s1" 90 91inductive_cases evaln_elim_cases: 92 "<SKIP,s> -n-> t" "<X:==a,s> -n-> t" "<LOCAL Y:=a IN c,s> -n-> t" 93 "<c1;;c2,s> -n-> t" "<IF b THEN c1 ELSE c2,s> -n-> t" 94 "<BODY P,s> -n-> s1" "<X:=CALL P(a),s> -n-> s1" 95 96inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t" 97inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t" 98 99declare evalc.intros [intro] 100declare evaln.intros [intro] 101 102declare evalc_elim_cases [elim!] 103declare evaln_elim_cases [elim!] 104 105(* evaluation of com is deterministic *) 106lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t \<Longrightarrow> (\<forall>u. <c,s> -c-> u \<longrightarrow> u=t)" 107apply (erule evalc.induct) 108apply (erule_tac [8] V = "<c,s1> -c-> s2" for c in thin_rl) 109apply (blast elim: evalc_WHILE_case)+ 110done 111 112lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t" 113apply (erule evaln.induct) 114apply (tactic \<open> 115 ALLGOALS (resolve_tac \<^context> @{thms evalc.intros} THEN_ALL_NEW assume_tac \<^context>) 116\<close>) 117done 118 119lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'" 120apply (frule Suc_le_D) 121apply blast 122done 123 124lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t \<Longrightarrow> \<forall>m. n<=m \<longrightarrow> <c,s> -m-> t" 125apply (erule evaln.induct) 126apply (auto elim!: Suc_le_D_lemma) 127done 128 129lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'" 130apply (erule evaln_nonstrict) 131apply auto 132done 133 134lemma evaln_max2: "[| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 |] ==> 135 \<exists>n. <c1,s1> -n -> t1 \<and> <c2,s2> -n -> t2" 136apply (cut_tac m = "n1" and n = "n2" in nat_le_linear) 137apply (blast dest: evaln_nonstrict) 138done 139 140lemma evalc_evaln: "<c,s> -c-> t \<Longrightarrow> \<exists>n. <c,s> -n-> t" 141apply (erule evalc.induct) 142apply (tactic \<open>ALLGOALS (REPEAT o eresolve_tac \<^context> [exE])\<close>) 143apply (tactic \<open>TRYALL (EVERY' [dresolve_tac \<^context> @{thms evaln_max2}, assume_tac \<^context>, 144 REPEAT o eresolve_tac \<^context> [exE, conjE]])\<close>) 145apply (tactic 146 \<open>ALLGOALS (resolve_tac \<^context> [exI] THEN' 147 resolve_tac \<^context> @{thms evaln.intros} THEN_ALL_NEW assume_tac \<^context>)\<close>) 148done 149 150lemma eval_eq: "<c,s> -c-> t = (\<exists>n. <c,s> -n-> t)" 151apply (fast elim: evalc_evaln evaln_evalc) 152done 153 154end 155