Theory Elimination

(*  Title:      CTT/ex/Elimination.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Some examples taken from P. Martin-Löf, Intuitionistic type theory
(Bibliopolis, 1984).
*)

section "Examples with elimination rules"

theory Elimination
imports "../CTT"
begin

text "This finds the functions fst and snd!"

schematic_goal [folded basic_defs]: "A type  ?a : (A × A)  A"
apply pc
done

schematic_goal [folded basic_defs]: "A type  ?a : (A × A)  A"
apply pc
back
done

text "Double negation of the Excluded Middle"
schematic_goal "A type  ?a : ((A + (AF))  F)  F"
apply intr
apply (rule ProdE)
apply assumption
apply pc
done

schematic_goal "A type; B type  ?a : (A × B)  (B × A)"
apply pc
done
(*The sequent version (ITT) could produce an interesting alternative
  by backtracking.  No longer.*)

text "Binary sums and products"
schematic_goal "A type; B type; C type  ?a : (A + B  C)  (A  C) × (B  C)"
apply pc
done

(*A distributive law*)
schematic_goal "A type; B type; C type  ?a : A × (B + C)  (A × B + A × C)"
apply pc
done

(*more general version, same proof*)
schematic_goal
  assumes "A type"
    and "x. x:A  B(x) type"
    and "x. x:A  C(x) type"
  shows "?a : (x:A. B(x) + C(x))  (x:A. B(x)) + (x:A. C(x))"
apply (pc assms)
done

text "Construction of the currying functional"
schematic_goal "A type; B type; C type  ?a : (A × B  C)  (A  (B  C))"
apply pc
done

(*more general goal with same proof*)
schematic_goal
  assumes "A type"
    and "x. x:A  B(x) type"
    and "z. z: (x:A. B(x))  C(z) type"
  shows "?a : f: (z : (x:A . B(x)) . C(z)).
                      (x:A . y:B(x) . C(<x,y>))"
apply (pc assms)
done

text "Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)"
schematic_goal "A type; B type; C type  ?a : (A  (B  C))  (A × B  C)"
apply pc
done

(*more general goal with same proof*)
schematic_goal
  assumes "A type"
    and "x. x:A  B(x) type"
    and "z. z: (x:A . B(x))  C(z) type"
  shows "?a : (x:A . y:B(x) . C(<x,y>))
         (z : (x:A . B(x)) . C(z))"
apply (pc assms)
done

text "Function application"
schematic_goal "A type; B type  ?a : ((A  B) × A)  B"
apply pc
done

text "Basic test of quantifier reasoning"
schematic_goal
  assumes "A type"
    and "B type"
    and "x y. x:A; y:B  C(x,y) type"
  shows
    "?a :     (y:B . x:A . C(x,y))
           (x:A . y:B . C(x,y))"
apply (pc assms)
done

text "Martin-Löf (1984) pages 36-7: the combinator S"
schematic_goal
  assumes "A type"
    and "x. x:A  B(x) type"
    and "x y. x:A; y:B(x)  C(x,y) type"
  shows "?a :    (x:A. y:B(x). C(x,y))
              (f: (x:A. B(x)). x:A. C(x, f`x))"
apply (pc assms)
done

text "Martin-Löf (1984) page 58: the axiom of disjunction elimination"
schematic_goal
  assumes "A type"
    and "B type"
    and "z. z: A+B  C(z) type"
  shows "?a : (x:A. C(inl(x)))  (y:B. C(inr(y)))
           (z: A+B. C(z))"
apply (pc assms)
done

(*towards AXIOM OF CHOICE*)
schematic_goal [folded basic_defs]:
  "A type; B type; C type  ?a : (A  B × C)  (A  B) × (A  C)"
apply pc
done


(*Martin-Löf (1984) page 50*)
text "AXIOM OF CHOICE!  Delicate use of elimination rules"
schematic_goal
  assumes "A type"
    and "x. x:A  B(x) type"
    and "x y. x:A; y:B(x)  C(x,y) type"
  shows "?a : (x:A. y:B(x). C(x,y))  (f: (x:A. B(x)). x:A. C(x, f`x))"
apply (intr assms)
prefer 2 apply add_mp
prefer 2 apply add_mp
apply (erule SumE_fst)
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (rule_tac [4] SumE_snd)
apply (typechk SumE_fst assms)
done

text "Axiom of choice.  Proof without fst, snd.  Harder still!"
schematic_goal [folded basic_defs]:
  assumes "A type"
    and "x. x:A  B(x) type"
    and "x y. x:A; y:B(x)  C(x,y) type"
  shows "?a : (x:A. y:B(x). C(x,y))  (f: (x:A. B(x)). x:A. C(x, f`x))"
apply (intr assms)
(*Must not use add_mp as subst_prodE hides the construction.*)
apply (rule ProdE [THEN SumE])
apply assumption
apply assumption
apply assumption
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (erule_tac [4] ProdE [THEN SumE])
apply (typechk assms)
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (typechk assms)
apply assumption
done

text "Example of sequent-style deduction"
(*When splitting z:A × B, the assumption C(z) is affected;  ?a becomes
    λu. split(u,λv w.split(v,λx y.❙ λz. <x,<y,z>>) ` w)     *)
schematic_goal
  assumes "A type"
    and "B type"
    and "z. z:A × B  C(z) type"
  shows "?a : (z:A × B. C(z))  (u:A. v:B. C(<u,v>))"
apply (rule intr_rls)
apply (tactic biresolve_tac context safe_brls 2)
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
apply (rule_tac [2] a = "y" in ProdE)
apply (typechk assms)
apply (rule SumE, assumption)
apply intr
defer 1
apply assumption+
apply (typechk assms)
done

end