Quelle Extraction.thy Sprache: Isabelle

(*  Title:      HOL/Extraction.thy
    Author:     Stefan Berghofer, TU Muenchen
*)

section \<open>Program extraction for HOL\<close>

theory Extraction
imports Option
begin

subsection \<open>Setup\<close>

setup \<open>
  Extraction.add_types
      [("bool", ([], NONE))] #>
  Extraction.set_preprocessor (fn thy =>
    Proofterm.rewrite_proof_notypes
      ([], Rewrite_HOL_Proof.elim_cong :: Proof_Rewrite_Rules.rprocs true) o
    Proofterm.rewrite_proof thy
      (Rewrite_HOL_Proof.rews,
       Proof_Rewrite_Rules.rprocs true @ [Proof_Rewrite_Rules.expand_of_class thy]) o
    Proof_Rewrite_Rules.elim_vars (curry Const \<^const_name>\<open>default\<close>))
\<close>

lemmas [extraction_expand] =
  meta_spec atomize_eq atomize_all atomize_imp atomize_conj
  allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
  notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
  induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
  induct_atomize induct_atomize' induct_rulify induct_rulify'
  induct_rulify_fallback induct_trueI
  True_implies_equals implies_True_equals TrueE
  False_implies_equals implies_False_swap

lemmas [extraction_expand_def] =
  HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
  HOL.induct_true_def HOL.induct_false_def

datatype (plugins only: code extraction) sumbool = Left | Right

subsection \<open>Type of extracted program\<close>

extract_type
  "typeof (Trueprop P) \ typeof P"

  "typeof P \ Type (TYPE(Null)) \ typeof Q \ Type (TYPE('Q)) \
     typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('Q))"

  "typeof Q \ Type (TYPE(Null)) \ typeof (P \ Q) \ Type (TYPE(Null))"

  "typeof P \ Type (TYPE('P)) \ typeof Q \ Type (TYPE('Q)) \
     typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('P \<Rightarrow> 'Q))"

  "(\x. typeof (P x)) \ (\x. Type (TYPE(Null))) \
     typeof (\<forall>x. P x) \<equiv> Type (TYPE(Null))"

  "(\x. typeof (P x)) \ (\x. Type (TYPE('P))) \
     typeof (\<forall>x::'a. P x) \<equiv> Type (TYPE('a \<Rightarrow> 'P))"

  "(\x. typeof (P x)) \ (\x. Type (TYPE(Null))) \
     typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a))"

  "(\x. typeof (P x)) \ (\x. Type (TYPE('P))) \
     typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a \<times> 'P))"

  "typeof P \ Type (TYPE(Null)) \ typeof Q \ Type (TYPE(Null)) \
     typeof (P \<or> Q) \<equiv> Type (TYPE(sumbool))"

  "typeof P \ Type (TYPE(Null)) \ typeof Q \ Type (TYPE('Q)) \
     typeof (P \<or> Q) \<equiv> Type (TYPE('Q option))"

  "typeof P \ Type (TYPE('P)) \ typeof Q \ Type (TYPE(Null)) \
     typeof (P \<or> Q) \<equiv> Type (TYPE('P option))"

  "typeof P \ Type (TYPE('P)) \ typeof Q \ Type (TYPE('Q)) \
     typeof (P \<or> Q) \<equiv> Type (TYPE('P + 'Q))"

  "typeof P \ Type (TYPE(Null)) \ typeof Q \ Type (TYPE('Q)) \
     typeof (P \<and> Q) \<equiv> Type (TYPE('Q))"

  "typeof P \ Type (TYPE('P)) \ typeof Q \ Type (TYPE(Null)) \
     typeof (P \<and> Q) \<equiv> Type (TYPE('P))"

  "typeof P \ Type (TYPE('P)) \ typeof Q \ Type (TYPE('Q)) \
     typeof (P \<and> Q) \<equiv> Type (TYPE('P \<times> 'Q))"

  "typeof (P = Q) \ typeof ((P \ Q) \ (Q \ P))"

  "typeof (x \ P) \ typeof P"

subsection \<open>Realizability\<close>

