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