19761

1 
(* Title: CTT/ex/Elimination.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Some examples taken from P. MartinL\"of, Intuitionistic type theory


7 
(Bibliopolis, 1984).


8 
*)


9 


10 
header "Examples with elimination rules"


11 


12 
theory Elimination


13 
imports CTT


14 
begin


15 


16 
text "This finds the functions fst and snd!"


17 


18 
lemma [folded basic_defs]: "A type ==> ?a : (A*A) > A"


19 
apply (tactic {* pc_tac [] 1 *})


20 
done


21 


22 
lemma [folded basic_defs]: "A type ==> ?a : (A*A) > A"


23 
apply (tactic {* pc_tac [] 1 *})


24 
back


25 
done


26 


27 
text "Double negation of the Excluded Middle"


28 
lemma "A type ==> ?a : ((A + (A>F)) > F) > F"


29 
apply (tactic "intr_tac []")


30 
apply (rule ProdE)


31 
apply assumption


32 
apply (tactic "pc_tac [] 1")


33 
done


34 


35 
lemma "[ A type; B type ] ==> ?a : (A*B) > (B*A)"


36 
apply (tactic "pc_tac [] 1")


37 
done


38 
(*The sequent version (ITT) could produce an interesting alternative


39 
by backtracking. No longer.*)


40 


41 
text "Binary sums and products"


42 
lemma "[ A type; B type; C type ] ==> ?a : (A+B > C) > (A>C) * (B>C)"


43 
apply (tactic "pc_tac [] 1")


44 
done


45 


46 
(*A distributive law*)


47 
lemma "[ A type; B type; C type ] ==> ?a : A * (B+C) > (A*B + A*C)"


48 
apply (tactic "pc_tac [] 1")


49 
done


50 


51 
(*more general version, same proof*)


52 
lemma


53 
assumes "A type"


54 
and "!!x. x:A ==> B(x) type"


55 
and "!!x. x:A ==> C(x) type"


56 
shows "?a : (SUM x:A. B(x) + C(x)) > (SUM x:A. B(x)) + (SUM x:A. C(x))"


57 
apply (tactic {* pc_tac (thms "prems") 1 *})


58 
done


59 


60 
text "Construction of the currying functional"


61 
lemma "[ A type; B type; C type ] ==> ?a : (A*B > C) > (A> (B>C))"


62 
apply (tactic "pc_tac [] 1")


63 
done


64 


65 
(*more general goal with same proof*)


66 
lemma


67 
assumes "A type"


68 
and "!!x. x:A ==> B(x) type"


69 
and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"


70 
shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).


71 
(PROD x:A . PROD y:B(x) . C(<x,y>))"


72 
apply (tactic {* pc_tac (thms "prems") 1 *})


73 
done


74 


75 
text "MartinLof (1984), page 48: axiom of sumelimination (uncurry)"


76 
lemma "[ A type; B type; C type ] ==> ?a : (A > (B>C)) > (A*B > C)"


77 
apply (tactic "pc_tac [] 1")


78 
done


79 


80 
(*more general goal with same proof*)


81 
lemma


82 
assumes "A type"


83 
and "!!x. x:A ==> B(x) type"


84 
and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"


85 
shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))


86 
> (PROD z : (SUM x:A . B(x)) . C(z))"


87 
apply (tactic {* pc_tac (thms "prems") 1 *})


88 
done


89 


90 
text "Function application"


91 
lemma "[ A type; B type ] ==> ?a : ((A > B) * A) > B"


92 
apply (tactic "pc_tac [] 1")


93 
done


94 


95 
text "Basic test of quantifier reasoning"


96 
lemma


97 
assumes "A type"


98 
and "B type"


99 
and "!!x y.[ x:A; y:B ] ==> C(x,y) type"


100 
shows


101 
"?a : (SUM y:B . PROD x:A . C(x,y))


102 
> (PROD x:A . SUM y:B . C(x,y))"


103 
apply (tactic {* pc_tac (thms "prems") 1 *})


104 
done


105 


