# HG changeset patch # User desharna # Date 1405498380 -7200 # Node ID e3e7c86168b4f9fdcb2fd574b61fefba8df8e133 # Parent c1238062184bd7cb955ff7c55049d3886a8c9a6c generate 'rel_sel' theorem for (co)datatypes diff -r c1238062184b -r e3e7c86168b4 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 16 10:11:25 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 16 10:13:00 2014 +0200 @@ -111,8 +111,9 @@ fun merge data : T = Symtab.merge (K true) data; ); -fun choose_relator Rs AB = find_first - (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) Rs; +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 build_rel_app ctxt Rs Ts a b = build_the_rel ctxt Rs Ts (fastype_of a) (fastype_of b) $ a $ b; fun fp_sugar_of ctxt = Symtab.lookup (Data.get (Context.Proof ctxt)) @@ -1390,7 +1391,8 @@ map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th) rel_inject_thms ms; - val (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs)) = + val (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, + (rel_cases_thm, rel_cases_attrs)) = let val (((Ds, As), Bs), names_lthy) = lthy |> mk_TFrees (dead_of_bnf fp_bnf) @@ -1399,24 +1401,55 @@ val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf; val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf; val fTs = map2 (curry op -->) As Bs; - val ((fs, ta), names_lthy) = names_lthy + val rel = mk_rel_of_bnf Ds As Bs fp_bnf; + val ((((fs, Rs), ta), tb), names_lthy) = names_lthy |> mk_Frees "f" fTs - ||>> yield_singleton (mk_Frees "a") TA; + ||>> mk_Frees "R" (map2 mk_pred2T As Bs) + ||>> yield_singleton (mk_Frees "a") TA + ||>> yield_singleton (mk_Frees "b") TB; val map_term = mk_map_of_bnf Ds As Bs fp_bnf; - val discsA = map (mk_disc_or_sel ADs) discs; - val selssA = map (map (mk_disc_or_sel ADs)) selss; - val disc_sel_pairs = flat (map2 (map o pair) discsA selssA); + val discAs = map (mk_disc_or_sel ADs) discs; + val selAss = map (map (mk_disc_or_sel ADs)) selss; + val discAs_selAss = flat (map2 (map o pair) discAs selAss); + + val rel_sel_thms = + let + val discBs = map (mk_disc_or_sel BDs) discs; + val selBss = map (map (mk_disc_or_sel BDs)) selss; + val n = length discAs; + + fun mk_rhs n k discA selAs discB selBs = + (if k = n then [] else [HOLogic.mk_eq (discA $ ta, discB $ tb)]) @ + (case (selAs, selBs) of + ([], []) => [] + | (_ :: _, _ :: _) => [Library.foldr HOLogic.mk_imp + (if n = 1 then [] else [discA $ ta, discB $ tb], + Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app names_lthy Rs []) + (map (rapp ta) selAs) (map (rapp tb) selBs)))]); + + val goals = if n = 0 then [] + else [mk_Trueprop_eq + (build_rel_app names_lthy Rs [] ta tb, + Library.foldr1 HOLogic.mk_conj + (flat (map5 (mk_rhs n) (1 upto n) discAs selAss discBs selBss)))]; + in + if null goals then + [] + else + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, prems = _} => + mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust + (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts + rel_distinct_thms) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + end; val (rel_cases_thm, rel_cases_attrs) = let - val rel = mk_rel_of_bnf Ds As Bs fp_bnf; - val (((thesis, Rs), tb), names_lthy) = names_lthy - |> yield_singleton (mk_Frees "thesis") HOLogic.boolT - |>> HOLogic.mk_Trueprop - ||>> mk_Frees "R" (map2 mk_pred2T As Bs) - ||>> yield_singleton (mk_Frees "b") TB; + val (thesis, names_lthy) = apfst HOLogic.mk_Trueprop + (yield_singleton (mk_Frees "thesis") HOLogic.boolT names_lthy); - val _ = apfst HOLogic.mk_Trueprop; val rel_Rs_a_b = list_comb (rel, Rs) $ ta $ tb; val ctrAs = map (mk_ctr ADs) ctrs; val ctrBs = map (mk_ctr BDs) ctrs; @@ -1464,7 +1497,7 @@ val disc_map_iff_thms = let val discsB = map (mk_disc_or_sel BDs) discs; - val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discsA; + val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discAs; fun mk_goal (discA_t, discB) = if head_of discA_t aconv HOLogic.Not orelse is_refl_bool discA_t then @@ -1505,7 +1538,7 @@ if is_refl_bool prem then concl else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl) end; - val goals = map mk_goal disc_sel_pairs; + val goals = map mk_goal discAs_selAss; in if null goals then [] @@ -1570,7 +1603,7 @@ ([], ctxt) end; val (goals, names_lthy) = apfst (flat o flat) (fold_map (fn (disc, sel) => - fold_map (mk_goal disc sel) setsA) disc_sel_pairs names_lthy); + fold_map (mk_goal disc sel) setsA) discAs_selAss names_lthy); in if null goals then [] @@ -1583,7 +1616,8 @@ |> Proof_Context.export names_lthy lthy end; in - (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs)) + (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, + (rel_cases_thm, rel_cases_attrs)) end; val anonymous_notes = @@ -1598,6 +1632,7 @@ (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, []), diff -r c1238062184b -r e3e7c86168b4 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Jul 16 10:11:25 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Jul 16 10:13:00 2014 +0200 @@ -33,6 +33,8 @@ thm list -> thm list -> thm list -> tactic val mk_rel_induct0_tac: Proof.context -> thm -> thm list -> cterm list -> thm list -> thm list list -> thm list -> thm list -> thm list -> thm list -> tactic + val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> + thm list -> thm list -> tactic 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 @@ -263,6 +265,16 @@ TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac)) cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses); +fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels rel_injects distincts rel_distincts = + HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW + rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW + hyp_subst_tac ctxt) THEN + Local_Defs.unfold_tac ctxt (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @ + ((discs @ distincts) RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ + (rel_injects RL @{thms iffD2[OF eq_True]}) @ + (rel_distincts RL @{thms iffD2[OF eq_False]})) THEN + TRYALL (resolve_tac [TrueI, refl]); + fun mk_sel_map_tac ctxt ct exhaust discs maps sels = TRYALL Goal.conjunction_tac THEN ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW diff -r c1238062184b -r e3e7c86168b4 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Jul 16 10:11:25 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Jul 16 10:13:00 2014 +0200 @@ -130,6 +130,7 @@ val rel_injectN: string val rel_introsN: string val rel_distinctN: string + val rel_selN: string val rvN: string val sel_corecN: string val set_inclN: string @@ -411,6 +412,7 @@ val rel_injectN = relN ^ "_" ^ injectN val rel_introsN = relN ^ "_intros" val rel_coinductN = relN ^ "_" ^ coinductN +val rel_selN = relN ^ "_sel" val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN val rel_inductN = relN ^ "_" ^ inductN val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN