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
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Def_Ass_Small imports Star Com Def_Ass_Exp
     4 begin
     5 
     6 subsection "Initialization-Sensitive Small Step Semantics"
     7 
     8 inductive
     9   small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
    10 where
    11 Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
    12 
    13 Semi1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
    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')" |
    15 
    16 IfTrue:  "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
    17 IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
    18 
    19 While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
    20 
    21 lemmas small_step_induct = small_step.induct[split_format(complete)]
    22 
    23 abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
    24 where "x \<rightarrow>* y == star small_step x y"
    25 
    26 end