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