--- 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') \<longleftrightarrow> False"
unfolding sum_rel_def by simp+
+lemma spec2: "\<forall>x y. P x y \<Longrightarrow> 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"
--- 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 \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
by auto
-lemma spec2: "\<forall>x y. P x y \<Longrightarrow> 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"
--- 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 ());
--- 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");
--- 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");
--- 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]},