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