# HG changeset patch # User traytel # Date 1368012784 -7200 # Node ID 3c152334f79464792b1be7ef994cfc7a860ee056 # Parent f964a98877131b620dadf0cf59675ea2dc51be59 relator induction for datatypes diff -r f964a9887713 -r 3c152334f794 src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed May 08 11:57:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed May 08 13:33:04 2013 +0200 @@ -93,6 +93,8 @@ val morN: string val nchotomyN: string val recN: string + val rel_coinductN: string + val rel_inductN: string val rel_injectN: string val rel_distinctN: string val rvN: string @@ -310,6 +312,8 @@ val rel_distinctN = relN ^ "_" ^ distinctN val injectN = "inject" val rel_injectN = relN ^ "_" ^ injectN +val rel_coinductN = relN ^ "_" ^ coinductN +val rel_inductN = relN ^ "_" ^ inductN val selN = "sel" val sel_unfoldN = selN ^ "_" ^ unfoldN val sel_corecN = selN ^ "_" ^ corecN diff -r f964a9887713 -r 3c152334f794 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed May 08 11:57:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed May 08 13:33:04 2013 +0200 @@ -1366,6 +1366,13 @@ fun mk_ctor_Irel_DEADID_thm ctor_inject bnf = trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym]; + val IphiTs = map2 mk_pred2T passiveAs passiveBs; + val activeIphiTs = map2 mk_pred2T Ts Ts'; + val ((Iphis, activeIphis), names_lthy) = names_lthy + |> mk_Frees "R" IphiTs + ||>> mk_Frees "IR" activeIphiTs; + val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; + (*register new datatypes as BNFs*) val (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) = if m = 0 then @@ -1383,10 +1390,9 @@ val AXTs = map HOLogic.mk_setT passiveXs; val XTs = mk_Ts passiveXs; val YTs = mk_Ts passiveYs; - val IphiTs = map2 mk_pred2T passiveAs passiveBs; - val ((((((((((((((fs, fs'), fs_copy), us), - B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), Iphis), + val (((((((((((((fs, fs'), fs_copy), us), + B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), names_lthy) = names_lthy |> mk_Frees' "f" fTs ||>> mk_Frees "f" fTs @@ -1399,8 +1405,7 @@ ||>> mk_Frees "f2" f2Ts ||>> mk_Frees "p1" p1Ts ||>> mk_Frees "p2" p2Ts - ||>> mk_Frees' "y" passiveAs - ||>> mk_Frees "R" IphiTs; + ||>> mk_Frees' "y" passiveAs; val map_FTFT's = map2 (fn Ds => mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; @@ -1746,7 +1751,6 @@ val timer = time (timer "registered new datatypes as BNFs"); - val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels; @@ -1803,9 +1807,33 @@ lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd) end; + val Irel_induct_thm = + let + val relphis = map (fn rel => Term.list_comb (rel, Iphis @ activeIphis)) rels; + fun mk_prem relphi phi x y ctor ctor' = + fold_rev Logic.all [x, y] (Logic.mk_implies (HOLogic.mk_Trueprop (relphi $ x $ y), + HOLogic.mk_Trueprop (phi $ (ctor $ x) $ (ctor' $ y)))); + val prems = map6 mk_prem relphis activeIphis xFs yFs ctors ctor's; + + val Irels = if m = 0 then map HOLogic.eq_const Ts + else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; + val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels; + val concl = + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq Irelphis activeIphis)); + in + Goal.prove_sorry lthy [] [] + (fold_rev Logic.all (Iphis @ activeIphis) (Logic.list_implies (prems, concl))) + (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms + (map rel_mono_strong_of_bnf bnfs)) + |> Thm.close_derivation + end; + + val timer = time (timer "relator induction"); + val common_notes = [(ctor_inductN, [ctor_induct_thm]), - (ctor_induct2N, [ctor_induct2_thm])] + (ctor_induct2N, [ctor_induct2_thm]), + (rel_inductN, [Irel_induct_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r f964a9887713 -r 3c152334f794 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed May 08 11:57:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed May 08 13:33:04 2013 +0200 @@ -64,6 +64,8 @@ val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list -> thm list -> tactic val mk_mor_str_tac: 'a list -> thm -> tactic + val mk_rel_induct_tac: int -> thm -> int list -> thm list -> thm list -> + {prems: 'a, context: Proof.context} -> tactic val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic @@ -844,4 +846,19 @@ EVERY' [rtac iffI, if_tac, only_if_tac] 1 end; +fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = _} = + let val n = length ks; + in + unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN + EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2, + EVERY' (map3 (fn i => fn ctor_rel => fn rel_mono_strong => + EVERY' [rtac impI, dtac (ctor_rel RS iffD1), select_prem_tac n (dtac @{thm meta_spec2}) i, + etac meta_mp, etac rel_mono_strong, + REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]}, + EVERY' (map (fn j => + EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]}, + Goal.assume_rule_tac ctxt]) ks)]) + ks ctor_rels rel_mono_strongs)] 1 + end; + end;