--- a/src/HOL/Codatatype/BNF_Def.thy Fri Sep 21 12:07:59 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Def.thy Fri Sep 21 12:27:56 2012 +0200
@@ -25,6 +25,23 @@
"R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
unfolding converse_def by auto
+definition convol ("<_ , _>") where
+"<f , g> \<equiv> %a. (f a, g a)"
+
+lemma fst_convol:
+"fst o <f , g> = f"
+apply(rule ext)
+unfolding convol_def by simp
+
+lemma snd_convol:
+"snd o <f , g> = g"
+apply(rule ext)
+unfolding convol_def by simp
+
+lemma convol_memI:
+"\<lbrakk>f x = f' x; g x = g' x; P x\<rbrakk> \<Longrightarrow> <f , g> x \<in> {(f' a, g' a) |a. P a}"
+unfolding convol_def by auto
+
definition csquare where
"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
--- a/src/HOL/Codatatype/BNF_FP.thy Fri Sep 21 12:07:59 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy Fri Sep 21 12:27:56 2012 +0200
@@ -38,19 +38,6 @@
lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
by simp
-definition convol ("<_ , _>") where
-"<f , g> \<equiv> %a. (f a, g a)"
-
-lemma fst_convol:
-"fst o <f , g> = f"
-apply(rule ext)
-unfolding convol_def by simp
-
-lemma snd_convol:
-"snd o <f , g> = g"
-apply(rule ext)
-unfolding convol_def by simp
-
lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x"
unfolding o_def fun_eq_iff by simp
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 12:07:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 12:27:56 2012 +0200
@@ -989,8 +989,7 @@
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal
- (mk_rel_Gr_tac rel_O_Grs (#map_id axioms) (#map_cong axioms)
- (#map_wpull axioms) (Lazy.force in_cong) (Lazy.force map_id')
+ (mk_rel_Gr_tac rel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
end;
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 12:07:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 12:27:56 2012 +0200
@@ -15,7 +15,7 @@
val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_set_natural': thm -> thm
- val mk_rel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_rel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
val mk_rel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
@@ -63,7 +63,7 @@
rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
-fun mk_rel_Gr_tac rel_O_Grs map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
+fun mk_rel_Gr_tac rel_O_Grs map_id map_cong map_id' map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
@@ -89,17 +89,19 @@
rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
- rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
- REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
- rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
- CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
- rtac @{thm image_mono}, atac]) set_naturals,
- rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
rtac @{thm relcompI}, rtac @{thm converseI},
- REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
- rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, etac sym,
- etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
- REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
+ EVERY' (map2 (fn convol => fn map_id =>
+ EVERY' [rtac CollectI, rtac exI, rtac conjI,
+ rtac Pair_eqI, rtac conjI, rtac refl, rtac sym,
+ rtac (box_equals OF [map_cong, map_comp RS sym, map_id]),
+ REPEAT_DETERM_N n o rtac (convol RS fun_cong),
+ REPEAT_DETERM o eresolve_tac [CollectE, conjE],
+ rtac CollectI,
+ CONJ_WRAP' (fn thm =>
+ EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
+ rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac])
+ set_naturals])
+ @{thms fst_convol snd_convol} [map_id', refl])] 1
end;
fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =