src/HOL/IMPP/Natural.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 41589 bbd861837ebc
child 46459 73823dbbecc4
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:      HOL/IMPP/Natural.thy
     2     Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     3 *)
     4 
     5 header {* Natural semantics of commands *}
     6 
     7 theory Natural
     8 imports Com
     9 begin
    10 
    11 (** Execution of commands **)
    12 
    13 consts
    14   newlocs :: locals
    15   setlocs :: "state => locals => state"
    16   getlocs :: "state => locals"
    17   update  :: "state => vname => val => state"     ("_/[_/::=/_]" [900,0,0] 900)
    18 
    19 abbreviation
    20   loc :: "state => locals"  ("_<_>" [75,0] 75) where
    21   "s<X> == getlocs s X"
    22 
    23 inductive
    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 
    54 inductive
    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 
    86 inductive_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 
    91 inductive_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 
    96 inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
    97 inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
    98 
    99 declare evalc.intros [intro]
   100 declare evaln.intros [intro]
   101 
   102 declare evalc_elim_cases [elim!]
   103 declare evaln_elim_cases [elim!]
   104 
   105 (* evaluation of com is deterministic *)
   106 lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
   107 apply (erule evalc.induct)
   108 apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
   109 (*blast needs unify_search_bound = 40*)
   110 apply (best elim: evalc_WHILE_case)+
   111 done
   112 
   113 lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
   114 apply (erule evaln.induct)
   115 apply (tactic {* ALLGOALS (resolve_tac @{thms evalc.intros} THEN_ALL_NEW atac) *})
   116 done
   117 
   118 lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
   119 apply (frule Suc_le_D)
   120 apply blast
   121 done
   122 
   123 lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"
   124 apply (erule evaln.induct)
   125 apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac @{thm Suc_le_D_lemma}, REPEAT o smp_tac 1]) *})
   126 apply (tactic {* ALLGOALS (resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
   127 done
   128 
   129 lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"
   130 apply (erule evaln_nonstrict)
   131 apply auto
   132 done
   133 
   134 lemma evaln_max2: "[| <c1,s1> -n1-> t1;  <c2,s2> -n2-> t2 |] ==>  
   135     ? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2"
   136 apply (cut_tac m = "n1" and n = "n2" in nat_le_linear)
   137 apply (blast dest: evaln_nonstrict)
   138 done
   139 
   140 lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
   141 apply (erule evalc.induct)
   142 apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
   143 apply (tactic {* TRYALL (EVERY' [datac @{thm evaln_max2} 1, REPEAT o eresolve_tac [exE, conjE]]) *})
   144 apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
   145 done
   146 
   147 lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)"
   148 apply (fast elim: evalc_evaln evaln_evalc)
   149 done
   150 
   151 end