src/HOL/Product_Type.thy
changeset 35364 b8c62d60195c
parent 35115 446c5063e4fd
child 35365 2fcd08c62495
     1.1 --- a/src/HOL/Product_Type.thy	Thu Feb 25 22:17:33 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Feb 25 22:32:09 2010 +0100
     1.3 @@ -448,44 +448,44 @@
     1.4  *}
     1.5  
     1.6  ML {*
     1.7 -
     1.8  local
     1.9 -  val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"]
    1.10 -  fun  Pair_pat k 0 (Bound m) = (m = k)
    1.11 -  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
    1.12 -                        m = k+i andalso Pair_pat k (i-1) t
    1.13 -  |    Pair_pat _ _ _ = false;
    1.14 -  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
    1.15 -  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
    1.16 -  |   no_args k i (Bound m) = m < k orelse m > k+i
    1.17 -  |   no_args _ _ _ = true;
    1.18 -  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
    1.19 -  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
    1.20 -  |   split_pat tp i _ = NONE;
    1.21 +  val cond_split_eta_ss = HOL_basic_ss addsimps @{thms cond_split_eta};
    1.22 +  fun Pair_pat k 0 (Bound m) = (m = k)
    1.23 +    | Pair_pat k i (Const (@{const_name Pair},  _) $ Bound m $ t) =
    1.24 +        i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t
    1.25 +    | Pair_pat _ _ _ = false;
    1.26 +  fun no_args k i (Abs (_, _, t)) = no_args (k + 1) i t
    1.27 +    | no_args k i (t $ u) = no_args k i t andalso no_args k i u
    1.28 +    | no_args k i (Bound m) = m < k orelse m > k + i
    1.29 +    | no_args _ _ _ = true;
    1.30 +  fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
    1.31 +    | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
    1.32 +    | split_pat tp i _ = NONE;
    1.33    fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
    1.34 -        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
    1.35 +        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
    1.36          (K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1)));
    1.37  
    1.38 -  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
    1.39 -  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
    1.40 -                        (beta_term_pat k i t andalso beta_term_pat k i u)
    1.41 -  |   beta_term_pat k i t = no_args k i t;
    1.42 -  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
    1.43 -  |    eta_term_pat _ _ _ = false;
    1.44 +  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t
    1.45 +    | beta_term_pat k i (t $ u) =
    1.46 +        Pair_pat k i (t $ u) orelse (beta_term_pat k i t andalso beta_term_pat k i u)
    1.47 +    | beta_term_pat k i t = no_args k i t;
    1.48 +  fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
    1.49 +    | eta_term_pat _ _ _ = false;
    1.50    fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
    1.51 -  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
    1.52 -                              else (subst arg k i t $ subst arg k i u)
    1.53 -  |   subst arg k i t = t;
    1.54 -  fun beta_proc ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
    1.55 +    | subst arg k i (t $ u) =
    1.56 +        if Pair_pat k i (t $ u) then incr_boundvars k arg
    1.57 +        else (subst arg k i t $ subst arg k i u)
    1.58 +    | subst arg k i t = t;
    1.59 +  fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) =
    1.60          (case split_pat beta_term_pat 1 t of
    1.61 -        SOME (i,f) => SOME (metaeq ss s (subst arg 0 i f))
    1.62 +          SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
    1.63          | NONE => NONE)
    1.64 -  |   beta_proc _ _ = NONE;
    1.65 -  fun eta_proc ss (s as Const ("split", _) $ Abs (_, _, t)) =
    1.66 +    | beta_proc _ _ = NONE;
    1.67 +  fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) =
    1.68          (case split_pat eta_term_pat 1 t of
    1.69 -          SOME (_,ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
    1.70 +          SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
    1.71          | NONE => NONE)
    1.72 -  |   eta_proc _ _ = NONE;
    1.73 +    | eta_proc _ _ = NONE;
    1.74  in
    1.75    val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
    1.76    val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
    1.77 @@ -565,11 +565,11 @@
    1.78  
    1.79  ML {*
    1.80  local (* filtering with exists_p_split is an essential optimization *)
    1.81 -  fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true
    1.82 +  fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
    1.83      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
    1.84      | exists_p_split (Abs (_, _, t)) = exists_p_split t
    1.85      | exists_p_split _ = false;
    1.86 -  val ss = HOL_basic_ss addsimps [thm "split_conv"];
    1.87 +  val ss = HOL_basic_ss addsimps @{thms split_conv};
    1.88  in
    1.89  val split_conv_tac = SUBGOAL (fn (t, i) =>
    1.90      if exists_p_split t then safe_full_simp_tac ss i else no_tac);
    1.91 @@ -634,10 +634,11 @@
    1.92  lemma internal_split_conv: "internal_split c (a, b) = c a b"
    1.93    by (simp only: internal_split_def split_conv)
    1.94  
    1.95 +use "Tools/split_rule.ML"
    1.96 +setup SplitRule.setup
    1.97 +
    1.98  hide const internal_split
    1.99  
   1.100 -use "Tools/split_rule.ML"
   1.101 -setup SplitRule.setup
   1.102  
   1.103  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
   1.104  
   1.105 @@ -1049,7 +1050,6 @@
   1.106    "Pair"    ("(_,/ _)")
   1.107  
   1.108  setup {*
   1.109 -
   1.110  let
   1.111  
   1.112  fun strip_abs_split 0 t = ([], t)
   1.113 @@ -1058,16 +1058,18 @@
   1.114          val s' = Codegen.new_name t s;
   1.115          val v = Free (s', T)
   1.116        in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
   1.117 -  | strip_abs_split i (u as Const ("split", _) $ t) = (case strip_abs_split (i+1) t of
   1.118 +  | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
   1.119 +      (case strip_abs_split (i+1) t of
   1.120          (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
   1.121        | _ => ([], u))
   1.122    | strip_abs_split i t =
   1.123        strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
   1.124  
   1.125 -fun let_codegen thy defs dep thyname brack t gr = (case strip_comb t of
   1.126 -    (t1 as Const ("Let", _), t2 :: t3 :: ts) =>
   1.127 +fun let_codegen thy defs dep thyname brack t gr =
   1.128 +  (case strip_comb t of
   1.129 +    (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
   1.130      let
   1.131 -      fun dest_let (l as Const ("Let", _) $ t $ u) =
   1.132 +      fun dest_let (l as Const (@{const_name Let}, _) $ t $ u) =
   1.133            (case strip_abs_split 1 u of
   1.134               ([p], u') => apfst (cons (p, t)) (dest_let u')
   1.135             | _ => ([], l))
   1.136 @@ -1098,7 +1100,7 @@
   1.137    | _ => NONE);
   1.138  
   1.139  fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
   1.140 -    (t1 as Const ("split", _), t2 :: ts) =>
   1.141 +    (t1 as Const (@{const_name split}, _), t2 :: ts) =>
   1.142        let
   1.143          val ([p], u) = strip_abs_split 1 (t1 $ t2);
   1.144          val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;