19761

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


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1991 University of Cambridge


4 


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

35762

6 
(Bibliopolis, 1984).

19761

7 
*)


8 


9 
header "Examples with elimination rules"


10 


11 
theory Elimination


12 
imports CTT


13 
begin


14 


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


16 

36319

17 
schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) > A"

19761

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


19 
done


20 

36319

21 
schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) > A"

19761

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


23 
back


24 
done


25 


26 
text "Double negation of the Excluded Middle"

36319

27 
schematic_lemma "A type ==> ?a : ((A + (A>F)) > F) > F"

19761

28 
apply (tactic "intr_tac []")


29 
apply (rule ProdE)


30 
apply assumption


31 
apply (tactic "pc_tac [] 1")


32 
done


33 

36319

34 
schematic_lemma "[ A type; B type ] ==> ?a : (A*B) > (B*A)"

19761

35 
apply (tactic "pc_tac [] 1")


36 
done


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


38 
by backtracking. No longer.*)


39 


40 
text "Binary sums and products"

36319

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

19761

42 
apply (tactic "pc_tac [] 1")


43 
done


44 


45 
(*A distributive law*)

36319

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

19761

47 
apply (tactic "pc_tac [] 1")


48 
done


49 


50 
(*more general version, same proof*)

36319

51 
schematic_lemma

19761

52 
assumes "A type"


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


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


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


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


57 
done


58 


59 
text "Construction of the currying functional"

36319

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

19761

61 
apply (tactic "pc_tac [] 1")


62 
done


63 


64 
(*more general goal with same proof*)

36319

65 
schematic_lemma

19761

66 
assumes "A type"


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


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


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


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


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


72 
done


73 


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

36319

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

19761

76 
apply (tactic "pc_tac [] 1")


77 
done


78 


79 
(*more general goal with same proof*)

36319

80 
schematic_lemma

19761

81 
assumes "A type"


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


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


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


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


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


87 
done


88 


89 
text "Function application"

36319

90 
schematic_lemma "[ A type; B type ] ==> ?a : ((A > B) * A) > B"

19761

91 
apply (tactic "pc_tac [] 1")


92 
done


93 


94 
text "Basic test of quantifier reasoning"

36319

95 
schematic_lemma

19761

96 
assumes "A type"


97 
and "B type"


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


99 
shows


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


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


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


103 
done


104 


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

36319

106 
schematic_lemma

19761

107 
assumes "A type"


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


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


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


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


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


113 
done


114 


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

36319

116 
schematic_lemma

19761

117 
assumes "A type"


118 
and "B type"


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


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


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


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


123 
done


124 


125 
(*towards AXIOM OF CHOICE*)

36319

126 
schematic_lemma [folded basic_defs]:

19761

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


128 
apply (tactic "pc_tac [] 1")


129 
done


130 


131 


132 
(*MartinLof (1984) page 50*)


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

36319

134 
schematic_lemma

19761

135 
assumes "A type"


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


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


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


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


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


141 
apply (tactic "add_mp_tac 2")


142 
apply (tactic "add_mp_tac 1")


143 
apply (erule SumE_fst)


144 
apply (rule replace_type)


145 
apply (rule subst_eqtyparg)


146 
apply (rule comp_rls)


147 
apply (rule_tac [4] SumE_snd)


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


149 
done


150 


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

36319

152 
schematic_lemma [folded basic_defs]:

19761

153 
assumes "A type"


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


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


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


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


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


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


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


161 
apply (tactic "TRYALL assume_tac")


162 
apply (rule replace_type)


163 
apply (rule subst_eqtyparg)


164 
apply (rule comp_rls)


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


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


167 
apply (rule replace_type)


168 
apply (rule subst_eqtyparg)


169 
apply (rule comp_rls)


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


171 
apply assumption


172 
done


173 


174 
text "Example of sequent_style deduction"


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


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

36319

177 
schematic_lemma

19761

178 
assumes "A type"


179 
and "B type"


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


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


182 
apply (rule intr_rls)


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


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


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


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


187 
apply (rule SumE, assumption)


188 
apply (tactic "intr_tac []")


189 
apply (tactic "TRYALL assume_tac")


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


191 
done


192 


193 
end
