src/HOL/IMPP/Natural.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27362 a6dc1769fdda
child 39159 0dec18004e75
permissions -rw-r--r--
moved global ML bindings to global place;
     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 
     7 header {* Natural semantics of commands *}
     8 
     9 theory Natural
    10 imports Com
    11 begin
    12 
    13 (** Execution of commands **)
    14 
    15 consts
    16   newlocs :: locals
    17   setlocs :: "state => locals => state"
    18   getlocs :: "state => locals"
    19   update  :: "state => vname => val => state"     ("_/[_/::=/_]" [900,0,0] 900)
    20 
    21 abbreviation
    22   loc :: "state => locals"  ("_<_>" [75,0] 75) where
    23   "s<X> == getlocs s X"
    24 
    25 inductive
    26   evalc :: "[com,state,    state] => bool"  ("<_,_>/ -c-> _" [0,0,  51] 51)
    27   where
    28     Skip:    "<SKIP,s> -c-> s"
    29 
    30   | Assign:  "<X :== a,s> -c-> s[X::=a s]"
    31 
    32   | Local:   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
    33               <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
    34 
    35   | Semi:    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
    36               <c0;; c1, s0> -c-> s2"
    37 
    38   | IfTrue:  "[| b s; <c0,s> -c-> s1 |] ==>
    39               <IF b THEN c0 ELSE c1, s> -c-> s1"
    40 
    41   | IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==>
    42               <IF b THEN c0 ELSE c1, s> -c-> s1"
    43 
    44   | WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
    45 
    46   | WhileTrue:  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
    47                  <WHILE b DO c, s0> -c-> s2"
    48 
    49   | Body:       "<the (body pn), s0> -c-> s1 ==>
    50                  <BODY pn, s0> -c-> s1"
    51 
    52   | Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
    53                  <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
    54                                           [X::=s1<Res>]"
    55 
    56 inductive
    57   evaln :: "[com,state,nat,state] => bool"  ("<_,_>/ -_-> _" [0,0,0,51] 51)
    58   where
    59     Skip:    "<SKIP,s> -n-> s"
    60 
    61   | Assign:  "<X :== a,s> -n-> s[X::=a s]"
    62 
    63   | Local:   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
    64               <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
    65 
    66   | Semi:    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
    67               <c0;; c1, s0> -n-> s2"
    68 
    69   | IfTrue:  "[| b s; <c0,s> -n-> s1 |] ==>
    70               <IF b THEN c0 ELSE c1, s> -n-> s1"
    71 
    72   | IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
    73               <IF b THEN c0 ELSE c1, s> -n-> s1"
    74 
    75   | WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
    76 
    77   | WhileTrue:  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
    78                  <WHILE b DO c, s0> -n-> s2"
    79 
    80   | Body:       "<the (body pn), s0> -    n-> s1 ==>
    81                  <BODY pn, s0> -Suc n-> s1"
    82 
    83   | Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
    84                  <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
    85                                           [X::=s1<Res>]"
    86 
    87 
    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"
    92 
    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 
   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 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
   152 
   153 end