1.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy Thu May 29 13:27:13 2008 +0200
1.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy Thu May 29 22:45:33 2008 +0200
1.3 @@ -35,56 +35,52 @@
1.4 The semantics is given by two evaluation functions:
1.5 *}
1.6
1.7 -consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
1.8 - evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool";
1.9 +primrec evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" and
1.10 + evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool" where
1.11 +"evala (IF b a1 a2) env =
1.12 + (if evalb b env then evala a1 env else evala a2 env)" |
1.13 +"evala (Sum a1 a2) env = evala a1 env + evala a2 env" |
1.14 +"evala (Diff a1 a2) env = evala a1 env - evala a2 env" |
1.15 +"evala (Var v) env = env v" |
1.16 +"evala (Num n) env = n" |
1.17 +
1.18 +"evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" |
1.19 +"evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)" |
1.20 +"evalb (Neg b) env = (\<not> evalb b env)"
1.21
1.22 text{*\noindent
1.23 -Both take an expression and an environment (a mapping from variables @{typ"'a"} to values
1.24 -@{typ"nat"}) and return its arithmetic/boolean
1.25 -value. Since the datatypes are mutually recursive, so are functions that
1.26 -operate on them. Hence they need to be defined in a single \isacommand{primrec}
1.27 -section:
1.28 -*}
1.29
1.30 -primrec
1.31 - "evala (IF b a1 a2) env =
1.32 - (if evalb b env then evala a1 env else evala a2 env)"
1.33 - "evala (Sum a1 a2) env = evala a1 env + evala a2 env"
1.34 - "evala (Diff a1 a2) env = evala a1 env - evala a2 env"
1.35 - "evala (Var v) env = env v"
1.36 - "evala (Num n) env = n"
1.37 +Both take an expression and an environment (a mapping from variables
1.38 +@{typ"'a"} to values @{typ"nat"}) and return its arithmetic/boolean
1.39 +value. Since the datatypes are mutually recursive, so are functions
1.40 +that operate on them. Hence they need to be defined in a single
1.41 +\isacommand{primrec} section. Notice the \isakeyword{and} separating
1.42 +the declarations of @{const evala} and @{const evalb}. Their defining
1.43 +equations need not be split into two groups;
1.44 +the empty line is purely for readability.
1.45
1.46 - "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
1.47 - "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)"
1.48 - "evalb (Neg b) env = (\<not> evalb b env)"
1.49 -
1.50 -text{*\noindent
1.51 In the same fashion we also define two functions that perform substitution:
1.52 *}
1.53
1.54 -consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
1.55 - substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp";
1.56 +primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp" and
1.57 + substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp" where
1.58 +"substa s (IF b a1 a2) =
1.59 + IF (substb s b) (substa s a1) (substa s a2)" |
1.60 +"substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)" |
1.61 +"substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)" |
1.62 +"substa s (Var v) = s v" |
1.63 +"substa s (Num n) = Num n" |
1.64 +
1.65 +"substb s (Less a1 a2) = Less (substa s a1) (substa s a2)" |
1.66 +"substb s (And b1 b2) = And (substb s b1) (substb s b2)" |
1.67 +"substb s (Neg b) = Neg (substb s b)"
1.68
1.69 text{*\noindent
1.70 -The first argument is a function mapping variables to expressions, the
1.71 +Their first argument is a function mapping variables to expressions, the
1.72 substitution. It is applied to all variables in the second argument. As a
1.73 result, the type of variables in the expression may change from @{typ"'a"}
1.74 to @{typ"'b"}. Note that there are only arithmetic and no boolean variables.
1.75 -*}
1.76
1.77 -primrec
1.78 - "substa s (IF b a1 a2) =
1.79 - IF (substb s b) (substa s a1) (substa s a2)"
1.80 - "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"
1.81 - "substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)"
1.82 - "substa s (Var v) = s v"
1.83 - "substa s (Num n) = Num n"
1.84 -
1.85 - "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"
1.86 - "substb s (And b1 b2) = And (substb s b1) (substb s b2)"
1.87 - "substb s (Neg b) = Neg (substb s b)";
1.88 -
1.89 -text{*
1.90 Now we can prove a fundamental theorem about the interaction between
1.91 evaluation and substitution: applying a substitution $s$ to an expression $a$
1.92 and evaluating the result in an environment $env$ yields the same result as
1.93 @@ -128,18 +124,16 @@
1.94 \end{exercise}
1.95 *}
1.96 (*<*)
1.97 -consts norma :: "'a aexp \<Rightarrow> 'a aexp"
1.98 - normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp"
1.99 -
1.100 -primrec
1.101 -"norma (IF b t e) = (normb b (norma t) (norma e))"
1.102 -"norma (Sum a1 a2) = Sum (norma a1) (norma a2)"
1.103 -"norma (Diff a1 a2) = Diff (norma a1) (norma a2)"
1.104 -"norma (Var v) = Var v"
1.105 -"norma (Num n) = Num n"
1.106 +primrec norma :: "'a aexp \<Rightarrow> 'a aexp" and
1.107 + normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp" where
1.108 +"norma (IF b t e) = (normb b (norma t) (norma e))" |
1.109 +"norma (Sum a1 a2) = Sum (norma a1) (norma a2)" |
1.110 +"norma (Diff a1 a2) = Diff (norma a1) (norma a2)" |
1.111 +"norma (Var v) = Var v" |
1.112 +"norma (Num n) = Num n" |
1.113
1.114 -"normb (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e"
1.115 -"normb (And b1 b2) t e = normb b1 (normb b2 t e) e"
1.116 +"normb (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e" |
1.117 +"normb (And b1 b2) t e = normb b1 (normb b2 t e) e" |
1.118 "normb (Neg b) t e = normb b e t"
1.119
1.120 lemma " evala (norma a) env = evala a env
1.121 @@ -148,18 +142,16 @@
1.122 apply (simp_all)
1.123 done
1.124
1.125 -consts normala :: "'a aexp \<Rightarrow> bool"
1.126 - normalb :: "'b bexp \<Rightarrow> bool"
1.127 +primrec normala :: "'a aexp \<Rightarrow> bool" and
1.128 + normalb :: "'a bexp \<Rightarrow> bool" where
1.129 +"normala (IF b t e) = (normalb b \<and> normala t \<and> normala e)" |
1.130 +"normala (Sum a1 a2) = (normala a1 \<and> normala a2)" |
1.131 +"normala (Diff a1 a2) = (normala a1 \<and> normala a2)" |
1.132 +"normala (Var v) = True" |
1.133 +"normala (Num n) = True" |
1.134
1.135 -primrec
1.136 -"normala (IF b t e) = (normalb b \<and> normala t \<and> normala e)"
1.137 -"normala (Sum a1 a2) = (normala a1 \<and> normala a2)"
1.138 -"normala (Diff a1 a2) = (normala a1 \<and> normala a2)"
1.139 -"normala (Var v) = True"
1.140 -"normala (Num n) = True"
1.141 -
1.142 -"normalb (Less a1 a2) = (normala a1 \<and> normala a2)"
1.143 -"normalb (And b1 b2) = False"
1.144 +"normalb (Less a1 a2) = (normala a1 \<and> normala a2)" |
1.145 +"normalb (And b1 b2) = False" |
1.146 "normalb (Neg b) = False"
1.147
1.148 lemma "normala (norma (a::'a aexp)) \<and>