src/HOL/Extraction.thy
author berghofe
Mon Sep 30 16:10:32 2002 +0200 (2002-09-30)
changeset 13599 cfdf7e4cd0d2
parent 13468 71118807d303
child 13725 12404b452034
permissions -rw-r--r--
Added elim_vars to preprocessor.
berghofe@13403
     1
(*  Title:      HOL/Extraction.thy
berghofe@13403
     2
    ID:         $Id$
berghofe@13403
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@13403
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@13403
     5
*)
berghofe@13403
     6
berghofe@13403
     7
header {* Program extraction for HOL *}
berghofe@13403
     8
berghofe@13403
     9
theory Extraction = Datatype
berghofe@13403
    10
files
berghofe@13403
    11
  "Tools/rewrite_hol_proof.ML":
berghofe@13403
    12
berghofe@13403
    13
subsection {* Setup *}
berghofe@13403
    14
berghofe@13403
    15
ML_setup {*
berghofe@13403
    16
  Context.>> (fn thy => thy |>
berghofe@13403
    17
    Extraction.set_preprocessor (fn sg =>
berghofe@13403
    18
      Proofterm.rewrite_proof_notypes
berghofe@13403
    19
        ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
berghofe@13403
    20
          ProofRewriteRules.rprocs true) o
berghofe@13403
    21
      Proofterm.rewrite_proof (Sign.tsig_of sg)
berghofe@13599
    22
        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
berghofe@13599
    23
      ProofRewriteRules.elim_vars (curry Const "arbitrary")))
berghofe@13403
    24
*}
berghofe@13403
    25
berghofe@13403
    26
lemmas [extraction_expand] =
berghofe@13468
    27
  atomize_eq atomize_all atomize_imp
berghofe@13403
    28
  allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
berghofe@13403
    29
  notE' impE' impE iffE imp_cong simp_thms
berghofe@13403
    30
  induct_forall_eq induct_implies_eq induct_equal_eq
berghofe@13403
    31
  induct_forall_def induct_implies_def
berghofe@13403
    32
  induct_atomize induct_rulify1 induct_rulify2
berghofe@13403
    33
berghofe@13403
    34
datatype sumbool = Left | Right
berghofe@13403
    35
berghofe@13403
    36
subsection {* Type of extracted program *}
berghofe@13403
    37
berghofe@13403
    38
extract_type
berghofe@13403
    39
  "typeof (Trueprop P) \<equiv> typeof P"
berghofe@13403
    40
berghofe@13403
    41
  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
berghofe@13403
    42
     typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('Q))"
berghofe@13403
    43
berghofe@13403
    44
  "typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE(Null))"
berghofe@13403
    45
berghofe@13403
    46
  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
berghofe@13403
    47
     typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('P \<Rightarrow> 'Q))"
berghofe@13403
    48
berghofe@13403
    49
  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
    50
     typeof (\<forall>x. P x) \<equiv> Type (TYPE(Null))"
berghofe@13403
    51
berghofe@13403
    52
  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow>
berghofe@13403
    53
     typeof (\<forall>x::'a. P x) \<equiv> Type (TYPE('a \<Rightarrow> 'P))"
berghofe@13403
    54
berghofe@13403
    55
  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
    56
     typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a))"
berghofe@13403
    57
berghofe@13403
    58
  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow>
berghofe@13403
    59
     typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a \<times> 'P))"
berghofe@13403
    60
berghofe@13403
    61
  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow>
berghofe@13403
    62
     typeof (P \<or> Q) \<equiv> Type (TYPE(sumbool))"
berghofe@13403
    63
berghofe@13403
    64
  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
