added record_ex_sel_eq_simproc
authorschirmer
Wed Mar 03 22:58:23 2004 +0100 (2004-03-03)
changeset 14427cea7d2f76112
parent 14426 de890c247b38
child 14428 bb2b0e10d9be
added record_ex_sel_eq_simproc
NEWS
src/HOL/Tools/record_package.ML
     1.1 --- a/NEWS	Tue Mar 02 11:06:37 2004 +0100
     1.2 +++ b/NEWS	Wed Mar 03 22:58:23 2004 +0100
     1.3 @@ -109,6 +109,8 @@
     1.4      the reference "print_record_type_abbr".
     1.5    - Simproc "record_upd_simproc" for simplification of multiple updates added 
     1.6      (not enabled by default).
     1.7 +  - Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp.
     1.8 +    EX x. x = sel r to True (not enabled by default).
     1.9    - Tactic "record_split_simp_tac" to split and simplify records added.
    1.10   
    1.11  * 'specification' command added, allowing for definition by
     2.1 --- a/src/HOL/Tools/record_package.ML	Tue Mar 02 11:06:37 2004 +0100
     2.2 +++ b/src/HOL/Tools/record_package.ML	Wed Mar 03 22:58:23 2004 +0100
     2.3 @@ -43,6 +43,7 @@
     2.4    val setup: (theory -> theory) list
     2.5    val record_upd_simproc: simproc
     2.6    val record_split_simproc: (term -> bool) -> simproc
     2.7 +  val record_ex_sel_eq_simproc: simproc
     2.8    val record_split_simp_tac: (term -> bool) -> int -> tactic
     2.9  end;
    2.10  
    2.11 @@ -819,6 +820,41 @@
    2.12           else None
    2.13         | _ => None))
    2.14  
    2.15 +(* record_ex_sel_eq_simproc *)
    2.16 +(* record: (EX r. x = sel r) resp. (EX r. sel r = x) to True *) 
    2.17 +val record_ex_sel_eq_simproc =
    2.18 +  Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
    2.19 +    (fn sg => fn _ => fn t =>
    2.20 +       let fun prove prop = (quick_and_dirty_prove sg [] [] prop 
    2.21 +                             (fn _ => (simp_tac ((get_simpset sg) addsimps simp_thms
    2.22 +                                       addsimprocs [record_split_simproc (K true)]) 1)));
    2.23 +       in     
    2.24 +         (case t of 
    2.25 +           (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X)) =>
    2.26 +             (case get_selectors sg sel of Some () =>
    2.27 +                let 
    2.28 +                  val X' = ("x",range_type Tsel);
    2.29 +		  val prop = list_all ([X'], 
    2.30 +                               Logic.mk_equals
    2.31 +		                 (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$
    2.32 +                                                      (Const (sel,Tsel)$Bound 0)$Bound 1),
    2.33 +                                  Const ("True",HOLogic.boolT)));
    2.34 +                in Some (prove prop) end
    2.35 +              | None => None)
    2.36 +          |(Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0))) =>
    2.37 +             (case get_selectors sg sel of Some () =>
    2.38 +                let 
    2.39 +                  val X' = ("x",range_type Tsel);
    2.40 +		  val prop = list_all ([X'], 
    2.41 +                               Logic.mk_equals
    2.42 +		                 (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$
    2.43 +                                                     Bound 1$(Const (sel,Tsel)$Bound 0)),
    2.44 +                                  Const ("True",HOLogic.boolT)));
    2.45 +                in Some (prove prop) end 
    2.46 +            | None => None)
    2.47 +          | _ => None)
    2.48 +         end)
    2.49 +
    2.50  (** record field splitting **)
    2.51  
    2.52  (* tactic *)