realizability
  "(realizes t (Trueprop P)) \ (Trueprop (realizes t P))"

  "(typeof P) \ (Type (TYPE(Null))) \
     (realizes t (P \<longrightarrow> Q)) \<equiv> (realizes Null P \<longrightarrow> realizes t Q)"

  "(typeof P) \ (Type (TYPE('P))) \
   (typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
     (realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x::'P. realizes x P \<longrightarrow> realizes Null Q)"

  "(realizes t (P \ Q)) \ (\x. realizes x P \ realizes (t x) Q)"

  "(\x. typeof (P x)) \ (\x. Type (TYPE(Null))) \
     (realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes Null (P x))"

  "(realizes t (\x. P x)) \ (\x. realizes (t x) (P x))"

  "(\x. typeof (P x)) \ (\x. Type (TYPE(Null))) \
     (realizes t (\<exists>x. P x)) \<equiv> (realizes Null (P t))"

  "(realizes t (\x. P x)) \ (realizes (snd t) (P (fst t)))"

  "(typeof P) \ (Type (TYPE(Null))) \
   (typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
     (realizes t (P \<or> Q)) \<equiv>
     (case t of Left \<Rightarrow> realizes Null P | Right \<Rightarrow> realizes Null Q)"

  "(typeof P) \ (Type (TYPE(Null))) \
     (realizes t (P \<or> Q)) \<equiv>
     (case t of None \<Rightarrow> realizes Null P | Some q \<Rightarrow> realizes q Q)"

  "(typeof Q) \ (Type (TYPE(Null))) \
     (realizes t (P \<or> Q)) \<equiv>
     (case t of None \<Rightarrow> realizes Null Q | Some p \<Rightarrow> realizes p P)"

  "(realizes t (P \ Q)) \
   (case t of Inl p \<Rightarrow> realizes p P | Inr q \<Rightarrow> realizes q Q)"

  "(typeof P) \ (Type (TYPE(Null))) \
     (realizes t (P \<and> Q)) \<equiv> (realizes Null P \<and> realizes t Q)"

  "(typeof Q) \ (Type (TYPE(Null))) \
     (realizes t (P \<and> Q)) \<equiv> (realizes t P \<and> realizes Null Q)"

  "(realizes t (P \ Q)) \ (realizes (fst t) P \ realizes (snd t) Q)"

  "typeof P \ Type (TYPE(Null)) \
     realizes t (\<not> P) \<equiv> \<not> realizes Null P"

  "typeof P \ Type (TYPE('P)) \
     realizes t (\<not> P) \<equiv> (\<forall>x::'P. \<not> realizes x P)"

  "typeof (P::bool) \ Type (TYPE(Null)) \
   typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow>
     realizes t (P = Q) \<equiv> realizes Null P = realizes Null Q"

  "(realizes t (P = Q)) \ (realizes t ((P \ Q) \ (Q \ P)))"

subsection \<open>Computational content of basic inference rules\<close>

theorem disjE_realizer:
  assumes r: "case x of Inl p \ P p | Inr q \ Q q"
  and r1: "\p. P p \ R (f p)" and r2: "\q. Q q \ R (g q)"
  shows "R (case x of Inl p \ f p | Inr q \ g q)"
proof (cases x)
  case Inl
  with r show ?thesis by simp (rule r1)
next
  case Inr
  with r show ?thesis by simp (rule r2)
qed

theorem disjE_realizer2:
  assumes r: "case x of None \ P | Some q \ Q q"
  and r1: "P \ R f" and r2: "\q. Q q \ R (g q)"
  shows "R (case x of None \ f | Some q \ g q)"
proof (cases x)
  case None
  with r show ?thesis by simp (rule r1)
next
  case Some
  with r show ?thesis by simp (rule r2)
qed

theorem disjE_realizer3:
  assumes r: "case x of Left \ P | Right \ Q"
  and r1: "P \ R f" and r2: "Q \ R g"
  shows "R (case x of Left \ f | Right \ g)"
proof (cases x)
  case Left
  with r show ?thesis by simp (rule r1)
next
  case Right
  with r show ?thesis by simp (rule r2)
qed

theorem conjI_realizer:
  "P p \ Q q \ P (fst (p, q)) \ Q (snd (p, q))"
  by simp

theorem exI_realizer:
  "P y x \ P (snd (x, y)) (fst (x, y))" by simp

theorem exE_realizer: "P (snd p) (fst p) \
  (\<And>x y. P y x \<Longrightarrow> Q (f x y)) \<Longrightarrow> Q (let (x, y) = p in f x y)"
  by (cases p) (simp add: Let_def)

theorem exE_realizer': "P (snd p) (fst p) \
  (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp

realizers
  impI (P, Q): "\pq. pq"
    "\<^bold>\(c: _) (d: _) P Q pq (h: _). allI \ _ \ c \ (\<^bold>\x. impI \ _ \ _ \ (h \ x))"

  impI (P): "Null"
    "\<^bold>\(c: _) P Q (h: _). allI \ _ \ c \ (\<^bold>\x. impI \ _ \ _ \ (h \ x))"

  impI (Q): "\q. q" "\<^bold>\(c: _) P Q q. impI \ _ \ _"

  impI: "Null" "impI"

  mp (P, Q): "\pq. pq"
    "\<^bold>\(c: _) (d: _) P Q pq (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ c \ h)"

  mp (P): "Null"
    "\<^bold>\(c: _) P Q (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ c \ h)"

  mp (Q): "\q. q" "\<^bold>\(c: _) P Q q. mp \ _ \ _"

  mp: "Null" "mp"

  allI (P): "\p. p" "\<^bold>\(c: _) P (d: _) p. allI \ _ \ d"

  allI: "Null" "allI"

  spec (P): "\x p. p x" "\<^bold>\(c: _) P x (d: _) p. spec \ _ \ x \ d"

  spec: "Null" "spec"

  exI (P): "\x p. (x, p)" "\<^bold>\(c: _) P x (d: _) p. exI_realizer \ P \ p \ x \ c \ d"

  exI: "\x. x" "\<^bold>\P x (c: _) (h: _). h"

  exE (P, Q): "\p pq. let (x, y) = p in pq x y"
    "\<^bold>\(c: _) (d: _) P Q (e: _) p (h: _) pq. exE_realizer \ P \ p \ Q \ pq \ c \ e \ d \ h"

  exE (P): "Null"
    "\<^bold>\(c: _) P Q (d: _) p. exE_realizer' \ _ \ _ \ _ \ c \ d"

  exE (Q): "\x pq. pq x"
    "\<^bold>\(c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \ x \ h1"

  exE: "Null"
    "\<^bold>\P Q (c: _) x (h1: _) (h2: _). h2 \ x \ h1"

  conjI (P, Q): "Pair"
    "\<^bold>\(c: _) (d: _) P Q p (h: _) q. conjI_realizer \ P \ p \ Q \ q \ c \ d \ h"

  conjI (P): "\p. p"
    "\<^bold>\(c: _) P Q p. conjI \ _ \ _"

  conjI (Q): "\q. q"
    "\<^bold>\(c: _) P Q (h: _) q. conjI \ _ \ _ \ h"

  conjI: "Null" "conjI"

  conjunct1 (P, Q): "fst"
    "\<^bold>\(c: _) (d: _) P Q pq. conjunct1 \ _ \ _"

  conjunct1 (P): "\p. p"
    "\<^bold>\(c: _) P Q p. conjunct1 \ _ \ _"

  conjunct1 (Q): "Null"
    "\<^bold>\(c: _) P Q q. conjunct1 \ _ \ _"

  conjunct1: "Null" "conjunct1"

  conjunct2 (P, Q): "snd"
    "\<^bold>\(c: _) (d: _) P Q pq. conjunct2 \ _ \ _"

  conjunct2 (P): "Null"
    "\<^bold>\(c: _) P Q p. conjunct2 \ _ \ _"

  conjunct2 (Q): "\p. p"
    "\<^bold>\(c: _) P Q p. conjunct2 \ _ \ _"

  conjunct2: "Null" "conjunct2"

  disjI1 (P, Q): "Inl"
    "\<^bold>\(c: _) (d: _) P Q p. iffD2 \ _ \ _ \ (sum.case_1 \ P \ _ \ p \ arity_type_bool \ c \ d)"

  disjI1 (P): "Some"
    "\<^bold>\(c: _) P Q p. iffD2 \ _ \ _ \ (option.case_2 \ _ \ P \ p \ arity_type_bool \ c)"

  disjI1 (Q): "None"
    "\<^bold>\(c: _) P Q. iffD2 \ _ \ _ \ (option.case_1 \ _ \ _ \ arity_type_bool \ c)"

  disjI1: "Left"
    "\<^bold>\P Q. iffD2 \ _ \ _ \ (sumbool.case_1 \ _ \ _ \ arity_type_bool)"

  disjI2 (P, Q): "Inr"
    "\<^bold>\(d: _) (c: _) Q P q. iffD2 \ _ \ _ \ (sum.case_2 \ _ \ Q \ q \ arity_type_bool \ c \ d)"

  disjI2 (P): "None"
    "\<^bold>\(c: _) Q P. iffD2 \ _ \ _ \ (option.case_1 \ _ \ _ \ arity_type_bool \ c)"

  disjI2 (Q): "Some"
    "\<^bold>\(c: _) Q P q. iffD2 \ _ \ _ \ (option.case_2 \ _ \ Q \ q \ arity_type_bool \ c)"

  disjI2: "Right"
    "\<^bold>\Q P. iffD2 \ _ \ _ \ (sumbool.case_2 \ _ \ _ \ arity_type_bool)"

  disjE (P, Q, R): "\pq pr qr.
     (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
    "\<^bold>\(c: _) (d: _) (e: _) P Q R pq (h1: _) pr (h2: _) qr.
       disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> e \<bullet> h1 \<bullet> h2"

  disjE (Q, R): "\pq pr qr.
     (case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)"
    "\<^bold>\(c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr.
       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h2"

  disjE (P, R): "\pq pr qr.
     (case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)"
    "\<^bold>\(c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr (h3: _).
       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h3 \<bullet> h2"

  disjE (R): "\pq pr qr.
     (case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)"
    "\<^bold>\(c: _) P Q R pq (h1: _) pr (h2: _) qr.
       disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> h1 \<bullet> h2"

  disjE (P, Q): "Null"
    "\<^bold>\(c: _) (d: _) P Q R pq. disjE_realizer \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ c \ d \ arity_type_bool"

  disjE (Q): "Null"
    "\<^bold>\(c: _) P Q R pq. disjE_realizer2 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ c \ arity_type_bool"

  disjE (P): "Null"
    "\<^bold>\(c: _) P Q R pq (h1: _) (h2: _) (h3: _).
       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool \<bullet> h1 \<bullet> h3 \<bullet> h2"

  disjE: "Null"
    "\<^bold>\P Q R pq. disjE_realizer3 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ arity_type_bool"

  FalseE (P): "default"
    "\<^bold>\(c: _) P. FalseE \ _"

  FalseE: "Null" "FalseE"

  notI (P): "Null"
    "\<^bold>\(c: _) P (h: _). allI \ _ \ c \ (\<^bold>\x. notI \ _ \ (h \ x))"

  notI: "Null" "notI"

  notE (P, R): "\p. default"
    "\<^bold>\(c: _) (d: _) P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ c \ h)"

  notE (P): "Null"
    "\<^bold>\(c: _) P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ c \ h)"

  notE (R): "default"
    "\<^bold>\(c: _) P R. notE \ _ \ _"

  notE: "Null" "notE"

  subst (P): "\s t ps. ps"
    "\<^bold>\(c: _) s t P (d: _) (h: _) ps. subst \ s \ t \ P ps \ d \ h"

  subst: "Null" "subst"

  iffD1 (P, Q): "fst"
    "\<^bold>\(d: _) (c: _) Q P pq (h: _) p.
       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> d \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"

  iffD1 (P): "\p. p"
    "\<^bold>\(c: _) Q P p (h: _). mp \ _ \ _ \ (conjunct1 \ _ \ _ \ h)"

  iffD1 (Q): "Null"
    "\<^bold>\(c: _) Q P q1 (h: _) q2.
       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"

  iffD1: "Null" "iffD1"

  iffD2 (P, Q): "snd"
    "\<^bold>\(c: _) (d: _) P Q pq (h: _) q.
       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> d \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"

  iffD2 (P): "\p. p"
    "\<^bold>\(c: _) P Q p (h: _). mp \ _ \ _ \ (conjunct2 \ _ \ _ \ h)"

  iffD2 (Q): "Null"
    "\<^bold>\(c: _) P Q q1 (h: _) q2.
       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"

  iffD2: "Null" "iffD2"

  iffI (P, Q): "Pair"
    "\<^bold>\(c: _) (d: _) P Q pq (h1 : _) qp (h2 : _). conjI_realizer \
       (\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot>
       (\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet>
       (arity_type_fun \<bullet> c \<bullet> d) \<bullet>
       (arity_type_fun \<bullet> d \<bullet> c) \<bullet>
       (allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
       (allI \<cdot> _ \<bullet> d \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"

  iffI (P): "\p. p"
    "\<^bold>\(c: _) P Q (h1 : _) p (h2 : _). conjI \ _ \ _ \
       (allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
       (impI \<cdot> _ \<cdot> _ \<bullet> h2)"

  iffI (Q): "\q. q"
    "\<^bold>\(c: _) P Q q (h1 : _) (h2 : _). conjI \ _ \ _ \
       (impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet>
       (allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"

  iffI: "Null" "iffI"

end

quality100%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.