43141

1 
theory BExp imports AExp begin


2 


3 
subsection "Boolean Expressions"


4 

45255

5 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbexpdef}{% *}

45200

6 
datatype bexp = Bc bool  Not bexp  And bexp bexp  Less aexp aexp

45255

7 
text_raw{*}\end{isaverbatimwrite}*}

43141

8 

45255

9 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbvaldef}{% *}

43141

10 
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where

45216

11 
"bval (Bc v) s = v" 

43141

12 
"bval (Not b) s = (\<not> bval b s)" 

45255

13 
"bval (And b\<^isub>1 b\<^isub>2) s = (bval b\<^isub>1 s \<and> bval b\<^isub>2 s)" 


14 
"bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)"


15 
text_raw{*}\end{isaverbatimwrite}*}

43141

16 


17 
value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))

44036

18 
<''x'' := 3, ''y'' := 1>"

43141

19 


20 

45255

21 
text{* To improve automation: *}

43141

22 

45255

23 
lemma bval_And_if[simp]:


24 
"bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)"


25 
by(simp)


26 


27 
declare bval.simps(3)[simp del] "remove the original eqn"


28 

43141

29 

45255

30 
subsection "Constant Folding"


31 


32 
text{* Optimizing constructors: *}


33 


34 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BExplessdef}{% *}

43141

35 
fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where

45255

36 
"less (N n\<^isub>1) (N n\<^isub>2) = Bc(n\<^isub>1 < n\<^isub>2)" 


37 
"less a\<^isub>1 a\<^isub>2 = Less a\<^isub>1 a\<^isub>2"


38 
text_raw{*}\end{isaverbatimwrite}*}

43141

39 


40 
lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"

45015

41 
apply(induction a1 a2 rule: less.induct)

43141

42 
apply simp_all


43 
done


44 

45255

45 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpanddef}{% *}

43141

46 
fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where

45200

47 
"and (Bc True) b = b" 


48 
"and b (Bc True) = b" 


49 
"and (Bc False) b = Bc False" 


50 
"and b (Bc False) = Bc False" 

45255

51 
"and b\<^isub>1 b\<^isub>2 = And b\<^isub>1 b\<^isub>2"


52 
text_raw{*}\end{isaverbatimwrite}*}

43141

53 


54 
lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"

45015

55 
apply(induction b1 b2 rule: and.induct)

43141

56 
apply simp_all


57 
done


58 

45255

59 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpnotdef}{% *}

43141

60 
fun not :: "bexp \<Rightarrow> bexp" where

45200

61 
"not (Bc True) = Bc False" 


62 
"not (Bc False) = Bc True" 

43141

63 
"not b = Not b"

45255

64 
text_raw{*}\end{isaverbatimwrite}*}

43141

65 

45255

66 
lemma bval_not[simp]: "bval (not b) s = (\<not> bval b s)"

45015

67 
apply(induction b rule: not.induct)

43141

68 
apply simp_all


69 
done


70 


71 
text{* Now the overall optimizer: *}


72 

45255

73 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbsimpdef}{% *}

43141

74 
fun bsimp :: "bexp \<Rightarrow> bexp" where

45256

75 
"bsimp (Bc v) = Bc v" 


76 
"bsimp (Not b) = not(bsimp b)" 

45255

77 
"bsimp (And b\<^isub>1 b\<^isub>2) = and (bsimp b\<^isub>1) (bsimp b\<^isub>2)" 

45256

78 
"bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)"

45255

79 
text_raw{*}\end{isaverbatimwrite}*}

43141

80 


81 
value "bsimp (And (Less (N 0) (N 1)) b)"


82 


83 
value "bsimp (And (Less (N 1) (N 0)) (B True))"


84 


85 
theorem "bval (bsimp b) s = bval b s"

45015

86 
apply(induction b)

43141

87 
apply simp_all


88 
done


89 


90 
end
