1section \<open>Lambda Cube Examples\<close> 2 3theory Example 4imports Cube 5begin 6 7text \<open>Examples taken from: 8 9 H. Barendregt. Introduction to Generalised Type Systems. 10 J. Functional Programming.\<close> 11 12method_setup depth_solve = 13 \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts => 14 (DEPTH_SOLVE (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close> 15 16method_setup depth_solve1 = 17 \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts => 18 (DEPTH_SOLVE_1 (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close> 19 20method_setup strip_asms = 21 \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts => 22 REPEAT (resolve_tac ctxt @{thms strip_b strip_s} 1 THEN 23 DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close> 24 25 26subsection \<open>Simple types\<close> 27 28schematic_goal "A:* \<turnstile> A\<rightarrow>A : ?T" 29 by (depth_solve rules) 30 31schematic_goal "A:* \<turnstile> \<^bold>\<lambda>a:A. a : ?T" 32 by (depth_solve rules) 33 34schematic_goal "A:* B:* b:B \<turnstile> \<^bold>\<lambda>x:A. b : ?T" 35 by (depth_solve rules) 36 37schematic_goal "A:* b:A \<turnstile> (\<^bold>\<lambda>a:A. a)\<cdot>b: ?T" 38 by (depth_solve rules) 39 40schematic_goal "A:* B:* c:A b:B \<turnstile> (\<^bold>\<lambda>x:A. b)\<cdot> c: ?T" 41 by (depth_solve rules) 42 43schematic_goal "A:* B:* \<turnstile> \<^bold>\<lambda>a:A. \<^bold>\<lambda>b:B. a : ?T" 44 by (depth_solve rules) 45 46 47subsection \<open>Second-order types\<close> 48 49schematic_goal (in L2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>a:A. a : ?T" 50 by (depth_solve rules) 51 52schematic_goal (in L2) "A:* \<turnstile> (\<^bold>\<lambda>B:*. \<^bold>\<lambda>b:B. b)\<cdot>A : ?T" 53 by (depth_solve rules) 54 55schematic_goal (in L2) "A:* b:A \<turnstile> (\<^bold>\<lambda>B:*. \<^bold>\<lambda>b:B. b) \<cdot> A \<cdot> b: ?T" 56 by (depth_solve rules) 57 58schematic_goal (in L2) "\<turnstile> \<^bold>\<lambda>B:*. \<^bold>\<lambda>a:(\<Prod>A:*.A).a \<cdot> ((\<Prod>A:*.A)\<rightarrow>B) \<cdot> a: ?T" 59 by (depth_solve rules) 60 61 62subsection \<open>Weakly higher-order propositional logic\<close> 63 64schematic_goal (in Lomega) "\<turnstile> \<^bold>\<lambda>A:*.A\<rightarrow>A : ?T" 65 by (depth_solve rules) 66 67schematic_goal (in Lomega) "B:* \<turnstile> (\<^bold>\<lambda>A:*.A\<rightarrow>A) \<cdot> B : ?T" 68 by (depth_solve rules) 69 70schematic_goal (in Lomega) "B:* b:B \<turnstile> (\<^bold>\<lambda>y:B. b): ?T" 71 by (depth_solve rules) 72 73schematic_goal (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F\<cdot>(F\<cdot>A): ?T" 74 by (depth_solve rules) 75 76schematic_goal (in Lomega) "A:* \<turnstile> \<^bold>\<lambda>F:*\<rightarrow>*.F\<cdot>(F\<cdot>A): ?T" 77 by (depth_solve rules) 78 79 80subsection \<open>LP\<close> 81 82schematic_goal (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T" 83 by (depth_solve rules) 84 85schematic_goal (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P\<cdot>a: ?T" 86 by (depth_solve rules) 87 88schematic_goal (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Prod>a:A. P\<cdot>a\<cdot>a: ?T" 89 by (depth_solve rules) 90 91schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Prod>a:A. P\<cdot>a \<rightarrow> Q\<cdot>a: ?T" 92 by (depth_solve rules) 93 94schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Prod>a:A. P\<cdot>a \<rightarrow> P\<cdot>a: ?T" 95 by (depth_solve rules) 96 97schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<^bold>\<lambda>a:A. \<^bold>\<lambda>x:P\<cdot>a. x: ?T" 98 by (depth_solve rules) 99 100schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* \<turnstile> (\<Prod>a:A. P\<cdot>a\<rightarrow>Q) \<rightarrow> (\<Prod>a:A. P\<cdot>a) \<rightarrow> Q : ?T" 101 by (depth_solve rules) 102 103schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile> 104 \<^bold>\<lambda>x:\<Prod>a:A. P\<cdot>a\<rightarrow>Q. \<^bold>\<lambda>y:\<Prod>a:A. P\<cdot>a. x\<cdot>a0\<cdot>(y\<cdot>a0): ?T" 105 by (depth_solve rules) 106 107 108subsection \<open>Omega-order types\<close> 109 110schematic_goal (in L2) "A:* B:* \<turnstile> \<Prod>C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" 111 by (depth_solve rules) 112 113schematic_goal (in Lomega2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>B:*.\<Prod>C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" 114 by (depth_solve rules) 115 116schematic_goal (in Lomega2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>B:*. \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : ?T" 117 by (depth_solve rules) 118 119schematic_goal (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Prod>P:*.P)\<rightarrow>(A\<rightarrow>\<Prod>P:*.P))" 120 apply (strip_asms rules) 121 apply (rule lam_ss) 122 apply (depth_solve1 rules) 123 prefer 2 124 apply (depth_solve1 rules) 125 apply (rule lam_ss) 126 apply (depth_solve1 rules) 127 prefer 2 128 apply (depth_solve1 rules) 129 apply (rule lam_ss) 130 apply assumption 131 prefer 2 132 apply (depth_solve1 rules) 133 apply (erule pi_elim) 134 apply assumption 135 apply (erule pi_elim) 136 apply assumption 137 apply assumption 138 done 139 140 141subsection \<open>Second-order Predicate Logic\<close> 142 143schematic_goal (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<^bold>\<lambda>a:A. P\<cdot>a\<rightarrow>(\<Prod>A:*.A) : ?T" 144 by (depth_solve rules) 145 146schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile> 147 (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P : ?T" 148 by (depth_solve rules) 149 150schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile> 151 ?p: (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P" 152 \<comment> \<open>Antisymmetry implies irreflexivity:\<close> 153 apply (strip_asms rules) 154 apply (rule lam_ss) 155 apply (depth_solve1 rules) 156 prefer 2 157 apply (depth_solve1 rules) 158 apply (rule lam_ss) 159 apply assumption 160 prefer 2 161 apply (depth_solve1 rules) 162 apply (rule lam_ss) 163 apply (depth_solve1 rules) 164 prefer 2 165 apply (depth_solve1 rules) 166 apply (erule pi_elim, assumption, assumption?)+ 167 done 168 169 170subsection \<open>LPomega\<close> 171 172schematic_goal (in LPomega) "A:* \<turnstile> \<^bold>\<lambda>P:A\<rightarrow>A\<rightarrow>*. \<^bold>\<lambda>a:A. P\<cdot>a\<cdot>a : ?T" 173 by (depth_solve rules) 174 175schematic_goal (in LPomega) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>P:A\<rightarrow>A\<rightarrow>*. \<^bold>\<lambda>a:A. P\<cdot>a\<cdot>a : ?T" 176 by (depth_solve rules) 177 178 179subsection \<open>Constructions\<close> 180 181schematic_goal (in CC) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>P:A\<rightarrow>*. \<^bold>\<lambda>a:A. P\<cdot>a\<rightarrow>\<Prod>P:*.P: ?T" 182 by (depth_solve rules) 183 184schematic_goal (in CC) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>P:A\<rightarrow>*.\<Prod>a:A. P\<cdot>a: ?T" 185 by (depth_solve rules) 186 187schematic_goal (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Prod>a:A. P\<cdot>a)\<rightarrow>P\<cdot>a" 188 apply (strip_asms rules) 189 apply (rule lam_ss) 190 apply (depth_solve1 rules) 191 prefer 2 192 apply (depth_solve1 rules) 193 apply (erule pi_elim, assumption, assumption) 194 done 195 196 197subsection \<open>Some random examples\<close> 198 199schematic_goal (in LP2) "A:* c:A f:A\<rightarrow>A \<turnstile> 200 \<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>a : ?T" 201 by (depth_solve rules) 202 203schematic_goal (in CC) "\<^bold>\<lambda>A:*. \<^bold>\<lambda>c:A. \<^bold>\<lambda>f:A\<rightarrow>A. 204 \<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>a : ?T" 205 by (depth_solve rules) 206 207schematic_goal (in LP2) 208 "A:* a:A b:A \<turnstile> ?p: (\<Prod>P:A\<rightarrow>*.P\<cdot>a\<rightarrow>P\<cdot>b) \<rightarrow> (\<Prod>P:A\<rightarrow>*.P\<cdot>b\<rightarrow>P\<cdot>a)" 209 \<comment> \<open>Symmetry of Leibnitz equality\<close> 210 apply (strip_asms rules) 211 apply (rule lam_ss) 212 apply (depth_solve1 rules) 213 prefer 2 214 apply (depth_solve1 rules) 215 apply (erule_tac a = "\<^bold>\<lambda>x:A. \<Prod>Q:A\<rightarrow>*.Q\<cdot>x\<rightarrow>Q\<cdot>a" in pi_elim) 216 apply (depth_solve1 rules) 217 apply (unfold beta) 218 apply (erule imp_elim) 219 apply (rule lam_bs) 220 apply (depth_solve1 rules) 221 prefer 2 222 apply (depth_solve1 rules) 223 apply (rule lam_ss) 224 apply (depth_solve1 rules) 225 prefer 2 226 apply (depth_solve1 rules) 227 apply assumption 228 apply assumption 229 done 230 231end 232