products/sources/formale Sprachen/Isabelle/Cube/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: integral.prf   Sprache: Shell

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.19 Sekunden  (vorverarbeitet)  ¤



Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
sprechenden Kalenders

Eigene Datei ansehen




Lebenszyklus

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff