use balanced tuples in 'primcorec'
authorblanchet
Fri Mar 07 14:21:15 2014 +0100 (2014-03-07)
changeset 559698820ddb8f9f4
parent 55968 94242fa87638
child 55970 6d123f0ae358
use balanced tuples in 'primcorec'
src/HOL/String.thy
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
     1.1 --- a/src/HOL/String.thy	Fri Mar 07 14:21:15 2014 +0100
     1.2 +++ b/src/HOL/String.thy	Fri Mar 07 14:21:15 2014 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Character and string types *}
     1.5  
     1.6  theory String
     1.7 -imports List Enum
     1.8 +imports Enum
     1.9  begin
    1.10  
    1.11  subsection {* Characters and strings *}
    1.12 @@ -443,4 +443,3 @@
    1.13  hide_type (open) literal
    1.14  
    1.15  end
    1.16 -
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 14:21:15 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 14:21:15 2014 +0100
     2.3 @@ -128,6 +128,7 @@
     2.4    val split_conj_prems: int -> thm -> thm
     2.5  
     2.6    val mk_sumTN: typ list -> typ
     2.7 +  val mk_tupleT_balanced: typ list -> typ
     2.8    val mk_sumprodT_balanced: typ list list -> typ
     2.9  
    2.10    val mk_proj: typ -> int -> int -> term
    2.11 @@ -136,6 +137,8 @@
    2.12  
    2.13    val Inl_const: typ -> typ -> term
    2.14    val Inr_const: typ -> typ -> term
    2.15 +  val mk_tuple_balanced: term list -> term
    2.16 +  val mk_tuple1_balanced: typ list -> term list -> term
    2.17  
    2.18    val mk_case_sum: term * term -> term
    2.19    val mk_case_sumN: term list -> term
    2.20 @@ -373,8 +376,13 @@
    2.21  fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
    2.22  fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
    2.23  
    2.24 -fun mk_tuple_balanced [] = HOLogic.unit
    2.25 -  | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts;
    2.26 +fun mk_prod1 bound_Ts (t, u) =
    2.27 +  HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
    2.28 +
    2.29 +fun mk_tuple1_balanced _ [] = HOLogic.unit
    2.30 +  | mk_tuple1_balanced bound_Ts ts = Balanced_Tree.make (mk_prod1 bound_Ts) ts;
    2.31 +
    2.32 +val mk_tuple_balanced = mk_tuple1_balanced [];
    2.33  
    2.34  fun mk_absumprod absT abs0 n k ts =
    2.35    let val abs = mk_abs absT abs0;
     3.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Mar 07 14:21:15 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Mar 07 14:21:15 2014 +0100
     3.3 @@ -477,7 +477,7 @@
     3.4  
     3.5  val undef_const = Const (@{const_name undefined}, dummyT);
     3.6  
     3.7 -val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
     3.8 +val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;
     3.9  
    3.10  fun abstract vs =
    3.11    let
    3.12 @@ -489,10 +489,6 @@
    3.13          end;
    3.14    in abs 0 end;
    3.15  
    3.16 -fun mk_prod1 bound_Ts (t, u) =
    3.17 -  HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
    3.18 -fun mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts));
    3.19 -
    3.20  type coeqn_data_disc = {
    3.21    fun_name: string,
    3.22    fun_T: typ,
    3.23 @@ -734,12 +730,12 @@
    3.24    if is_none (#pred (nth ctr_specs ctr_no)) then I else
    3.25      s_conjs prems
    3.26      |> curry subst_bounds (List.rev fun_args)
    3.27 -    |> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args)
    3.28 +    |> abs_tuple_balanced fun_args
    3.29      |> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
    3.30  
    3.31  fun build_corec_arg_no_call (sel_eqns : coeqn_data_sel list) sel =
    3.32    find_first (curry (op =) sel o #sel) sel_eqns
    3.33 -  |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple fun_args rhs_term)
    3.34 +  |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple_balanced fun_args rhs_term)
    3.35    |> the_default undef_const
    3.36    |> K;
    3.37  
    3.38 @@ -752,9 +748,9 @@
    3.39        fun rewrite_stop _ t = if has_call t then @{term False} else @{term True};
    3.40        fun rewrite_end _ t = if has_call t then undef_const else t;
    3.41        fun rewrite_cont bound_Ts t =
    3.42 -        if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const;
    3.43 +        if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const;
    3.44        fun massage f _ = massage_let_if_case lthy has_call f bound_Ts rhs_term
    3.45 -        |> abs_tuple fun_args;
    3.46 +        |> abs_tuple_balanced fun_args;
    3.47      in
    3.48        (massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
    3.49      end);
    3.50 @@ -770,7 +766,7 @@
    3.51              | rewrite bound_Ts (t as _ $ _) =
    3.52                let val (u, vs) = strip_comb t in
    3.53                  if is_Free u andalso has_call u then
    3.54 -                  Inr_const U T $ mk_tuple1 bound_Ts vs
    3.55 +                  Inr_const U T $ mk_tuple1_balanced bound_Ts vs
    3.56                  else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
    3.57                    map (rewrite bound_Ts) vs |> chop 1
    3.58                    |>> HOLogic.mk_split o the_single
    3.59 @@ -789,7 +785,7 @@
    3.60        fun build t =
    3.61          rhs_term
    3.62          |> massage_nested_corec_call lthy has_call massage bound_Ts (range_type (fastype_of t))
    3.63 -        |> abs_tuple fun_args;
    3.64 +        |> abs_tuple_balanced fun_args;
    3.65      in
    3.66        build
    3.67      end);
    3.68 @@ -827,7 +823,7 @@
    3.69        |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
    3.70        |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;
    3.71      fun currys [] t = t
    3.72 -      | currys Ts t = t $ mk_tuple1 (List.rev Ts) (map Bound (length Ts - 1 downto 0))
    3.73 +      | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
    3.74            |> fold_rev (Term.abs o pair Name.uu) Ts;
    3.75  
    3.76  (*
    3.77 @@ -907,7 +903,7 @@
    3.78      val thy = Proof_Context.theory_of lthy;
    3.79  
    3.80      val (bs, mxs) = map_split (apfst fst) fixes;
    3.81 -    val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
    3.82 +    val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
    3.83  
    3.84      val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
    3.85          [] => ()