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

58974

12 
imports "../CTT"

19761

13 
begin


14 


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


16 

61391

17 
schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"

58972

18 
apply pc

19761

19 
done


20 

61391

21 
schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"

58972

22 
apply pc

19761

23 
back


24 
done


25 


26 
text "Double negation of the Excluded Middle"

61391

27 
schematic_goal "A type \<Longrightarrow> ?a : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"

58972

28 
apply intr

19761

29 
apply (rule ProdE)


30 
apply assumption

58972

31 
apply pc

19761

32 
done


33 

61391

34 
schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B) \<longrightarrow> (B \<times> 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"

61391

41 
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A + B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> C) \<times> (B \<longrightarrow> C)"

58972

42 
apply pc

19761

43 
done


44 


45 
(*A distributive law*)

61391

46 
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A \<times> (B + C) \<longrightarrow> (A \<times> B + A \<times> C)"

58972

47 
apply pc

19761

48 
done


49 


50 
(*more general version, same proof*)

61337

51 
schematic_goal

19761

52 
assumes "A type"

58977

53 
and "\<And>x. x:A \<Longrightarrow> B(x) type"


54 
and "\<And>x. x:A \<Longrightarrow> C(x) type"

61391

55 
shows "?a : (\<Sum>x:A. B(x) + C(x)) \<longrightarrow> (\<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"

61391

60 
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))"

58972

61 
apply pc

19761

62 
done


63 


64 
(*more general goal with same proof*)

61337

65 
schematic_goal

19761

66 
assumes "A type"

58977

67 
and "\<And>x. x:A \<Longrightarrow> B(x) type"

61391

68 
and "\<And>z. z: (\<Sum>x:A. B(x)) \<Longrightarrow> 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 

61391

74 
text "MartinLöf (1984), page 48: axiom of sumelimination (uncurry)"


75 
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<times> B \<longrightarrow> C)"

58972

76 
apply pc

19761

77 
done


78 


79 
(*more general goal with same proof*)

61337

80 
schematic_goal

19761

81 
assumes "A type"

58977

82 
and "\<And>x. x:A \<Longrightarrow> B(x) type"

61391

83 
and "\<And>z. z: (\<Sum>x:A . B(x)) \<Longrightarrow> C(z) type"


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


85 
\<longrightarrow> (\<Prod>z : (\<Sum>x:A . B(x)) . C(z))"

58972

86 
apply (pc assms)

19761

87 
done


88 


89 
text "Function application"

61391

90 
schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A \<longrightarrow> B) \<times> A) \<longrightarrow> B"

58972

91 
apply pc

19761

92 
done


93 


94 
text "Basic test of quantifier reasoning"

61337

95 
schematic_goal

19761

96 
assumes "A type"


97 
and "B type"

58977

98 
and "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> C(x,y) type"

19761

99 
shows

61391

100 
"?a : (\<Sum>y:B . \<Prod>x:A . C(x,y))


101 
\<longrightarrow> (\<Prod>x:A . \<Sum>y:B . C(x,y))"

58972

102 
apply (pc assms)

19761

103 
done


104 

61391

105 
text "MartinLöf (1984) pages 367: the combinator S"

61337

106 
schematic_goal

19761

107 
assumes "A type"

58977

108 
and "\<And>x. x:A \<Longrightarrow> B(x) type"


109 
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"

61391

110 
shows "?a : (\<Prod>x:A. \<Prod>y:B(x). C(x,y))


111 
\<longrightarrow> (\<Prod>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"

58972

112 
apply (pc assms)

19761

113 
done


114 

61391

115 
text "MartinLöf (1984) page 58: the axiom of disjunction elimination"

61337

116 
schematic_goal

19761

117 
assumes "A type"


118 
and "B type"

58977

119 
and "\<And>z. z: A+B \<Longrightarrow> C(z) type"

61391

120 
shows "?a : (\<Prod>x:A. C(inl(x))) \<longrightarrow> (\<Prod>y:B. C(inr(y)))


121 
\<longrightarrow> (\<Prod>z: A+B. C(z))"

58972

122 
apply (pc assms)

19761

123 
done


124 


125 
(*towards AXIOM OF CHOICE*)

61337

126 
schematic_goal [folded basic_defs]:

61391

127 
"\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> B \<times> C) \<longrightarrow> (A \<longrightarrow> B) \<times> (A \<longrightarrow> C)"

58972

128 
apply pc

19761

129 
done


130 


131 

61391

132 
(*MartinLöf (1984) page 50*)

19761

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

61337

134 
schematic_goal

19761

135 
assumes "A type"

58977

136 
and "\<And>x. x:A \<Longrightarrow> B(x) type"


137 
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"

64980

138 
shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"

58972

139 
apply (intr assms)


140 
prefer 2 apply add_mp


141 
prefer 2 apply add_mp

19761

142 
apply (erule SumE_fst)


143 
apply (rule replace_type)


144 
apply (rule subst_eqtyparg)


145 
apply (rule comp_rls)


146 
apply (rule_tac [4] SumE_snd)

58972

147 
apply (typechk SumE_fst assms)

19761

148 
done


149 


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

61337

151 
schematic_goal [folded basic_defs]:

19761

152 
assumes "A type"

58977

153 
and "\<And>x. x:A \<Longrightarrow> B(x) type"


154 
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"

64980

155 
shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"

58972

156 
apply (intr assms)


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


158 
apply (rule ProdE [THEN SumE])


159 
apply assumption


160 
apply assumption


161 
apply assumption

19761

162 
apply (rule replace_type)


163 
apply (rule subst_eqtyparg)


164 
apply (rule comp_rls)


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

58972

166 
apply (typechk assms)

19761

167 
apply (rule replace_type)


168 
apply (rule subst_eqtyparg)


169 
apply (rule comp_rls)

58972

170 
apply (typechk assms)

19761

171 
apply assumption


172 
done


173 

63505

174 
text "Example of sequentstyle deduction"

61391

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


176 
\<^bold>\<lambda>u. split(u,\<lambda>v w.split(v,\<lambda>x y.\<^bold> \<lambda>z. <x,<y,z>>) ` w) *)

61337

177 
schematic_goal

19761

178 
assumes "A type"


179 
and "B type"

61391

180 
and "\<And>z. z:A \<times> B \<Longrightarrow> C(z) type"


181 
shows "?a : (\<Sum>z:A \<times> B. C(z)) \<longrightarrow> (\<Sum>u:A. \<Sum>v:B. C(<u,v>))"

19761

182 
apply (rule intr_rls)

69593

183 
apply (tactic \<open>biresolve_tac \<^context> safe_brls 2\<close>)

19761

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


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

58972

186 
apply (typechk assms)

19761

187 
apply (rule SumE, assumption)

58972

188 
apply intr


189 
defer 1


190 
apply assumption+


191 
apply (typechk assms)

19761

192 
done


193 


194 
end
