# Theory Extraction

Up to index of Isabelle/HOL

theory Extraction
imports Datatype
uses Tools/rewrite_hol_proof.ML
begin

    (*  Title:      HOL/Extraction.thy
        ID:         $Id: Extraction.thy,v 1.16 2005/08/31 13:46:41 wenzelm Exp $
        Author:     Stefan Berghofer, TU Muenchen
    *)

    header {* Program extraction for HOL *}

    theory Extraction
    imports Datatype
    uses "Tools/rewrite_hol_proof.ML"
    begin

    subsection {* Setup *}

    setup {*
    let
    fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
          (Const ("op :", _) $ x $ S)) = (case strip_comb S of
            (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @
               [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
          | (Free (s, U), ts) => SOME (list_comb (Free (s, binder_types U @
               [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
          | _ => NONE)
      | realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $
          (Const ("op :", _) $ x $ S)) = (case strip_comb S of
            (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T :: binder_types U @
               [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
          | (Free (s, U), ts) => SOME (list_comb (Free (s, T :: binder_types U @
               [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
          | _ => NONE)
      | realizes_set_proc _ = NONE;

    fun mk_realizes_set r rT s (setT as Type ("set", [elT])) =
      Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $
        incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
          Bound 0 $ incr_boundvars 1 s));
    in
      [Extraction.add_types
          [("bool", ([], NONE)),
           ("set", ([realizes_set_proc], SOME mk_realizes_set))],
        Extraction.set_preprocessor (fn thy =>
          Proofterm.rewrite_proof_notypes
            ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
              ProofRewriteRules.rprocs true) o
          Proofterm.rewrite_proof thy
            (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
          ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
    end
    *}

    lemmas [extraction_expand] =
      atomize_eq atomize_all atomize_imp
      allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
      notE' impE' impE iffE imp_cong simp_thms
      induct_forall_eq induct_implies_eq induct_equal_eq
      induct_forall_def induct_implies_def induct_impliesI
      induct_atomize induct_rulify1 induct_rulify2

    datatype sumbool = Left | Right

    subsection {* Type of extracted program *}

    extract_type
      "typeof (Trueprop P) ≡ typeof P"

      "typeof P ≡ Type (TYPE(Null)) ==> typeof Q ≡ Type (TYPE('Q)) ==>
         typeof (P --> Q) ≡ 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 --> Q) ≡ Type (TYPE('P => 'Q))"

      "(λx. typeof (P x)) ≡ (λx. Type (TYPE(Null))) ==>
         typeof (∀x. P x) ≡ Type (TYPE(Null))"

      "(λx. typeof (P x)) ≡ (λx. Type (TYPE('P))) ==>
         typeof (∀x::'a. P x) ≡ Type (TYPE('a => 'P))"

      "(λx. typeof (P x)) ≡ (λx. Type (TYPE(Null))) ==>
         typeof (∃x::'a. P x) ≡ Type (TYPE('a))"

      "(λx. typeof (P x)) ≡ (λx. Type (TYPE('P))) ==>
         typeof (∃x::'a. P x) ≡ Type (TYPE('a × 'P))"

      "typeof P ≡ Type (TYPE(Null)) ==> typeof Q ≡ Type (TYPE(Null)) ==>
         typeof (P ∨ Q) ≡ Type (TYPE(sumbool))"

      "typeof P ≡ Type (TYPE(Null)) ==> typeof Q ≡ Type (TYPE('Q)) ==>
         typeof (P ∨ Q) ≡ Type (TYPE('Q option))"

      "typeof P ≡ Type (TYPE('P)) ==> typeof Q ≡ Type (TYPE(Null)) ==>
         typeof (P ∨ Q) ≡ Type (TYPE('P option))"

      "typeof P ≡ Type (TYPE('P)) ==> typeof Q ≡ Type (TYPE('Q)) ==>
         typeof (P ∨ Q) ≡ Type (TYPE('P + 'Q))"

      "typeof P ≡ Type (TYPE(Null)) ==> typeof Q ≡ Type (TYPE('Q)) ==>
         typeof (P ∧ Q) ≡ Type (TYPE('Q))"

      "typeof P ≡ Type (TYPE('P)) ==> typeof Q ≡ Type (TYPE(Null)) ==>
         typeof (P ∧ Q) ≡ Type (TYPE('P))"

      "typeof P ≡ Type (TYPE('P)) ==> typeof Q ≡ Type (TYPE('Q)) ==>
         typeof (P ∧ Q) ≡ Type (TYPE('P × 'Q))"

      "typeof (P = Q) ≡ typeof ((P --> Q) ∧ (Q --> P))"

      "typeof (x ∈ P) ≡ typeof P"

    subsection {* Realizability *}

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

      "(typeof P) ≡ (Type (TYPE(Null))) ==>
         (realizes t (P --> Q)) ≡ (realizes Null P --> realizes t Q)"

      "(typeof P) ≡ (Type (TYPE('P))) ==>
       (typeof Q) ≡ (Type (TYPE(Null))) ==>
         (realizes t (P --> Q)) ≡ (∀x::'P. realizes x P --> 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 (∀x. P x)) ≡ (∀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 (∃x. P x)) ≡ (realizes Null (P t))"

      "(realizes t (∃x. P x)) ≡ (realizes (snd t) (P (fst t)))"

      "(typeof P) ≡ (Type (TYPE(Null))) ==>
       (typeof Q) ≡ (Type (TYPE(Null))) ==>
         (realizes t (P ∨ Q)) ≡
         (case t of Left => realizes Null P | Right => realizes Null Q)"

      "(typeof P) ≡ (Type (TYPE(Null))) ==>
         (realizes t (P ∨ Q)) ≡
         (case t of None => realizes Null P | Some q => realizes q Q)"

      "(typeof Q) ≡ (Type (TYPE(Null))) ==>
         (realizes t (P ∨ Q)) ≡
         (case t of None => realizes Null Q | Some p => realizes p P)"

      "(realizes t (P ∨ Q)) ≡
       (case t of Inl p => realizes p P | Inr q => realizes q Q)"

      "(typeof P) ≡ (Type (TYPE(Null))) ==>
         (realizes t (P ∧ Q)) ≡ (realizes Null P ∧ realizes t Q)"

      "(typeof Q) ≡ (Type (TYPE(Null))) ==>
         (realizes t (P ∧ Q)) ≡ (realizes t P ∧ realizes Null Q)"

      "(realizes t (P ∧ Q)) ≡ (realizes (fst t) P ∧ realizes (snd t) Q)"

      "typeof P ≡ Type (TYPE(Null)) ==>
         realizes t (¬ P) ≡ ¬ realizes Null P"

      "typeof P ≡ Type (TYPE('P)) ==>
         realizes t (¬ P) ≡ (∀x::'P. ¬ realizes x P)"

      "typeof (P::bool) ≡ Type (TYPE(Null)) ==>
       typeof Q ≡ Type (TYPE(Null)) ==>
         realizes t (P = Q) ≡ realizes Null P = realizes Null Q"

      "(realizes t (P = Q)) ≡ (realizes t ((P --> Q) ∧ (Q --> P)))"

    subsection {* Computational content of basic inference rules *}

    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) ==>
      (!!x y. P y x ==> Q (f x y)) ==> Q (let (x, y) = p in f x y)"
      by (cases p) (simp add: Let_def)

    theorem exE_realizer': "P (snd p) (fst p) ==>
      (!!x y. P y x ==> Q) ==> Q" by (cases p) simp

    realizers
      impI (P, Q): "λpq. pq"
        "Λ P Q pq (h: _). allI · _ • (Λ x. impI · _ · _ • (h · x))"

      impI (P): "Null"
        "Λ P Q (h: _). allI · _ • (Λ x. impI · _ · _ • (h · x))"

      impI (Q): "λq. q" "Λ P Q q. impI · _ · _"

      impI: "Null" "impI"

      mp (P, Q): "λpq. pq"
        "Λ P Q pq (h: _) p. mp · _ · _ • (spec · _ · p • h)"

      mp (P): "Null"
        "Λ P Q (h: _) p. mp · _ · _ • (spec · _ · p • h)"

      mp (Q): "λq. q" "Λ P Q q. mp · _ · _"

      mp: "Null" "mp"

      allI (P): "λp. p" "Λ P p. allI · _"

      allI: "Null" "allI"

      spec (P): "λx p. p x" "Λ P x p. spec · _ · x"

      spec: "Null" "spec"

      exI (P): "λx p. (x, p)" "Λ P x p. exI_realizer · P · p · x"

      exI: "λx. x" "Λ P x (h: _). h"

      exE (P, Q): "λp pq. let (x, y) = p in pq x y"
        "Λ P Q p (h: _) pq. exE_realizer · P · p · Q · pq • h"

      exE (P): "Null"
        "Λ P Q p. exE_realizer' · _ · _ · _"

      exE (Q): "λx pq. pq x"
        "Λ P Q x (h1: _) pq (h2: _). h2 · x • h1"

      exE: "Null"
        "Λ P Q x (h1: _) (h2: _). h2 · x • h1"

      conjI (P, Q): "Pair"
        "Λ P Q p (h: _) q. conjI_realizer · P · p · Q · q • h"

      conjI (P): "λp. p"
        "Λ P Q p. conjI · _ · _"

      conjI (Q): "λq. q"
        "Λ P Q (h: _) q. conjI · _ · _ • h"

      conjI: "Null" "conjI"

      conjunct1 (P, Q): "fst"
        "Λ P Q pq. conjunct1 · _ · _"

      conjunct1 (P): "λp. p"
        "Λ P Q p. conjunct1 · _ · _"

      conjunct1 (Q): "Null"
        "Λ P Q q. conjunct1 · _ · _"

      conjunct1: "Null" "conjunct1"

      conjunct2 (P, Q): "snd"
        "Λ P Q pq. conjunct2 · _ · _"

      conjunct2 (P): "Null"
        "Λ P Q p. conjunct2 · _ · _"

      conjunct2 (Q): "λp. p"
        "Λ P Q p. conjunct2 · _ · _"

      conjunct2: "Null" "conjunct2"

      disjI1 (P, Q): "Inl"
        "Λ P Q p. iffD2 · _ · _ • (sum.cases_1 · P · _ · p)"

      disjI1 (P): "Some"
        "Λ P Q p. iffD2 · _ · _ • (option.cases_2 · _ · P · p)"

      disjI1 (Q): "None"
        "Λ P Q. iffD2 · _ · _ • (option.cases_1 · _ · _)"

      disjI1: "Left"
        "Λ P Q. iffD2 · _ · _ • (sumbool.cases_1 · _ · _)"

      disjI2 (P, Q): "Inr"
        "Λ Q P q. iffD2 · _ · _ • (sum.cases_2 · _ · Q · q)"

      disjI2 (P): "None"
        "Λ Q P. iffD2 · _ · _ • (option.cases_1 · _ · _)"

      disjI2 (Q): "Some"
        "Λ Q P q. iffD2 · _ · _ • (option.cases_2 · _ · Q · q)"

      disjI2: "Right"
        "Λ Q P. iffD2 · _ · _ • (sumbool.cases_2 · _ · _)"

      disjE (P, Q, R): "λpq pr qr.
         (case pq of Inl p => pr p | Inr q => qr q)"
        "Λ P Q R pq (h1: _) pr (h2: _) qr.
           disjE_realizer · _ · _ · pq · R · pr · qr • h1 • h2"

      disjE (Q, R): "λpq pr qr.
         (case pq of None => pr | Some q => qr q)"
        "Λ P Q R pq (h1: _) pr (h2: _) qr.
           disjE_realizer2 · _ · _ · pq · R · pr · qr • h1 • h2"

      disjE (P, R): "λpq pr qr.
         (case pq of None => qr | Some p => pr p)"
        "Λ P Q R pq (h1: _) pr (h2: _) qr (h3: _).
           disjE_realizer2 · _ · _ · pq · R · qr · pr • h1 • h3 • h2"

      disjE (R): "λpq pr qr.
         (case pq of Left => pr | Right => qr)"
        "Λ P Q R pq (h1: _) pr (h2: _) qr.
           disjE_realizer3 · _ · _ · pq · R · pr · qr • h1 • h2"

      disjE (P, Q): "Null"
        "Λ P Q R pq. disjE_realizer · _ · _ · pq · (λx. R) · _ · _"

      disjE (Q): "Null"
        "Λ P Q R pq. disjE_realizer2 · _ · _ · pq · (λx. R) · _ · _"

      disjE (P): "Null"
        "Λ P Q R pq (h1: _) (h2: _) (h3: _).
           disjE_realizer2 · _ · _ · pq · (λx. R) · _ · _ • h1 • h3 • h2"

      disjE: "Null"
        "Λ P Q R pq. disjE_realizer3 · _ · _ · pq · (λx. R) · _ · _"

      FalseE (P): "arbitrary"
        "Λ P. FalseE · _"

      FalseE: "Null" "FalseE"

      notI (P): "Null"
        "Λ P (h: _). allI · _ • (Λ x. notI · _ • (h · x))"

      notI: "Null" "notI"

      notE (P, R): "λp. arbitrary"
        "Λ P R (h: _) p. notE · _ · _ • (spec · _ · p • h)"

      notE (P): "Null"
        "Λ P R (h: _) p. notE · _ · _ • (spec · _ · p • h)"

      notE (R): "arbitrary"
        "Λ P R. notE · _ · _"

      notE: "Null" "notE"

      subst (P): "λs t ps. ps"
        "Λ s t P (h: _) ps. subst · s · t · P ps • h"

      subst: "Null" "subst"

      iffD1 (P, Q): "fst"
        "Λ Q P pq (h: _) p.
           mp · _ · _ • (spec · _ · p • (conjunct1 · _ · _ • h))"

      iffD1 (P): "λp. p"
        "Λ Q P p (h: _). mp · _ · _ • (conjunct1 · _ · _ • h)"

      iffD1 (Q): "Null"
        "Λ Q P q1 (h: _) q2.
           mp · _ · _ • (spec · _ · q2 • (conjunct1 · _ · _ • h))"

      iffD1: "Null" "iffD1"

      iffD2 (P, Q): "snd"
        "Λ P Q pq (h: _) q.
           mp · _ · _ • (spec · _ · q • (conjunct2 · _ · _ • h))"

      iffD2 (P): "λp. p"
        "Λ P Q p (h: _). mp · _ · _ • (conjunct2 · _ · _ • h)"

      iffD2 (Q): "Null"
        "Λ P Q q1 (h: _) q2.
           mp · _ · _ • (spec · _ · q2 • (conjunct2 · _ · _ • h))"

      iffD2: "Null" "iffD2"

      iffI (P, Q): "Pair"
        "Λ P Q pq (h1 : _) qp (h2 : _). conjI_realizer ·
           (λpq. ∀x. P x --> Q (pq x)) · pq ·
           (λqp. ∀x. Q x --> P (qp x)) · qp •
           (allI · _ • (Λ x. impI · _ · _ • (h1 · x))) •
           (allI · _ • (Λ x. impI · _ · _ • (h2 · x)))"

      iffI (P): "λp. p"
        "Λ P Q (h1 : _) p (h2 : _). conjI · _ · _ •
           (allI · _ • (Λ x. impI · _ · _ • (h1 · x))) •
           (impI · _ · _ • h2)"

      iffI (Q): "λq. q"
        "Λ P Q q (h1 : _) (h2 : _). conjI · _ · _ •
           (impI · _ · _ • h1) •
           (allI · _ • (Λ x. impI · _ · _ • (h2 · x)))"

      iffI: "Null" "iffI"

    (*
      classical: "Null"
        "Λ P. classical · _"
    *)

    end

### Setup

lemmas

      (x == y) == x = y

      (!!x. P x) == ∀x. P x

      (A ==> B) == A --> B

      [| ∀x. P x; P x ==> R |] ==> R

      [| P; P --> Q |] ==> Q

      [| P ∧ Q; [| P; Q |] ==> R |] ==> R

      P ==> P == True

      ¬ P ==> P == False

      P ==> P = True

      P = True ==> P

      u = u' ==> (t == u) == t == u'

      [| ¬ P; ¬ P ==> P |] ==> R

      [| P --> Q; Q ==> R; P --> Q ==> P |] ==> R

      [| P --> Q; P; Q ==> R |] ==> R

      [| P = Q; [| P --> Q; Q --> P |] ==> R |] ==> R

      [| P = P'; P' ==> Q = Q' |] ==> (P --> Q) = (P' --> Q')

      (¬ ¬ P) = P

      ((¬ P) = (¬ Q)) = (P = Q)

      (P ≠ Q) = (P = (¬ Q))

      (P ∨ ¬ P) = True

      (¬ P ∨ P) = True

      (x = x) = True

      (¬ True) = False

      (¬ False) = True

      (¬ P) ≠ P

      P ≠ (¬ P)

      (True = P) = P

      (P = True) = P

      (False = P) = (¬ P)

      (P = False) = (¬ P)

      (True --> P) = P

      (False --> P) = True

      (P --> True) = True

      (P --> P) = True

      (P --> False) = (¬ P)

      (P --> ¬ P) = (¬ P)

      (P ∧ True) = P

      (True ∧ P) = P

      (P ∧ False) = False

      (False ∧ P) = False

      (P ∧ P) = P

      (P ∧ P ∧ Q) = (P ∧ Q)

      (P ∧ ¬ P) = False

      (¬ P ∧ P) = False

      (P ∨ True) = True

      (True ∨ P) = True

      (P ∨ False) = P

      (False ∨ P) = P

      (P ∨ P) = P

      (P ∨ P ∨ Q) = (P ∨ Q)

      (∀x. P) = P

      (∃x. P) = P

      ∃x. x = t

      ∃x. t = x

      (∃x. x = t ∧ P x) = P t

      (∃x. t = x ∧ P x) = P t

      (∀x. x = t --> P x) = P t

      (∀x. t = x --> P x) = P t

      (!!x. P x) == ??.HOL.induct_forall P

      (A ==> B) == ??.HOL.induct_implies A B

      (x == y) == ??.HOL.induct_equal x y

      ??.HOL.induct_forall P == ∀x. P x

      ??.HOL.induct_implies A B == A --> B

      (A ==> B) ==> ??.HOL.induct_implies A B

      (A && B) == A ∧ B

      (!!x. P x) == ??.HOL.induct_forall P

      (A ==> B) == ??.HOL.induct_implies A B

      (x == y) == ??.HOL.induct_equal x y

      ??.HOL.induct_forall P == (!!x. P x)

      ??.HOL.induct_implies A B == (A ==> B)

      ??.HOL.induct_equal x y == x == y

      ??.HOL.induct_forall P == ∀x. P x

      ??.HOL.induct_implies A B == A --> B

      ??.HOL.induct_equal x y == x = y

      ??.HOL.induct_conj A B == A ∧ B

lemmas

      (x == y) == x = y

      (!!x. P x) == ∀x. P x

      (A ==> B) == A --> B

      [| ∀x. P x; P x ==> R |] ==> R

      [| P; P --> Q |] ==> Q

      [| P ∧ Q; [| P; Q |] ==> R |] ==> R

      P ==> P == True

      ¬ P ==> P == False

      P ==> P = True

      P = True ==> P

      u = u' ==> (t == u) == t == u'

      [| ¬ P; ¬ P ==> P |] ==> R

      [| P --> Q; Q ==> R; P --> Q ==> P |] ==> R

      [| P --> Q; P; Q ==> R |] ==> R

      [| P = Q; [| P --> Q; Q --> P |] ==> R |] ==> R

      [| P = P'; P' ==> Q = Q' |] ==> (P --> Q) = (P' --> Q')

      (¬ ¬ P) = P

      ((¬ P) = (¬ Q)) = (P = Q)

      (P ≠ Q) = (P = (¬ Q))

      (P ∨ ¬ P) = True

      (¬ P ∨ P) = True

      (x = x) = True

      (¬ True) = False

      (¬ False) = True

      (¬ P) ≠ P

      P ≠ (¬ P)

      (True = P) = P

      (P = True) = P

      (False = P) = (¬ P)

      (P = False) = (¬ P)

      (True --> P) = P

      (False --> P) = True

      (P --> True) = True

      (P --> P) = True

      (P --> False) = (¬ P)

      (P --> ¬ P) = (¬ P)

      (P ∧ True) = P

      (True ∧ P) = P

      (P ∧ False) = False

      (False ∧ P) = False

      (P ∧ P) = P

      (P ∧ P ∧ Q) = (P ∧ Q)

      (P ∧ ¬ P) = False

      (¬ P ∧ P) = False

      (P ∨ True) = True

      (True ∨ P) = True

      (P ∨ False) = P

      (False ∨ P) = P

      (P ∨ P) = P

      (P ∨ P ∨ Q) = (P ∨ Q)

      (∀x. P) = P

      (∃x. P) = P

      ∃x. x = t

      ∃x. t = x

      (∃x. x = t ∧ P x) = P t

      (∃x. t = x ∧ P x) = P t

      (∀x. x = t --> P x) = P t

      (∀x. t = x --> P x) = P t

      (!!x. P x) == ??.HOL.induct_forall P

      (A ==> B) == ??.HOL.induct_implies A B

      (x == y) == ??.HOL.induct_equal x y

      ??.HOL.induct_forall P == ∀x. P x

      ??.HOL.induct_implies A B == A --> B

      (A ==> B) ==> ??.HOL.induct_implies A B

      (A && B) == A ∧ B

      (!!x. P x) == ??.HOL.induct_forall P

      (A ==> B) == ??.HOL.induct_implies A B

      (x == y) == ??.HOL.induct_equal x y

      ??.HOL.induct_forall P == (!!x. P x)

      ??.HOL.induct_implies A B == (A ==> B)

      ??.HOL.induct_equal x y == x == y

      ??.HOL.induct_forall P == ∀x. P x

      ??.HOL.induct_implies A B == A --> B

      ??.HOL.induct_equal x y == x = y

      ??.HOL.induct_conj A B == A ∧ B

### Type of extracted program

### Realizability

### Computational content of basic inference rules

theorem disjE_realizer:

      [| case x of Inl p => P p | Inr q => Q q; !!p. P p ==> R (f p);
         !!q. Q q ==> R (g q) |]
      ==> R (case x of Inl p => f p | Inr q => g q)

theorem disjE_realizer2:

      [| case x of None => P | Some q => Q q; P ==> R f; !!q. Q q ==> R (g q) |]
      ==> R (case x of None => f | Some q => g q)

theorem disjE_realizer3:

      [| case x of Left => P | Right => Q; P ==> R f; Q ==> R g |]
      ==> R (case x of Left => f | Right => g)

theorem conjI_realizer:

      [| P p; Q q |] ==> P (fst (p, q)) ∧ Q (snd (p, q))

theorem exI_realizer:

      P y x ==> P (snd (x, y)) (fst (x, y))

theorem exE_realizer:

      [| P (snd p) (fst p); !!x y. P y x ==> Q (f x y) |]
      ==> Q (let (x, y) = p in f x y)

theorem exE_realizer':

      [| P (snd p) (fst p); !!x y. P y x ==> Q |] ==> Q