src/HOL/IMP/BExp.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 60170 031ec3d34d31
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
nipkow@43141
     1
theory BExp imports AExp begin
nipkow@43141
     2
nipkow@43141
     3
subsection "Boolean Expressions"
nipkow@43141
     4
blanchet@58310
     5
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
nipkow@43141
     6
nipkow@49191
     7
text_raw{*\snip{BExpbvaldef}{1}{2}{% *}
nipkow@43141
     8
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
nipkow@45216
     9
"bval (Bc v) s = v" |
nipkow@43141
    10
"bval (Not b) s = (\<not> bval b s)" |
wenzelm@53015
    11
"bval (And b\<^sub>1 b\<^sub>2) s = (bval b\<^sub>1 s \<and> bval b\<^sub>2 s)" |
wenzelm@53015
    12
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
nipkow@49191
    13
text_raw{*}%endsnip*}
nipkow@43141
    14
nipkow@43141
    15
value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
kleing@44036
    16
            <''x'' := 3, ''y'' := 1>"
nipkow@43141
    17
nipkow@43141
    18
nipkow@45255
    19
subsection "Constant Folding"
nipkow@45255
    20
nipkow@45255
    21
text{* Optimizing constructors: *}
nipkow@45255
    22
nipkow@49191
    23
text_raw{*\snip{BExplessdef}{0}{2}{% *}
nipkow@43141
    24
fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
wenzelm@53015
    25
"less (N n\<^sub>1) (N n\<^sub>2) = Bc(n\<^sub>1 < n\<^sub>2)" |
wenzelm@53015
    26
"less a\<^sub>1 a\<^sub>2 = Less a\<^sub>1 a\<^sub>2"
nipkow@49191
    27
text_raw{*}%endsnip*}
nipkow@43141
    28
nipkow@43141
    29
lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
nipkow@45015
    30
apply(induction a1 a2 rule: less.induct)
nipkow@43141
    31
apply simp_all
nipkow@43141
    32
done
nipkow@43141
    33
nipkow@49191
    34
text_raw{*\snip{BExpanddef}{2}{2}{% *}
nipkow@43141
    35
fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
nipkow@45200
    36
"and (Bc True) b = b" |
nipkow@45200
    37
"and b (Bc True) = b" |
nipkow@45200
    38
"and (Bc False) b = Bc False" |
nipkow@45200
    39
"and b (Bc False) = Bc False" |
wenzelm@53015
    40
"and b\<^sub>1 b\<^sub>2 = And b\<^sub>1 b\<^sub>2"
nipkow@49191
    41
text_raw{*}%endsnip*}
nipkow@43141
    42
nipkow@43141
    43
lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
nipkow@45015
    44
apply(induction b1 b2 rule: and.induct)
nipkow@43141
    45
apply simp_all
nipkow@43141
    46
done
nipkow@43141
    47
nipkow@49191
    48
text_raw{*\snip{BExpnotdef}{2}{2}{% *}
nipkow@43141
    49
fun not :: "bexp \<Rightarrow> bexp" where
nipkow@45200
    50
"not (Bc True) = Bc False" |
nipkow@45200
    51
"not (Bc False) = Bc True" |
nipkow@43141
    52
"not b = Not b"
nipkow@49191
    53
text_raw{*}%endsnip*}
nipkow@43141
    54
nipkow@45255
    55
lemma bval_not[simp]: "bval (not b) s = (\<not> bval b s)"
nipkow@45015
    56
apply(induction b rule: not.induct)
nipkow@43141
    57
apply simp_all
nipkow@43141
    58
done
nipkow@43141
    59
nipkow@43141
    60
text{* Now the overall optimizer: *}
nipkow@43141
    61
nipkow@49191
    62
text_raw{*\snip{BExpbsimpdef}{0}{2}{% *}
nipkow@43141
    63
fun bsimp :: "bexp \<Rightarrow> bexp" where
nipkow@45256
    64
"bsimp (Bc v) = Bc v" |
nipkow@45256
    65
"bsimp (Not b) = not(bsimp b)" |
wenzelm@53015
    66
"bsimp (And b\<^sub>1 b\<^sub>2) = and (bsimp b\<^sub>1) (bsimp b\<^sub>2)" |
wenzelm@53015
    67
"bsimp (Less a\<^sub>1 a\<^sub>2) = less (asimp a\<^sub>1) (asimp a\<^sub>2)"
nipkow@49191
    68
text_raw{*}%endsnip*}
nipkow@43141
    69
nipkow@43141
    70
value "bsimp (And (Less (N 0) (N 1)) b)"
nipkow@43141
    71
nipkow@49920
    72
value "bsimp (And (Less (N 1) (N 0)) (Bc True))"
nipkow@43141
    73
nipkow@43141
    74
theorem "bval (bsimp b) s = bval b s"
nipkow@45015
    75
apply(induction b)
nipkow@43141
    76
apply simp_all
nipkow@43141
    77
done
nipkow@43141
    78
nipkow@43141
    79
end