# HG changeset patch # User traytel # Date 1372863207 -7200 # Node ID e62f3fd2035efc740b67fc24a2ce2b5ac995457a # Parent 52cd8bebc3b62a2f4c939341efeab2c62871787a share some code between codatatypes, datatypes and eventually prim(co)rec diff -r 52cd8bebc3b6 -r e62f3fd2035e src/HOL/BNF/BNF_FP_Basic.thy --- a/src/HOL/BNF/BNF_FP_Basic.thy Wed Jul 03 16:07:00 2013 +0200 +++ b/src/HOL/BNF/BNF_FP_Basic.thy Wed Jul 03 16:53:27 2013 +0200 @@ -139,6 +139,9 @@ "sum_rel P Q (Inr y) (Inl x') \ False" unfolding sum_rel_def by simp+ +lemma spec2: "\x y. P x y \ P x y" +by blast + ML_file "Tools/bnf_fp_util.ML" ML_file "Tools/bnf_fp_def_sugar_tactics.ML" ML_file "Tools/bnf_fp_def_sugar.ML" diff -r 52cd8bebc3b6 -r e62f3fd2035e src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Wed Jul 03 16:07:00 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Wed Jul 03 16:53:27 2013 +0200 @@ -338,9 +338,6 @@ lemma Collect_splitD: "x \ Collect (split A) \ A (fst x) (snd x)" by auto -lemma spec2: "\x y. P x y \ P x y" -by blast - ML_file "Tools/bnf_gfp_util.ML" ML_file "Tools/bnf_gfp_tactics.ML" ML_file "Tools/bnf_gfp.ML" diff -r 52cd8bebc3b6 -r e62f3fd2035e src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Jul 03 16:07:00 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Jul 03 16:53:27 2013 +0200 @@ -166,6 +166,10 @@ val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list + val mk_rel_co_induct_thm: fp_kind -> term list -> term list -> term list -> term list -> + term list -> term list -> term list -> term list -> + ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm + val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) -> binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory -> @@ -459,6 +463,29 @@ Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)}, right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k; +fun mk_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy = + let + val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels; + val relphis = map (fn rel => Term.list_comb (rel, phis)) rels; + fun mk_xtor fp' xtor x = if fp = fp' then xtor $ x else x; + val dtor = mk_xtor Greatest_FP; + val ctor = mk_xtor Least_FP; + fun flip f x y = if fp = Greatest_FP then f y x else f x y; + + fun mk_prem pre_relphi phi x y xtor xtor' = + HOLogic.mk_Trueprop (list_all_free [x, y] (flip (curry HOLogic.mk_imp) + (pre_relphi $ (dtor xtor x) $ (dtor xtor' y)) (phi $ (ctor xtor x) $ (ctor xtor' y)))); + val prems = map6 mk_prem pre_relphis pre_phis xs ys xtors xtor's; + + val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map2 (flip mk_leq) relphis pre_phis)); + in + Goal.prove_sorry lthy [] [] + (fold_rev Logic.all (phis @ pre_phis) (Logic.list_implies (prems, concl))) tac + |> Thm.close_derivation + |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]})) + end; + fun fp_bnf construct_fp bs resBs eqs lthy = let val timer = time (Timer.startRealTimer ()); diff -r 52cd8bebc3b6 -r e62f3fd2035e src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Jul 03 16:07:00 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Jul 03 16:53:27 2013 +0200 @@ -2995,7 +2995,7 @@ |> transpose; val in_Jrels = map in_rel_of_bnf Jbnfs; - val Jrel_coinduct_thm = + val Jrel_coinduct_tac = let fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' = let @@ -3031,20 +3031,20 @@ |> split_conj_thm; val helper_coind1_thms = mk_helper_coind_thms (Jzs @ Jzs_copy) helper_coind1_concl; val helper_coind2_thms = mk_helper_coind_thms (Jz's @ Jz's_copy) helper_coind2_concl; - + fun mk_helper_ind_concl phi ab' ab fst snd z active_phi x y zip_unfold set = mk_Ball (set $ z) (Term.absfree ab' (list_all_free [x, y] (HOLogic.mk_imp (HOLogic.mk_conj (active_phi $ x $ y, HOLogic.mk_eq (z, zip_unfold $ HOLogic.mk_prod (x, y))), phi $ (fst $ ab) $ (snd $ ab))))); - + val mk_helper_ind_concls = map6 (fn Jphi => fn ab' => fn ab => fn fst => fn snd => fn zip_sets => map6 (mk_helper_ind_concl Jphi ab' ab fst snd) zip_zs activeJphis Jzs Jz's zip_unfolds zip_sets) Jphis abs' abs fstABs sndABs zip_setss |> map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj); - + val helper_ind_thmss = if m = 0 then replicate n [] else map3 (fn concl => fn j => fn set_induct => Goal.prove_sorry lthy [] [] @@ -3055,26 +3055,16 @@ |> split_conj_thm) mk_helper_ind_concls ls dtor_set_induct_thms |> transpose; - - val relphis = map (fn rel => Term.list_comb (rel, Jphis @ activeJphis)) rels; - fun mk_prem relphi phi x y dtor dtor' = - HOLogic.mk_Trueprop (list_all_free [x, y] - (HOLogic.mk_imp (phi $ x $ y, relphi $ (dtor $ x) $ (dtor' $ y)))); - val prems = map6 mk_prem relphis activeJphis Jzs Jz's dtors dtor's; - - val Jrels = if m = 0 then map HOLogic.eq_const Ts - else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs; - val Jrelphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jrels; - val concl = - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq activeJphis Jrelphis)); in - Goal.prove_sorry lthy [] [] - (fold_rev Logic.all (Jphis @ activeJphis) (Logic.list_implies (prems, concl))) - (mk_rel_coinduct_tac in_rels in_Jrels - helper_ind_thmss helper_coind1_thms helper_coind2_thms) - |> Thm.close_derivation - |> (fn thm => thm OF (replicate n @{thm allI[OF allI[OF impI]]})) + mk_rel_coinduct_tac in_rels in_Jrels + helper_ind_thmss helper_coind1_thms helper_coind2_thms end; + + val Jrels = if m = 0 then map HOLogic.eq_const Ts + else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs; + val Jrel_coinduct_thm = + mk_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's + Jrel_coinduct_tac lthy; val timer = time (timer "relator coinduction"); diff -r 52cd8bebc3b6 -r e62f3fd2035e src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed Jul 03 16:07:00 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Jul 03 16:53:27 2013 +0200 @@ -1808,26 +1808,12 @@ lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd) end; + val Irels = if m = 0 then map HOLogic.eq_const Ts + else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; 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; + mk_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's + (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs)) + lthy; val timer = time (timer "relator induction"); diff -r 52cd8bebc3b6 -r e62f3fd2035e src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Jul 03 16:07:00 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Jul 03 16:53:27 2013 +0200 @@ -852,8 +852,8 @@ 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, + EVERY' [rtac impI, dtac (ctor_rel RS iffD1), select_prem_tac n (dtac @{thm spec2}) i, + etac 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]},