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:*  AA : ?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:*.AA : ?T"
  by (depth_solve rules)

schematic_goal (in Lomega) "B:*  (λA:*.AA)  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(FA): ?T"
  by (depth_solve rules)

schematic_goal (in Lomega) "A:*  λF:**.F(FA): ?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  Pa: ?T"
  by (depth_solve rules)

schematic_goal (in LP) "A:* P:AA* a:A  a:A. Paa: ?T"
  by (depth_solve rules)

schematic_goal (in LP) "A:* P:A* Q:A*  a:A. Pa  Qa: ?T"
  by (depth_solve rules)

schematic_goal (in LP) "A:* P:A*  a:A. Pa  Pa: ?T"
  by (depth_solve rules)

schematic_goal (in LP) "A:* P:A*  λa:A. λx:Pa. x: ?T"
  by (depth_solve rules)

schematic_goal (in LP) "A:* P:A* Q:*  (a:A. PaQ)  (a:A. Pa)  Q : ?T"
  by (depth_solve rules)

schematic_goal (in LP) "A:* P:A* Q:* a0:A 
        λx:a:A. PaQ. λy:a:A. Pa. xa0(ya0): ?T"
  by (depth_solve rules)


subsection Omega-order types

schematic_goal (in L2) "A:* B:*  C:*.(ABC)C : ?T"
  by (depth_solve rules)

schematic_goal (in Lomega2) " λA:*. λB:*.C:*.(ABC)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 : (AB)  ((BP:*.P)(AP:*.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. Pa(A:*.A) : ?T"
  by (depth_solve rules)

schematic_goal (in LP2) "A:* P:AA* 
    (a:A. b:A. PabPbaP:*.P)  a:A. PaaP:*.P : ?T"
  by (depth_solve rules)

schematic_goal (in LP2) "A:* P:AA* 
    ?p: (a:A. b:A. PabPbaP:*.P)  a:A. PaaP:*.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:AA*. λa:A. Paa : ?T"
  by (depth_solve rules)

schematic_goal (in LPomega) " λA:*. λP:AA*. λa:A. Paa : ?T"
  by (depth_solve rules)


subsection Constructions

schematic_goal (in CC) " λA:*. λP:A*. λa:A. PaP:*.P: ?T"
  by (depth_solve rules)

schematic_goal (in CC) " λA:*. λP:A*.a:A. Pa: ?T"
  by (depth_solve rules)

schematic_goal (in CC) "A:* P:A* a:A  ?p : (a:A. Pa)Pa"
  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:AA 
    λa:A. P:A*.Pc  (x:A. PxP(fx))  Pa : ?T"
  by (depth_solve rules)

schematic_goal (in CC) "λA:*. λc:A. λf:AA.
    λa:A. P:A*.Pc  (x:A. PxP(fx))  Pa : ?T"
  by (depth_solve rules)

schematic_goal (in LP2)
  "A:* a:A b:A  ?p: (P:A*.PaPb)  (P:A*.PbPa)"
  ― ‹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*.QxQa" 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