# HG changeset patch # User desharna # Date 1406710228 -7200 # Node ID a2c4adb839a998a8c48b275905d2ee552e675ccb # Parent a6cf197c1f1e18063d7e2ba0128bb8f2cfd4cf6c generate 'set_induct' theorem for codatatypes diff -r a6cf197c1f1e -r a2c4adb839a9 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 30 00:50:41 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 30 10:50:28 2014 +0200 @@ -103,6 +103,7 @@ val sel_mapN = "sel_map"; val sel_setN = "sel_set"; val set_emptyN = "set_empty"; +val set_inductN = "set_induct"; structure Data = Generic_Data ( @@ -112,10 +113,16 @@ fun merge data : T = Symtab.merge (K true) data; ); -fun choose_relator Rs AB = find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) Rs; -fun build_the_rel ctxt Rs Ts A B = build_rel ctxt Ts (the o choose_relator Rs) (A, B); +fun choose_binary_fun fs AB = + find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs; +fun build_binary_fun_app fs a b = + Option.map (rapp b o rapp a) (choose_binary_fun fs (fastype_of a, fastype_of b)); + +fun build_the_rel ctxt Rs Ts A B = build_rel ctxt Ts (the o choose_binary_fun Rs) (A, B); fun build_rel_app ctxt Rs Ts a b = build_the_rel ctxt Rs Ts (fastype_of a) (fastype_of b) $ a $ b; +val name_of_set = name_of_const "set"; + fun fp_sugar_of ctxt = Symtab.lookup (Data.get (Context.Proof ctxt)) #> Option.map (transfer_fp_sugar ctxt); @@ -759,6 +766,98 @@ mk_coinduct_attributes fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss) end; +fun derive_set_induct_thms_for_types lthy nn fpTs ctrss setss dtor_set_inducts exhausts + set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses = + let + fun mk_prems A Ps ctr_args t ctxt = + (case fastype_of t of + Type (type_name, xs) => + (case bnf_of ctxt type_name of + NONE => ([], ctxt) + | SOME bnf => + let + fun seq_assm a set ctxt = + let + val X = HOLogic.dest_setT (range_type (fastype_of set)); + val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt; + val assm = mk_Trueprop_mem (x, set $ a); + in + (case build_binary_fun_app Ps x a of + NONE => + mk_prems A Ps ctr_args x ctxt' + |>> map (Logic.all x o Logic.mk_implies o pair assm) + | SOME f => + ([Logic.all x + (Logic.mk_implies (assm, + Logic.mk_implies (HOLogic.mk_Trueprop f, + HOLogic.mk_Trueprop (the (build_binary_fun_app Ps x ctr_args)))))], + ctxt')) + end; + in + fold_map (seq_assm t o mk_set xs) (sets_of_bnf bnf) ctxt + |>> flat + end) + | T => + if T = A then ([HOLogic.mk_Trueprop (the (build_binary_fun_app Ps t ctr_args))], ctxt) + else ([], ctxt)); + + fun mk_prems_for_ctr A Ps ctr ctxt = + let + val (args, ctxt') = mk_Frees "arg" (binder_types (fastype_of ctr)) ctxt; + in + fold_map (mk_prems A Ps (list_comb (ctr, args))) args ctxt' + |>> map (fold_rev Logic.all args) o flat + |>> (fn prems => (prems, mk_names (length prems) (name_of_ctr ctr))) + end; + + fun mk_prems_and_concl_for_type A Ps ((fpT, ctrs), set) ctxt = + let + val ((x, fp), ctxt') = ctxt + |> yield_singleton (mk_Frees "x") A + ||>> yield_singleton (mk_Frees "a") fpT; + val concl = mk_Ball (set $ fp) (Term.absfree (dest_Free x) + (the (build_binary_fun_app Ps x fp))); + in + fold_map (mk_prems_for_ctr A Ps) ctrs ctxt' + |>> split_list + |>> map_prod flat flat + |>> apfst (rpair concl) + end; + + fun mk_thm ctxt fpTs ctrss sets = + let + val A = HOLogic.dest_setT (range_type (fastype_of (hd sets))); + val (Ps, ctxt') = mk_Frees "P" (map (fn fpT => A --> fpT --> HOLogic.boolT) fpTs) ctxt; + val (((premises, conclusion), case_names), ctxt'') = + (fold_map (mk_prems_and_concl_for_type A Ps) (fpTs ~~ ctrss ~~ sets) ctxt') + |>> apfst split_list o split_list + |>> apfst (apfst flat) + |>> apfst (apsnd (Library.foldr1 HOLogic.mk_conj)) + |>> apsnd flat; + + val thm = Goal.prove_sorry lthy [] premises (HOLogic.mk_Trueprop conclusion) + (fn {context = ctxt, prems = prems} => + mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts + set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses) + |> singleton (Proof_Context.export ctxt'' ctxt) + |> Thm.close_derivation; + + val case_names_attr = + Attrib.internal (K (Rule_Cases.case_names (quasi_unambiguous_case_names case_names))); + val induct_set_attrs = map (Attrib.internal o K o Induct.induct_pred o name_of_set) sets; + in + (thm, case_names_attr :: induct_set_attrs) + end + val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); + in + map (fn Asets => + let + fun massage_thm thm = rotate_prems (~1) (thm RS bspec); + in + mk_thm lthy fpTs ctrss Asets |> nn = 1 ? map_prod massage_thm (cons consumes_attr) + end) (transpose setss) + end; + fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _)) dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) @@ -1072,7 +1171,7 @@ val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, - xtor_co_rec_thms, rel_xtor_co_induct_thm, ...}, + xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms, ...}, lthy)) = fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) (map dest_TFree killed_As) fp_eqs no_defs_lthy0 @@ -1143,8 +1242,8 @@ fun massage_simple_notes base = filter_out (null o #2) - #> map (fn (thmN, thms, attrs) => - ((Binding.qualify true base (Binding.name thmN), attrs), [(thms, [])])); + #> map (fn (thmN, thms, f_attrs) => + ((Binding.qualify true base (Binding.name thmN), []), map_index (fn (i, thm) => ([thm], f_attrs i)) thms)); val massage_multi_notes = maps (fn (thmN, thmss, attrs) => @@ -1611,17 +1710,17 @@ |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); val notes = - [(disc_map_iffN, disc_map_iff_thms, simp_attrs), - (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs), - (rel_casesN, [rel_cases_thm], rel_cases_attrs), - (rel_distinctN, rel_distinct_thms, simp_attrs), - (rel_injectN, rel_inject_thms, simp_attrs), - (rel_introsN, rel_intro_thms, []), - (rel_selN, rel_sel_thms, []), - (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs), - (sel_mapN, sel_map_thms, []), - (sel_setN, sel_set_thms, []), - (set_emptyN, set_empty_thms, [])] + [(disc_map_iffN, disc_map_iff_thms, K simp_attrs), + (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)), + (rel_casesN, [rel_cases_thm], K rel_cases_attrs), + (rel_distinctN, rel_distinct_thms, K simp_attrs), + (rel_injectN, rel_inject_thms, K simp_attrs), + (rel_introsN, rel_intro_thms, K []), + (rel_selN, rel_sel_thms, K []), + (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)), + (sel_mapN, sel_map_thms, K []), + (sel_setN, sel_set_thms, K []), + (set_emptyN, set_empty_thms, K [])] |> massage_simple_notes fp_b_name; val (noted, lthy') = @@ -1692,8 +1791,8 @@ val common_notes = (if nn > 1 then - [(inductN, [induct_thm], induct_attrs), - (rel_inductN, common_rel_induct_thms, common_rel_induct_attrs)] + [(inductN, [induct_thm], K induct_attrs), + (rel_inductN, common_rel_induct_thms, K common_rel_induct_attrs)] else []) |> massage_simple_notes fp_common_name; @@ -1765,17 +1864,25 @@ (rel_coinduct_attrs, common_rel_coinduct_attrs)) end; + val (set_induct_thms, set_induct_attrss) = + derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars) + (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_induct_thms + (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss) + dtor_ctors abs_inverses + |> split_list; + val simp_thmss = map6 mk_simp_thms ctr_sugars (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss) mapss rel_injectss rel_distinctss setss; val common_notes = + (set_inductN, set_induct_thms, nth set_induct_attrss) :: (if nn > 1 then - [(coinductN, [coinduct_thm], common_coinduct_attrs), - (rel_coinductN, common_rel_coinduct_thms, common_rel_coinduct_attrs), - (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)] - else []) + [(coinductN, [coinduct_thm], K common_coinduct_attrs), + (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs), + (strong_coinductN, [strong_coinduct_thm], K common_coinduct_attrs)] + else []) |> massage_simple_notes fp_common_name; val notes = diff -r a6cf197c1f1e -r a2c4adb839a9 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Jul 30 00:50:41 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Jul 30 10:50:28 2014 +0200 @@ -39,6 +39,8 @@ val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic + val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> + thm list -> thm list -> thm list -> thm list -> tactic end; structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS = @@ -257,7 +259,7 @@ HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2) THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN - unfold_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @ + unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @ @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN TRYALL (hyp_subst_tac ctxt) THEN unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False @@ -306,4 +308,28 @@ SOME (thm RS eqFalseI) handle THM _ => NONE) discs) THEN ALLGOALS (rtac refl ORELSE' etac FalseE); +fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors + Abs_pre_inverses = + let + val assms_ctor_defs = + map (unfold_thms ctxt (@{thm BNF_Comp.id_bnf_comp_def} :: ctor_defs)) assms; + val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts + |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts; + in + ALLGOALS (resolve_tac dtor_set_inducts) THEN + TRYALL (resolve_tac exhausts' THEN_ALL_NEW + (resolve_tac (map (fn ct => refl RS + cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts) + THEN' atac THEN' hyp_subst_tac ctxt)) THEN + unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @ + @{thms BNF_Comp.id_bnf_comp_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert + Un_empty_left Un_empty_right empty_iff singleton_iff}) THEN + REPEAT_DETERM (HEADGOAL + (TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN' + REPEAT_DETERM o eresolve_tac @{thms UN_E UnE singletonE} THEN' + fold (curry (op ORELSE')) (map (fn thm => + funpow (length (prems_of thm)) (fn tac => tac THEN' atac) (rtac thm)) assms_ctor_defs) + (etac FalseE))) + end; + end; diff -r a6cf197c1f1e -r a2c4adb839a9 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Jul 30 00:50:41 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Jul 30 10:50:28 2014 +0200 @@ -463,7 +463,8 @@ xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*), xtor_co_rec_thms = xtor_co_rec_thms, xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*), - rel_xtor_co_induct_thm = rel_xtor_co_induct_thm} + rel_xtor_co_induct_thm = rel_xtor_co_induct_thm, + dtor_set_induct_thms = []} |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); in (fp_res, lthy) diff -r a6cf197c1f1e -r a2c4adb839a9 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Jul 30 00:50:41 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Jul 30 10:50:28 2014 +0200 @@ -25,7 +25,8 @@ xtor_rel_thms: thm list, xtor_co_rec_thms: thm list, xtor_co_rec_o_map_thms: thm list, - rel_xtor_co_induct_thm: thm} + rel_xtor_co_induct_thm: thm, + dtor_set_induct_thms: thm list} val morph_fp_result: morphism -> fp_result -> fp_result @@ -237,11 +238,12 @@ xtor_rel_thms: thm list, xtor_co_rec_thms: thm list, xtor_co_rec_o_map_thms: thm list, - rel_xtor_co_induct_thm: thm}; + rel_xtor_co_induct_thm: thm, + dtor_set_induct_thms: thm list}; fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, - xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} = + xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, ctors = map (Morphism.term phi) ctors, @@ -257,7 +259,8 @@ xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms, - rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm}; + rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm, + dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *) type fp_sugar = {T: typ, diff -r a6cf197c1f1e -r a2c4adb839a9 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Jul 30 00:50:41 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Jul 30 10:50:28 2014 +0200 @@ -1659,12 +1659,12 @@ (*register new codatatypes as BNFs*) val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jset_thmss', - dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, lthy) = + dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, dtor_Jset_induct_thms, lthy) = if m = 0 then (timer, replicate n DEADID_bnf, map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids), replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, - mk_Jrel_DEADID_coinduct_thm (), [], lthy) + mk_Jrel_DEADID_coinduct_thm (), [], [], lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; val gTs = map2 (curry op -->) passiveBs passiveCs; @@ -2464,7 +2464,8 @@ bs thmss) in (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jset_thmss', - dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, lthy) + dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, dtor_Jset_induct_thms, + lthy) end; val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m @@ -2526,7 +2527,8 @@ ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss', xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms, - xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm} + xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm, + dtor_set_induct_thms = dtor_Jset_induct_thms} |> morph_fp_result (substitute_noted_thm noted); in timer; (fp_res, lthy') diff -r a6cf197c1f1e -r a2c4adb839a9 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Jul 30 00:50:41 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Jul 30 10:50:28 2014 +0200 @@ -1814,7 +1814,8 @@ ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss', xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms, - xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm} + xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm, + dtor_set_induct_thms = []} |> morph_fp_result (substitute_noted_thm noted); in timer; (fp_res, lthy') diff -r a6cf197c1f1e -r a2c4adb839a9 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Jul 30 00:50:41 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Jul 30 10:50:28 2014 +0200 @@ -255,12 +255,6 @@ fun mk_disc_or_sel Ts t = subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t; -fun name_of_const what t = - (case head_of t of - Const (s, _) => s - | Free (s, _) => s - | _ => error ("Cannot extract name of " ^ what)); - val name_of_ctr = name_of_const "constructor"; fun name_of_disc t = diff -r a6cf197c1f1e -r a2c4adb839a9 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Jul 30 00:50:41 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Jul 30 10:50:28 2014 +0200 @@ -39,6 +39,8 @@ (string * sort) list * Proof.context val variant_tfrees: string list -> Proof.context -> typ list * Proof.context + val name_of_const: string -> term -> string + val typ_subst_nonatomic: (typ * typ) list -> typ -> typ val subst_nonatomic_types: (typ * typ) list -> term -> term @@ -177,6 +179,12 @@ apfst (map TFree) o variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type}); +fun name_of_const what t = + (case head_of t of + Const (s, _) => s + | Free (s, _) => s + | _ => error ("Cannot extract name of " ^ what)); + (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*) fun typ_subst_nonatomic [] = I | typ_subst_nonatomic inst =