# HG changeset patch # User wenzelm # Date 981148843 -3600 # Node ID 37716a82a3d9a50eb278b97a9ab99f73afcc4d04 # Parent 3c30f7b97a50708b2ced32bb9604dd649cccabff module setup; use hidden internal_split constants; diff -r 3c30f7b97a50 -r 37716a82a3d9 src/HOL/Tools/split_rule.ML --- 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;