# Theory Example

```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
```