berghofe@13403
    65
     typeof (P \<or> Q) \<equiv> Type (TYPE('Q option))"
berghofe@13403
    66
berghofe@13403
    67
  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow>
berghofe@13403
    68
     typeof (P \<or> Q) \<equiv> Type (TYPE('P option))"
berghofe@13403
    69
berghofe@13403
    70
  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
berghofe@13403
    71
     typeof (P \<or> Q) \<equiv> Type (TYPE('P + 'Q))"
berghofe@13403
    72
berghofe@13403
    73
  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
berghofe@13403
    74
     typeof (P \<and> Q) \<equiv> Type (TYPE('Q))"
berghofe@13403
    75
berghofe@13403
    76
  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow>
berghofe@13403
    77
     typeof (P \<and> Q) \<equiv> Type (TYPE('P))"
berghofe@13403
    78
berghofe@13403
    79
  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
berghofe@13403
    80
     typeof (P \<and> Q) \<equiv> Type (TYPE('P \<times> 'Q))"
berghofe@13403
    81
berghofe@13403
    82
  "typeof (P = Q) \<equiv> typeof ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))"
berghofe@13403
    83
berghofe@13403
    84
  "typeof (x \<in> P) \<equiv> typeof P"
berghofe@13403
    85
berghofe@13403
    86
subsection {* Realizability *}
berghofe@13403
    87
berghofe@13403
    88
realizability
berghofe@13403
    89
  "(realizes t (Trueprop P)) \<equiv> (Trueprop (realizes t P))"
berghofe@13403
    90
berghofe@13403
    91
  "(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
    92
     (realizes t (P \<longrightarrow> Q)) \<equiv> (realizes Null P \<longrightarrow> realizes t Q)"
berghofe@13403
    93
berghofe@13403
    94
  "(typeof P) \<equiv> (Type (TYPE('P))) \<Longrightarrow>
berghofe@13403
    95
   (typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
    96
     (realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x::'P. realizes x P \<longrightarrow> realizes Null Q)"
berghofe@13403
    97
berghofe@13403
    98
  "(realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x. realizes x P \<longrightarrow> realizes (t x) Q)"
berghofe@13403
    99
berghofe@13403
   100
  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
   101
     (realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes Null (P x))"
berghofe@13403
   102
berghofe@13403
   103
  "(realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes (t x) (P x))"
berghofe@13403
   104
berghofe@13403
   105
  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
   106
     (realizes t (\<exists>x. P x)) \<equiv> (realizes Null (P t))"
berghofe@13403
   107
berghofe@13403
   108
  "(realizes t (\<exists>x. P x)) \<equiv> (realizes (snd t) (P (fst t)))"
berghofe@13403
   109
berghofe@13403
   110
  "(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
   111
   (typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
   112
     (realizes t (P \<or> Q)) \<equiv>
berghofe@13403
   113
     (case t of Left \<Rightarrow> realizes Null P | Right \<Rightarrow> realizes Null Q)"
berghofe@13403
   114
berghofe@13403
   115
  "(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
   116
     (realizes t (P \<or> Q)) \<equiv>
berghofe@13403
   117
     (case t of None \<Rightarrow> realizes Null P | Some q \<Rightarrow> realizes q Q)"
berghofe@13403
   118
berghofe@13403
   119
  "(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
   120
     (realizes t (P \<or> Q)) \<equiv>
berghofe@13403
   121
     (case t of None \<Rightarrow> realizes Null Q | Some p \<Rightarrow> realizes p P)"
berghofe@13403
   122
berghofe@13403
   123
  "(realizes t (P \<or> Q)) \<equiv>
berghofe@13403
   124
   (case t of Inl p \<Rightarrow> realizes p P | Inr q \<Rightarrow> realizes q Q)"
berghofe@13403
   125
berghofe@13403
   126
  "(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
   127
     (realizes t (P \<and> Q)) \<equiv> (realizes Null P \<and> realizes t Q)"
berghofe@13403
   128
berghofe@13403
   129
  "(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
berghofe@13403
   130
     (realizes t (P \<and> Q)) \<equiv> (realizes t P \<and> realizes Null Q)"
berghofe@13403
   131
berghofe@13403
   132
  "(realizes t (P \<and> Q)) \<equiv> (realizes (fst t) P \<and> realizes (snd t) Q)"
berghofe@13403
   133
berghofe@13403
   134
  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow>
berghofe@13403
   135
     realizes t (\<not> P) \<equiv> \<not> realizes Null P"
berghofe@13403
   136
berghofe@13403
   137
  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow>
berghofe@13403
   138
     realizes t (\<not> P) \<equiv> (\<forall>x::'P. \<not> realizes x P)"
berghofe@13403
   139
berghofe@13403
   140
  "typeof (P::bool) \<equiv> Type (TYPE(Null)) \<Longrightarrow>
berghofe@13403
   141
   typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow>
berghofe@13403
   142
     realizes t (P = Q) \<equiv> realizes Null P = realizes Null Q"
berghofe@13403
   143
berghofe@13403
   144
  "(realizes t (P = Q)) \<equiv> (realizes t ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)))"
berghofe@13403
   145
berghofe@13403
   146
subsection {* Computational content of basic inference rules *}
berghofe@13403
   147
berghofe@13403
   148
theorem disjE_realizer:
berghofe@13403
   149
  assumes r: "case x of Inl p \<Rightarrow> P p | Inr q \<Rightarrow> Q q"
berghofe@13403
   150
  and r1: "\<And>p. P p \<Longrightarrow> R (f p)" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)"
berghofe@13403
   151
  shows "R (case x of Inl p \<Rightarrow> f p | Inr q \<Rightarrow> g q)"
berghofe@13403
   152
proof (cases x)
berghofe@13403
   153
  case Inl
berghofe@13403
   154
  with r show ?thesis by simp (rule r1)
berghofe@13403
   155
next
berghofe@13403
   156
  case Inr
berghofe@13403
   157
  with r show ?thesis by simp (rule r2)
berghofe@13403
   158
qed
berghofe@13403
   159
berghofe@13403
   160
theorem disjE_realizer2:
berghofe@13403
   161
  assumes r: "case x of None \<Rightarrow> P | Some q \<Rightarrow> Q q"
berghofe@13403
   162
  and r1: "P \<Longrightarrow> R f" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)"
berghofe@13403
   163
  shows "R (case x of None \<Rightarrow> f | Some q \<Rightarrow> g q)"
berghofe@13403
   164
proof (cases x)
berghofe@13403
   165
  case None
berghofe@13403
   166
  with r show ?thesis by simp (rule r1)
berghofe@13403
   167
next
berghofe@13403
   168
  case Some
berghofe@13403
   169
  with r show ?thesis by simp (rule r2)
berghofe@13403
   170
qed
berghofe@13403
   171
berghofe@13403
   172
theorem disjE_realizer3:
berghofe@13403
   173
  assumes r: "case x of Left \<Rightarrow> P | Right \<Rightarrow> Q"
berghofe@13403
   174
  and r1: "P \<Longrightarrow> R f" and r2: "Q \<Longrightarrow> R g"
berghofe@13403
   175
  shows "R (case x of Left \<Rightarrow> f | Right \<Rightarrow> g)"
berghofe@13403
   176
proof (cases x)
berghofe@13403
   177
  case Left
berghofe@13403
   178
  with r show ?thesis by simp (rule r1)
berghofe@13403
   179
next
berghofe@13403
   180
  case Right
berghofe@13403
   181
  with r show ?thesis by simp (rule r2)
berghofe@13403
   182
qed
berghofe@13403
   183
berghofe@13403
   184
theorem conjI_realizer:
berghofe@13403
   185
  "P p \<Longrightarrow> Q q \<Longrightarrow> P (fst (p, q)) \<and> Q (snd (p, q))"
berghofe@13403
   186
  by simp
berghofe@13403
   187
berghofe@13403
   188
theorem exI_realizer:
berghofe@13403
   189
  "P x y \<Longrightarrow> P (fst (x, y)) (snd (x, y))" by simp
berghofe@13403
   190
berghofe@13403
   191
realizers
berghofe@13403
   192
  impI (P, Q): "\<lambda>P Q pq. pq"
berghofe@13403
   193
    "\<Lambda>P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
berghofe@13403
   194
berghofe@13403
   195
  impI (P): "Null"
berghofe@13403
   196
    "\<Lambda>P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
berghofe@13403
   197
berghofe@13403
   198
  impI (Q): "\<lambda>P Q q. q" "\<Lambda>P Q q. impI \<cdot> _ \<cdot> _"
berghofe@13403
   199
berghofe@13403
   200
  impI: "Null" "\<Lambda>P Q. impI \<cdot> _ \<cdot> _"
berghofe@13403
   201
berghofe@13403
   202
  mp (P, Q): "\<lambda>P Q pq. pq"
berghofe@13403
   203
    "\<Lambda>P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
berghofe@13403
   204
berghofe@13403
   205
  mp (P): "Null"
berghofe@13403
   206
    "\<Lambda>P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
berghofe@13403
   207
berghofe@13403
   208
  mp (Q): "\<lambda>P Q q. q" "\<Lambda>P Q q. mp \<cdot> _ \<cdot> _"
berghofe@13403
   209
berghofe@13403
   210
  mp: "Null" "\<Lambda>P Q. mp \<cdot> _ \<cdot> _"
berghofe@13403
   211
berghofe@13403
   212
  allI (P): "\<lambda>P p. p" "\<Lambda>P p. allI \<cdot> _"
berghofe@13403
   213
berghofe@13403
   214
  allI: "Null" "\<Lambda>P. allI \<cdot> _"
berghofe@13403
   215
berghofe@13403
   216
  spec (P): "\<lambda>P x p. p x" "\<Lambda>P x p. spec \<cdot> _ \<cdot> x"
berghofe@13403
   217
berghofe@13403
   218
  spec: "Null" "\<Lambda>P x. spec \<cdot> _ \<cdot> x"
berghofe@13403
   219
berghofe@13403
   220
  exI (P): "\<lambda>P x p. (x, p)" "\<Lambda>P. exI_realizer \<cdot> _"
berghofe@13403
   221
berghofe@13403
   222
  exI: "\<lambda>P x. x" "\<Lambda>P x (h: _). h"
berghofe@13403
   223
berghofe@13403
   224
  exE (P, Q): "\<lambda>P Q p pq. pq (fst p) (snd p)"
berghofe@13403
   225
    "\<Lambda>P Q p (h1: _) pq (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1"
berghofe@13403
   226
berghofe@13403
   227
  exE (P): "Null"
berghofe@13403
   228
    "\<Lambda>P Q p (h1: _) (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1"
berghofe@13403
   229
berghofe@13403
   230
  exE (Q): "\<lambda>P Q x pq. pq x"
berghofe@13403
   231
    "\<Lambda>P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
berghofe@13403
   232
berghofe@13403
   233
  exE: "Null"
berghofe@13403
   234
    "\<Lambda>P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
berghofe@13403
   235
berghofe@13403
   236
  conjI (P, Q): "\<lambda>P Q p q. (p, q)"
berghofe@13403
   237
    "\<Lambda>P Q p (h: _) q. conjI_realizer \<cdot>
berghofe@13403
   238
       (\<lambda>p. realizes p P) \<cdot> p \<cdot> (\<lambda>q. realizes q Q) \<cdot> q \<bullet> h"
berghofe@13403
   239
berghofe@13403
   240
  conjI (P): "\<lambda>P Q p. p"
berghofe@13403
   241
    "\<Lambda>P Q p. conjI \<cdot> _ \<cdot> _"
berghofe@13403
   242
berghofe@13403
   243
  conjI (Q): "\<lambda>P Q q. q"
berghofe@13403
   244
    "\<Lambda>P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
berghofe@13403
   245
berghofe@13403
   246
  conjI: "Null"
berghofe@13403
   247
    "\<Lambda>P Q. conjI \<cdot> _ \<cdot> _"
berghofe@13403
   248
berghofe@13403
   249
  conjunct1 (P, Q): "\<lambda>P Q. fst"
berghofe@13403
   250
    "\<Lambda>P Q pq. conjunct1 \<cdot> _ \<cdot> _"
berghofe@13403
   251
berghofe@13403
   252
  conjunct1 (P): "\<lambda>P Q p. p"
berghofe@13403
   253
    "\<Lambda>P Q p. conjunct1 \<cdot> _ \<cdot> _"
berghofe@13403
   254
berghofe@13403
   255
  conjunct1 (Q): "Null"
berghofe@13403
   256
    "\<Lambda>P Q q. conjunct1 \<cdot> _ \<cdot> _"
berghofe@13403
   257
berghofe@13403
   258
  conjunct1: "Null"
berghofe@13403
   259
    "\<Lambda>P Q. conjunct1 \<cdot> _ \<cdot> _"
berghofe@13403
   260
berghofe@13403
   261
  conjunct2 (P, Q): "\<lambda>P Q. snd"
berghofe@13403
   262
    "\<Lambda>P Q pq. conjunct2 \<cdot> _ \<cdot> _"
berghofe@13403
   263
berghofe@13403
   264
  conjunct2 (P): "Null"
berghofe@13403
   265
    "\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _"
berghofe@13403
   266
berghofe@13403
   267
  conjunct2 (Q): "\<lambda>P Q p. p"
berghofe@13403
   268
    "\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _"
berghofe@13403
   269
berghofe@13403
   270
  conjunct2: "Null"
berghofe@13403
   271
    "\<Lambda>P Q. conjunct2 \<cdot> _ \<cdot> _"
berghofe@13403
   272
berghofe@13403
   273
  disjI1 (P, Q): "\<lambda>P Q. Inl"
berghofe@13403
   274
    "\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> (\<lambda>p. realizes p P) \<cdot> _ \<cdot> p)"
berghofe@13403
   275
berghofe@13403
   276
  disjI1 (P): "\<lambda>P Q. Some"
berghofe@13403
   277
    "\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> (\<lambda>p. realizes p P) \<cdot> p)"
berghofe@13403
   278
berghofe@13403
   279
  disjI1 (Q): "\<lambda>P Q. None"
berghofe@13403
   280
    "\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
berghofe@13403
   281
berghofe@13403
   282
  disjI1: "\<lambda>P Q. Left"
berghofe@13403
   283
    "\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)"
berghofe@13403
   284
berghofe@13403
   285
  disjI2 (P, Q): "\<lambda>Q P. Inr"
berghofe@13403
   286
    "\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> (\<lambda>q. realizes q Q) \<cdot> q)"
berghofe@13403
   287
berghofe@13403
   288
  disjI2 (P): "\<lambda>Q P. None"
berghofe@13403
   289
    "\<Lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
berghofe@13403
   290
berghofe@13403
   291
  disjI2 (Q): "\<lambda>Q P. Some"
berghofe@13403
   292
    "\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> (\<lambda>q. realizes q Q) \<cdot> q)"
berghofe@13403
   293
berghofe@13403
   294
  disjI2: "\<lambda>Q P. Right"
berghofe@13403
   295
    "\<Lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)"
berghofe@13403
   296
berghofe@13403
   297
  disjE (P, Q, R): "\<lambda>P Q R pq pr qr.
berghofe@13403
   298
     (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
berghofe@13403
   299
    "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr.
berghofe@13403
   300
       disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
berghofe@13403
   301
berghofe@13403
   302
  disjE (Q, R): "\<lambda>P Q R pq pr qr.
berghofe@13403
   303
     (case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)"
berghofe@13403
   304
    "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr.
berghofe@13403
   305
       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
berghofe@13403
   306
berghofe@13403
   307
  disjE (P, R): "\<lambda>P Q R pq pr qr.
berghofe@13403
   308
     (case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)"
berghofe@13403
   309
    "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr (h3: _).
berghofe@13403
   310
       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2"
berghofe@13403
   311
berghofe@13403
   312
  disjE (R): "\<lambda>P Q R pq pr qr.
berghofe@13403
   313
     (case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)"
berghofe@13403
   314
    "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr.
berghofe@13403
   315
       disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
berghofe@13403
   316
berghofe@13403
   317
  disjE (P, Q): "Null"
berghofe@13403
   318
    "\<Lambda>P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _"
berghofe@13403
   319
berghofe@13403
   320
  disjE (Q): "Null"
berghofe@13403
   321
    "\<Lambda>P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _"
berghofe@13403
   322
berghofe@13403
   323
  disjE (P): "Null"
berghofe@13403
   324
    "\<Lambda>P Q R pq (h1: _) (h2: _) (h3: _).
berghofe@13403
   325
       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2"
berghofe@13403
   326
berghofe@13403
   327
  disjE: "Null"
berghofe@13403
   328
    "\<Lambda>P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _"
berghofe@13403
   329
berghofe@13403
   330
  FalseE (P): "\<lambda>P. arbitrary"
berghofe@13403
   331
    "\<Lambda>P. FalseE \<cdot> _"
berghofe@13403
   332
berghofe@13403
   333
  FalseE: "Null"
berghofe@13403
   334
    "\<Lambda>P. FalseE \<cdot> _"
berghofe@13403
   335
berghofe@13403
   336
  notI (P): "Null"
berghofe@13403
   337
    "\<Lambda>P (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
berghofe@13403
   338
berghofe@13403
   339
  notI: "Null"
berghofe@13403
   340
    "\<Lambda>P. notI \<cdot> _"
berghofe@13403
   341
berghofe@13403
   342
  notE (P, R): "\<lambda>P R p. arbitrary"
berghofe@13403
   343
    "\<Lambda>P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
berghofe@13403
   344
berghofe@13403
   345
  notE (P): "Null"
berghofe@13403
   346
    "\<Lambda>P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
berghofe@13403
   347
berghofe@13403
   348
  notE (R): "\<lambda>P R. arbitrary"
berghofe@13403
   349
    "\<Lambda>P R. notE \<cdot> _ \<cdot> _"
berghofe@13403
   350
berghofe@13403
   351
  notE: "Null"
berghofe@13403
   352
    "\<Lambda>P R. notE \<cdot> _ \<cdot> _"
berghofe@13403
   353
berghofe@13403
   354
  subst (P): "\<lambda>s t P ps. ps"
berghofe@13403
   355
    "\<Lambda>s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> (\<lambda>x. realizes ps (P x)) \<bullet> h"
berghofe@13403
   356
berghofe@13403
   357
  subst: "Null"
berghofe@13403
   358
    "\<Lambda>s t P. subst \<cdot> s \<cdot> t \<cdot> (\<lambda>x. realizes Null (P x))"
berghofe@13403
   359
berghofe@13403
   360
  iffD1 (P, Q): "\<lambda>Q P. fst"
berghofe@13403
   361
    "\<Lambda>Q P pq (h: _) p.
berghofe@13403
   362
       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
berghofe@13403
   363
berghofe@13403
   364
  iffD1 (P): "\<lambda>Q P p. p"
berghofe@13403
   365
    "\<Lambda>Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
berghofe@13403
   366
berghofe@13403
   367
  iffD1 (Q): "Null"
berghofe@13403
   368
    "\<Lambda>Q P q1 (h: _) q2.
berghofe@13403
   369
       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
berghofe@13403
   370
berghofe@13403
   371
  iffD1: "Null"
berghofe@13403
   372
    "\<Lambda>Q P. iffD1 \<cdot> _ \<cdot> _"
berghofe@13403
   373
berghofe@13403
   374
  iffD2 (P, Q): "\<lambda>P Q. snd"
berghofe@13403
   375
    "\<Lambda>P Q pq (h: _) q.
berghofe@13403
   376
       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
berghofe@13403
   377
berghofe@13403
   378
  iffD2 (P): "\<lambda>P Q p. p"
berghofe@13403
   379
    "\<Lambda>P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
berghofe@13403
   380
berghofe@13403
   381
  iffD2 (Q): "Null"
berghofe@13403
   382
    "\<Lambda>P Q q1 (h: _) q2.
berghofe@13403
   383
       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
berghofe@13403
   384
berghofe@13403
   385
  iffD2: "Null"
berghofe@13403
   386
    "\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _"
berghofe@13403
   387
berghofe@13403
   388
  iffI (P, Q): "\<lambda>P Q pq qp. (pq, qp)"
berghofe@13403
   389
    "\<Lambda>P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
berghofe@13403
   390
       (\<lambda>pq. \<forall>x. realizes x P \<longrightarrow> realizes (pq x) Q) \<cdot> pq \<cdot>
berghofe@13403
   391
       (\<lambda>qp. \<forall>x. realizes x Q \<longrightarrow> realizes (qp x) P) \<cdot> qp \<bullet>
berghofe@13403
   392
       (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
berghofe@13403
   393
       (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
berghofe@13403
   394
berghofe@13403
   395
  iffI (P): "\<lambda>P Q p. p"
berghofe@13403
   396
    "\<Lambda>P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
berghofe@13403
   397
       (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
berghofe@13403
   398
       (impI \<cdot> _ \<cdot> _ \<bullet> h2)"
berghofe@13403
   399
berghofe@13403
   400
  iffI (Q): "\<lambda>P Q q. q"
berghofe@13403
   401
    "\<Lambda>P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
berghofe@13403
   402
       (impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet>
berghofe@13403
   403
       (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
berghofe@13403
   404
berghofe@13403
   405
  iffI: "Null"
berghofe@13403
   406
    "\<Lambda>P Q. iffI \<cdot> _ \<cdot> _"
berghofe@13403
   407
berghofe@13403
   408
  classical: "Null"
berghofe@13403
   409
    "\<Lambda>P. classical \<cdot> _"
berghofe@13403
   410
berghofe@13403
   411
end