--- 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 * <split_posns> *)
-
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";