src/HOL/IMP/BExp.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45216 a51a70687517
child 45255 ffc06165d272
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
nipkow@43141
     1
theory BExp imports AExp begin
nipkow@43141
     2
nipkow@43141
     3
subsection "Boolean Expressions"
nipkow@43141
     4
nipkow@45200
     5
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
nipkow@43141
     6
nipkow@43141
     7
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
nipkow@45216
     8
"bval (Bc v) s = v" |
nipkow@43141
     9
"bval (Not b) s = (\<not> bval b s)" |
nipkow@43141
    10
"bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
nipkow@43141
    11
"bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
nipkow@43141
    12
nipkow@43141
    13
value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
kleing@44036
    14
            <''x'' := 3, ''y'' := 1>"
nipkow@43141
    15
nipkow@43141
    16
nipkow@43141
    17
subsection "Optimization"
nipkow@43141
    18
nipkow@43141
    19
text{* Optimized constructors: *}
nipkow@43141
    20
nipkow@43141
    21
fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
nipkow@45200
    22
"less (N n1) (N n2) = Bc(n1 < n2)" |
nipkow@43141
    23
"less a1 a2 = Less a1 a2"
nipkow@43141
    24
nipkow@43141
    25
lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
nipkow@45015
    26
apply(induction a1 a2 rule: less.induct)
nipkow@43141
    27
apply simp_all
nipkow@43141
    28
done
nipkow@43141
    29
nipkow@43141
    30
fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
nipkow@45200
    31
"and (Bc True) b = b" |
nipkow@45200
    32
"and b (Bc True) = b" |
nipkow@45200
    33
"and (Bc False) b = Bc False" |
nipkow@45200
    34
"and b (Bc False) = Bc False" |
nipkow@43141
    35
"and b1 b2 = And b1 b2"
nipkow@43141
    36
nipkow@43141
    37
lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
nipkow@45015
    38
apply(induction b1 b2 rule: and.induct)
nipkow@43141
    39
apply simp_all
nipkow@43141
    40
done
nipkow@43141
    41
nipkow@43141
    42
fun not :: "bexp \<Rightarrow> bexp" where
nipkow@45200
    43
"not (Bc True) = Bc False" |
nipkow@45200
    44
"not (Bc False) = Bc True" |
nipkow@43141
    45
"not b = Not b"
nipkow@43141
    46
nipkow@43141
    47
lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
nipkow@45015
    48
apply(induction b rule: not.induct)
nipkow@43141
    49
apply simp_all
nipkow@43141
    50
done
nipkow@43141
    51
nipkow@43141
    52
text{* Now the overall optimizer: *}
nipkow@43141
    53
nipkow@43141
    54
fun bsimp :: "bexp \<Rightarrow> bexp" where
nipkow@43141
    55
"bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" |
nipkow@43141
    56
"bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" |
nipkow@43141
    57
"bsimp (Not b) = not(bsimp b)" |
nipkow@45200
    58
"bsimp (Bc v) = Bc v"
nipkow@43141
    59
nipkow@43141
    60
value "bsimp (And (Less (N 0) (N 1)) b)"
nipkow@43141
    61
nipkow@43141
    62
value "bsimp (And (Less (N 1) (N 0)) (B True))"
nipkow@43141
    63
nipkow@43141
    64
theorem "bval (bsimp b) s = bval b s"
nipkow@45015
    65
apply(induction b)
nipkow@43141
    66
apply simp_all
nipkow@43141
    67
done
nipkow@43141
    68
nipkow@43141
    69
end