src/HOL/Extraction.thy
 changeset 13918 2134ed516b1b parent 13725 12404b452034 child 13942 dc93e3a68142
1.1 --- a/src/HOL/Extraction.thy	Wed Apr 23 00:13:32 2003 +0200
1.2 +++ b/src/HOL/Extraction.thy	Wed Apr 23 00:14:55 2003 +0200
1.3 @@ -210,7 +210,14 @@
1.4    by simp
1.6  theorem exI_realizer:
1.7 -  "P x y \<Longrightarrow> P (fst (x, y)) (snd (x, y))" by simp
1.8 +  "P y x \<Longrightarrow> P (snd (x, y)) (fst (x, y))" by simp
1.9 +
1.10 +theorem exE_realizer: "P (snd p) (fst p) \<Longrightarrow>
1.11 +  (\<And>x y. P y x \<Longrightarrow> Q (f x y)) \<Longrightarrow> Q (case p of (x, y) \<Rightarrow> f x y)"
1.12 +  by (cases p) simp
1.13 +
1.14 +theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow>
1.15 +  (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp
1.17  realizers
1.18    impI (P, Q): "\<lambda>pq. pq"
1.19 @@ -241,15 +248,15 @@
1.21    spec: "Null" "spec"
1.23 -  exI (P): "\<lambda>x p. (x, p)" "\<Lambda>P. exI_realizer \<cdot> _"
1.24 +  exI (P): "\<lambda>x p. (x, p)" "\<Lambda>P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x"
1.26    exI: "\<lambda>x. x" "\<Lambda>P x (h: _). h"
1.28 -  exE (P, Q): "\<lambda>p pq. pq (fst p) (snd p)"
1.29 -    "\<Lambda>P Q p (h1: _) pq (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1"
1.30 +  exE (P, Q): "\<lambda>p pq. case p of (x, y) \<Rightarrow> pq x y"
1.31 +    "\<Lambda>P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h"
1.33    exE (P): "Null"
1.34 -    "\<Lambda>P Q p (h1: _) (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1"
1.35 +    "\<Lambda>P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _"
1.37    exE (Q): "\<lambda>x pq. pq x"
1.38      "\<Lambda>P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"