src/HOL/IMP/Big_Step.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45324 4ef9220b886b
child 47818 151d137f1095
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     1
(* Author: Gerwin Klein, Tobias Nipkow *)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     2
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     3
theory Big_Step imports Com begin
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     4
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     5
subsection "Big-Step Semantics of Commands"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     6
45321
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
     7
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepdef}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     8
inductive
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     9
  big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    10
where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    11
Skip:    "(SKIP,s) \<Rightarrow> s" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    12
Assign:  "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    13
Semi:    "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    14
          (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    15
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    16
IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    17
         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    18
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    19
         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    20
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    21
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    22
WhileTrue:  "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    23
             (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
45321
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
    24
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    25
45324
4ef9220b886b more IMP fragments
kleing
parents: 45321
diff changeset
    26
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEx}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    27
schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    28
apply(rule Semi)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    29
apply(rule Assign)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    30
apply simp
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    31
apply(rule Assign)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    32
done
45324
4ef9220b886b more IMP fragments
kleing
parents: 45321
diff changeset
    33
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    34
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    35
thm ex[simplified]
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    36
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    37
text{* We want to execute the big-step rules: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    38
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    39
code_pred big_step .
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    40
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    41
text{* For inductive definitions we need command
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    42
       \texttt{values} instead of \texttt{value}. *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    43
44923
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44070
diff changeset
    44
values "{t. (SKIP, \<lambda>_. 0) \<Rightarrow> t}"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    45
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    46
text{* We need to translate the result state into a list
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    47
to display it. *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    48
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43158
diff changeset
    49
values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \<Rightarrow> t}"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    50
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43158
diff changeset
    51
values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) \<Rightarrow> t}"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    52
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    53
values "{map t [''x'',''y''] |t.
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    54
  (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43158
diff changeset
    55
   <''x'' := 0, ''y'' := 13>) \<Rightarrow> t}"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    56
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    57
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    58
text{* Proof automation: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    59
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    60
declare big_step.intros [intro]
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    61
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    62
text{* The standard induction rule 
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    63
@{thm [display] big_step.induct [no_vars]} *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    64
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    65
thm big_step.induct
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    66
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    67
text{* A customized induction rule for (c,s) pairs: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    68
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    69
lemmas big_step_induct = big_step.induct[split_format(complete)]
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    70
thm big_step_induct
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    71
text {*
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    72
@{thm [display] big_step_induct [no_vars]}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    73
*}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    74
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    75
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    76
subsection "Rule inversion"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    77
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    78
text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    79
That @{prop "s = t"}. This is how we can automatically prove it: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    80
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    81
inductive_cases skipE[elim!]: "(SKIP,s) \<Rightarrow> t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    82
thm skipE
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    83
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    84
text{* This is an \emph{elimination rule}. The [elim] attribute tells auto,
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    85
blast and friends (but not simp!) to use it automatically; [elim!] means that
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    86
it is applied eagerly.
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    87
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    88
Similarly for the other commands: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    89
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    90
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    91
thm AssignE
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    92
inductive_cases SemiE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    93
thm SemiE
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    94
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    95
thm IfE
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    96
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    97
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    98
thm WhileE
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    99
text{* Only [elim]: [elim!] would not terminate. *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   100
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   101
text{* An automatic example: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   102
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   103
lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   104
by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   105
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   106
text{* Rule inversion by hand via the ``cases'' method: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   107
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   108
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   109
shows "t = s"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   110
proof-
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   111
  from assms show ?thesis
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   112
  proof cases  --"inverting assms"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   113
    case IfTrue thm IfTrue
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   114
    thus ?thesis by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   115
  next
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   116
    case IfFalse thus ?thesis by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   117
  qed
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   118
qed
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   119
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents: 44036
diff changeset
   120
(* Using rule inversion to prove simplification rules: *)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents: 44036
diff changeset
   121
lemma assign_simp:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents: 44036
diff changeset
   122
  "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents: 44036
diff changeset
   123
  by auto
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   124
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   125
subsection "Command Equivalence"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   126
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   127
text {*
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   128
  We call two statements @{text c} and @{text c'} equivalent wrt.\ the
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   129
  big-step semantics when \emph{@{text c} started in @{text s} terminates
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   130
  in @{text s'} iff @{text c'} started in the same @{text s} also terminates
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   131
  in the same @{text s'}}. Formally:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   132
*}
45321
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
   133
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEquiv}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   134
abbreviation
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   135
  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   136
  "c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"
45321
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
   137
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   138
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   139
text {*
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   140
Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   142
  As an example, we show that loop unfolding is an equivalence
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   143
  transformation on programs:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   144
*}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   145
lemma unfold_while:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   146
  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   147
proof -
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   148
  -- "to show the equivalence, we look at the derivation tree for"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   149
  -- "each side and from that construct a derivation tree for the other side"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   150
  { fix s t assume "(?w, s) \<Rightarrow> t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   151
    -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   152
    -- "then both statements do nothing:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   153
    { assume "\<not>bval b s"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   154
      hence "t = s" using `(?w,s) \<Rightarrow> t` by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   155
      hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   156
    }
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   157
    moreover
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   158
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   159
    -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   160
    { assume "bval b s"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   161
      with `(?w, s) \<Rightarrow> t` obtain s' where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   162
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   163
      -- "now we can build a derivation tree for the @{text IF}"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   164
      -- "first, the body of the True-branch:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   165
      hence "(c; ?w, s) \<Rightarrow> t" by (rule Semi)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   166
      -- "then the whole @{text IF}"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   167
      with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   168
    }
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   169
    ultimately
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   170
    -- "both cases together give us what we want:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   171
    have "(?iw, s) \<Rightarrow> t" by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   172
  }
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   173
  moreover
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   174
  -- "now the other direction:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   175
  { fix s t assume "(?iw, s) \<Rightarrow> t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   176
    -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   177
    -- "of the @{text IF} is executed, and both statements do nothing:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   178
    { assume "\<not>bval b s"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   179
      hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   180
      hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   181
    }
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   182
    moreover
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   183
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   184
    -- {* then this time only the @{text IfTrue} rule can have be used *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   185
    { assume "bval b s"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   186
      with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   187
      -- "and for this, only the Semi-rule is applicable:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   188
      then obtain s' where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   189
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   190
      -- "with this information, we can build a derivation tree for the @{text WHILE}"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   191
      with `bval b s`
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   192
      have "(?w, s) \<Rightarrow> t" by (rule WhileTrue)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   193
    }
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   194
    ultimately
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   195
    -- "both cases together again give us what we want:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   196
    have "(?w, s) \<Rightarrow> t" by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   197
  }
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   198
  ultimately
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   199
  show ?thesis by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   200
qed
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   201
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   202
text {* Luckily, such lengthy proofs are seldom necessary.  Isabelle can
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   203
prove many such facts automatically.  *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   204
45321
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
   205
lemma while_unfold:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   206
  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   207
by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   208
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   209
lemma triv_if:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   210
  "(IF b THEN c ELSE c) \<sim> c"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   211
by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   212
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   213
lemma commute_if:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   214
  "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2) 
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   215
   \<sim> 
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   216
   (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   217
by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   218
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   219
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   220
subsection "Execution is deterministic"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   221
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   222
text {* This proof is automatic. *}
45321
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
   223
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepDeterministic}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   224
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
45321
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
   225
  by (induction arbitrary: u rule: big_step.induct) blast+
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
   226
text_raw{*}\end{isaverbatimwrite}*}
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
   227
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   228
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   229
text {*
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   230
  This is the proof as you might present it in a lecture. The remaining
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   231
  cases are simple enough to be proved automatically:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   232
*}
45324
4ef9220b886b more IMP fragments
kleing
parents: 45321
diff changeset
   233
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepDetLong}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   234
theorem
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   235
  "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   236
proof (induction arbitrary: t' rule: big_step.induct)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   237
  -- "the only interesting case, @{text WhileTrue}:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   238
  fix b c s s1 t t'
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   239
  -- "The assumptions of the rule:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   240
  assume "bval b s" and "(c,s) \<Rightarrow> s1" and "(WHILE b DO c,s1) \<Rightarrow> t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   241
  -- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   242
  assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s1"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   243
  assume IHw: "\<And>t'. (WHILE b DO c,s1) \<Rightarrow> t' \<Longrightarrow> t' = t"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   244
  -- "Premise of implication:"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   245
  assume "(WHILE b DO c,s) \<Rightarrow> t'"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   246
  with `bval b s` obtain s1' where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   247
      c: "(c,s) \<Rightarrow> s1'" and
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   248
      w: "(WHILE b DO c,s1') \<Rightarrow> t'"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   249
    by auto
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   250
  from c IHc have "s1' = s1" by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   251
  with w IHw show "t' = t" by blast
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   252
qed blast+ -- "prove the rest automatically"
45321
b227989b6ee6 more IMP text fragments
kleing
parents: 45015
diff changeset
   253
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   254
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   255
end