(* Title: HOL/IMPP/Natural.thy Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM *) section \Natural semantics of commands\ theory Natural imports Com begin (** Execution of commands **) consts newlocs :: locals setlocs :: "state => locals => state" getlocs :: "state => locals" update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900) abbreviation loc :: "state => locals" ("_<_>" [75,0] 75) where "s == getlocs s X" inductive evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51) where Skip: " -c-> s" | Assign: " -c-> s[X::=a s]" | Local: " -c-> s1 ==> -c-> s1[Loc Y::=s0]" | Semi: "[| -c-> s1; -c-> s2 |] ==> -c-> s2" | IfTrue: "[| b s; -c-> s1 |] ==> -c-> s1" | IfFalse: "[| ~b s; -c-> s1 |] ==> -c-> s1" | WhileFalse: "~b s ==> -c-> s" | WhileTrue: "[| b s0; -c-> s1; -c-> s2 |] ==> -c-> s2" | Body: " -c-> s1 ==> -c-> s1" | Call: " -c-> s1 ==> -c-> (setlocs s1 (getlocs s0)) [X::=s1]" inductive evaln :: "[com,state,nat,state] => bool" ("<_,_>/ -_-> _" [0,0,0,51] 51) where Skip: " -n-> s" | Assign: " -n-> s[X::=a s]" | Local: " -n-> s1 ==> -n-> s1[Loc Y::=s0]" | Semi: "[| -n-> s1; -n-> s2 |] ==> -n-> s2" | IfTrue: "[| b s; -n-> s1 |] ==> -n-> s1" | IfFalse: "[| ~b s; -n-> s1 |] ==> -n-> s1" | WhileFalse: "~b s ==> -n-> s" | WhileTrue: "[| b s0; -n-> s1; -n-> s2 |] ==> -n-> s2" | Body: " - n-> s1 ==> -Suc n-> s1" | Call: " -n-> s1 ==> -n-> (setlocs s1 (getlocs s0)) [X::=s1]" inductive_cases evalc_elim_cases: " -c-> t" " -c-> t" " -c-> t" " -c-> t" " -c-> t" " -c-> s1" " -c-> s1" inductive_cases evaln_elim_cases: " -n-> t" " -n-> t" " -n-> t" " -n-> t" " -n-> t" " -n-> s1" " -n-> s1" inductive_cases evalc_WHILE_case: " -c-> t" inductive_cases evaln_WHILE_case: " -n-> t" declare evalc.intros [intro] declare evaln.intros [intro] declare evalc_elim_cases [elim!] declare evaln_elim_cases [elim!] (* evaluation of com is deterministic *) lemma com_det [rule_format (no_asm)]: " -c-> t \ (\u. -c-> u \ u=t)" apply (erule evalc.induct) apply (erule_tac [8] V = " -c-> s2" for c in thin_rl) apply (blast elim: evalc_WHILE_case)+ done lemma evaln_evalc: " -n-> t ==> -c-> t" apply (erule evaln.induct) apply (tactic \ ALLGOALS (resolve_tac \<^context> @{thms evalc.intros} THEN_ALL_NEW assume_tac \<^context>) \) done lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'" apply (frule Suc_le_D) apply blast done lemma evaln_nonstrict [rule_format]: " -n-> t \ \m. n<=m \ -m-> t" apply (erule evaln.induct) apply (auto elim!: Suc_le_D_lemma) done lemma evaln_Suc: " -n-> s' ==> -Suc n-> s'" apply (erule evaln_nonstrict) apply auto done lemma evaln_max2: "[| -n1-> t1; -n2-> t2 |] ==> \n. -n -> t1 \ -n -> t2" apply (cut_tac m = "n1" and n = "n2" in nat_le_linear) apply (blast dest: evaln_nonstrict) done lemma evalc_evaln: " -c-> t \ \n. -n-> t" apply (erule evalc.induct) apply (tactic \ALLGOALS (REPEAT o eresolve_tac \<^context> [exE])\) apply (tactic \TRYALL (EVERY' [dresolve_tac \<^context> @{thms evaln_max2}, assume_tac \<^context>, REPEAT o eresolve_tac \<^context> [exE, conjE]])\) apply (tactic \ALLGOALS (resolve_tac \<^context> [exI] THEN' resolve_tac \<^context> @{thms evaln.intros} THEN_ALL_NEW assume_tac \<^context>)\) done lemma eval_eq: " -c-> t = (\n. -n-> t)" apply (fast elim: evalc_evaln evaln_evalc) done end