# HG changeset patch # User wenzelm # Date 1399304935 -7200 # Node ID 1902d7c260174b6fccd175e183934ef0bfe5c2e1 # Parent bc50d5e04e902add478c7fa5c25133ddb37807cb# Parent 6e26ae897badccf581b32aed33269d9e578a4892 merged diff -r 6e26ae897bad -r 1902d7c26017 src/HOL/SMT_Examples/SMT_Tests.thy --- a/src/HOL/SMT_Examples/SMT_Tests.thy Mon May 05 17:27:42 2014 +0200 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Mon May 05 17:48:55 2014 +0200 @@ -731,7 +731,7 @@ "p = \ cx = 3, cy = 4, black = True \ \ p \ black := True \ \ cx := 3 \ \ cy := 4 \ = p" using point.simps bw_point.simps - by smt+ (* FIXME: bad Z3-4.3.x proof with smt2 *) + by smt+ (* smt2 FIXME: bad Z3 4.3.x proof *) lemma "\ cx = 3, cy = 4, black = b \ \ black := w \ = \ cx = 3, cy = 4, black = w \" diff -r 6e26ae897bad -r 1902d7c26017 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon May 05 17:27:42 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon May 05 17:48:55 2014 +0200 @@ -78,6 +78,7 @@ type corec_spec = {corec: term, disc_exhausts: thm list, + sel_defs: thm list, nested_maps: thm list, nested_map_idents: thm list, nested_map_comps: thm list, @@ -459,12 +460,11 @@ disc_excludesss collapses corec_thms disc_corecs sel_corecss end; - fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_rec = corec, + fun mk_spec ({T, ctr_sugar as {disc_exhausts, sel_defs, ...}, co_rec = corec, co_rec_thms = corec_thms, disc_co_recs = disc_corecs, sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = - {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, - disc_exhausts = disc_exhausts, - nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs, + {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts, + sel_defs = sel_defs, nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs, nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs, nested_map_comps = map map_comp_of_bnf nested_bnfs, ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs @@ -786,7 +786,9 @@ fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list) ({fun_args, ctr_no, prems, ...} : coeqn_data_disc) = - if is_none (#pred (nth ctr_specs ctr_no)) then I else + if is_none (#pred (nth ctr_specs ctr_no)) then + I + else s_conjs prems |> curry subst_bounds (List.rev fun_args) |> abs_tuple_balanced fun_args @@ -1171,9 +1173,10 @@ |> single end; - fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...} + fun prove_sel ({sel_defs, nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...} : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss - ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, eqn_pos, ...} : coeqn_data_sel) = + ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, code_rhs_opt, eqn_pos, ...} + : coeqn_data_sel) = let val SOME ctr_spec = find_first (curry (op =) ctr o #ctr) ctr_specs; val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs; @@ -1196,12 +1199,14 @@ nested_map_idents nested_map_comps sel_corec k m excludesss |> K |> Goal.prove_sorry lthy [] [] goal |> Thm.close_derivation + |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*) |> pair sel |> pair eqn_pos end; - fun prove_ctr disc_alist sel_alist (disc_eqns : coeqn_data_disc list) - (sel_eqns : coeqn_data_sel list) ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) = + fun prove_ctr disc_alist sel_alist ({sel_defs, ...} : corec_spec) + (disc_eqns : coeqn_data_disc list) (sel_eqns : coeqn_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 (curry (op =) ctr o #ctr) disc_eqns) andalso not (exists (curry (op =) ctr o #ctr) sel_eqns) @@ -1212,17 +1217,17 @@ [] else let - val (fun_name, fun_T, fun_args, prems, rhs_opt, eqn_pos) = + val (fun_name, fun_T, fun_args, prems, ctr_rhs_opt, code_rhs_opt, eqn_pos) = (find_first (curry (op =) ctr o #ctr) disc_eqns, find_first (curry (op =) ctr o #ctr) sel_eqns) |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x, - #ctr_rhs_opt x, #eqn_pos x)) - ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #ctr_rhs_opt x, - #eqn_pos x)) + #ctr_rhs_opt x, #code_rhs_opt x, #eqn_pos x)) + ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], + #ctr_rhs_opt x, #code_rhs_opt x, #eqn_pos x)) |> the o merge_options; val m = length prems; val goal = - (case rhs_opt of + (case ctr_rhs_opt of SOME rhs => rhs | NONE => filter (curry (op =) ctr o #ctr) sel_eqns @@ -1233,11 +1238,14 @@ |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) |> curry Logic.list_all (map dest_Free fun_args); val disc_thm_opt = AList.lookup (op =) disc_alist disc; - val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist); + val sel_thms = map (snd o snd) (filter (member (op =) sels o fst) sel_alist); in - if prems = [@{term False}] then [] else + if prems = [@{term False}] then + [] + else mk_primcorec_ctr_tac lthy m collapse disc_thm_opt sel_thms |> K |> Goal.prove_sorry lthy [] [] goal + |> is_some code_rhs_opt ? fold_thms lthy sel_defs (*mildly too aggressive*) |> Thm.close_derivation |> pair ctr |> pair eqn_pos @@ -1274,7 +1282,9 @@ | NONE => let fun prove_code_ctr ({ctr, sels, ...} : corec_ctr_spec) = - if not (exists (curry (op =) ctr o fst) ctr_alist) then NONE else + if not (exists (curry (op =) ctr o fst) ctr_alist) then + NONE + else let val prems = find_first (curry (op =) ctr o #ctr) disc_eqns |> Option.map #prems |> the_default []; @@ -1337,7 +1347,7 @@ val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss; val disc_thmss = map (map snd o sort_list_duplicates o flat) disc_alistss; val disc_thmsss' = map (map (map (snd o snd))) disc_alistss; - val sel_thmss = map (map snd o sort_list_duplicates) sel_alists; + val sel_thmss = map (map (fst o snd) o sort_list_duplicates) sel_alists; fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss' (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms @@ -1366,8 +1376,8 @@ disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss |> map sort_list_duplicates; - val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists) - disc_eqnss sel_eqnss ctr_specss; + val ctr_alists = map6 (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists + (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss; val ctr_thmss' = map (map snd) ctr_alists; val ctr_thmss = map (map snd o order_list) ctr_alists; diff -r 6e26ae897bad -r 1902d7c26017 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon May 05 17:27:42 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon May 05 17:48:55 2014 +0200 @@ -136,7 +136,7 @@ val thy = Proof_Context.theory_of lthy0; val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps, - induct_thm, n2m, lthy) = + common_induct, n2m, lthy) = get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0; val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars; @@ -159,7 +159,7 @@ fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs; fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs; - val induct_thms = unpermute0 (conj_dests nn induct_thm); + val inducts = unpermute0 (conj_dests nn common_induct); val lfpTs = unpermute perm_lfpTs; val Cs = unpermute perm_Cs; @@ -198,8 +198,7 @@ nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps, ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms}; in - ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm, induct_thms), - lthy) + ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts), lthy) end; val undef_const = Const (@{const_name undefined}, dummyT); @@ -452,7 +451,7 @@ [] => () | (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", [])); - val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) = + val ((n2m, rec_specs, _, common_induct, inducts), lthy) = rec_specs_of bs arg_Ts res_Ts frees callssss lthy0; val actual_nn = length funs_data; @@ -493,8 +492,7 @@ val notes = (if n2m then - map2 (fn name => fn thm => (name, inductN, [thm], [])) fun_names - (take actual_nn induct_thms) + map2 (fn name => fn thm => (name, inductN, [thm], [])) fun_names (take actual_nn inducts) else []) |> map (fn (prefix, thmN, thms, attrs) => @@ -503,7 +501,7 @@ val common_name = mk_common_name fun_names; val common_notes = - (if n2m then [(inductN, [induct_thm], [])] else []) + (if n2m then [(inductN, [common_induct], [])] else []) |> map (fn (thmN, thms, attrs) => ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); in diff -r 6e26ae897bad -r 1902d7c26017 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon May 05 17:27:42 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon May 05 17:48:55 2014 +0200 @@ -29,8 +29,8 @@ fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 = let val ((missing_arg_Ts, perm0_kks, - fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), - lthy) = + fp_sugars as {nested_bnfs, common_co_inducts = [common_induct], ...} :: _, + (lfp_sugar_thms, _)), lthy) = nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0; val Ts = map #T fp_sugars; @@ -51,7 +51,7 @@ val nested_map_comps = map map_comp_of_bnf nested_bnfs; in (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, - nested_map_idents, nested_map_comps, induct_thm, is_some lfp_sugar_thms, lthy) + nested_map_idents, nested_map_comps, common_induct, is_some lfp_sugar_thms, lthy) end; exception NOT_A_MAP of term; diff -r 6e26ae897bad -r 1902d7c26017 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon May 05 17:27:42 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon May 05 17:48:55 2014 +0200 @@ -21,8 +21,10 @@ weak_case_cong: thm, split: thm, split_asm: thm, + disc_defs: thm list, disc_thmss: thm list list, discIs: thm list, + sel_defs: thm list, sel_thmss: thm list list, disc_excludesss: thm list list list, disc_exhausts: thm list, @@ -90,8 +92,10 @@ weak_case_cong: thm, split: thm, split_asm: thm, + disc_defs: thm list, disc_thmss: thm list list, discIs: thm list, + sel_defs: thm list, sel_thmss: thm list list, disc_excludesss: thm list list list, disc_exhausts: thm list, @@ -103,9 +107,9 @@ case_eq_ifs: thm list}; fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, - case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss, - disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, - case_eq_ifs} = + case_thms, case_cong, weak_case_cong, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs, + sel_thmss, disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, + sel_split_asms, case_eq_ifs} = {ctrs = map (Morphism.term phi) ctrs, casex = Morphism.term phi casex, discs = map (Morphism.term phi) discs, @@ -119,8 +123,10 @@ weak_case_cong = Morphism.thm phi weak_case_cong, split = Morphism.thm phi split, split_asm = Morphism.thm phi split_asm, + disc_defs = map (Morphism.thm phi) disc_defs, disc_thmss = map (map (Morphism.thm phi)) disc_thmss, discIs = map (Morphism.thm phi) discIs, + sel_defs = map (Morphism.thm phi) sel_defs, sel_thmss = map (map (Morphism.thm phi)) sel_thmss, disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss, disc_exhausts = map (Morphism.thm phi) disc_exhausts, @@ -692,12 +698,12 @@ (thm, asm_thm) end; - val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms, - nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms, - sel_exhaust_thms, all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms, - sel_split_asm_thms, case_eq_if_thms) = + val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss, + discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, + disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, safe_collapse_thms, + expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) = if no_discs_sels then - ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []) + ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []) else let val udiscs = map (rapp u) discs; @@ -908,10 +914,10 @@ |> Thm.close_derivation end; in - (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms, - nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, [disc_exhaust_thm], - [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm], - [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm]) + (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss, + discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, + [disc_exhaust_thm], [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, + [expand_thm], [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm]) end; val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); @@ -956,11 +962,12 @@ {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm, nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms, case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm, - split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss, - discIs = discI_thms, sel_thmss = sel_thmss, disc_excludesss = disc_exclude_thmsss, - disc_exhausts = disc_exhaust_thms, sel_exhausts = sel_exhaust_thms, - collapses = all_collapse_thms, expands = expand_thms, sel_splits = sel_split_thms, - sel_split_asms = sel_split_asm_thms, case_eq_ifs = case_eq_if_thms}; + split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs, + disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss, + disc_excludesss = disc_exclude_thmsss, disc_exhausts = disc_exhaust_thms, + sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms, + sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms, + case_eq_ifs = case_eq_if_thms}; in (ctr_sugar, lthy diff -r 6e26ae897bad -r 1902d7c26017 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Mon May 05 17:27:42 2014 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon May 05 17:48:55 2014 +0200 @@ -109,8 +109,10 @@ weak_case_cong = weak_case_cong, split = split, split_asm = split_asm, + disc_defs = [], disc_thmss = [], discIs = [], + sel_defs = [], sel_thmss = [], disc_excludesss = [], disc_exhausts = [],