Quelle  Example.thy

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