# HG changeset patch # User blanchet # Date 1387535647 -3600 # Node ID 431133d07192b33664feea768d811b280ca05142 # Parent b125539be102857b609eb7cf2f9e9c028c50aea7 note manually proved exclusiveness property diff -r b125539be102 -r 431133d07192 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Dec 20 11:12:51 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Dec 20 11:34:07 2013 +0100 @@ -34,6 +34,7 @@ val codeN = "code" val ctrN = "ctr" val discN = "disc" +val excludeN = "exclude" val selN = "sel" val nitpicksimp_attrs = @{attributes [nitpick_simp]}; @@ -784,7 +785,7 @@ space_implode "\n \ " (map (Syntax.string_of_term lthy) corec_args)); *) - val exclss' = + val excludess' = disc_eqnss |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x)) #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs []) @@ -801,7 +802,7 @@ |> Syntax.check_terms lthy |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) bs mxs - |> rpair exclss' + |> rpair excludess' end; fun mk_real_disc_eqns fun_binding arg_Ts ({ctr_specs, ...} : corec_spec) @@ -897,22 +898,22 @@ val arg_Tss = map (binder_types o snd o fst) fixes; val disc_eqnss = map5 mk_real_disc_eqns bs arg_Tss corec_specs sel_eqnss disc_eqnss'; - val (defs, exclss') = + val (defs, excludess') = build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss; - fun excl_tac (c, c', a) = + fun exclude_tac (c, c', a) = if a orelse c = c' orelse seq then SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy []))) else maybe_tac; (* val _ = tracing ("exclusiveness properties:\n \ " ^ - space_implode "\n \ " (maps (map (Syntax.string_of_term lthy o snd)) exclss')); + space_implode "\n \ " (maps (map (Syntax.string_of_term lthy o snd)) excludess')); *) - val exclss'' = exclss' |> map (map (fn (idx, t) => - (idx, (Option.map (Goal.prove lthy [] [] t #> Thm.close_derivation) (excl_tac idx), t)))); - val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss''; - val (goal_idxss, goalss') = exclss'' + val excludess'' = excludess' |> map (map (fn (idx, t) => + (idx, (Option.map (Goal.prove lthy [] [] t #> Thm.close_derivation) (exclude_tac idx), t)))); + 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)) |> split_list o map split_list; @@ -932,16 +933,17 @@ val maybe_exhaust_thms = if not exhaustive then map (K NONE) def_thms else map SOME (if is_none maybe_tac then hd thmss'' else exhaust_taut_thms); - val thmss' = if exhaustive andalso is_none maybe_tac then tl thmss'' else thmss''; + val exclude_thmss = if exhaustive andalso is_none maybe_tac then tl thmss'' else thmss''; - val exclss' = map (op ~~) (goal_idxss ~~ thmss'); - fun mk_exclsss excls n = - (excls, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1)) + val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss); + fun mk_excludesss excludes n = + (excludes, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1)) |-> fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm]))); - val exclssss = (exclss' ~~ taut_thmss |> map (op @), fun_names ~~ corec_specs) - |-> map2 (fn excls => fn (_, {ctr_specs, ...}) => mk_exclsss excls (length ctr_specs)); + val excludessss = (excludess' ~~ taut_thmss |> map (op @), fun_names ~~ corec_specs) + |-> map2 (fn excludes => fn (_, {ctr_specs, ...}) => + mk_excludesss excludes (length ctr_specs)); - fun prove_disc ({ctr_specs, ...} : corec_spec) exclsss + fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss ({fun_name, fun_T, fun_args, ctr_no, prems, ...} : coeqn_data_disc) = if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\x. x = x"}) then [] @@ -958,7 +960,7 @@ |> 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 + 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)) @@ -966,7 +968,7 @@ end; fun prove_sel ({nested_map_idents, nested_map_comps, ctr_specs, ...} : corec_spec) - (disc_eqns : coeqn_data_disc list) exclsss + (disc_eqns : coeqn_data_disc list) excludesss ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, ...} : coeqn_data_sel) = let val SOME ctr_spec = find_first (equal ctr o #ctr) ctr_specs; @@ -987,7 +989,7 @@ val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term; in mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_map_idents - nested_map_comps sel_corec k m exclsss + nested_map_comps sel_corec k m excludesss |> K |> Goal.prove lthy [] [] t |> Thm.close_derivation |> pair sel @@ -1120,8 +1122,8 @@ 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_alists = map3 (maps oo prove_disc) corec_specs excludessss disc_eqnss; + val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss; val disc_thmss = map (map snd) disc_alists; val sel_thmss = map (map snd) sel_alists; @@ -1141,6 +1143,7 @@ (codeN, code_thmss, code_nitpicksimp_attrs), (ctrN, ctr_thmss, []), (discN, disc_thmss, simp_attrs), + (excludeN, exclude_thmss, []), (exhaustN, map the_list maybe_exhaust_thms, []), (selN, sel_thmss, simp_attrs), (simpsN, simp_thmss, []),