Quelle  Elimination.thy   Sprache: Isabelle

(*  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 + (A\F)) \ F) \ F"
  apply intr
  apply (rule ProdE)
   apply assumption
  apply pc
  done

text ‹Experiment: the proof above in Isar›
lemma
  assumes "A type" shows "(\<^bold>\f. f ` inr(\<^bold>\y. f ` inl(y))) : ((A + (A\F)) \ F) \ F"
proof intr
  fix f
  assume f: "f : A + (A \ F) \ F" 
  with assms have "inr(\<^bold>\y. f ` inl(y)) : A + (A \ F)"
    by pc
  then show "f ` inr(\<^bold>\y. f ` inl(y)) : F" 
    by (rule ProdE [OF f])
qed (rule assms)+

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)"
  by pc

(*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())
        ⟶ (∏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 ‹A structured proof of AC›
lemma Axiom_of_Choice:
  assumes "A type"
    and "\x. x:A \ B(x) type"
    and "\x y. \x:A; y:B(x)\ \ C(x,y) type"
  shows "(\<^bold>\f. <\<^bold>\x. fst(f`x), \<^bold>\x. snd(f`x)>)
        : (∏x:A. ∑y:B(x). C(x,y)) ⟶ (∑f: (∏x:A. B(x)). ∏x:A. C(x, f`x))"
proof (intr assms)
  fix f a
  assume f: "f : \x:A. Sum(B(x), C(x))" and "a : A" 
  then have fa: "f`a : Sum(B(a), C(a))"
    by (rule ProdE)
  then show "fst(f ` a) : B(a)" 
    by (rule SumE_fst)
  have "snd(f ` a) : C(a, fst(f ` a))"
    by (rule SumE_snd [OF fa]) (typechk SumE_fst assms ‹a : A›)
  moreover have "(\<^bold>\x. fst(f ` x)) ` a = fst(f ` a) : B(a)"
    by (rule ProdC [OF ‹a : A›]) (typechk SumE_fst f)
  ultimately show "snd(f`a) : C(a, (\<^bold>\x. fst(f ` x)) ` a)"
    by (intro replace_type [OF subst_eqtyparg]) (typechk SumE_fst assms ‹a : A›)
qed

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 \<times> B, the assumption C(z) is affected;  ?a becomes
    \<^bold>\<lambda>u. split(u,\<lambda>v w.split(v,\<lambda>x y.\<^bold> \<lambda>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())"
  apply (rule intr_rls)
   apply (tactic ‹biresolve_tac 🍋 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