Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Example.thy Sprache: Isabelle

Original von: Isabelle^©

section \<open>Lambda Cube Examples\<close>

theory Example
imports Cube
begin

text \<open>Examples taken from:

  H. Barendregt. Introduction to Generalised Type Systems.
  J. Functional Programming.\<close>

method_setup depth_solve =
  \<open>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 =
  \<open>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 =
  \<open>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))))\<close>

subsection \<open>Simple types\<close>

schematic_goal "A:* \ A\A : ?T"
  by (depth_solve rules)

schematic_goal "A:* \ \<^bold>\a:A. a : ?T"
  by (depth_solve rules)

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

schematic_goal "A:* b:A \ (\<^bold>\a:A. a)\b: ?T"
  by (depth_solve rules)

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

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

subsection \<open>Second-order types\<close>

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

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

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

schematic_goal (in L2) "\ \<^bold>\B:*. \<^bold>\a:(\A:*.A).a \ ((\A:*.A)\B) \ a: ?T"
  by (depth_solve rules)

subsection \<open>Weakly higher-order propositional logic\<close>

schematic_goal (in Lomega) "\ \<^bold>\A:*.A\A : ?T"
  by (depth_solve rules)

schematic_goal (in Lomega) "B:* \ (\<^bold>\A:*.A\A) \ B : ?T"
  by (depth_solve rules)

schematic_goal (in Lomega) "B:* b:B \ (\<^bold>\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:* \ \<^bold>\F:*\*.F\(F\A): ?T"
  by (depth_solve rules)

subsection \<open>LP\<close>

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\* \ \<^bold>\a:A. \<^bold>\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 \
        \<^bold>\<lambda>x:\<Prod>a:A. P\<cdot>a\<rightarrow>Q. \<^bold>\<lambda>y:\<Prod>a:A. P\<cdot>a. x\<cdot>a0\<cdot>(y\<cdot>a0): ?T"
  by (depth_solve rules)

subsection \<open>Omega-order types\<close>

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

schematic_goal (in Lomega2) "\ \<^bold>\A:*. \<^bold>\B:*.\C:*.(A\B\C)\C : ?T"
  by (depth_solve rules)

schematic_goal (in Lomega2) "\ \<^bold>\A:*. \<^bold>\B:*. \<^bold>\x:A. \<^bold>\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 \<open>Second-order Predicate Logic\<close>

schematic_goal (in LP2) "A:* P:A\* \ \<^bold>\a:A. P\a\(\A:*.A) : ?T"
  by (depth_solve rules)

schematic_goal (in LP2) "A:* P:A\A\* \
    (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P : ?T"
  by (depth_solve rules)

schematic_goal (in LP2) "A:* P:A\A\* \
    ?p: (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P"
  \<comment> \<open>Antisymmetry implies irreflexivity:\<close>
  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 \<open>LPomega\<close>

schematic_goal (in LPomega) "A:* \ \<^bold>\P:A\A\*. \<^bold>\a:A. P\a\a : ?T"
  by (depth_solve rules)

schematic_goal (in LPomega) "\ \<^bold>\A:*. \<^bold>\P:A\A\*. \<^bold>\a:A. P\a\a : ?T"
  by (depth_solve rules)

subsection \<open>Constructions\<close>

schematic_goal (in CC) "\ \<^bold>\A:*. \<^bold>\P:A\*. \<^bold>\a:A. P\a\\P:*.P: ?T"
  by (depth_solve rules)

schematic_goal (in CC) "\ \<^bold>\A:*. \<^bold>\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 \<open>Some random examples\<close>

schematic_goal (in LP2) "A:* c:A f:A\A \
    \<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>a : ?T"
  by (depth_solve rules)

schematic_goal (in CC) "\<^bold>\A:*. \<^bold>\c:A. \<^bold>\f:A\A.
    \<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>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)"
  \<comment> \<open>Symmetry of Leibnitz equality\<close>
  apply (strip_asms rules)
  apply (rule lam_ss)
    apply (depth_solve1 rules)
   prefer 2
   apply (depth_solve1 rules)
  apply (erule_tac a = "\<^bold>\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

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.