# HG changeset patch # User wenzelm # Date 1256660371 -3600 # Node ID 99577c7085c8e9c89ef237949ec49362a246279a # Parent ea4e3f1eee69c01a03d45fee3a3b7bf63446336a misc tuning and simplification; diff -r ea4e3f1eee69 -r 99577c7085c8 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Tue Oct 27 16:49:57 2009 +0100 +++ b/src/Provers/splitter.ML Tue Oct 27 17:19:31 2009 +0100 @@ -26,9 +26,10 @@ signature SPLITTER = sig (* somewhat more internal functions *) - val cmap_of_split_thms : thm list -> (string * (typ * term * thm * typ * int) list) list - val split_posns : (string * (typ * term * thm * typ * int) list) list -> theory -> typ list -> term -> - (thm * (typ * typ * int list) list * int list * typ * term) list (* first argument is a "cmap", returns a list of "split packs" *) + val cmap_of_split_thms: thm list -> (string * (typ * term * thm * typ * int) list) list + val split_posns: (string * (typ * term * thm * typ * int) list) list -> + theory -> typ list -> term -> (thm * (typ * typ * int list) list * int list * typ * term) list + (* first argument is a "cmap", returns a list of "split packs" *) (* the "real" interface, providing a number of tactics *) val split_tac : thm list -> int -> tactic val split_inside_tac: thm list -> int -> tactic @@ -57,37 +58,33 @@ fun split_format_err () = error "Wrong format for split rule"; -(* thm -> (string * typ) * bool *) fun split_thm_info thm = case concl_of (Data.mk_eq thm) of Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false) | _ => split_format_err ()) | _ => split_format_err (); -(* thm list -> (string * (typ * term * thm * typ * int) list) list *) fun cmap_of_split_thms thms = let val splits = map Data.mk_eq thms - fun add_thm (cmap, thm) = - (case concl_of thm of _$(t as _$lhs)$_ => - (case strip_comb lhs of (Const(a,aT),args) => - let val info = (aT,lhs,thm,fastype_of t,length args) - in case AList.lookup (op =) cmap a of - SOME infos => AList.update (op =) (a, info::infos) cmap - | NONE => (a,[info])::cmap - end - | _ => split_format_err()) - | _ => split_format_err()) + fun add_thm thm cmap = + (case concl_of thm of _ $ (t as _ $ lhs) $ _ => + (case strip_comb lhs of (Const(a,aT),args) => + let val info = (aT,lhs,thm,fastype_of t,length args) + in case AList.lookup (op =) cmap a of + SOME infos => AList.update (op =) (a, info::infos) cmap + | NONE => (a,[info])::cmap + end + | _ => split_format_err()) + | _ => split_format_err()) in - Library.foldl add_thm ([], splits) + fold add_thm splits [] end; (* ------------------------------------------------------------------------- *) (* mk_case_split_tac *) (* ------------------------------------------------------------------------- *) -(* (int * int -> order) -> thm list -> int -> tactic * *) - fun mk_case_split_tac order = let @@ -225,13 +222,11 @@ local exception MATCH in - (* Context.theory -> Type.tyenv * (Term.typ * Term.typ) -> Type.tyenv *) fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv) handle Type.TYPE_MATCH => raise MATCH - (* Context.theory -> Term.typ list * Term.term * Term.term -> bool *) + fun fomatch sg args = let - (* Type.tyenv -> Term.typ list * Term.term * Term.term -> Type.tyenv *) fun mtch tyinsts = fn (Ts, Var(_,T), t) => typ_match sg (tyinsts, (T, fastype_of1(Ts,t))) @@ -247,10 +242,8 @@ mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u) | _ => raise MATCH in (mtch Vartab.empty args; true) handle MATCH => false end; -end (* local *) +end; -(* (string * (Term.typ * Term.term * Thm.thm * Term.typ * int) list) list -> Context.theory -> Term.typ list -> Term.term -> - (Thm.thm * (Term.typ * Term.typ * int list) list * int list * Term.typ * Term.term) list *) fun split_posns (cmap : (string * (typ * term * thm * typ * int) list) list) sg Ts t = let val T' = fastype_of1 (Ts, t); @@ -355,8 +348,6 @@ i : number of subgoal the tactic should be applied to *****************************************************************************) -(* thm list -> int -> tactic *) - fun split_tac [] i = no_tac | split_tac splits i = let val cmap = cmap_of_split_thms splits @@ -379,9 +370,9 @@ in (split_tac, exported_split_posns) end; (* mk_case_split_tac *) -val (split_tac, split_posns) = mk_case_split_tac int_ord; +val (split_tac, split_posns) = mk_case_split_tac int_ord; -val (split_inside_tac, _) = mk_case_split_tac (rev_order o int_ord); +val (split_inside_tac, _) = mk_case_split_tac (rev_order o int_ord); (***************************************************************************** @@ -389,7 +380,7 @@ splits : list of split-theorems to be tried ****************************************************************************) -fun split_asm_tac [] = K no_tac +fun split_asm_tac [] = K no_tac | split_asm_tac splits = let val cname_list = map (fst o fst o split_thm_info) splits; @@ -431,25 +422,28 @@ (* addsplits / delsplits *) -fun string_of_typ (Type (s, Ts)) = (if null Ts then "" - else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s +fun string_of_typ (Type (s, Ts)) = + (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s | string_of_typ _ = "_"; fun split_name (name, T) asm = "split " ^ (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T; fun ss addsplits splits = - let fun addsplit (ss,split) = - let val (name,asm) = split_thm_info split - in Simplifier.addloop (ss, (split_name name asm, - (if asm then split_asm_tac else split_tac) [split])) end - in Library.foldl addsplit (ss,splits) end; + let + fun addsplit split ss = + let + val (name, asm) = split_thm_info split + val tac = (if asm then split_asm_tac else split_tac) [split] + in Simplifier.addloop (ss, (split_name name asm, tac)) end + in fold addsplit splits ss end; fun ss delsplits splits = - let fun delsplit(ss,split) = - let val (name,asm) = split_thm_info split - in Simplifier.delloop (ss, split_name name asm) - end in Library.foldl delsplit (ss,splits) end; + let + fun delsplit split ss = + let val (name, asm) = split_thm_info split + in Simplifier.delloop (ss, split_name name asm) end + in fold delsplit splits ss end; (* attributes *) @@ -471,7 +465,8 @@ (* theory setup *) val setup = - Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #> + Attrib.setup @{binding split} + (Attrib.add_del split_add split_del) "declare case split rule" #> Method.setup @{binding split} (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) "apply case split rule";