theory week01B_demo
imports Main
begin
section "Simply Typed \-calculus"
declare [[show_types=true]] (* show types *)
declare [[eta_contract=false]] (* don't do eta reduction in output *)
term "\f x. f x" (* see what happens when we have eta reduction turned on *)
lemma "(\f x. f x) = (\f. f)"
apply(rule refl)
done
term "\x y. x"
term "\f x. f x x"
term "\x. x"
term "\x::int. x"
lemma "(\x. x) = (\x::int. x)"
by(rule refl)
text {*
An example with a free variable. In this case Isabelle infers the needed type of the
free variable.
*}
term "\ y f. x (f y)"
section "Types and Terms in Isabelle"
term "True"
term "x"
term "x :: int set"
term "{0} :: nat set"
term "{x} :: 'a set"
text \
Turn on displaying typeclass information
\
declare [[show_sorts]]
term "x::'a::order"
thm order.refl
declare [[show_sorts=false]]
section "Higher Order Unification"
text \
@term is called an \emph{antiquotation}. It allows embedding Isabelle terms inside
text blocks like this: @{term "\x. x + x"}.
\
text \
Unify schematic ?t with @{term y}
\
thm refl
lemma "y = y"
apply(rule refl)
done
thm add.commute
text \
Unify schematics ?a and ?b with @{term x} and @{term y} respectively.
\
lemma "(x::nat) + y = y + x"
apply(rule add.commute)
done
text \
schematic_goal command used to state lemmas that involve schematic variables which may be
instantiated during their proofs. Used quite rarely. Here we use it for illustrating higher-
order unification.
\
thm TrueI
text \
Unify schematic ?P with @{term "(\x. True)"}
\
schematic_goal mylemma: "?P x"
apply(rule TrueI)
done
thm mylemma
text \
Note that the theorem @{thm mylemma} contains just what was proved (namely the proposition
@{prop True}) not the more general result as originally stated (which isn't true for all ?P,
as consider if ?P were instantiated with @{term "\x. False"}.
\
end