# HG changeset patch # User panny # Date 1381501883 -7200 # Node ID 92c5bd3b342dabc19159f70333cd0b18ed10ac8f # Parent 8ab8794410cd268b7674c3e40981aace67599127 prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.; generate code-style theorems (currently commented out since this still fails for many cases); filter tautologies (False ==> ...) out of generated theorems; diff -r 8ab8794410cd -r 92c5bd3b342d src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Oct 10 08:23:57 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Oct 11 16:31:23 2013 +0200 @@ -455,6 +455,8 @@ disc: term, prems: term list, auto_gen: bool, + maybe_ctr_rhs: term option, + maybe_code_rhs: term option, user_eqn: term }; @@ -472,8 +474,8 @@ Disc of co_eqn_data_disc | Sel of co_eqn_data_sel; -fun co_dissect_eqn_disc seq fun_names (corec_specs : corec_spec list) prems' concl - matchedsss = +fun co_dissect_eqn_disc seq fun_names (corec_specs : corec_spec list) maybe_ctr_rhs maybe_code_rhs + prems' concl matchedsss = let fun find_subterm p = let (* FIXME \? *) fun f (t as u $ v) = if p t then SOME t else merge_options (f u, f v) @@ -514,9 +516,9 @@ |> cons (fun_name, if seq then matchedss @ [prems] else matchedss @ [real_prems]); val user_eqn = - (real_prems, betapply (#disc (nth ctr_specs ctr_no), applied_fun)) - |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop - |> Logic.list_implies; + (real_prems, concl) + |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract (List.rev fun_args) + |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies; in (Disc { fun_name = fun_name, @@ -527,6 +529,8 @@ disc = #disc (nth ctr_specs ctr_no), prems = real_prems, auto_gen = catch_all, + maybe_ctr_rhs = maybe_ctr_rhs, + maybe_code_rhs = maybe_code_rhs, user_eqn = user_eqn }, matchedsss') end; @@ -560,11 +564,11 @@ } end; -fun co_dissect_eqn_ctr seq fun_names (corec_specs : corec_spec list) eqn' prems concl - matchedsss = +fun co_dissect_eqn_ctr seq fun_names (corec_specs : corec_spec list) eqn' maybe_code_rhs + prems concl matchedsss = let val (lhs, rhs) = HOLogic.dest_eq concl; - val fun_name = head_of lhs |> fst o dest_Free; + val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; val {ctr_specs, ...} = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name); val (ctr, ctr_args) = strip_comb (unfold_let rhs); val {disc, sels, ...} = the (find_first (equal ctr o #ctr) ctr_specs) @@ -573,8 +577,8 @@ val disc_concl = betapply (disc, lhs); val (maybe_eqn_data_disc, matchedsss') = if length ctr_specs = 1 then (NONE, matchedsss) - else apfst SOME (co_dissect_eqn_disc - seq fun_names corec_specs prems disc_concl matchedsss); + else apfst SOME (co_dissect_eqn_disc seq fun_names corec_specs + (SOME (abstract (List.rev fun_args) rhs)) maybe_code_rhs prems disc_concl matchedsss); val sel_concls = (sels ~~ ctr_args) |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)); @@ -582,7 +586,9 @@ (* val _ = tracing ("reduced\n " ^ Syntax.string_of_term @{context} concl ^ "\nto\n \ " ^ (is_some maybe_eqn_data_disc ? K (Syntax.string_of_term @{context} disc_concl ^ "\n \ ")) "" ^ - space_implode "\n \ " (map (Syntax.string_of_term @{context}) sel_concls)); + space_implode "\n \ " (map (Syntax.string_of_term @{context}) sel_concls) ^ + "\nfor premise(s)\n \ " ^ + space_implode "\n \ " (map (Syntax.string_of_term @{context}) prems)); *) val eqns_data_sel = map (co_dissect_eqn_sel fun_names corec_specs eqn' (SOME ctr)) sel_concls; @@ -593,7 +599,7 @@ fun co_dissect_eqn_code lthy has_call fun_names corec_specs eqn' concl matchedsss = let val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs lthy has_call []); - val fun_name = head_of lhs |> fst o dest_Free; + val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; val {ctr_specs, ...} = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name); val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ => @@ -610,10 +616,12 @@ |> curry list_comb ctr |> curry HOLogic.mk_eq lhs); in - fold_map2 (co_dissect_eqn_ctr false fun_names corec_specs eqn') ctr_premss ctr_concls matchedsss + fold_map2 (co_dissect_eqn_ctr false fun_names corec_specs eqn' + (SOME (abstract (List.rev fun_args) rhs))) + ctr_premss ctr_concls matchedsss end; -fun co_dissect_eqn lthy has_call seq fun_names (corec_specs : corec_spec list) eqn' of_spec +fun co_dissect_eqn lthy seq has_call fun_names (corec_specs : corec_spec list) eqn' of_spec matchedsss = let val eqn = drop_All eqn' @@ -634,13 +642,13 @@ if member (op =) discs head orelse is_some maybe_rhs andalso member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then - co_dissect_eqn_disc seq fun_names corec_specs prems concl matchedsss + co_dissect_eqn_disc seq fun_names corec_specs NONE NONE prems concl matchedsss |>> single else if member (op =) sels head then ([co_dissect_eqn_sel fun_names corec_specs eqn' of_spec concl], matchedsss) else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso member (op =) ctrs (head_of (unfold_let (the maybe_rhs))) then - co_dissect_eqn_ctr seq fun_names corec_specs eqn' prems concl matchedsss + co_dissect_eqn_ctr seq fun_names corec_specs eqn' NONE prems concl matchedsss else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso null prems then co_dissect_eqn_code lthy has_call fun_names corec_specs eqn' concl matchedsss @@ -670,11 +678,13 @@ if is_none maybe_sel_eqn then (I, I, I) else let val {fun_args, rhs_term, ... } = the maybe_sel_eqn; + val bound_Ts = List.rev (map fastype_of fun_args); fun rewrite_q _ t = if has_call t then @{term False} else @{term True}; fun rewrite_g _ t = if has_call t then undef_const else t; fun rewrite_h bound_Ts t = if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const; - fun massage f _ = massage_direct_corec_call lthy has_call f [] rhs_term |> abs_tuple fun_args; + fun massage f _ = massage_direct_corec_call lthy has_call f bound_Ts rhs_term + |> abs_tuple fun_args; in (massage rewrite_q, massage rewrite_g, @@ -689,6 +699,7 @@ if is_none maybe_sel_eqn then I else let val {fun_args, rhs_term, ...} = the maybe_sel_eqn; + val bound_Ts = List.rev (map fastype_of fun_args); fun rewrite bound_Ts U T (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) U T b) | rewrite bound_Ts U T (t as _ $ _) = let val (u, vs) = strip_comb t in @@ -702,7 +713,8 @@ | rewrite _ U T t = if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t; fun massage t = - massage_indirect_corec_call lthy has_call rewrite [] (range_type (fastype_of t)) rhs_term + rhs_term + |> massage_indirect_corec_call lthy has_call rewrite bound_Ts (range_type (fastype_of t)) |> abs_tuple fun_args; in massage @@ -786,6 +798,8 @@ disc = #disc (nth ctr_specs n), prems = maps (s_not_conj o #prems) disc_eqns, auto_gen = true, + maybe_ctr_rhs = NONE, + maybe_code_rhs = NONE, user_eqn = undef_const}; in chop n disc_eqns ||> cons extra_disc_eqn |> (op @) @@ -808,7 +822,7 @@ val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); val eqns_data = - fold_map2 (co_dissect_eqn lthy has_call seq fun_names corec_specs) + fold_map2 (co_dissect_eqn lthy seq has_call fun_names corec_specs) (map snd specs) of_specs [] |> flat o fst; @@ -876,6 +890,7 @@ |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) |> curry Logic.list_all (map dest_Free fun_args); in + if prems = [@{term False}] then [] else mk_primcorec_disc_tac lthy def_thms disc_corec k m exclsss |> K |> Goal.prove lthy [] [] t |> pair (#disc (nth ctr_specs ctr_no)) @@ -911,24 +926,27 @@ fun prove_ctr disc_alist sel_alist (disc_eqns : co_eqn_data_disc list) (sel_eqns : co_eqn_data_sel list) ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) = + (* don't try to prove theorems when some sel_eqns are missing *) if not (exists (equal ctr o #ctr) disc_eqns) andalso not (exists (equal ctr o #ctr) sel_eqns) - orelse (* don't try to prove theorems when some sel_eqns are missing *) + orelse filter (equal ctr o #ctr) sel_eqns |> fst o finds ((op =) o apsnd #sel) sels |> exists (null o snd) then [] else let - val (fun_name, fun_T, fun_args, prems) = + val (fun_name, fun_T, fun_args, prems, maybe_rhs) = (find_first (equal ctr o #ctr) disc_eqns, find_first (equal ctr o #ctr) sel_eqns) - |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x)) - ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [])) + |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x, + #maybe_ctr_rhs x)) + ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], NONE)) |> the o merge_options; val m = length prems; - val t = filter (equal 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) - |> curry list_comb ctr + val t = (if is_some maybe_rhs then the maybe_rhs else + filter (equal 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) + |> curry list_comb ctr) |> curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0))) |> HOLogic.mk_Trueprop @@ -937,18 +955,87 @@ val maybe_disc_thm = AList.lookup (op =) disc_alist disc; val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist); in - mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms - |> K |> Goal.prove lthy [] [] t - |> single + if prems = [@{term False}] then [] else + mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms + |> K |> Goal.prove lthy [] [] t + |> pair ctr + |> single end; + fun prove_code disc_eqns sel_eqns ctr_alist + {distincts, sel_splits, sel_split_asms, ctr_specs, ...} = +(* FIXME doesn't work reliably yet *) +[](* let + val (fun_name, fun_T, fun_args, maybe_rhs) = + (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns, + find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns) + |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x)) + ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE)) + |> the o merge_options; + + val maybe_rhs' = if is_some maybe_rhs then maybe_rhs else + let + fun prove_code_ctr {ctr, disc, sels, ...} = + if not (exists (equal ctr o fst) ctr_alist) then NONE else + let + val (fun_name, fun_T, fun_args, prems) = + (find_first (equal ctr o #ctr) disc_eqns, + find_first (equal ctr o #ctr) sel_eqns) + |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x)) + ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [])) + |> the o merge_options; + val m = length prems; + val t = + filter (equal 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) + |> curry list_comb ctr; + in + SOME (prems, t) + end; + val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; + in + if exists is_none maybe_ctr_conds_argss then NONE else + fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t) + maybe_ctr_conds_argss (Const (@{const_name undefined}, body_type fun_T)) + |> SOME + end; + in + if is_none maybe_rhs' then [] else + let + val rhs = the maybe_rhs'; + val bound_Ts = List.rev (map fastype_of fun_args); + val rhs' = expand_corec_code_rhs lthy has_call bound_Ts rhs; + val cond_ctrs = fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts rhs' []; + val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs; + val ms = map (Logic.count_prems o prop_of) ctr_thms; + val (t', t) = (rhs', rhs) + |> pairself + (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T), + map Bound (length fun_args - 1 downto 0))) + #> HOLogic.mk_Trueprop + #> curry Logic.list_all (map dest_Free fun_args)); + val discIs = map #discI ctr_specs; + val raw_code = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits + sel_split_asms ms ctr_thms + |> K |> Goal.prove lthy [] [] t'; + in + mk_primcorec_code_of_raw_code_tac sel_splits raw_code + |> K |> Goal.prove lthy [] [] t + |> single + end + end;*) + val disc_alists = map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss; val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss; - val disc_thmss = map (map snd) disc_alists; val sel_thmss = map (map snd) sel_alists; - val ctr_thmss = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss + + val ctr_alists = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss (map #ctr_specs corec_specs); + val ctr_thmss = map (map snd) ctr_alists; + + val code_thmss = map4 prove_code disc_eqnss sel_eqnss ctr_alists corec_specs; val simp_thmss = map2 append disc_thmss sel_thmss @@ -956,7 +1043,7 @@ val notes = [(coinductN, map (if n2m then single else K []) coinduct_thms, []), - (codeN, ctr_thmss(*FIXME*), code_nitpick_attrs), + (codeN, code_thmss, code_nitpick_attrs), (ctrN, ctr_thmss, []), (discN, disc_thmss, simp_attrs), (selN, sel_thmss, simp_attrs), diff -r 8ab8794410cd -r 92c5bd3b342d src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Oct 10 08:23:57 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Oct 11 16:31:23 2013 +0200 @@ -49,6 +49,9 @@ nested_maps: thm list, nested_map_idents: thm list, nested_map_comps: thm list, + distincts: thm list, + sel_splits: thm list, + sel_split_asms: thm list, ctr_specs: corec_ctr_spec list} val s_not: term -> term @@ -131,6 +134,9 @@ nested_maps: thm list, nested_map_idents: thm list, nested_map_comps: thm list, + distincts: thm list, + sel_splits: thm list, + sel_split_asms: thm list, ctr_specs: corec_ctr_spec list}; val id_def = @{thm id_def}; @@ -295,6 +301,8 @@ fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else (); + fun beta_contract (t as Abs (_, T, f $ Bound 0)) = incr_boundvars ~1 f + | beta_contract (t as Abs (v, T, b)) = Abs (v, T, beta_contract b); fun massage_abs bound_Ts (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) t) | massage_abs bound_Ts t = massage_rec bound_Ts t and massage_rec bound_Ts t = @@ -306,11 +314,12 @@ let val branches' = map (massage_rec bound_Ts) branches in Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches') end - | (Const (c, _), args as _ :: _ :: _) => + | (Const (c, c_T), args as _ :: _ :: _) => let val gen_T = Sign.the_const_type thy c; val (gen_branch_Ts, gen_body_fun_T) = strip_fun_type gen_T; val n = length gen_branch_Ts; + val n_res_T = strip_typeN n c_T |> length o binder_types o snd; in if n < length args then (case gen_body_fun_T of @@ -318,7 +327,8 @@ if case_of ctxt T_name = SOME c then let val (branches, obj_leftovers) = chop n args; - val branches' = map (massage_abs bound_Ts o Envir.eta_long bound_Ts) branches; + val branches' = map (massage_abs bound_Ts o funpow (n_res_T - 1) beta_contract o + Envir.eta_long bound_Ts) branches; val branch_Ts' = map typof branches'; val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> snd (strip_typeN (num_binder_types (hd gen_branch_Ts)) (hd branch_Ts'))); @@ -648,6 +658,9 @@ nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs, nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs, nested_map_comps = map map_comp_of_bnf nested_bnfs, + distincts = #distincts (nth ctr_sugars index), + sel_splits = #sel_splits (nth ctr_sugars index), + sel_split_asms = #sel_split_asms (nth ctr_sugars index), ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss sel_coiterssss}; in