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:* ⊨ \<lambda>a:A. a : ?T"
  by (depth_solve rules)

schematic_goal "A:* B:* b:B ⊨ \<lambda>x:A. b : ?T"
  by (depth_solve rules)

schematic_goal "A:* b:A ⊨ (\<lambda>a:A. a)⋅b: ?T"
  by (depth_solve rules)

schematic_goal "A:* B:* c:A b:B ⊨ (\<lambda>x:A. b)⋅ c: ?T"
  by (depth_solve rules)

schematic_goal "A:* B:* ⊨ \<lambda>a:A. \<lambda>b:B. a : ?T"
  by (depth_solve rules)


subsection ‹Second-order types›

schematic_goal (in L2) "⊨ \<lambda>A:*. \<lambda>a:A. a : ?T"
  by (depth_solve rules)

schematic_goal (in L2) "A:* ⊨ (\<lambda>B:*. \<lambda>b:B. b)⋅A : ?T"
  by (depth_solve rules)

schematic_goal (in L2) "A:* b:A ⊨ (\<lambda>B:*. \<lambda>b:B. b) ⋅ A ⋅ b: ?T"
  by (depth_solve rules)

schematic_goal (in L2) "⊨ \<lambda>B:*. \<lambda>a:(∏A:*.A).a ⋅ ((∏A:*.A)→B) ⋅ a: ?T"
  by (depth_solve rules)


subsection ‹Weakly higher-order propositional logic›

schematic_goal (in Lomega) "⊨ \<lambda>A:*.A→A : ?T"
  by (depth_solve rules)

schematic_goal (in Lomega) "B:* ⊨ (\<lambda>A:*.A→A) ⋅ B : ?T"
  by (depth_solve rules)

schematic_goal (in Lomega) "B:* b:B ⊨ (\<lambda>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:* ⊨ \<lambda>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→* ⊨ \<lambda>a:A. \<lambda>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 ⊨
        \<lambda>x:∏a:A. P⋅a→Q. \<lambda>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) "⊨ \<lambda>A:*. \<lambda>B:*.∏C:*.(A→B→C)→C : ?T"
  by (depth_solve rules)

schematic_goal (in Lomega2) "⊨ \<lambda>A:*. \<lambda>B:*. \<lambda>x:A. \<lambda>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→* ⊨ \<lambda>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:* ⊨ \<lambda>P:A→A→*. \<lambda>a:A. P⋅a⋅a : ?T"
  by (depth_solve rules)

schematic_goal (in LPomega) "⊨ \<lambda>A:*. \<lambda>P:A→A→*. \<lambda>a:A. P⋅a⋅a : ?T"
  by (depth_solve rules)


subsection ‹Constructions›

schematic_goal (in CC) "⊨ \<lambda>A:*. \<lambda>P:A→*. \<lambda>a:A. P⋅a→∏P:*.P: ?T"
  by (depth_solve rules)

schematic_goal (in CC) "⊨ \<lambda>A:*. \<lambda>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 ⊨
    \<lambda>a:A. ∏P:A→*.P⋅c → (∏x:A. P⋅x→P⋅(f⋅x)) → P⋅a : ?T"
  by (depth_solve rules)

schematic_goal (in CC) "\<lambda>A:*. \<lambda>c:A. \<lambda>f:A→A.
    \<lambda>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 = "\<lambda>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