# HG changeset patch # User blanchet # Date 1436471956 -7200 # Node ID fdd965b35bcd52897e7f2877a653a1e54bcd12ef # Parent 8963331cc0de3beca9c031bcf9d53d5766e90406 tuned ML signature (and rationalized code a bit) diff -r 8963331cc0de -r fdd965b35bcd src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Jul 09 17:36:04 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Jul 09 21:59:16 2015 +0200 @@ -44,8 +44,19 @@ fp_nesting_map_comps: thm list, ctr_specs: corec_ctr_spec list} + val abstract_over_list: term list -> term -> term val abs_tuple_balanced: term list -> term -> term + val mk_conjs: term list -> term + val mk_disjs: term list -> term + val mk_dnf: term list list -> term + val conjuncts_s: term -> term list + val s_not: term -> term + val s_not_conj: term list -> term list + val s_conjs: term list -> term + val s_disjs: term list -> term + val s_dnf: term list list -> term list + val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list -> term -> 'a -> 'a val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) -> @@ -161,8 +172,25 @@ exception NO_MAP of term; +fun abstract_over_list rev_vs = + let + val vs = rev rev_vs; + + fun abs n (t $ u) = abs n t $ abs n u + | abs n (Abs (s, T, t)) = Abs (s, T, abs (n + 1) t) + | abs n t = + let val j = find_index (curry (op =) t) vs in + if j < 0 then t else Bound (n + j) + end; + in + abs 0 + end; + val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced; +fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = + Ts ---> T; + fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs); val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True}; @@ -308,8 +336,6 @@ fun massage_let_if_case_corec ctxt has_call massage_leaf bound_Ts t0 = massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call ctxt [t0])) bound_Ts t0; -fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T; - fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 = let fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else (); @@ -562,16 +588,6 @@ val undef_const = Const (@{const_name undefined}, dummyT); -fun abstract vs = - let - fun abs n (t $ u) = abs n t $ abs n u - | abs n (Abs (s, T, t)) = Abs (s, T, abs (n + 1) t) - | abs n t = - let val j = find_index (curry (op =) t) vs in - if j < 0 then t else Bound (n + j) - end; - in abs 0 end; - type coeqn_data_disc = {fun_name: string, fun_T: typ, @@ -687,7 +703,7 @@ if exists is_catch_all_prem prems0 then error_at ctxt [concl] "Superfluous premises" else false); val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default []; - val prems = map (abstract (List.rev fun_args)) prems0; + val prems = map (abstract_over_list fun_args) prems0; val actual_prems = (if catch_all orelse sequential then maps s_not_conj matchedss else []) @ (if catch_all then [] else prems); @@ -697,7 +713,7 @@ val user_eqn = (actual_prems, concl) - |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract (List.rev fun_args) + |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract_over_list fun_args |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies; val _ = check_extra_frees ctxt fun_args fun_names user_eqn; @@ -755,7 +771,7 @@ (NONE, matchedsss) else apfst SOME (dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos - (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss); + (SOME (abstract_over_list fun_args rhs)) code_rhs_opt prems disc_concl matchedsss); val sel_concls = sels ~~ ctr_args |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)) @@ -764,7 +780,8 @@ val eqns_data_sel = map (dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos - (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls; + (SOME (abstract_over_list fun_args rhs)) code_rhs_opt eqn0 (SOME ctr)) + sel_concls; in (the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss') end; @@ -798,7 +815,7 @@ val sequentials = replicate (length fun_names) false; in @{fold_map 2} (dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0 - (SOME (abstract (List.rev fun_args) rhs))) + (SOME (abstract_over_list fun_args rhs))) ctr_premss ctr_concls matchedsss end; @@ -920,14 +937,14 @@ rewrite bound_Ts t0 end; - fun massage_noncall bound_Ts U T t = + fun massage_noncall U T t = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t; val bound_Ts = List.rev (map fastype_of fun_args); in fn t => rhs_term - |> massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts + |> massage_nested_corec_call ctxt has_call massage_call (K massage_noncall) bound_Ts (range_type (fastype_of t)) (fastype_of1 (bound_Ts, rhs_term)) |> abs_tuple_balanced fun_args end); @@ -1271,7 +1288,7 @@ val goal = applied_fun_of fun_name fun_T fun_args |> curry betapply sel - |> rpair (abstract (List.rev fun_args) rhs_term) + |> rpair (abstract_over_list fun_args rhs_term) |> HOLogic.mk_Trueprop o HOLogic.mk_eq |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) |> curry Logic.list_all (map dest_Free fun_args); @@ -1314,7 +1331,8 @@ | NONE => filter (curry (op =) ctr o #ctr) sel_eqns |> fst o finds (op = o apsnd #sel) sels - |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract) + |> map (snd #> (fn [x] => (#fun_args x, #rhs_term x)) + #-> abstract_over_list) |> curry Term.list_comb ctr) |> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args) |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) @@ -1373,8 +1391,8 @@ val t = filter (curry (op =) ctr o #ctr) sel_eqns |> fst o finds (op = o apsnd #sel) sels - |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) - #-> abstract) + |> map (snd #> (fn [x] => (#fun_args x, #rhs_term x)) + #-> abstract_over_list) |> curry Term.list_comb ctr; in SOME (prems, t)