Realizer for exE now uses let instead of case.
authorberghofe
Fri Dec 10 16:47:15 2004 +0100 (2004-12-10)
changeset 153932e6a9146caca
parent 15392 290bc97038c7
child 15394 a2c34e6ca4f8
Realizer for exE now uses let instead of case.
src/HOL/Extraction.thy
     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"