templates/000755 000770 000024 00000000000 13340465062 013525 5ustar00nipkowstaff000000 000000 templates/Chapter9_2.thy000644 000770 000024 00000005476 13361065462 016172 0ustar00nipkowstaff000000 000000 theory Chapter9_2
imports "HOL-IMP.Sec_Typing" "Short_Theory"
begin
text{*
\exercise
Reformulate the inductive predicate @{const sec_type}
as a recursive function and prove the equivalence of the two formulations:
*}
fun ok :: "level \ com \ bool" where
(* your definition/proof here *)
theorem "(l \ c) = ok l c"
(* your definition/proof here *)
text{*
Try to reformulate the bottom-up system @{prop "\ c : l"}
as a function that computes @{text l} from @{text c}. What difficulty do you face?
\endexercise
\exercise
Define a bottom-up termination insensitive security type system
@{text"\' c : l"} with subsumption rule:
*}
inductive sec_type2' :: "com \ level \ bool" ("(\' _ : _)" [0,0] 50) where
(* your definition/proof here *)
text{*
Prove equivalence with the bottom-up system @{prop "\ c : l"}
without subsumption rule:
*}
lemma "\ c : l \ \' c : l"
(* your definition/proof here *)
lemma "\' c : l \ \l' \ l. \ c : l'"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Define a function that erases those parts of a command that
contain variables above some security level: *}
fun erase :: "level \ com \ com" where
(* your definition/proof here *)
text{*
Function @{term "erase l"} should replace all assignments to variables with
security level @{text"\ l"} by @{const SKIP}.
It should also erase certain @{text IF}s and @{text WHILE}s,
depending on the security level of the boolean condition. Now show
that @{text c} and @{term "erase l c"} behave the same on the variables up
to level @{text l}: *}
theorem "\ (c,s) \ s'; (erase l c,t) \ t'; 0 \ c; s = t (< l) \
\ s' = t' (< l)"
(* your definition/proof here *)
text{* This theorem looks remarkably like the noninterference lemma from
theory \mbox{@{short_theory "Sec_Typing"}} (although @{text"\"} has been replaced by @{text"<"}).
You may want to start with that proof and modify it.
The structure should remain the same. You may also need one or
two simple additional lemmas.
In the theorem above we assume that both @{term"(c,s)"}
and @{term "(erase l c,t)"} terminate. How about the following two properties: *}
lemma "\ (c,s) \ s'; 0 \ c; s = t (< l) \
\ \t'. (erase l c, t) \ t' \ s' = t' (< l)"
(* your definition/proof here *)
lemma "\ (erase l c,s) \ s'; 0 \ c; s = t (< l) \
\ \t'. (c,t) \ t' \ s' = t' (< l)"
(* your definition/proof here *)
text{* Give proofs or counterexamples.
\endexercise
*}
end
templates/Chapter11.thy000644 000770 000024 00000013410 13361065462 016005 0ustar00nipkowstaff000000 000000 theory Chapter11
imports "HOL-IMP.Denotational" "HOL-IMP.Vars" "Short_Theory"
begin
text{*
\section*{Chapter 11}
\begin{exercise}
Building on Exercise~\ref{exe:IMP:REPEAT}, extend the denotational
semantics and the equivalence proof with the big-step semantics
with a @{text REPEAT} loop.
\end{exercise}
\exercise
Consider Example~11.14 and prove the following equation by induction on @{text n}:
*}
lemma "((W (\s. s ''x'' \ 0) ({(s,t). t = s(''x'' := s ''x'' - 1)}))^^n) {} =
{(s,t). 0 \ s ''x'' & s ''x'' < int n & t = s(''x'' := 0)}"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Consider Example~11.14 but with the loop condition
@{prop"b = Less (N 0) (V ''x'')"}. Find a closed expression @{text M}
(containing @{text n})
for @{prop"(f ^^ n) {}"} and prove @{prop"(f ^^ n) {} = M"}.
*}
text {*
\endexercise
\exercise
Define an operator @{text B} such that you
can express the equation for @{term "D (IF b THEN c1 ELSE c2)"}
in a point free way.
*}
definition B :: "bexp \ (state \ state) set" where
(* your definition/proof here *)
lemma
"D (IF b THEN c1 ELSE c2) = (B b O D c1) \ (B (Not b) O D c2)"
(* your definition/proof here *)
text {*
Similarly, find a point free equation for @{term "W (bval b) dc"}
and use it to write down a point free version of
@{term "D (WHILE b DO c)"} (still using @{text lfp}).
Prove that your equations are equivalent to the old ones.
*}
(* your definition/proof here *)
text{*
\endexercise
\exercise
Let the `thin' part of a relation be its single-valued subset:
*}
definition thin :: "'a rel \ 'a rel" where
"thin R = {(a,b) . (a,b) \ R \ (\ c. (a,c) \ R \ c = b)}"
text{* Prove *}
lemma fixes f :: "'a rel \ 'a rel"
assumes "mono f" and thin_f: "\ R. f (thin R) \ thin (f R)"
shows "single_valued (lfp f)"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Generalise our set-theoretic treatment of continuity and least fixpoints to
\concept{chain-complete partial order}s (\concept{cpo}s),
i.e.\ partial orders @{text"\"} that have a least element @{text "\"} and
where every chain @{text"c 0 \ c 1 \ \"} has a least upper bound
@{term"lub c"} where \noquotes{@{term[source]"c :: nat \ 'a"}}.
This setting is described by the following type class @{text cpo}
which is an extension of the type class @{class order} of partial orders.
For details see the decription of type classes in Chapter~13.
*}
context order
begin
definition chain :: "(nat \ 'a) \ bool" where
"chain c = (\n. c n \ c (Suc n))"
end
class cpo = order +
fixes bot :: 'a and lub :: "(nat \ 'a) \ 'a"
assumes bot_least: "bot \ x"
and lub_ub: "chain c \ c n \ lub c"
and lub_least: "chain c \ (\n. c n \ u) \ lub c \ u"
text{*
A function \noquotes{@{term[source] "f :: 'a \ 'b"}}
between two cpos @{typ 'a} and @{typ 'b}
is called \concept{continuous} if @{prop"f(lub c) = lub (f o c)"}.
Prove that if @{text f} is monotone and continuous then
\ \mbox{@{text"lub (\n. (f ^^ n) \)"}} \ is the least (pre)fixpoint of @{text f}:
*}
definition cont :: "('a::cpo \ 'b::cpo) \ bool" where
"cont f = (\c. chain c \ f (lub c) = lub (f o c))"
abbreviation "fix f \ lub (\n. (f^^n) bot)"
lemma fix_lpfp: assumes "mono f" and "f p \ p" shows "fix f \ p"
(* your definition/proof here *)
theorem fix_fp: assumes "mono f" and "cont f" shows "f(fix f) = fix f"
(* your definition/proof here *)
text{*
\endexercise
\exercise
We define a dependency analysis @{text Dep} that maps commands to relations
between variables such that @{term "(x,y) : Dep c"} means that in
the execution of @{text c}
the initial value of @{text x} can influence the final value of @{text y}:
*}
fun Dep :: "com \ (vname * vname) set" where
"Dep SKIP = Id" |
"Dep (x::=a) = {(u,v). if v = x then u \ vars a else u = v}" |
"Dep (c1;;c2) = Dep c1 O Dep c2" |
"Dep (IF b THEN c1 ELSE c2) = Dep c1 \ Dep c2 \ vars b \ UNIV" |
"Dep (WHILE b DO c) = lfp(\R. Id \ vars b \ UNIV \ Dep c O R)"
text{*
where @{text"\"} is the cross product of two sets.
Prove monotonicity of the function @{const lfp} is applied to.
*}
text{* For the correctness statement define *}
abbreviation Deps :: "com \ vname set \ vname set" where
"Deps c X \ (\ x\X. {y. (y,x) : Dep c})"
text{* and prove *}
lemma "\ (c,s) \ s'; (c,t) \ t'; s = t on Deps c X \ \ s' = t' on X"
(* your definition/proof here *)
text{*
Give an example that the following stronger termination-sensitive property
@{prop[display] "\ (c,s) \ s'; s = t on Deps c X \
\ \t'. (c,t) \ t' \ s' = t' on X"}
does not hold. Hint: @{prop"X = {}"}.
In the definition of @{term"Dep(IF b THEN c1 ELSE c2)"} the variables
in @{text b} can influence all variables (@{text UNIV}). However,
if a variable is not assigned to in @{text c1} and @{text c2}
it is not influenced by @{text b} (ignoring termination).
Theory @{short_theory "Vars"} defines a function @{const lvars} such
that @{term"lvars c"} is the set of variables on the left-hand side
of an assignment in @{text c}.
Modify the definition of @{const Dep} as follows:
replace @{const UNIV} by @{term"lvars c1 \ lvars c2"}
(in the case @{term"IF b THEN c1 ELSE c2"}) and by \mbox{@{term"lvars c"}}
(in the case @{term"WHILE b DO c"}).
Adjust the proof of the above correctness statement.
*}
text{*
\endexercise
*}
end
templates/Chapter2.thy000644 000770 000024 00000015614 13361065462 015735 0ustar00nipkowstaff000000 000000 theory Chapter2
imports Main
begin
text{*
\section*{Chapter 2}
\exercise
Use the \textbf{value} command to evaluate the following expressions:
*}
"1 + (2::nat)"
"1 + (2::int)"
"1 - (2::nat)"
"1 - (2::int)"
"[a,b] @ [c,d]"
text{*
\endexercise
\exercise
Recall the definition of our own addition function on @{typ nat}:
*}
fun add :: "nat \ nat \ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"
text{*
Prove that @{const add} is associative and commutative.
You will need additional lemmas.
*}
lemma add_assoc: "add (add m n) p = add m (add n p)"
(* your definition/proof here *)
lemma add_comm: "add m n = add n m"
(* your definition/proof here *)
text{* Define a recursive function *}
fun double :: "nat \ nat" where
(* your definition/proof here *)
text{* and prove that *}
lemma double_add: "double m = add m m"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Define a function that counts the number of occurrences of
an element in a list:
*}
fun count :: "'a list \ 'a \ nat" where
(* your definition/proof here *)
text {*
Test your definition of @{term count} on some examples.
Prove the following inequality:
*}
theorem "count xs x \ length xs"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Define a function @{text snoc} that appends an element to the end of a list.
Do not use the existing append operator @{text "@"} for lists.
*}
fun snoc :: "'a list \ 'a \ 'a list" where
(* your definition/proof here *)
text {*
Convince yourself on some test cases that your definition
of @{term snoc} behaves as expected.
With the help of @{text snoc} define a recursive function @{text reverse}
that reverses a list. Do not use the predefined function @{const rev}.
*}
fun reverse :: "'a list \ 'a list" where
(* your definition/proof here *)
text {*
Prove the following theorem. You will need an additional lemma.
*}
theorem "reverse (reverse xs) = xs"
(* your definition/proof here *)
text{*
\endexercise
\exercise
The aim of this exercise is to prove the summation formula
\[ \sum_{i=0}^{n}i = \frac{n(n+1)}{2} \]
Define a recursive function @{text "sum_upto n = 0 + ... + n"}:
*}
fun sum_upto :: "nat \ nat" where
(* your definition/proof here *)
text {*
Now prove the summation formula by induction on @{text "n"}.
First, write a clear but informal proof by hand following the examples
in the main text. Then prove the same property in Isabelle:
*}
lemma "sum_upto n = n * (n+1) div 2"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Starting from the type @{text "'a tree"} defined in the text, define
a function that collects all values in a tree in a list, in any order,
without removing duplicates.
*}
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
fun contents :: "'a tree \ 'a list" where
(* your definition/proof here *)
text{*
Then define a function that sums up all values in a tree of natural numbers
*}
fun sum_tree :: "nat tree \ nat" where
(* your definition/proof here *)
text{* and prove *}
lemma "sum_tree t = sum_list(contents t)"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Define a new type @{text "'a tree2"} of binary trees where values are also
stored in the leaves of the tree. Also reformulate the
@{text mirror} function accordingly. Define two functions *}
fun pre_order :: "'a tree2 \ 'a list" where
(* your definition/proof here *)
fun post_order :: "'a tree2 \ 'a list" where
(* your definition/proof here *)
text{*
that traverse a tree and collect all stored values in the respective order in
a list. Prove *}
lemma "pre_order (mirror t) = rev (post_order t)"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Define a recursive function
*}
fun intersperse :: "'a \ 'a list \ 'a list" where
(* your definition/proof here *)
text{*
such that @{text "intersperse a [x\<^sub>1, ..., x\<^sub>n] = [x\<^sub>1, a, x\<^sub>2, a, ..., a, x\<^sub>n]"}.
Prove
*}
lemma "map f (intersperse a xs) = intersperse (f a) (map f xs)"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Write a tail-recursive variant of the @{text add} function on @{typ nat}:
*}
fun itadd :: "nat \ nat \ nat" where
(* your definition/proof here *)
text{*
Tail-recursive means that in the recursive case, @{const itadd} needs to call
itself directly: \mbox{@{term"itadd (Suc m) n"}} @{text"= itadd \"}.
Prove
*}
lemma "itadd m n = add m n"
(* your definition/proof here *)
text{*
\endexercise
\exercise\label{exe:tree0}
Define a datatype @{text tree0} of binary tree skeletons which do not store
any information, neither in the inner nodes nor in the leaves.
Define a function that counts the number of all nodes (inner nodes and leaves)
in such a tree:
*}
fun nodes :: "tree0 \ nat" where
(* your definition/proof here *)
text {*
Consider the following recursive function:
*}
fun explode :: "nat \ tree0 \ tree0" where
"explode 0 t = t" |
"explode (Suc n) t = explode n (Node t t)"
text {*
Experiment how @{text explode} influences the size of a binary tree
and find an equation expressing the size of a tree after exploding it
(\noquotes{@{term [source] "nodes (explode n t)"}}) as a function
of @{term "nodes t"} and @{text n}. Prove your equation.
You may use the usual arithmetic operations including the exponentiation
operator ``@{text"^"}''. For example, \noquotes{@{prop [source] "2 ^ 2 = 4"}}.
Hint: simplifying with the list of theorems @{thm[source] algebra_simps}
takes care of common algebraic properties of the arithmetic operators.
\endexercise
*}
text{*
\exercise
Define arithmetic expressions in one variable over integers (type @{typ int})
as a data type:
*}
datatype exp = Var | Const int | Add exp exp | Mult exp exp
text{*
Define a function @{text eval} that evaluates an expression at some value:
*}
fun eval :: "exp \ int \ int" where
(* your definition/proof here *)
text{*
For example, @{prop"eval (Add (Mult (Const 2) Var) (Const 3)) i = 2*i+3"}.
A polynomial can be represented as a list of coefficients, starting with
the constant. For example, @{term "[4, 2, -1, 3::int]"} represents the
polynomial $4 + 2x - x^2 + 3x^3$.
Define a function @{text evalp} that evaluates a polynomial at a given value:
*}
fun evalp :: "int list \ int \ int" where
(* your definition/proof here *)
text{*
Define a function @{text coeffs} that transforms an expression into a polynomial.
This will require auxiliary functions.
*}
fun coeffs :: "exp \ int list" where
(* your definition/proof here *)
text{*
Prove that @{text coeffs} preserves the value of the expression:
*}
theorem evalp_coeffs: "evalp (coeffs e) x = eval e x"
(* your definition/proof here *)
text{*
Hint: consider the hint in Exercise~\ref{exe:tree0}.
\endexercise
*}
end
templates/Chapter9_1.thy000644 000770 000024 00000005707 13361065462 016166 0ustar00nipkowstaff000000 000000 theory Chapter9_1
imports "HOL-IMP.Types" "Short_Theory"
begin
text{*
\section*{Chapter 9}
\exercise
Reformulate the inductive predicates \ @{prop"\ \ a : \"},
\ @{prop"\ \ (b::bexp)"} \
and \ \mbox{@{prop"\ \ (c::com)"}} \ as three recursive functions
*}
fun atype :: "tyenv \ aexp \ ty option" where
(* your definition/proof here *)
fun bok :: "tyenv \ bexp \ bool" where
(* your definition/proof here *)
fun cok :: "tyenv \ com \ bool" where
(* your definition/proof here *)
text{* and prove *}
lemma atyping_atype: "(\ \ a : \) = (atype \ a = Some \)"
(* your definition/proof here *)
lemma btyping_bok: "(\ \ b) = bok \ b"
(* your definition/proof here *)
lemma ctyping_cok: "(\ \ c) = cok \ c"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Modify the evaluation and typing of @{typ aexp} by allowing @{typ int}s to be coerced
to @{typ real}s with the predefined coercion function
\noquotes{@{term[source] "real_of_int :: int \ real"}} where necessary.
Now every @{typ aexp} has a value. Define an evaluation function:
*}
fun aval :: "aexp \ state \ val" where
(* your definition/proof here *)
text{*
Similarly, every @{typ aexp} has a type.
Define a function that computes the type of an @{typ aexp}
*}
fun atyp :: "tyenv \ aexp \ ty" where
(* your definition/proof here *)
text{* and prove that it computes the correct type: *}
lemma "\ \ s \ atyp \ a = type (aval a s)"
(* your definition/proof here *)
text{*
Note that Isabelle inserts the coercion @{typ real} automatically.
For example, if you write @{term "Rv(i+r)"} where @{text"i :: int"} and
@{text "r :: real"} then it becomes @{term "Rv(real i + x)"}.
\endexercise
\bigskip
For the following two exercises copy theory @{short_theory "Types"} and modify it as required.
\begin{exercise}
Add a @{text REPEAT} loop (see Exercise~\ref{exe:IMP:REPEAT}) to the typed version of IMP
and update the type soundness proof.
\end{exercise}
\begin{exercise}
Modify the typed version of IMP as follows. Values are now either integers or booleans.
Thus variables can have boolean values too. Merge the two expressions types
@{typ aexp} and @{typ bexp} into one new type @{text exp} of expressions
that has the constructors of both types (of course without real constants).
Combine @{const taval} and @{const tbval} into one evaluation predicate
@{text "eval :: exp \ state \ val \ bool"}. Similarly combine the two typing predicates
into one: @{text "\ \ e : \"} where @{text "e :: exp"} and the IMP-type @{text \} can
be one of @{text Ity} or @{text Bty}.
Adjust the small-step semantics and the type soundness proof.
\end{exercise}
*}
end
templates/Chapter3.thy000644 000770 000024 00000031533 13361065462 015734 0ustar00nipkowstaff000000 000000 theory Chapter3
imports "HOL-IMP.BExp"
"HOL-IMP.ASM"
"Short_Theory"
begin
text{*
\section*{Chapter 3}
\exercise
To show that @{const asimp_const} really folds all subexpressions of the form
@{term "Plus (N i) (N j)"}, define a function
*}
fun optimal :: "aexp \ bool" where
(* your definition/proof here *)
text{*
that checks that its argument does not contain a subexpression of the form
@{term "Plus (N i) (N j)"}. Then prove that the result of @{const asimp_const}
is optimal:
*}
lemma "optimal (asimp_const a)"
(* your definition/proof here *)
text{*
This proof needs the same @{text "split:"} directive as the correctness proof of
@{const asimp_const}. This increases the chance of nontermination
of the simplifier. Therefore @{const optimal} should be defined purely by
pattern matching on the left-hand side,
without @{text case} expressions on the right-hand side.
\endexercise
\exercise
In this exercise we verify constant folding for @{typ aexp}
where we sum up all constants, even if they are not next to each other.
For example, @{term "Plus (N 1) (Plus (V x) (N 2))"} becomes
@{term "Plus (V x) (N 3)"}. This goes beyond @{const asimp}.
Below we follow a particular solution strategy but there are many others.
First, define a function @{text sumN} that returns the sum of all
constants in an expression and a function @{text zeroN} that replaces all
constants in an expression by zeroes (they will be optimized away later):
*}
fun sumN :: "aexp \ int" where
(* your definition/proof here *)
fun zeroN :: "aexp \ aexp" where
(* your definition/proof here *)
text {*
Next, define a function @{text sepN} that produces an arithmetic expression
that adds the results of @{const sumN} and @{const zeroN}. Prove that
@{text sepN} preserves the value of an expression.
*}
definition sepN :: "aexp \ aexp" where
(* your definition/proof here *)
lemma aval_sepN: "aval (sepN t) s = aval t s"
(* your definition/proof here *)
text {*
Finally, define a function @{text full_asimp} that uses @{const asimp}
to eliminate the zeroes left over by @{const sepN}.
Prove that it preserves the value of an arithmetic expression.
*}
definition full_asimp :: "aexp \ aexp" where
(* your definition/proof here *)
lemma aval_full_asimp: "aval (full_asimp t) s = aval t s"
(* your definition/proof here *)
text{*
\endexercise
\exercise\label{exe:subst}
Substitution is the process of replacing a variable
by an expression in an expression. Define a substitution function
*}
fun subst :: "vname \ aexp \ aexp \ aexp" where
(* your definition/proof here *)
text{*
such that @{term "subst x a e"} is the result of replacing
every occurrence of variable @{text x} by @{text a} in @{text e}.
For example:
@{lemma[display] "subst ''x'' (N 3) (Plus (V ''x'') (V ''y'')) = Plus (N 3) (V ''y'')" by simp}
Prove the so-called \concept{substitution lemma} that says that we can either
substitute first and evaluate afterwards or evaluate with an updated state:
*}
lemma subst_lemma: "aval (subst x a e) s = aval e (s(x := aval a s))"
(* your definition/proof here *)
text {*
As a consequence prove that we can substitute equal expressions by equal expressions
and obtain the same result under evaluation:
*}
lemma "aval a1 s = aval a2 s
\ aval (subst x a1 e) s = aval (subst x a2 e) s"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Take a copy of theory @{short_theory "AExp"} and modify it as follows.
Extend type @{typ aexp} with a binary constructor @{text Times} that
represents multiplication. Modify the definition of the functions @{const aval}
and @{const asimp} accordingly. You can remove @{const asimp_const}.
Function @{const asimp} should eliminate 0 and 1 from multiplications
as well as evaluate constant subterms. Update all proofs concerned.
*}
text{*
\endexercise
\exercise
Define a datatype @{text aexp2} of extended arithmetic expressions that has,
in addition to the constructors of @{typ aexp}, a constructor for
modelling a C-like post-increment operation $x{++}$, where $x$ must be a
variable. Define an evaluation function @{text "aval2 :: aexp2 \ state \ val \ state"}
that returns both the value of the expression and the new state.
The latter is required because post-increment changes the state.
Extend @{text aexp2} and @{text aval2} with a division operation. Model partiality of
division by changing the return type of @{text aval2} to
@{typ "(val \ state) option"}. In case of division by 0 let @{text aval2}
return @{const None}. Division on @{typ int} is the infix @{text div}.
*}
text{*
\endexercise
\exercise
The following type adds a @{text LET} construct to arithmetic expressions:
*}
datatype lexp = Nl int | Vl vname | Plusl lexp lexp | LET vname lexp lexp
text{* The @{const LET} constructor introduces a local variable:
the value of @{term "LET x e\<^sub>1 e\<^sub>2"} is the value of @{text e\<^sub>2}
in the state where @{text x} is bound to the value of @{text e\<^sub>1} in the original state.
Define a function @{const lval} @{text"::"} @{typ "lexp \ state \ int"}
that evaluates @{typ lexp} expressions. Remember @{term"s(x := i)"}.
Define a conversion @{const inline} @{text"::"} @{typ "lexp \ aexp"}.
The expression \mbox{@{term "LET x e\<^sub>1 e\<^sub>2"}} is inlined by substituting
the converted form of @{text e\<^sub>1} for @{text x} in the converted form of @{text e\<^sub>2}.
See Exercise~\ref{exe:subst} for more on substitution.
Prove that @{const inline} is correct w.r.t.\ evaluation.
\endexercise
\exercise
Show that equality and less-or-equal tests on @{text aexp} are definable
*}
definition Le :: "aexp \ aexp \ bexp" where
(* your definition/proof here *)
definition Eq :: "aexp \ aexp \ bexp" where
(* your definition/proof here *)
text{*
and prove that they do what they are supposed to:
*}
lemma bval_Le: "bval (Le a1 a2) s = (aval a1 s \ aval a2 s)"
(* your definition/proof here *)
lemma bval_Eq: "bval (Eq a1 a2) s = (aval a1 s = aval a2 s)"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Consider an alternative type of boolean expressions featuring a conditional: *}
datatype ifexp = Bc2 bool | If ifexp ifexp ifexp | Less2 aexp aexp
text {* First define an evaluation function analogously to @{const bval}: *}
fun ifval :: "ifexp \ state \ bool" where
(* your definition/proof here *)
text{* Then define two translation functions *}
fun b2ifexp :: "bexp \ ifexp" where
(* your definition/proof here *)
fun if2bexp :: "ifexp \ bexp" where
(* your definition/proof here *)
text{* and prove their correctness: *}
lemma "bval (if2bexp exp) s = ifval exp s"
(* your definition/proof here *)
lemma "ifval (b2ifexp exp) s = bval exp s"
(* your definition/proof here *)
text{*
\endexercise
\exercise
We define a new type of purely boolean expressions without any arithmetic
*}
datatype pbexp =
VAR vname | NOT pbexp | AND pbexp pbexp | OR pbexp pbexp
text{*
where variables range over values of type @{typ bool},
as can be seen from the evaluation function:
*}
fun pbval :: "pbexp \ (vname \ bool) \ bool" where
"pbval (VAR x) s = s x" |
"pbval (NOT b) s = (\ pbval b s)" |
"pbval (AND b1 b2) s = (pbval b1 s \ pbval b2 s)" |
"pbval (OR b1 b2) s = (pbval b1 s \ pbval b2 s)"
text {* Define a function that checks whether a boolean exression is in NNF
(negation normal form), i.e., if @{const NOT} is only applied directly
to @{const VAR}s: *}
fun is_nnf :: "pbexp \ bool" where
(* your definition/proof here *)
text{*
Now define a function that converts a @{text bexp} into NNF by pushing
@{const NOT} inwards as much as possible:
*}
fun nnf :: "pbexp \ pbexp" where
(* your definition/proof here *)
text{*
Prove that @{const nnf} does what it is supposed to do:
*}
lemma pbval_nnf: "pbval (nnf b) s = pbval b s"
(* your definition/proof here *)
lemma is_nnf_nnf: "is_nnf (nnf b)"
(* your definition/proof here *)
text{*
An expression is in DNF (disjunctive normal form) if it is in NNF
and if no @{const OR} occurs below an @{const AND}. Define a corresponding
test:
*}
fun is_dnf :: "pbexp \ bool" where
(* your definition/proof here *)
text {*
An NNF can be converted into a DNF in a bottom-up manner.
The critical case is the conversion of @{term (sub) "AND b1 b2"}.
Having converted @{text b\<^sub>1} and @{text b\<^sub>2}, apply distributivity of @{const AND}
over @{const OR}. If we write @{const OR} as a multi-argument function,
we can express the distributivity step as follows:
@{text "dist_AND (OR a\<^sub>1 ... a\<^sub>n) (OR b\<^sub>1 ... b\<^sub>m)"}
= @{text "OR (AND a\<^sub>1 b\<^sub>1) (AND a\<^sub>1 b\<^sub>2) ... (AND a\<^sub>n b\<^sub>m)"}. Define
*}
fun dist_AND :: "pbexp \ pbexp \ pbexp" where
(* your definition/proof here *)
text {* and prove that it behaves as follows: *}
lemma pbval_dist: "pbval (dist_AND b1 b2) s = pbval (AND b1 b2) s"
(* your definition/proof here *)
lemma is_dnf_dist: "is_dnf b1 \ is_dnf b2 \ is_dnf (dist_AND b1 b2)"
(* your definition/proof here *)
text {* Use @{const dist_AND} to write a function that converts an NNF
to a DNF in the above bottom-up manner.
*}
fun dnf_of_nnf :: "pbexp \ pbexp" where
(* your definition/proof here *)
text {* Prove the correctness of your function: *}
lemma "pbval (dnf_of_nnf b) s = pbval b s"
(* your definition/proof here *)
lemma "is_nnf b \ is_dnf (dnf_of_nnf b)"
(* your definition/proof here *)
text{*
\endexercise
\exercise\label{exe:stack-underflow}
A \concept{stack underflow} occurs when executing an @{text ADD}
instruction on a stack of size less than 2. In our semantics
a term @{term "exec1 ADD s stk"} where @{prop "length stk < 2"}
is simply some unspecified value, not an error or exception --- HOL does not have those concepts.
Modify theory @{short_theory "ASM"}
such that stack underflow is modelled by @{const None}
and normal execution by @{text Some}, i.e., the execution functions
have return type @{typ "stack option"}. Modify all theorems and proofs
accordingly.
Hint: you may find @{text"split: option.split"} useful in your proofs.
*}
text{*
\endexercise
\exercise\label{exe:register-machine}
This exercise is about a register machine
and compiler for @{typ aexp}. The machine instructions are
*}
type_synonym reg = nat
datatype instr = LDI val reg | LD vname reg | ADD reg reg
text {*
where type @{text reg} is a synonym for @{typ nat}.
Instruction @{term "LDI i r"} loads @{text i} into register @{text r},
@{term "LD x r"} loads the value of @{text x} into register @{text r},
and @{term[names_short] "ADD r\<^sub>1 r\<^sub>2"} adds register @{text r\<^sub>2} to register @{text r\<^sub>1}.
Define the execution of an instruction given a state and a register state;
the result is the new register state: *}
type_synonym rstate = "reg \ val"
fun exec1 :: "instr \ state \ rstate \ rstate" where
(* your definition/proof here *)
text{*
Define the execution @{const[source] exec} of a list of instructions as for the stack machine.
The compiler takes an arithmetic expression @{text a} and a register @{text r}
and produces a list of instructions whose execution places the value of @{text a}
into @{text r}. The registers @{text "> r"} should be used in a stack-like fashion
for intermediate results, the ones @{text "< r"} should be left alone.
Define the compiler and prove it correct:
*}
theorem "exec (comp a r) s rs r = aval a s"
(* your definition/proof here *)
text{*
\endexercise
\exercise\label{exe:accumulator}
This exercise is a variation of the previous one
with a different instruction set:
*}
datatype instr0 = LDI0 val | LD0 vname | MV0 reg | ADD0 reg
text{*
All instructions refer implicitly to register 0 as a source or target:
@{const LDI0} and @{const LD0} load a value into register 0, @{term "MV0 r"}
copies the value in register 0 into register @{text r}, and @{term "ADD0 r"}
adds the value in register @{text r} to the value in register 0;
@{term "MV0 0"} and @{term "ADD0 0"} are legal. Define the execution functions
*}
fun exec01 :: "instr0 \ state \ rstate \ rstate" where
(* your definition/proof here *)
text{*
and @{const exec0} for instruction lists.
The compiler takes an arithmetic expression @{text a} and a register @{text r}
and produces a list of instructions whose execution places the value of @{text a}
into register 0. The registers @{text "> r"} should be used in a stack-like fashion
for intermediate results, the ones @{text "\ r"} should be left alone
(with the exception of 0). Define the compiler and prove it correct:
*}
theorem "exec0 (comp0 a r) s rs 0 = aval a s"
(* your definition/proof here *)
text{*
\endexercise
*}
end
templates/Chapter13_9.thy000644 000770 000024 00000000441 13361065462 016237 0ustar00nipkowstaff000000 000000 theory Chapter13_9
imports "HOL-IMP.Abs_Int3"
begin
(* 13.19 *)
value "show_acom (step_up_ivl 3 (steps test3_ivl 4))"
(* 13.20 *)
value "show_acom ((step_ivl \ ^^ 4) (step_up_ivl 3 (steps test3_ivl 4)))"
value "show_acom (step_down_ivl 4 (step_up_ivl 3 (steps test3_ivl 4)))"
end
templates/Chapter7.thy000644 000770 000024 00000016566 13361065462 015751 0ustar00nipkowstaff000000 000000 theory Chapter7
imports "HOL-IMP.Small_Step" "Short_Theory"
begin
text{*
\section*{Chapter 7}
\exercise
Define a function that computes the set of variables that are assigned to
in a command:
*}
fun assigned :: "com \ vname set" where
(* your definition/proof here *)
text{*
Prove that if some variable is not assigned to in a command,
then that variable is never modified by the command:
*}
lemma "\ (c, s) \ t; x \ assigned c \ \ s x = t x"
(* your definition/proof here *)
text {*
\endexercise
\exercise
Define a recursive function that determines if a command behaves like @{const SKIP}
and prove its correctness:
*}
fun skip :: "com \ bool" where
(* your definition/proof here *)
lemma "skip c \ c \ SKIP"
(* your definition/proof here *)
text{*
\endexercise
\exercise
Define a recursive function
*}
fun deskip :: "com \ com" where
(* your definition/proof here *)
text{*
that eliminates as many @{const SKIP}s as possible from a command. For example:
@{prop[display]"deskip (SKIP;; WHILE b DO (x::=a;; SKIP)) = WHILE b DO x::=a"}
Prove its correctness by induction on @{text c}: *}
lemma "deskip c \ c"
(* your definition/proof here *)
text{*
Remember lemma @{thm[source]sim_while_cong} for the @{text WHILE} case.
\endexercise
\exercise
A small-step semantics for the evaluation of arithmetic expressions
can be defined like this:
*}
inductive astep :: "aexp \ state \ aexp \ bool" (infix "\" 50) where
"(V x, s) \ N (s x)" |
"(Plus (N i) (N j), s) \ N (i + j)" |
(* your definition/proof here *)
text{*
Complete the definition with two rules for @{const Plus}
that model a left-to-right evaluation strategy:
reduce the first argument with @{text"\"} if possible,
reduce the second argument with @{text"\"} if the first argument is a number.
Prove that each @{text"\"} step preserves the value of the expression:
*}
lemma "(a, s) \ a' \ aval a s = aval a' s"
proof (induction rule: astep.induct [split_format (complete)])
(* your definition/proof here *)
text{*
Do not use the \isacom{case} idiom but write down explicitly what you assume
and show in each case: \isacom{fix} \dots \isacom{assume} \dots \isacom{show} \dots.
\endexercise
\exercise
Prove or disprove (by giving a counterexample):
*}
lemma "IF And b\<^sub>1 b\<^sub>2 THEN c\<^sub>1 ELSE c\<^sub>2 \