106 
text "MartinLof (1984) pages 367: the combinator S"


107 
lemma


108 
assumes "A type"


109 
and "!!x. x:A ==> B(x) type"


110 
and "!!x y.[ x:A; y:B(x) ] ==> C(x,y) type"


111 
shows "?a : (PROD x:A. PROD y:B(x). C(x,y))


112 
> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"


113 
apply (tactic {* pc_tac (thms "prems") 1 *})


114 
done


115 


116 
text "MartinLof (1984) page 58: the axiom of disjunction elimination"


117 
lemma


118 
assumes "A type"


119 
and "B type"


120 
and "!!z. z: A+B ==> C(z) type"


121 
shows "?a : (PROD x:A. C(inl(x))) > (PROD y:B. C(inr(y)))


122 
> (PROD z: A+B. C(z))"


123 
apply (tactic {* pc_tac (thms "prems") 1 *})


124 
done


125 


126 
(*towards AXIOM OF CHOICE*)


127 
lemma [folded basic_defs]:


128 
"[ A type; B type; C type ] ==> ?a : (A > B*C) > (A>B) * (A>C)"


129 
apply (tactic "pc_tac [] 1")


130 
done


131 


132 


133 
(*MartinLof (1984) page 50*)


134 
text "AXIOM OF CHOICE! Delicate use of elimination rules"


135 
lemma


136 
assumes "A type"


137 
and "!!x. x:A ==> B(x) type"


138 
and "!!x y.[ x:A; y:B(x) ] ==> C(x,y) type"


139 
shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).


140 
(SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"


141 
apply (tactic {* intr_tac (thms "prems") *})


142 
apply (tactic "add_mp_tac 2")


143 
apply (tactic "add_mp_tac 1")


144 
apply (erule SumE_fst)


145 
apply (rule replace_type)


146 
apply (rule subst_eqtyparg)


147 
apply (rule comp_rls)


148 
apply (rule_tac [4] SumE_snd)


149 
apply (tactic {* typechk_tac (thm "SumE_fst" :: thms "prems") *})


150 
done


151 


152 
text "Axiom of choice. Proof without fst, snd. Harder still!"


153 
lemma [folded basic_defs]:


154 
assumes "A type"


155 
and "!!x. x:A ==> B(x) type"


156 
and "!!x y.[ x:A; y:B(x) ] ==> C(x,y) type"


157 
shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).


158 
(SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"


159 
apply (tactic {* intr_tac (thms "prems") *})


160 
(*Must not use add_mp_tac as subst_prodE hides the construction.*)


161 
apply (rule ProdE [THEN SumE], assumption)


162 
apply (tactic "TRYALL assume_tac")


163 
apply (rule replace_type)


164 
apply (rule subst_eqtyparg)


165 
apply (rule comp_rls)


166 
apply (erule_tac [4] ProdE [THEN SumE])


167 
apply (tactic {* typechk_tac (thms "prems") *})


168 
apply (rule replace_type)


169 
apply (rule subst_eqtyparg)


170 
apply (rule comp_rls)


171 
apply (tactic {* typechk_tac (thms "prems") *})


172 
apply assumption


173 
done


174 


175 
text "Example of sequent_style deduction"


176 
(*When splitting z:A*B, the assumption C(z) is affected; ?a becomes


177 
lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w) *)


178 
lemma


179 
assumes "A type"


180 
and "B type"


181 
and "!!z. z:A*B ==> C(z) type"


182 
shows "?a : (SUM z:A*B. C(z)) > (SUM u:A. SUM v:B. C(<u,v>))"


183 
apply (rule intr_rls)


184 
apply (tactic {* biresolve_tac safe_brls 2 *})


185 
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)


186 
apply (rule_tac [2] a = "y" in ProdE)


187 
apply (tactic {* typechk_tac (thms "prems") *})


188 
apply (rule SumE, assumption)


189 
apply (tactic "intr_tac []")


190 
apply (tactic "TRYALL assume_tac")


191 
apply (tactic {* typechk_tac (thms "prems") *})


192 
done


193 


194 
end
