Curryfication.thy

theory Curryfication

imports Main

begin

section ‹Curryfication›

text ‹
  Curryfication, named after Haskell Curry, is a way to represent fonctions
  of several arguments with only functions of one argument. 
  In Isabelle, functions are in curryfied form:
     f: A × B → C
        (x, y) ↦ z
   is written as:
     f: A → (B → C)
        x ↦ (λy. z)
   so "f x" is a function which takes the second argument of f to provide the result,
   and "f x y" is read as "(f x) y"
›

term "(+)" ― ‹the "+" function›
value "(+) (2::int) 3"

text ‹Define sum as the function which returns the sum of two integers›
definition sum:: "int ⇒ int ⇒ int"
where "sum m n = m + n"

text ‹Check that it works as expected›
value "sum 2 3"

text ‹We can partially apply sum to one argument to define the increment function›
abbreviation "inc ≡ sum 1"

value "inc 41"

end

Exemple.thy

theory Exemple

imports Main

begin
text ‹Examples of terms›
term "a+b"
term "(a::nat)+b"

text ‹Examples of types›
typ "nat"
typ "nat ⇒ nat"
typ "nat ⇒ nat ⇒ nat"

text ‹Check the default associativity›
typ "nat ⇒ (nat ⇒ nat)"
typ "(nat ⇒ nat) ⇒ nat"

text ‹Pairs and tuples›
typ "nat × nat"

term "(0::nat, 0::nat)"
term "(0::nat, 0::nat, 0::nat)"
term "(0::nat, (0::nat, 0::nat))"
term "((0::nat, 0::nat), 0::nat)"

text ‹A simple inductive type for sequences›
datatype 'a seq =
  Empty ("∅")
| Append "'a seq" "'a" (infixl "." 60)

term "∅ . 0"
term "Append Empty 0"
term "∅ . (0::nat)"
term "∅ . (0::nat) . 1"
term "∅ . 0 . (1::nat)"

text ‹An inductive function defined on an inductive type›
fun len :: "'a seq ⇒ nat"
where
  "len ∅ = 0"
| "len (l . e) = Suc (len l)"

text ‹Theorems generated by the function definition›
thm len.simps

term "len (∅ . (0::nat) . 1)"

text ‹Evaluation through ML code generation›
value "len (∅ . (0::nat) . 1)"

fun prepend :: "'a ⇒ 'a seq ⇒ 'a seq" (infixr "<<" 60)
where
  "e << ∅ = ∅ . e"
| "e << (l . a) = (e << l) . a"

term "(0::nat) << 1 << ∅"
value "(0::nat) << 1 << ∅"

text ‹Proof of a theorem using induction›
lemma "len (e << l) = len (l . e)"
proof (induction l) print_cases
  case Empty
    from prepend.simps(1) have "e << ∅ = ∅ . e" .
    thus ?case by simp
next
  case (Append l' a) print_facts
    from prepend.simps(2) have "e << (l' . a) = (e << l') . a" .
    hence "len (e << (l' . a)) = len ((e << l') . a)" by simp
    also from len.simps(2) have "... = Suc (len (e << l'))" .
    finally have 1:"len (e << (l' . a)) = Suc (len (e << l'))" .
    from len.simps(2) have "len ((l' . a) . e) = Suc (len (l' . a))" .
    with Append.IH have "... = Suc (len (e << l'))" by simp
    with 1 have "len (e << (l' . a)) = len ((l' . a) . e)" by simp
    thus ?case .
qed

lemma "len (e << l) = len (l . e)"
apply (induction l)
apply simp
apply simp
done

lemma "len (e << l) = len (l . e)"
by (induction l, simp+)

section ‹Manual proof of totalness and termination of a function›
text ‹
  For some complex recursive definitions, the automated proof of
  totalness and termination performed by "fun" may fail.
  In that case, we can use "function" and make the proofs manually.
  Here is an example on the "len" function defined above, that we redefine
  here with manual proofs.
›
function len2 :: "'a seq ⇒ nat"
where
  "len2 ∅ = 0"
| "len2 (l . e) = Suc (len2 l)"
― ‹Function is total: 1) the patterns do not overlap and cover all possible terms›
proof -
― ‹Coverage: a sequence is either empty of the result of append (theorem seq.exhaust)›
  show ‹⋀P x. (x = ∅ ⟹ P) ⟹ (⋀l e. x = l . e ⟹ P) ⟹ P› by (rule seq.exhaust)
― ‹There is only one way to match the first equation›
  show ‹∅ = ∅ ⟹ 0 = 0› by simp
― ‹There is no overlap between the two equations›
  show ‹⋀l e. ∅ = l . e ⟹ 0 = Suc (len2_sumC l)› by simp
― ‹There is only one way to match the second equation›
  show ‹⋀l e la ea. l . e = la . ea ⟹ Suc (len2_sumC l) = Suc (len2_sumC la)› by simp
qed
― ‹2) recursion terminates›
termination
proof
― ‹"size" is a function that gives the size of a term, it is defined for seq by the datatype declaration›
― ‹"measure" builds a well founded relation from a function 'a => nat, using the fact that "<" is well founded›
  let ?R = ‹measure size›
― ‹We have to show that this relation is well founded›
  show ‹wf ?R› using wf_measure by simp
― ‹and that the terms involved in the recursive definition are in the relation›
  show ‹⋀l e. (l, l . e) ∈ ?R›  by simp
qed

end

InductiveExample.thy

theory InductiveExample

imports Main

begin

text ‹
  Definition of even numbers by a function.
›
fun isEvenFun :: "nat ⇒ bool"
where
  "isEvenFun 0 = True"
| "isEvenFun (Suc n) = (¬ (isEvenFun n))"

value "isEvenFun 0"
value "isEvenFun 1"
value "isEvenFun 2"

text ‹
  Definition of even numbers by an inductive predicate.
›
inductive isEvenPred :: "nat ⇒ bool"
where
  "isEvenPred 0"
| "isEvenPred n ⟹ isEvenPred (Suc (Suc n))"

text ‹
  Add some facts to the set of elimination and introduction rules
  to make proof automation more efficient.
›
thm "isEvenPred.intros"
lemmas isEvenPred.intros[intro]

thm "isEvenPred.cases"
lemmas isEvenPred.cases[elim]

text ‹
  Check proof automation on simple theorems
›
lemma "isEvenPred 0" ..

lemma "¬isEvenPred (Suc 0)" by auto

lemma "isEvenPred (Suc (Suc 0))" by auto

text ‹
  Show the equivalence of the function and the predicate.
  A preliminary lemma showing that the predicate alternates with Suc is useful for this. 
›
lemma evenPred_alt: "isEvenPred (Suc n) = (¬isEvenPred n)"
  by (induction n, blast+)

lemma "isEvenFun n = isEvenPred n"
proof (induction n)
  case 0
    thus ?case by (simp add: isEvenPred.intros(1))
next
  case (Suc n)
    thus ?case by (simp add: evenPred_alt)
qed

end