src/HOL/Tools/set_comprehension_pointfree.ML
changeset 61424 c3658c18b7bc
parent 61125 4c68426800de
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -85,14 +85,14 @@
     1.4  
     1.5  fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end
     1.6    | mk_split_abs vs (Const (@{const_name Product_Type.Pair}, _) $ u $ v) t =
     1.7 -      HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t))
     1.8 +      HOLogic.mk_case_prod (mk_split_abs vs u (mk_split_abs vs v t))
     1.9    | mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
    1.10  
    1.11 -(* a variant of HOLogic.strip_psplits *)
    1.12 -val strip_psplits =
    1.13 +(* a variant of HOLogic.strip_ptupleabs *)
    1.14 +val strip_ptupleabs =
    1.15    let
    1.16      fun strip [] qs vs t = (t, rev vs, qs)
    1.17 -      | strip (p :: ps) qs vs (Const (@{const_name uncurry}, _) $ t) =
    1.18 +      | strip (p :: ps) qs vs (Const (@{const_name case_prod}, _) $ t) =
    1.19            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t
    1.20        | strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t
    1.21        | strip (_ :: ps) qs vs t = strip ps qs
    1.22 @@ -129,11 +129,11 @@
    1.23    | is_collect_atom (Atom (_, Const (@{const_name "Groups.uminus_class.uminus"}, _) $ (Const(@{const_name Collect}, _) $ _))) = true
    1.24    | is_collect_atom _ = false
    1.25  
    1.26 -fun mk_split _ [(x, T)] t = (T, Abs (x, T, t))
    1.27 -  | mk_split rT ((x, T) :: vs) t =
    1.28 +fun mk_case_prod _ [(x, T)] t = (T, Abs (x, T, t))
    1.29 +  | mk_case_prod rT ((x, T) :: vs) t =
    1.30      let
    1.31 -      val (T', t') = mk_split rT vs t
    1.32 -      val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t'))
    1.33 +      val (T', t') = mk_case_prod rT vs t
    1.34 +      val t'' = HOLogic.case_prod_const (T, T', rT) $ (Abs (x, T, t'))
    1.35      in (domain_type (fastype_of t''), t'') end
    1.36  
    1.37  fun mk_term vs t =
    1.38 @@ -151,7 +151,7 @@
    1.39    let
    1.40      val (tuple, (vs', t')) = mk_term vs t
    1.41      val T = HOLogic.mk_tupleT (map snd vs')
    1.42 -    val s = HOLogic.Collect_const T $ (snd (mk_split @{typ bool} vs' t'))
    1.43 +    val s = HOLogic.Collect_const T $ (snd (mk_case_prod @{typ bool} vs' t'))
    1.44    in
    1.45      (tuple, Atom (tuple, s))
    1.46    end
    1.47 @@ -166,7 +166,7 @@
    1.48          let
    1.49            val (tuple, (vs', x')) = mk_term vs x 
    1.50            val rT = HOLogic.dest_setT (fastype_of s)
    1.51 -          val s = mk_vimage (snd (mk_split rT vs' x')) s
    1.52 +          val s = mk_vimage (snd (mk_case_prod rT vs' x')) s
    1.53          in (tuple, Atom (tuple, s)) end)
    1.54    | mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
    1.55    | mk_atom vs t = default_atom vs t
    1.56 @@ -219,7 +219,7 @@
    1.57      val bs = map (fn b => the (AList.lookup (op =) subst b)) pat'
    1.58      val rt = term_of_pattern Ts' (Pattern bs)
    1.59      val rT = type_of_pattern Ts' (Pattern bs)
    1.60 -    val (_, f) = mk_split rT vs' rt
    1.61 +    val (_, f) = mk_case_prod rT vs' rt
    1.62    in
    1.63      mk_image f t
    1.64    end;
    1.65 @@ -269,7 +269,7 @@
    1.66    end;
    1.67  
    1.68  fun is_reordering t =
    1.69 -  let val (t', _, _) = HOLogic.strip_psplits t
    1.70 +  let val (t', _, _) = HOLogic.strip_ptupleabs t
    1.71    in forall (fn Bound _ => true) (HOLogic.strip_tuple t') end
    1.72  
    1.73  fun mk_pointfree_expr t =
    1.74 @@ -305,7 +305,7 @@
    1.75  
    1.76  (* proof tactic *)
    1.77  
    1.78 -val case_prod_distrib = @{lemma "(uncurry g x) z = uncurry (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
    1.79 +val case_prod_beta = @{lemma "case_prod g x z = case_prod (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
    1.80  
    1.81  val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
    1.82  val vimageE' =
    1.83 @@ -327,7 +327,7 @@
    1.84        ORELSE' resolve_tac ctxt @{thms arg_cong2 [OF refl, where f = "op =", OF prod.case, THEN iffD2]}
    1.85        ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
    1.86          (HOLogic.Trueprop_conv
    1.87 -          (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
    1.88 +          (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_beta)))))) ctxt)))
    1.89  
    1.90  fun elim_image_tac ctxt =
    1.91    eresolve_tac ctxt @{thms imageE}
    1.92 @@ -421,7 +421,7 @@
    1.93      fun mk_term t =
    1.94        let
    1.95          val (T, t') = dest_Collect t
    1.96 -        val (t'', vs, fp) = case strip_psplits t' of
    1.97 +        val (t'', vs, fp) = case strip_ptupleabs t' of
    1.98              (_, [_], _) => raise TERM("mk_term", [t'])
    1.99            | (t'', vs, fp) => (t'', vs, fp)
   1.100          val Ts = map snd vs