theory week01B_demo
imports Main
begin

section "Simply Typed \<lambda>-calculus"

term "\<lambda>f x. f x" 

declare [[show_types=true]] (* show types *)
declare [[eta_contract=false]] (* don't do eta reduction in output *)

term "\<lambda>f x. f x"  (* see what happens when we have eta reduction turned on *)

thm refl

lemma "(\<lambda>f x. f x) = (\<lambda>f. f)"
  apply(rule refl)
  done

term "\<lambda>x y. x"

term "\<lambda>f x. f x x"

term "\<lambda>x. x"

term "\<lambda>x::int. x"

lemma "(\<lambda>x. x) = (\<lambda>x::int. x)"
  by(rule refl)

text \<open>
  An example with a free variable. In this case Isabelle infers the needed type of the
  free variable.
\<close>

term "\<lambda> 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 \<open>
  Turn on displaying typeclass information
\<close>
declare [[show_sorts]]
term "x::'a::order"

thm order.refl
declare [[show_sorts=false]]


section "Higher Order Unification"
text \<open>
  @term is called an \emph{antiquotation}. It allows embedding Isabelle terms inside
  text blocks like this: @{term "\<lambda>x. x + x"}.
\<close>

text  \<open>
  Unify schematic ?t with @{term y}
\<close>

thm refl
lemma "y = y"
  apply(rule refl)
  done

thm add.commute
text \<open>
  Unify schematics ?a and ?b with @{term x} and @{term y} respectively.
\<close>

lemma "(x::nat) + y = y + x"
  apply(rule add.commute)
  done



text \<open>
  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.
\<close>

thm TrueI
text \<open>
  Unify schematic ?P with @{term "(\<lambda>x. True)"}
\<close>


schematic_goal mylemma: "?P x" 
  apply(rule TrueI) (* instantiate ?P to be \<lambda>x. True *)
  (* therefore your statement is ((\<lambda>x. True) x) which reduced to True*)
  done

thm mylemma

lemma "P x"
  oops

text \<open>
  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 "\<lambda>x. False"}.
\<close>

end