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