diff -r 7a01387c47d5 -r 136fe16e726a src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100 @@ -33,6 +33,7 @@ val codeN = "code" val ctrN = "ctr" val discN = "disc" +val disc_iffN = "disc_iff" val excludeN = "exclude" val nchotomyN = "nchotomy" val selN = "sel" @@ -68,6 +69,7 @@ calls: corec_call list, discI: thm, sel_thms: thm list, + disc_excludess: thm list list, collapse: thm, corec_thm: thm, disc_corec: thm, @@ -92,6 +94,7 @@ val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True}; val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False}; +val mk_dnf = mk_disjs o map mk_conjs; val conjuncts_s = filter_out (curry (op =) @{const True}) o HOLogic.conjuncts; @@ -411,31 +414,28 @@ else No_Corec) g_i | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i'); - fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm - disc_corec sel_corecs = + fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms disc_excludess collapse + corec_thm disc_corec sel_corecs = let val nullary = not (can dest_funT (fastype_of ctr)) in - {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho, + {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io, calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms, - collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec, - sel_corecs = sel_corecs} + disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm, + disc_corec = disc_corec, sel_corecs = sel_corecs} end; - fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss coiter_thmsss - disc_coitersss sel_coiterssss = + fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss + sel_coiterssss = let - val ctrs = #ctrs (nth ctr_sugars index); - val discs = #discs (nth ctr_sugars index); - val selss = #selss (nth ctr_sugars index); + val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar = + nth ctr_sugars index; val p_ios = map SOME p_is @ [NONE]; val discIs = #discIs (nth ctr_sugars index); - val sel_thmss = #sel_thmss (nth ctr_sugars index); - val collapses = #collapses (nth ctr_sugars index); val corec_thms = co_rec_of (nth coiter_thmsss index); val disc_corecs = co_rec_of (nth disc_coitersss index); val sel_corecss = co_rec_of (nth sel_coiterssss index); in - map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses - corec_thms disc_corecs sel_corecss + map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss + disc_excludesss collapses corec_thms disc_corecs sel_corecss end; fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, @@ -471,7 +471,7 @@ fun_T: typ, fun_args: term list, ctr: term, - ctr_no: int, (*###*) + ctr_no: int, (*FIXME*) disc: term, prems: term list, auto_gen: bool, @@ -838,6 +838,9 @@ |> K |> nth_map sel_no |> AList.map_entry (op =) ctr end; +fun applied_fun_of fun_name fun_T fun_args = + list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); + fun add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy = let val thy = Proof_Context.theory_of lthy; @@ -877,7 +880,7 @@ strong_coinduct_thms), lthy') = corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy; val actual_nn = length bs; - val corec_specs = take actual_nn corec_specs'; (*###*) + val corec_specs = take actual_nn corec_specs'; (*FIXME*) val ctr_specss = map #ctr_specs corec_specs; val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data @@ -908,8 +911,9 @@ space_implode "\n \ " (maps (map (Syntax.string_of_term lthy o snd)) excludess')); *) - val excludess'' = excludess' |> map (map (fn (idx, t) => - (idx, (Option.map (Goal.prove lthy [] [] t #> Thm.close_derivation) (exclude_tac idx), t)))); + val excludess'' = excludess' |> map (map (fn (idx, goal) => + (idx, (Option.map (Goal.prove lthy [] [] goal #> Thm.close_derivation) (exclude_tac idx), + goal)))); val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess''; val (goal_idxss, goalss') = excludess'' |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd)) @@ -920,13 +924,13 @@ val nchotomy_goals = if exhaustive then - map (HOLogic.mk_Trueprop o mk_disjs o map (mk_conjs o #prems)) disc_eqnss - |> list_all_fun_args + map (HOLogic.mk_Trueprop o mk_dnf o map #prems) disc_eqnss |> list_all_fun_args else []; val nchotomy_taut_thms = if exhaustive andalso is_some maybe_tac then - map (fn t => Goal.prove lthy [] [] t (the maybe_tac) |> Thm.close_derivation) nchotomy_goals + map (fn goal => Goal.prove lthy [] [] goal (the maybe_tac) |> Thm.close_derivation) + nchotomy_goals else []; val goalss = @@ -973,22 +977,24 @@ [] else let - val {disc_corec, ...} = nth ctr_specs ctr_no; + val {disc, disc_corec, ...} = nth ctr_specs ctr_no; val k = 1 + ctr_no; val m = length prems; - val t = - list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)) - |> curry betapply (#disc (nth ctr_specs ctr_no)) (*###*) + val goal = + applied_fun_of fun_name fun_T fun_args + |> curry betapply disc |> HOLogic.mk_Trueprop |> 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 excludesss - |> K |> Goal.prove lthy [] [] t - |> Thm.close_derivation - |> pair (#disc (nth ctr_specs ctr_no)) - |> single + if prems = [@{term False}] then + [] + else + mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss + |> K |> Goal.prove lthy [] [] goal + |> Thm.close_derivation + |> pair (#disc (nth ctr_specs ctr_no)) + |> single end; fun prove_sel ({nested_map_idents, nested_map_comps, ctr_specs, ...} : corec_spec) @@ -998,13 +1004,13 @@ val SOME ctr_spec = find_first (equal ctr o #ctr) ctr_specs; val ctr_no = find_index (equal ctr o #ctr) ctr_specs; val prems = the_default (maps (s_not_conj o #prems) disc_eqns) - (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems); + (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems); val sel_corec = find_index (equal sel) (#sels ctr_spec) |> nth (#sel_corecs ctr_spec); val k = 1 + ctr_no; val m = length prems; - val t = - list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)) + val goal = + applied_fun_of fun_name fun_T fun_args |> curry betapply sel |> rpair (abstract (List.rev fun_args) rhs_term) |> HOLogic.mk_Trueprop o HOLogic.mk_eq @@ -1014,7 +1020,7 @@ in mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_map_idents nested_map_comps sel_corec k m excludesss - |> K |> Goal.prove lthy [] [] t + |> K |> Goal.prove lthy [] [] goal |> Thm.close_derivation |> pair sel end; @@ -1037,14 +1043,15 @@ ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #maybe_ctr_rhs x)) |> the o merge_options; val m = length prems; - 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 + val goal = + (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 mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args) |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) |> curry Logic.list_all (map dest_Free fun_args); val maybe_disc_thm = AList.lookup (op =) disc_alist disc; @@ -1052,7 +1059,7 @@ in 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 + |> K |> Goal.prove lthy [] [] goal |> Thm.close_derivation |> pair ctr |> single @@ -1073,8 +1080,7 @@ let val bound_Ts = List.rev (map fastype_of fun_args); - val lhs = - list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); + val lhs = applied_fun_of fun_name fun_T fun_args; val maybe_rhs_info = (case maybe_rhs of SOME rhs => @@ -1101,21 +1107,22 @@ SOME (prems, t) end; val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; + fun is_syntactically_exhaustive () = + forall null (map_filter (try (fst o the)) maybe_ctr_conds_argss) + orelse forall is_some maybe_ctr_conds_argss + andalso exists #auto_gen disc_eqns in let - val rhs = (if exhaustive - orelse map_filter (try (fst o the)) maybe_ctr_conds_argss - |> forall (equal []) - orelse forall is_some maybe_ctr_conds_argss - andalso exists #auto_gen disc_eqns then - split_last (map_filter I maybe_ctr_conds_argss) ||> snd - else - Const (@{const_name Code.abort}, @{typ String.literal} --> - (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ - HOLogic.mk_literal fun_name $ - absdummy @{typ unit} (incr_boundvars 1 lhs) - |> pair (map_filter I maybe_ctr_conds_argss)) - |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u) + val rhs = + (if exhaustive orelse is_syntactically_exhaustive () then + split_last (map_filter I maybe_ctr_conds_argss) ||> snd + else + Const (@{const_name Code.abort}, @{typ String.literal} --> + (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ + HOLogic.mk_literal fun_name $ + absdummy @{typ unit} (incr_boundvars 1 lhs) + |> pair (map_filter I maybe_ctr_conds_argss)) + |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u) in SOME (rhs, rhs, map snd ctr_alist) end end); in @@ -1124,22 +1131,19 @@ | SOME (rhs, raw_rhs, ctr_thms) => let val ms = map (Logic.count_prems o prop_of) ctr_thms; - val (raw_t, t) = (raw_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 + val (raw_goal, goal) = (raw_rhs, rhs) + |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args) #> curry Logic.list_all (map dest_Free fun_args)); val (distincts, discIs, sel_splits, sel_split_asms) = case_thms_of_term lthy bound_Ts raw_rhs; val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits sel_split_asms ms ctr_thms maybe_nchotomy - |> K |> Goal.prove lthy [] [] raw_t + |> K |> Goal.prove lthy [] [] raw_goal |> Thm.close_derivation; in mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm - |> K |> Goal.prove lthy [] [] t + |> K |> Goal.prove lthy [] [] goal |> Thm.close_derivation |> single end) @@ -1151,6 +1155,32 @@ val disc_thmss = map (map snd) disc_alists; val sel_thmss = map (map snd) sel_alists; + fun prove_disc_iff ({ctr_specs, ...} : corec_spec) maybe_exhaust_thm discs + ({fun_name, fun_T, fun_args, ctr_no, prems, ...} : coeqn_data_disc) = + if null discs orelse is_none maybe_exhaust_thm then + [] + else + let + val {disc, disc_excludess, ...} = nth ctr_specs ctr_no; + val m = length prems; + val goal = + mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args |> curry betapply disc, + mk_conjs prems) + |> curry Logic.list_all (map dest_Free fun_args); + in + if prems = [@{term False}] then + [] + else + mk_primcorec_disc_iff_tac lthy (ctr_no + 1) (the maybe_exhaust_thm) discs + disc_excludess + |> K |> Goal.prove lthy [] [] goal + |> Thm.close_derivation + |> single + end; + + val disc_iff_thmss = map4 (maps ooo prove_disc_iff) corec_specs maybe_exhaust_thms + disc_thmss disc_eqnss; + val ctr_alists = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss ctr_specss; val ctr_thmss = map (map snd) ctr_alists; @@ -1167,6 +1197,7 @@ (codeN, code_thmss, code_nitpicksimp_attrs), (ctrN, ctr_thmss, []), (discN, disc_thmss, simp_attrs), + (disc_iffN, disc_iff_thmss, []), (excludeN, exclude_thmss, []), (exhaustN, map the_list maybe_exhaust_thms, []), (nchotomyN, map the_list maybe_nchotomy_thms, []),