modernized structure Split_Rule;
authorwenzelm
Thu Feb 25 22:46:52 2010 +0100 (2010-02-25)
changeset 353652fcd08c62495
parent 35364 b8c62d60195c
child 35377 d84eec579695
child 35382 598ee3a4c1aa
modernized structure Split_Rule;
tuned signature;
more antiquotations;
src/HOL/Product_Type.thy
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/split_rule.ML
     1.1 --- a/src/HOL/Product_Type.thy	Thu Feb 25 22:32:09 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Feb 25 22:46:52 2010 +0100
     1.3 @@ -635,7 +635,7 @@
     1.4    by (simp only: internal_split_def split_conv)
     1.5  
     1.6  use "Tools/split_rule.ML"
     1.7 -setup SplitRule.setup
     1.8 +setup Split_Rule.setup
     1.9  
    1.10  hide const internal_split
    1.11  
     2.1 --- a/src/HOL/Tools/TFL/post.ML	Thu Feb 25 22:32:09 2010 +0100
     2.2 +++ b/src/HOL/Tools/TFL/post.ML	Thu Feb 25 22:46:52 2010 +0100
     2.3 @@ -125,7 +125,7 @@
     2.4  
     2.5  (*lcp: curry the predicate of the induction rule*)
     2.6  fun curry_rule rl =
     2.7 -  SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
     2.8 +  Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
     2.9  
    2.10  (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
    2.11  val meta_outer =
     3.1 --- a/src/HOL/Tools/split_rule.ML	Thu Feb 25 22:32:09 2010 +0100
     3.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Feb 25 22:46:52 2010 +0100
     3.3 @@ -4,49 +4,34 @@
     3.4  Some tools for managing tupled arguments and abstractions in rules.
     3.5  *)
     3.6  
     3.7 -signature BASIC_SPLIT_RULE =
     3.8 +signature SPLIT_RULE =
     3.9  sig
    3.10 +  val split_rule_var: term -> thm -> thm
    3.11 +  val split_rule_goal: Proof.context -> string list list -> thm -> thm
    3.12    val split_rule: thm -> thm
    3.13    val complete_split_rule: thm -> thm
    3.14 -end;
    3.15 -
    3.16 -signature SPLIT_RULE =
    3.17 -sig
    3.18 -  include BASIC_SPLIT_RULE
    3.19 -  val split_rule_var: term -> thm -> thm
    3.20 -  val split_rule_goal: Proof.context -> string list list -> thm -> thm
    3.21    val setup: theory -> theory
    3.22  end;
    3.23  
    3.24 -structure SplitRule: SPLIT_RULE =
    3.25 +structure Split_Rule: SPLIT_RULE =
    3.26  struct
    3.27  
    3.28 -
    3.29 -
    3.30 -(** theory context references **)
    3.31 -
    3.32 -val split_conv = thm "split_conv";
    3.33 -val fst_conv = thm "fst_conv";
    3.34 -val snd_conv = thm "snd_conv";
    3.35 -
    3.36 -fun internal_split_const (Ta, Tb, Tc) =
    3.37 -  Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
    3.38 -
    3.39 -val internal_split_def = thm "internal_split_def";
    3.40 -val internal_split_conv = thm "internal_split_conv";
    3.41 -
    3.42 -
    3.43 -
    3.44  (** split rules **)
    3.45  
    3.46 -val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv];
    3.47 +fun internal_split_const (Ta, Tb, Tc) =
    3.48 +  Const (@{const_name Product_Type.internal_split},
    3.49 +    [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
    3.50 +
    3.51 +val eval_internal_split =
    3.52 +  hol_simplify [@{thm internal_split_def}] o hol_simplify [@{thm internal_split_conv}];
    3.53 +
    3.54  val remove_internal_split = eval_internal_split o split_all;
    3.55  
    3.56  
    3.57  (*In ap_split S T u, term u expects separate arguments for the factors of S,
    3.58    with result type T.  The call creates a new term expecting one argument
    3.59    of type S.*)
    3.60 -fun ap_split (Type ("*", [T1, T2])) T3 u =
    3.61 +fun ap_split (Type (@{type_name "*"}, [T1, T2])) T3 u =
    3.62        internal_split_const (T1, T2, T3) $
    3.63        Abs ("v", T1,
    3.64            ap_split T2 T3
    3.65 @@ -127,7 +112,7 @@
    3.66    THEN' hyp_subst_tac
    3.67    THEN' K prune_params_tac;
    3.68  
    3.69 -val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
    3.70 +val split_rule_ss = HOL_basic_ss addsimps [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}];
    3.71  
    3.72  fun split_rule_goal ctxt xss rl =
    3.73    let
    3.74 @@ -159,5 +144,3 @@
    3.75  
    3.76  end;
    3.77  
    3.78 -structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
    3.79 -open BasicSplitRule;