# HG changeset patch # User wenzelm # Date 1400067395 -7200 # Node ID d0e04fdf4276b2d19a3541417e3a245f1fe873d4 # Parent 23a9cb098ccb6805a58420013a5e1319e1d2e3ff# Parent 9c2ca698690e284e9d4120aee9e77df4f4b654b9 merged diff -r 9c2ca698690e -r d0e04fdf4276 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed May 14 13:10:57 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed May 14 13:36:35 2014 +0200 @@ -887,6 +887,9 @@ \item[@{text "t."}\hthm{map\_id}\rm:] ~ \\ @{thm list.map_id[no_vars]} +\item[@{text "t."}\hthm{map\_id0}\rm:] ~ \\ +@{thm list.map_id0[no_vars]} + \item[@{text "t."}\hthm{map\_ident}\rm:] ~ \\ @{thm list.map_ident[no_vars]} @@ -905,6 +908,9 @@ \item[@{text "t."}\hthm{rel\_mono}\rm:] ~ \\ @{thm list.rel_mono[no_vars]} +\item[@{text "t."}\hthm{set\_empty}\rm:] ~ \\ +@{thm list.set_empty[no_vars]} + \item[@{text "t."}\hthm{set\_map}\rm:] ~ \\ @{thm list.set_map[no_vars]} diff -r 9c2ca698690e -r d0e04fdf4276 src/HOL/List.thy --- a/src/HOL/List.thy Wed May 14 13:10:57 2014 +0200 +++ b/src/HOL/List.thy Wed May 14 13:36:35 2014 +0200 @@ -3262,6 +3262,10 @@ "\ distinct xs; i < length xs; j < length xs \ \ (xs!i = xs!j) = (i = j)" by(auto simp: distinct_conv_nth) +lemma set_update_distinct: "\ distinct xs; n < length xs \ \ + set(xs[n := x]) = insert x (set xs - {xs!n})" +by(auto simp: set_eq_iff in_set_conv_nth nth_list_update nth_eq_iff_index_eq) + lemma distinct_card: "distinct xs ==> card (set xs) = size xs" by (induct xs) auto diff -r 9c2ca698690e -r d0e04fdf4276 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Wed May 14 13:10:57 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Wed May 14 13:36:35 2014 +0200 @@ -640,7 +640,6 @@ (in_relN, [Lazy.force (#in_rel facts)]), (inj_mapN, [Lazy.force (#inj_map facts)]), (map_comp0N, [#map_comp0 axioms]), - (map_id0N, [#map_id0 axioms]), (map_transferN, [Lazy.force (#map_transfer facts)]), (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), (set_map0N, #set_map0 axioms), @@ -661,6 +660,7 @@ (map_cong0N, [#map_cong0 axioms], []), (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs), (map_idN, [Lazy.force (#map_id facts)], []), + (map_id0N, [#map_id0 axioms], []), (map_identN, [Lazy.force (#map_ident facts)], []), (rel_comppN, [Lazy.force (#rel_OO facts)], []), (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []), diff -r 9c2ca698690e -r d0e04fdf4276 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed May 14 13:10:57 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed May 14 13:36:35 2014 +0200 @@ -97,6 +97,7 @@ open BNF_LFP_Size val EqN = "Eq_"; +val set_emptyN = "set_empty"; structure Data = Generic_Data ( @@ -1115,7 +1116,8 @@ free_constructors tacss ((wrap_opts, standard_binding), ctr_specs) lthy end; - fun derive_maps_sets_rels (ctr_sugar as {case_cong, ...} : ctr_sugar, lthy) = + fun derive_maps_sets_rels + (ctr_sugar as {case_cong, discs, ctrs, exhaust, disc_thmss, ...} : ctr_sugar, lthy) = if live = 0 then ((([], [], [], []), ctr_sugar), lthy) else @@ -1164,6 +1166,36 @@ val set_thmss = map mk_set_thms fp_set_thms; val set_thms = flat set_thmss; + fun mk_set t = + let + val Type (_, Ts0) = domain_type (fastype_of t); + val Type (_, Ts) = fpT; + in + Term.subst_atomic_types (Ts0 ~~ Ts) t + end; + + val sets = map mk_set (sets_of_bnf fp_bnf); + val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o + binder_types o fastype_of) ctrs; + val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets; + val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs; + fun mk_set_empty_goal disc set T = Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u), + mk_Trueprop_eq (set $ u, HOLogic.mk_set T [])); + val goals = map_filter I (flat + (map2 (fn names => fn disc => + map3 (fn name => fn setT => fn set => + if member (op =) names name then NONE + else SOME (mk_set_empty_goal disc set setT)) + setT_names setTs sets) + ctr_argT_namess discs)); + + val set_empty_thms = if null goals then [] + else Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, prems = _} => + mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss)) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy; + val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); fun mk_rel_thm postproc ctr_defs' cxIn cyIn = @@ -1208,7 +1240,8 @@ [(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs), (rel_distinctN, rel_distinct_thms, simp_attrs), (rel_injectN, rel_inject_thms, simp_attrs), - (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs)] + (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs), + (set_emptyN, set_empty_thms, [])] |> massage_simple_notes fp_b_name; in (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar), diff -r 9c2ca698690e -r d0e04fdf4276 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed May 14 13:10:57 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed May 14 13:36:35 2014 +0200 @@ -25,6 +25,7 @@ val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic + val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic end; structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS = @@ -191,4 +192,12 @@ (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss selsss)); +fun mk_set_empty_tac ctxt ct exhaust sets discs = + TRYALL Goal.conjunction_tac THEN + ALLGOALS(rtac (Ctr_Sugar_Util.cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW + hyp_subst_tac ctxt) THEN + Local_Defs.unfold_tac ctxt (sets @ map_filter (fn thm => + SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN + ALLGOALS(rtac refl ORELSE' etac FalseE); + end;