--- a/src/HOL/Tools/split_rule.ML Fri Feb 02 22:20:09 2001 +0100
+++ b/src/HOL/Tools/split_rule.ML Fri Feb 02 22:20:43 2001 +0100
@@ -1,14 +1,51 @@
-(*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
+(* Title: Tools/split_rule.ML
+ ID: $Id$
+ Author: Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+Some tools for managing tupled arguments and abstractions in rules.
+*)
+
+signature BASIC_SPLIT_RULE =
+sig
+ val split_rule: thm -> thm
+ val complete_split_rule: thm -> thm
+end;
-local
+signature SPLIT_RULE =
+sig
+ include BASIC_SPLIT_RULE
+ val split_rule_var: term * thm -> thm
+ val split_rule_goal: string list list -> thm -> thm
+ val setup: (theory -> theory) list
+end;
+
+structure SplitRule: SPLIT_RULE =
+struct
+
+
+(** theory context references **)
+
+fun internal_split_const (Ta, Tb, Tc) =
+ Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
+
+val internal_split_def = thm "internal_split_def";
+val internal_split_conv = thm "internal_split_conv";
+
+
+
+(** split rules **)
+
+val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv];
+val remove_internal_split = eval_internal_split o split_all;
+
(*In ap_split S T u, term u expects separate arguments for the factors of S,
with result type T. The call creates a new term expecting one argument
of type S.*)
fun ap_split (Type ("*", [T1, T2])) T3 u =
- HOLogic.split_const (T1, T2, T3) $
- Abs("v", T1,
+ internal_split_const (T1, T2, T3) $
+ Abs ("v", T1,
ap_split T2 T3
((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
Bound 0))
@@ -16,15 +53,14 @@
(*Curries any Var of function type in the rule*)
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
- let val T' = HOLogic.prodT_factors T1 ---> T2
- val newt = ap_split T1 T2 (Var (v, T'))
- val cterm = Thm.cterm_of (#sign (rep_thm rl))
- in
- instantiate ([], [(cterm t, cterm newt)]) rl
- end
+ let val T' = HOLogic.prodT_factors T1 ---> T2;
+ val newt = ap_split T1 T2 (Var (v, T'));
+ val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
+ in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
| split_rule_var' (t, rl) = rl;
-(*** Complete splitting of partially splitted rules ***)
+
+(* complete splitting of partially splitted rules *)
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
(ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U)
@@ -33,7 +69,7 @@
fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
let
- val cterm = Thm.cterm_of (#sign (rep_thm rl))
+ val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl))
val (Us', U') = strip_type T;
val Us = take (length ts, Us');
val U = drop (length ts, Us') ---> U';
@@ -41,13 +77,13 @@
fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
let
val Ts = HOLogic.prodT_factors T;
- val ys = variantlist (replicate (length Ts) a, xs);
+ val ys = Term.variantlist (replicate (length Ts) a, xs);
in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
(map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
end
| mk_tuple (x, _) = x;
val newt = ap_split' Us U (Var (v, T'));
- val cterm = Thm.cterm_of (#sign (rep_thm rl));
+ val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
val (vs', insts) = foldl mk_tuple ((vs, []), ts);
in
(instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
@@ -59,37 +95,60 @@
(v as Var _, ts) => (v, ts)::vs
| (t, ts) => foldl collect_vars (vs, ts));
-in
+
+val split_rule_var = Drule.standard o remove_internal_split o split_rule_var';
-val split_rule_var = standard o remove_split o split_rule_var';
-
-(*Curries ALL function variables occurring in a rule's conclusion*)
-fun split_rule rl = standard (remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)));
+(*curries ALL function variables occurring in a rule's conclusion*)
+fun split_rule rl =
+ foldr split_rule_var' (Term.term_vars (concl_of rl), rl)
+ |> remove_internal_split
+ |> Drule.standard;
fun complete_split_rule rl =
- standard (remove_split (fst (foldr complete_split_rule_var
+ fst (foldr complete_split_rule_var
(collect_vars ([], concl_of rl),
- (rl, map (fst o fst o dest_Var) (term_vars (#prop (rep_thm rl))))))))
- |> RuleCases.save rl;
+ (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))))
+ |> remove_internal_split
+ |> Drule.standard
+ |> RuleCases.save rl;
+
+
+val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
+
+fun split_rule_goal xss rl =
+ let
+ fun one_split i (th, s) = Tactic.rule_by_tactic (pair_tac s i) th;
+ fun one_goal (xs, i) th = foldl (one_split i) (th, xs);
+ in
+ Drule.standard (Simplifier.full_simplify split_rule_ss (Library.foldln one_goal xss rl))
+ |> RuleCases.save rl
+ end;
+
+
+(* attribute syntax *)
+
+fun complete_split x =
+ Attrib.no_args (Drule.rule_attribute (K complete_split_rule)) x;
+
+fun split_format x =
+ Attrib.syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name))
+ >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
+
+val split_attributes =
+ [("complete_split", (complete_split, complete_split),
+ "recursively split all pair-typed function arguments"),
+ ("split_format", (split_format, split_format),
+ "split given pair-typed subterms in premises")];
+
+
+
+(** theory setup **)
+
+val setup =
+ [Attrib.add_attributes split_attributes];
+
end;
-fun complete_split x =
- Attrib.no_args (Drule.rule_attribute (K complete_split_rule)) x;
-fun split_rule_goal xss rl = let
- val ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
- fun one_split i (th,s) = rule_by_tactic (pair_tac s i) th;
- fun one_goal (xs,i) th = foldl (one_split i) (th,xs);
- in standard (Simplifier.full_simplify ss (foldln one_goal xss rl))
- |> RuleCases.save rl
- end;
-fun split_format x =
- Attrib.syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name))
- >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
-
-val split_attributes = [Attrib.add_attributes
- [("complete_split", (complete_split, complete_split),
- "recursively split all pair-typed function arguments"),
- ("split_format", (split_format, split_format),
- "split given pair-typed subterms in premises")]];
-
+structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
+open BasicSplitRule;