# Theory Elimination

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

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 "(❙λf. f ` inr(❙λy. f ` inl(y))) : ((A + (A⟶F)) ⟶ F) ⟶ F"
proof intr
fix f
assume f: "f : A + (A ⟶ F) ⟶ F"
with assms have "inr(❙λy. f ` inl(y)) : A + (A ⟶ F)"
by pc
then show "f ` inr(❙λ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(<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)
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 "(❙λf. <❙λx. fst(f`x), ❙λ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 "(❙λ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, (❙λ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 × 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
```