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