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 

58889

9 
section "Examples with elimination rules"

19761

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"

58972

18 
apply pc

19761

19 
done


20 

36319

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

58972

22 
apply pc

19761

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"

58972

28 
apply intr

19761

29 
apply (rule ProdE)


30 
apply assumption

58972

31 
apply pc

19761

32 
done


33 

36319

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

58972

35 
apply pc

19761

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

58972

42 
apply pc

19761

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

58972

47 
apply pc

19761

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

58972

56 
apply (pc assms)

19761

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

58972

61 
apply pc

19761

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

58972

71 
apply (pc assms)

19761

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

58972

76 
apply pc

19761

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

58972

86 
apply (pc assms)

19761

87 
done


88 


89 
text "Function application"

36319

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

58972

91 
apply pc

19761

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

58972

102 
apply (pc assms)

19761

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

58972

112 
apply (pc assms)

19761

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

58972

122 
apply (pc assms)

19761

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

58972

128 
apply pc

19761

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

58972

140 
apply (intr assms)


141 
prefer 2 apply add_mp


142 
prefer 2 apply add_mp

19761

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)

58972

148 
apply (typechk SumE_fst assms)

19761

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

58972

158 
apply (intr assms)


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


160 
apply (rule ProdE [THEN SumE])


161 
apply assumption


162 
apply assumption


163 
apply assumption

19761

164 
apply (rule replace_type)


165 
apply (rule subst_eqtyparg)


166 
apply (rule comp_rls)


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

58972

168 
apply (typechk assms)

19761

169 
apply (rule replace_type)


170 
apply (rule subst_eqtyparg)


171 
apply (rule comp_rls)

58972

172 
apply (typechk assms)

19761

173 
apply assumption


174 
done


175 


176 
text "Example of sequent_style deduction"


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


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

36319

179 
schematic_lemma

19761

180 
assumes "A type"


181 
and "B type"


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


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


184 
apply (rule intr_rls)


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


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


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

58972

188 
apply (typechk assms)

19761

189 
apply (rule SumE, assumption)

58972

190 
apply intr


191 
defer 1


192 
apply assumption+


193 
apply (typechk assms)

19761

194 
done


195 


196 
end
