Tuned realizer for exE rule, to avoid blowup of extracted program.
authorberghofe
Wed Apr 23 00:14:55 2003 +0200 (2003-04-23)
changeset 139182134ed516b1b
parent 13917 a67c9e6570ac
child 13919 17d0e17c8efe
Tuned realizer for exE rule, to avoid blowup of extracted program.
src/HOL/Extraction.thy
     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.5  
     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.16  
    1.17  realizers
    1.18    impI (P, Q): "\<lambda>pq. pq"
    1.19 @@ -241,15 +248,15 @@
    1.20  
    1.21    spec: "Null" "spec"
    1.22  
    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.25  
    1.26    exI: "\<lambda>x. x" "\<Lambda>P x (h: _). h"
    1.27  
    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.32  
    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.36  
    1.37    exE (Q): "\<lambda>x pq. pq x"
    1.38      "\<Lambda>P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"