1(* Title: CTT/ex/Elimination.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1991 University of Cambridge 4 5Some examples taken from P. Martin-L\"of, Intuitionistic type theory 6(Bibliopolis, 1984). 7*) 8 9section "Examples with elimination rules" 10 11theory Elimination 12imports "../CTT" 13begin 14 15text "This finds the functions fst and snd!" 16 17schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A" 18apply pc 19done 20 21schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A" 22apply pc 23back 24done 25 26text "Double negation of the Excluded Middle" 27schematic_goal "A type \<Longrightarrow> ?a : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F" 28apply intr 29apply (rule ProdE) 30apply assumption 31apply pc 32done 33 34schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B) \<longrightarrow> (B \<times> A)" 35apply pc 36done 37(*The sequent version (ITT) could produce an interesting alternative 38 by backtracking. No longer.*) 39 40text "Binary sums and products" 41schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A + B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> C) \<times> (B \<longrightarrow> C)" 42apply pc 43done 44 45(*A distributive law*) 46schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A \<times> (B + C) \<longrightarrow> (A \<times> B + A \<times> C)" 47apply pc 48done 49 50(*more general version, same proof*) 51schematic_goal 52 assumes "A type" 53 and "\<And>x. x:A \<Longrightarrow> B(x) type" 54 and "\<And>x. x:A \<Longrightarrow> C(x) type" 55 shows "?a : (\<Sum>x:A. B(x) + C(x)) \<longrightarrow> (\<Sum>x:A. B(x)) + (\<Sum>x:A. C(x))" 56apply (pc assms) 57done 58 59text "Construction of the currying functional" 60schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))" 61apply pc 62done 63 64(*more general goal with same proof*) 65schematic_goal 66 assumes "A type" 67 and "\<And>x. x:A \<Longrightarrow> B(x) type" 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>))" 71apply (pc assms) 72done 73 74text "Martin-L��f (1984), page 48: axiom of sum-elimination (uncurry)" 75schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<times> B \<longrightarrow> C)" 76apply pc 77done 78 79(*more general goal with same proof*) 80schematic_goal 81 assumes "A type" 82 and "\<And>x. x:A \<Longrightarrow> B(x) type" 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))" 86apply (pc assms) 87done 88 89text "Function application" 90schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A \<longrightarrow> B) \<times> A) \<longrightarrow> B" 91apply pc 92done 93 94text "Basic test of quantifier reasoning" 95schematic_goal 96 assumes "A type" 97 and "B type" 98 and "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> C(x,y) type" 99 shows 100 "?a : (\<Sum>y:B . \<Prod>x:A . C(x,y)) 101 \<longrightarrow> (\<Prod>x:A . \<Sum>y:B . C(x,y))" 102apply (pc assms) 103done 104 105text "Martin-L��f (1984) pages 36-7: the combinator S" 106schematic_goal 107 assumes "A type" 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" 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))" 112apply (pc assms) 113done 114 115text "Martin-L��f (1984) page 58: the axiom of disjunction elimination" 116schematic_goal 117 assumes "A type" 118 and "B type" 119 and "\<And>z. z: A+B \<Longrightarrow> C(z) type" 120 shows "?a : (\<Prod>x:A. C(inl(x))) \<longrightarrow> (\<Prod>y:B. C(inr(y))) 121 \<longrightarrow> (\<Prod>z: A+B. C(z))" 122apply (pc assms) 123done 124 125(*towards AXIOM OF CHOICE*) 126schematic_goal [folded basic_defs]: 127 "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> B \<times> C) \<longrightarrow> (A \<longrightarrow> B) \<times> (A \<longrightarrow> C)" 128apply pc 129done 130 131 132(*Martin-L��f (1984) page 50*) 133text "AXIOM OF CHOICE! Delicate use of elimination rules" 134schematic_goal 135 assumes "A type" 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" 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))" 139apply (intr assms) 140prefer 2 apply add_mp 141prefer 2 apply add_mp 142apply (erule SumE_fst) 143apply (rule replace_type) 144apply (rule subst_eqtyparg) 145apply (rule comp_rls) 146apply (rule_tac [4] SumE_snd) 147apply (typechk SumE_fst assms) 148done 149 150text "Axiom of choice. Proof without fst, snd. Harder still!" 151schematic_goal [folded basic_defs]: 152 assumes "A type" 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" 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))" 156apply (intr assms) 157(*Must not use add_mp as subst_prodE hides the construction.*) 158apply (rule ProdE [THEN SumE]) 159apply assumption 160apply assumption 161apply assumption 162apply (rule replace_type) 163apply (rule subst_eqtyparg) 164apply (rule comp_rls) 165apply (erule_tac [4] ProdE [THEN SumE]) 166apply (typechk assms) 167apply (rule replace_type) 168apply (rule subst_eqtyparg) 169apply (rule comp_rls) 170apply (typechk assms) 171apply assumption 172done 173 174text "Example of sequent-style deduction" 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) *) 177schematic_goal 178 assumes "A type" 179 and "B type" 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>))" 182apply (rule intr_rls) 183apply (tactic \<open>biresolve_tac \<^context> safe_brls 2\<close>) 184(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *) 185apply (rule_tac [2] a = "y" in ProdE) 186apply (typechk assms) 187apply (rule SumE, assumption) 188apply intr 189defer 1 190apply assumption+ 191apply (typechk assms) 192done 193 194end 195