author berghofe Fri Dec 10 16:47:15 2004 +0100 (2004-12-10) changeset 15393 2e6a9146caca parent 15392 290bc97038c7 child 15394 a2c34e6ca4f8
Realizer for exE now uses let instead of case.
 src/HOL/Extraction.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Extraction.thy	Thu Dec 09 18:30:59 2004 +0100
1.2 +++ b/src/HOL/Extraction.thy	Fri Dec 10 16:47:15 2004 +0100
1.3 @@ -213,8 +213,8 @@
1.4    "P y x \<Longrightarrow> P (snd (x, y)) (fst (x, y))" by simp
1.5
1.6  theorem exE_realizer: "P (snd p) (fst p) \<Longrightarrow>
1.7 -  (\<And>x y. P y x \<Longrightarrow> Q (f x y)) \<Longrightarrow> Q (case p of (x, y) \<Rightarrow> f x y)"
1.8 -  by (cases p) simp
1.9 +  (\<And>x y. P y x \<Longrightarrow> Q (f x y)) \<Longrightarrow> Q (let (x, y) = p in f x y)"
1.10 +  by (cases p) (simp add: Let_def)
1.11
1.12  theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow>
1.13    (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp
1.14 @@ -252,7 +252,7 @@
1.15
1.16    exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h"
1.17
1.18 -  exE (P, Q): "\<lambda>p pq. case p of (x, y) \<Rightarrow> pq x y"
1.19 +  exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y"
1.20      "\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h"
1.21
1.22    exE (P): "Null"
```