--- 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 = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = 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
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
--- 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;
--- 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
--- 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;
--- 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
--- 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 = [],