module setup;
authorwenzelm
Fri Feb 02 22:20:43 2001 +0100 (2001-02-02)
changeset 1103737716a82a3d9
parent 11036 3c30f7b97a50
child 11038 932d66879fe7
module setup;
use hidden internal_split constants;
src/HOL/Tools/split_rule.ML
     1.1 --- a/src/HOL/Tools/split_rule.ML	Fri Feb 02 22:20:09 2001 +0100
     1.2 +++ b/src/HOL/Tools/split_rule.ML	Fri Feb 02 22:20:43 2001 +0100
     1.3 @@ -1,14 +1,51 @@
     1.4 -(*Attempts to remove occurrences of split, and pair-valued parameters*)
     1.5 -val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
     1.6 +(*  Title:      Tools/split_rule.ML
     1.7 +    ID:         $Id$
     1.8 +    Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
     1.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10 +
    1.11 +Some tools for managing tupled arguments and abstractions in rules.
    1.12 +*)
    1.13 +
    1.14 +signature BASIC_SPLIT_RULE =
    1.15 +sig
    1.16 +  val split_rule: thm -> thm
    1.17 +  val complete_split_rule: thm -> thm
    1.18 +end;
    1.19  
    1.20 -local
    1.21 +signature SPLIT_RULE =
    1.22 +sig
    1.23 +  include BASIC_SPLIT_RULE
    1.24 +  val split_rule_var: term * thm -> thm
    1.25 +  val split_rule_goal: string list list -> thm -> thm
    1.26 +  val setup: (theory -> theory) list
    1.27 +end;
    1.28 +
    1.29 +structure SplitRule: SPLIT_RULE =
    1.30 +struct
    1.31 +
    1.32 +
    1.33 +(** theory context references **)
    1.34 +
    1.35 +fun internal_split_const (Ta, Tb, Tc) =
    1.36 +  Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
    1.37 +
    1.38 +val internal_split_def = thm "internal_split_def";
    1.39 +val internal_split_conv = thm "internal_split_conv";
    1.40 +
    1.41 +
    1.42 +
    1.43 +(** split rules **)
    1.44 +
    1.45 +val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv];
    1.46 +val remove_internal_split = eval_internal_split o split_all;
    1.47 +
    1.48  
    1.49  (*In ap_split S T u, term u expects separate arguments for the factors of S,
    1.50    with result type T.  The call creates a new term expecting one argument
    1.51    of type S.*)
    1.52  fun ap_split (Type ("*", [T1, T2])) T3 u =
    1.53 -      HOLogic.split_const (T1, T2, T3) $
    1.54 -      Abs("v", T1,
    1.55 +      internal_split_const (T1, T2, T3) $
    1.56 +      Abs ("v", T1,
    1.57            ap_split T2 T3
    1.58               ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
    1.59                Bound 0))
    1.60 @@ -16,15 +53,14 @@
    1.61  
    1.62  (*Curries any Var of function type in the rule*)
    1.63  fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
    1.64 -      let val T' = HOLogic.prodT_factors T1 ---> T2
    1.65 -          val newt = ap_split T1 T2 (Var (v, T'))
    1.66 -          val cterm = Thm.cterm_of (#sign (rep_thm rl))
    1.67 -      in
    1.68 -          instantiate ([], [(cterm t, cterm newt)]) rl
    1.69 -      end
    1.70 +      let val T' = HOLogic.prodT_factors T1 ---> T2;
    1.71 +          val newt = ap_split T1 T2 (Var (v, T'));
    1.72 +          val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
    1.73 +      in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
    1.74    | split_rule_var' (t, rl) = rl;
    1.75  
    1.76 -(*** Complete splitting of partially splitted rules ***)
    1.77 +
    1.78 +(* complete splitting of partially splitted rules *)
    1.79  
    1.80  fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
    1.81        (ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U)
    1.82 @@ -33,7 +69,7 @@
    1.83  
    1.84  fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
    1.85        let
    1.86 -        val cterm = Thm.cterm_of (#sign (rep_thm rl))
    1.87 +        val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl))
    1.88          val (Us', U') = strip_type T;
    1.89          val Us = take (length ts, Us');
    1.90          val U = drop (length ts, Us') ---> U';
    1.91 @@ -41,13 +77,13 @@
    1.92          fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
    1.93                let
    1.94                  val Ts = HOLogic.prodT_factors T;
    1.95 -                val ys = variantlist (replicate (length Ts) a, xs);
    1.96 +                val ys = Term.variantlist (replicate (length Ts) a, xs);
    1.97                in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
    1.98                  (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
    1.99                end
   1.100            | mk_tuple (x, _) = x;
   1.101          val newt = ap_split' Us U (Var (v, T'));
   1.102 -        val cterm = Thm.cterm_of (#sign (rep_thm rl));
   1.103 +        val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
   1.104          val (vs', insts) = foldl mk_tuple ((vs, []), ts);
   1.105        in
   1.106          (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
   1.107 @@ -59,37 +95,60 @@
   1.108          (v as Var _, ts) => (v, ts)::vs
   1.109        | (t, ts) => foldl collect_vars (vs, ts));
   1.110  
   1.111 -in
   1.112 +
   1.113 +val split_rule_var = Drule.standard o remove_internal_split o split_rule_var';
   1.114  
   1.115 -val split_rule_var = standard o remove_split o split_rule_var';
   1.116 -
   1.117 -(*Curries ALL function variables occurring in a rule's conclusion*)
   1.118 -fun split_rule rl = standard (remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)));
   1.119 +(*curries ALL function variables occurring in a rule's conclusion*)
   1.120 +fun split_rule rl =
   1.121 +  foldr split_rule_var' (Term.term_vars (concl_of rl), rl)
   1.122 +  |> remove_internal_split
   1.123 +  |> Drule.standard;
   1.124  
   1.125  fun complete_split_rule rl =
   1.126 -  standard (remove_split (fst (foldr complete_split_rule_var
   1.127 +  fst (foldr complete_split_rule_var
   1.128      (collect_vars ([], concl_of rl),
   1.129 -     (rl, map (fst o fst o dest_Var) (term_vars (#prop (rep_thm rl))))))))
   1.130 -	|> RuleCases.save rl;
   1.131 +      (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))))
   1.132 +  |> remove_internal_split
   1.133 +  |> Drule.standard
   1.134 +  |> RuleCases.save rl;
   1.135 +
   1.136 +
   1.137 +val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
   1.138 +
   1.139 +fun split_rule_goal xss rl =
   1.140 +  let
   1.141 +    fun one_split i (th, s) = Tactic.rule_by_tactic (pair_tac s i) th;
   1.142 +    fun one_goal (xs, i) th = foldl (one_split i) (th, xs);
   1.143 +  in
   1.144 +    Drule.standard (Simplifier.full_simplify split_rule_ss (Library.foldln one_goal xss rl))
   1.145 +    |> RuleCases.save rl
   1.146 +  end;
   1.147 +
   1.148 +
   1.149 +(* attribute syntax *)
   1.150 +
   1.151 +fun complete_split x =
   1.152 +  Attrib.no_args (Drule.rule_attribute (K complete_split_rule)) x;
   1.153 +
   1.154 +fun split_format x =
   1.155 +  Attrib.syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name))
   1.156 +    >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
   1.157 +
   1.158 +val split_attributes =
   1.159 + [("complete_split", (complete_split, complete_split),
   1.160 +    "recursively split all pair-typed function arguments"),
   1.161 +  ("split_format", (split_format, split_format),
   1.162 +    "split given pair-typed subterms in premises")];
   1.163 +
   1.164 +
   1.165 +
   1.166 +(** theory setup **)
   1.167 +
   1.168 +val setup =
   1.169 + [Attrib.add_attributes split_attributes];
   1.170 +
   1.171  
   1.172  end;
   1.173 -fun complete_split x = 
   1.174 -	Attrib.no_args (Drule.rule_attribute (K complete_split_rule)) x;
   1.175  
   1.176 -fun split_rule_goal xss rl = let 
   1.177 -	val ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; 
   1.178 -	fun one_split i (th,s) = rule_by_tactic (pair_tac s i) th;
   1.179 -	fun one_goal (xs,i) th = foldl (one_split i) (th,xs);
   1.180 -        in standard (Simplifier.full_simplify ss (foldln one_goal xss rl))
   1.181 -	   |> RuleCases.save rl
   1.182 -        end;
   1.183 -fun split_format x = 
   1.184 -	Attrib.syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) 
   1.185 -	>> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
   1.186 -
   1.187 -val split_attributes = [Attrib.add_attributes 
   1.188 -	[("complete_split", (complete_split, complete_split), 
   1.189 -          "recursively split all pair-typed function arguments"),
   1.190 -	 ("split_format", (split_format, split_format), 
   1.191 -          "split given pair-typed subterms in premises")]];
   1.192 -
   1.193 +structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
   1.194 +open BasicSplitRule;