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:* ⊢ ❙λa:A. a : ?T" by (depth_solve rules) schematic_goal "A:* B:* b:B ⊢ ❙λx:A. b : ?T" by (depth_solve rules) schematic_goal "A:* b:A ⊢ (❙λa:A. a)⋅b: ?T" by (depth_solve rules) schematic_goal "A:* B:* c:A b:B ⊢ (❙λx:A. b)⋅ c: ?T" by (depth_solve rules) schematic_goal "A:* B:* ⊢ ❙λa:A. ❙λb:B. a : ?T" by (depth_solve rules) subsection ‹Second-order types› schematic_goal (in L2) "⊢ ❙λA:*. ❙λa:A. a : ?T" by (depth_solve rules) schematic_goal (in L2) "A:* ⊢ (❙λB:*. ❙λb:B. b)⋅A : ?T" by (depth_solve rules) schematic_goal (in L2) "A:* b:A ⊢ (❙λB:*. ❙λb:B. b) ⋅ A ⋅ b: ?T" by (depth_solve rules) schematic_goal (in L2) "⊢ ❙λB:*. ❙λa:(∏A:*.A).a ⋅ ((∏A:*.A)→B) ⋅ a: ?T" by (depth_solve rules) subsection ‹Weakly higher-order propositional logic› schematic_goal (in Lomega) "⊢ ❙λA:*.A→A : ?T" by (depth_solve rules) schematic_goal (in Lomega) "B:* ⊢ (❙λA:*.A→A) ⋅ B : ?T" by (depth_solve rules) schematic_goal (in Lomega) "B:* b:B ⊢ (❙λ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:* ⊢ ❙λ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→* ⊢ ❙λa:A. ❙λ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 ⊢ ❙λx:∏a:A. P⋅a→Q. ❙λ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) "⊢ ❙λA:*. ❙λB:*.∏C:*.(A→B→C)→C : ?T" by (depth_solve rules) schematic_goal (in Lomega2) "⊢ ❙λA:*. ❙λB:*. ❙λx:A. ❙λ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→* ⊢ ❙λ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:* ⊢ ❙λP:A→A→*. ❙λa:A. P⋅a⋅a : ?T" by (depth_solve rules) schematic_goal (in LPomega) "⊢ ❙λA:*. ❙λP:A→A→*. ❙λa:A. P⋅a⋅a : ?T" by (depth_solve rules) subsection ‹Constructions› schematic_goal (in CC) "⊢ ❙λA:*. ❙λP:A→*. ❙λa:A. P⋅a→∏P:*.P: ?T" by (depth_solve rules) schematic_goal (in CC) "⊢ ❙λA:*. ❙λ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 ⊢ ❙λa:A. ∏P:A→*.P⋅c → (∏x:A. P⋅x→P⋅(f⋅x)) → P⋅a : ?T" by (depth_solve rules) schematic_goal (in CC) "❙λA:*. ❙λc:A. ❙λf:A→A. ❙λ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 = "❙λ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