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