src/HOL/IMP/Def_Ass_Small.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 43158 686fa0a0696e
child 47818 151d137f1095
permissions -rw-r--r--
remove lemma stupid_ext
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
kleing@43158
     3
theory Def_Ass_Small imports Star Com Def_Ass_Exp
kleing@43158
     4
begin
kleing@43158
     5
kleing@43158
     6
subsection "Initialization-Sensitive Small Step Semantics"
kleing@43158
     7
kleing@43158
     8
inductive
kleing@43158
     9
  small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
kleing@43158
    10
where
kleing@43158
    11
Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
kleing@43158
    12
kleing@43158
    13
Semi1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
kleing@43158
    14
Semi2:   "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" |
kleing@43158
    15
kleing@43158
    16
IfTrue:  "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
kleing@43158
    17
IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
kleing@43158
    18
kleing@43158
    19
While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
kleing@43158
    20
kleing@43158
    21
lemmas small_step_induct = small_step.induct[split_format(complete)]
kleing@43158
    22
kleing@43158
    23
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
kleing@43158
    24
where "x \<rightarrow>* y == star small_step x y"
kleing@43158
    25
kleing@43158
    26
end