# HG changeset patch
# User schirmer
# Date 1078351103 -3600
# Node ID cea7d2f76112de990038685f37aba30b8eca8e8b
# Parent  de890c247b38775a6cdfcb61d2cccc231ef69d00
added record_ex_sel_eq_simproc

diff -r de890c247b38 -r cea7d2f76112 NEWS
--- a/NEWS	Tue Mar 02 11:06:37 2004 +0100
+++ b/NEWS	Wed Mar 03 22:58:23 2004 +0100
@@ -109,6 +109,8 @@
     the reference "print_record_type_abbr".
   - Simproc "record_upd_simproc" for simplification of multiple updates added 
     (not enabled by default).
+  - Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp.
+    EX x. x = sel r to True (not enabled by default).
   - Tactic "record_split_simp_tac" to split and simplify records added.
  
 * 'specification' command added, allowing for definition by
diff -r de890c247b38 -r cea7d2f76112 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Mar 02 11:06:37 2004 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Mar 03 22:58:23 2004 +0100
@@ -43,6 +43,7 @@
   val setup: (theory -> theory) list
   val record_upd_simproc: simproc
   val record_split_simproc: (term -> bool) -> simproc
+  val record_ex_sel_eq_simproc: simproc
   val record_split_simp_tac: (term -> bool) -> int -> tactic
 end;
 
@@ -819,6 +820,41 @@
          else None
        | _ => None))
 
+(* record_ex_sel_eq_simproc *)
+(* record: (EX r. x = sel r) resp. (EX r. sel r = x) to True *) 
+val record_ex_sel_eq_simproc =
+  Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
+    (fn sg => fn _ => fn t =>
+       let fun prove prop = (quick_and_dirty_prove sg [] [] prop 
+                             (fn _ => (simp_tac ((get_simpset sg) addsimps simp_thms
+                                       addsimprocs [record_split_simproc (K true)]) 1)));
+       in     
+         (case t of 
+           (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X)) =>
+             (case get_selectors sg sel of Some () =>
+                let 
+                  val X' = ("x",range_type Tsel);
+		  val prop = list_all ([X'], 
+                               Logic.mk_equals
+		                 (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$
+                                                      (Const (sel,Tsel)$Bound 0)$Bound 1),
+                                  Const ("True",HOLogic.boolT)));
+                in Some (prove prop) end
+              | None => None)
+          |(Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0))) =>
+             (case get_selectors sg sel of Some () =>
+                let 
+                  val X' = ("x",range_type Tsel);
+		  val prop = list_all ([X'], 
+                               Logic.mk_equals
+		                 (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$
+                                                     Bound 1$(Const (sel,Tsel)$Bound 0)),
+                                  Const ("True",HOLogic.boolT)));
+                in Some (prove prop) end 
+            | None => None)
+          | _ => None)
+         end)
+
 (** record field splitting **)
 
 (* tactic *)