record_split_simp_tac now can get simp rules as parameter
authorschirmer
Fri Oct 15 18:49:16 2004 +0200 (2004-10-15)
changeset 15248b436486091a6
parent 15247 98d3ca56684d
child 15249 0da6b3075bfa
record_split_simp_tac now can get simp rules as parameter
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Fri Oct 15 18:16:11 2004 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Fri Oct 15 18:49:16 2004 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val record_split_simproc: (term -> bool) -> simproc
     1.5    val record_ex_sel_eq_simproc: simproc
     1.6    val record_split_tac: int -> tactic
     1.7 -  val record_split_simp_tac: (term -> bool) -> int -> tactic
     1.8 +  val record_split_simp_tac: thm list -> (term -> bool) -> int -> tactic
     1.9    val record_split_name: string
    1.10    val record_split_wrapper: string * wrapper
    1.11    val print_record_type_abbr: bool ref
    1.12 @@ -267,7 +267,7 @@
    1.13          updates = Symtab.merge (K true) (upds1, upds2),
    1.14          simpset = Simplifier.merge_ss (ss1, ss2)}
    1.15        (Symtab.merge Thm.eq_thm (equalities1, equalities2))
    1.16 -      (extinjects1 @ extinjects2)
    1.17 +      (gen_merge_lists Thm.eq_thm extinjects1 extinjects2)
    1.18        (Symtab.merge Thm.eq_thm (extsplit1,extsplit2))
    1.19        (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) 
    1.20                       => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso 
    1.21 @@ -1109,7 +1109,7 @@
    1.22   * P can peek on the whole subterm (including the quantifier); for free variables P
    1.23   * can only peek on the variable itself. 
    1.24   *)
    1.25 -fun record_split_simp_tac P i st =
    1.26 +fun record_split_simp_tac thms P i st =
    1.27    let
    1.28      val sg = Thm.sign_of_thm st;
    1.29      val {sel_upd={simpset,...},...} 
    1.30 @@ -1149,7 +1149,7 @@
    1.31      val simprocs = if has_rec goal then [record_split_simproc P] else [];
    1.32     
    1.33    in st |> (EVERY split_frees_tacs) 
    1.34 -           THEN (Simplifier.full_simp_tac (simpset addsimprocs simprocs) i)
    1.35 +           THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i)
    1.36    end handle Library.LIST _ => Seq.empty;
    1.37  end;
    1.38