wenzelm@58889: section \Lambda Cube Examples\ wenzelm@17453: wenzelm@17453: theory Example wenzelm@17453: imports Cube wenzelm@17453: begin wenzelm@17453: wenzelm@58617: text \Examples taken from: wenzelm@17453: wenzelm@17453: H. Barendregt. Introduction to Generalised Type Systems. wenzelm@58617: J. Functional Programming.\ wenzelm@17453: wenzelm@58617: method_setup depth_solve = wenzelm@58617: \Attrib.thms >> (fn thms => K (METHOD (fn facts => wenzelm@58617: (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))\ wenzelm@17453: wenzelm@58617: method_setup depth_solve1 = wenzelm@58617: \Attrib.thms >> (fn thms => K (METHOD (fn facts => wenzelm@58617: (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))\ wenzelm@17453: wenzelm@58617: method_setup strip_asms = wenzelm@58617: \Attrib.thms >> (fn thms => K (METHOD (fn facts => wenzelm@30549: REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN wenzelm@58617: DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))\ wenzelm@17453: wenzelm@17453: wenzelm@58617: subsection \Simple types\ wenzelm@17453: wenzelm@45242: schematic_lemma "A:* \ A\A : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma "A:* \ \ a:A. a : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma "A:* B:* b:B \ \ x:A. b : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma "A:* b:A \ (\ a:A. a)^b: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma "A:* B:* c:A b:B \ (\ x:A. b)^ c: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma "A:* B:* \ \ a:A. \ b:B. a : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@17453: wenzelm@58617: subsection \Second-order types\ wenzelm@17453: wenzelm@45242: schematic_lemma (in L2) "\ \ A:*. \ a:A. a : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in L2) "A:* \ (\ B:*.\ b:B. b)^A : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in L2) "A:* b:A \ (\ B:*.\ b:B. b) ^ A ^ b: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in L2) "\ \ B:*.\ a:(\ A:*.A).a ^ ((\ A:*.A)\B) ^ a: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@17453: wenzelm@58617: subsection \Weakly higher-order propositional logic\ wenzelm@17453: wenzelm@45242: schematic_lemma (in Lomega) "\ \ A:*.A\A : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in Lomega) "B:* \ (\ A:*.A\A) ^ B : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in Lomega) "B:* b:B \ (\ y:B. b): ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in Lomega) "A:* F:*\* \ F^(F^A): ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in Lomega) "A:* \ \ F:*\*.F^(F^A): ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@17453: wenzelm@58617: subsection \LP\ wenzelm@17453: wenzelm@45242: schematic_lemma (in LP) "A:* \ A \ * : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LP) "A:* P:A\* a:A \ P^a: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LP) "A:* P:A\A\* a:A \ \ a:A. P^a^a: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LP) "A:* P:A\* Q:A\* \ \ a:A. P^a \ Q^a: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LP) "A:* P:A\* \ \ a:A. P^a \ P^a: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LP) "A:* P:A\* \ \ a:A. \ x:P^a. x: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LP) "A:* P:A\* Q:* \ (\ a:A. P^a\Q) \ (\ a:A. P^a) \ Q : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LP) "A:* P:A\* Q:* a0:A \ wenzelm@45242: \ x:\ a:A. P^a\Q. \ y:\ a:A. P^a. x^a0^(y^a0): ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@17453: wenzelm@58617: subsection \Omega-order types\ wenzelm@17453: wenzelm@45242: schematic_lemma (in L2) "A:* B:* \ \ C:*.(A\B\C)\C : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in Lomega2) "\ \ A:*.\ B:*.\ C:*.(A\B\C)\C : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in Lomega2) "\ \ A:*.\ B:*.\ x:A. \ y:B. x : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in Lomega2) "A:* B:* \ ?p : (A\B) \ ((B\\ P:*.P)\(A\\ P:*.P))" wenzelm@17453: apply (strip_asms rules) wenzelm@17453: apply (rule lam_ss) wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply (rule lam_ss) wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply (rule lam_ss) wenzelm@17453: apply assumption wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply (erule pi_elim) wenzelm@17453: apply assumption wenzelm@17453: apply (erule pi_elim) wenzelm@17453: apply assumption wenzelm@17453: apply assumption wenzelm@17453: done wenzelm@17453: wenzelm@17453: wenzelm@58617: subsection \Second-order Predicate Logic\ wenzelm@17453: wenzelm@45242: schematic_lemma (in LP2) "A:* P:A\* \ \ a:A. P^a\(\ A:*.A) : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LP2) "A:* P:A\A\* \ wenzelm@45242: (\ a:A. \ b:A. P^a^b\P^b^a\\ P:*.P) \ \ a:A. P^a^a\\ P:*.P : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LP2) "A:* P:A\A\* \ wenzelm@45242: ?p: (\ a:A. \ b:A. P^a^b\P^b^a\\ P:*.P) \ \ a:A. P^a^a\\ P:*.P" wenzelm@58617: -- \Antisymmetry implies irreflexivity:\ wenzelm@17453: apply (strip_asms rules) wenzelm@17453: apply (rule lam_ss) wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply (rule lam_ss) wenzelm@17453: apply assumption wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply (rule lam_ss) wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply (erule pi_elim, assumption, assumption?)+ wenzelm@17453: done wenzelm@17453: wenzelm@17453: wenzelm@58617: subsection \LPomega\ wenzelm@17453: wenzelm@45242: schematic_lemma (in LPomega) "A:* \ \ P:A\A\*.\ a:A. P^a^a : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in LPomega) "\ \ A:*.\ P:A\A\*.\ a:A. P^a^a : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@17453: wenzelm@58617: subsection \Constructions\ wenzelm@17453: wenzelm@45242: schematic_lemma (in CC) "\ \ A:*.\ P:A\*.\ a:A. P^a\\ P:*.P: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in CC) "\ \ A:*.\ P:A\*.\ a:A. P^a: ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in CC) "A:* P:A\* a:A \ ?p : (\ a:A. P^a)\P^a" wenzelm@17453: apply (strip_asms rules) wenzelm@17453: apply (rule lam_ss) wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply (erule pi_elim, assumption, assumption) wenzelm@17453: done wenzelm@17453: wenzelm@17453: wenzelm@58617: subsection \Some random examples\ wenzelm@17453: wenzelm@45242: schematic_lemma (in LP2) "A:* c:A f:A\A \ wenzelm@45242: \ a:A. \ P:A\*.P^c \ (\ x:A. P^x\P^(f^x)) \ P^a : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@45242: schematic_lemma (in CC) "\ A:*.\ c:A. \ f:A\A. wenzelm@45242: \ a:A. \ P:A\*.P^c \ (\ x:A. P^x\P^(f^x)) \ P^a : ?T" wenzelm@17453: by (depth_solve rules) wenzelm@17453: wenzelm@36319: schematic_lemma (in LP2) wenzelm@45242: "A:* a:A b:A \ ?p: (\ P:A\*.P^a\P^b) \ (\ P:A\*.P^b\P^a)" wenzelm@58617: -- \Symmetry of Leibnitz equality\ wenzelm@17453: apply (strip_asms rules) wenzelm@17453: apply (rule lam_ss) wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@45242: apply (erule_tac a = "\ x:A. \ Q:A\*.Q^x\Q^a" in pi_elim) wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply (unfold beta) wenzelm@17453: apply (erule imp_elim) wenzelm@17453: apply (rule lam_bs) wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply (rule lam_ss) wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: prefer 2 wenzelm@17453: apply (depth_solve1 rules) wenzelm@17453: apply assumption wenzelm@17453: apply assumption wenzelm@17453: done wenzelm@17453: wenzelm@17453: end