| author | immler |
| Thu, 24 Sep 2015 15:21:12 +0200 | |
| changeset 61244 | 6026c14f5e5d |
| parent 61242 | 1f92b0ac9c96 (diff) |
| parent 61243 | 44b2d133063e (current diff) |
| child 61245 | b77bf45efe21 |
--- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 24 14:29:08 2015 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 24 15:21:12 2015 +0200 @@ -1000,9 +1000,30 @@ The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin (Section~\ref{ssec:lifting}). +\item[@{text "t."}\hthm{rel_mono_strong}\rm:] ~ \\ +@{thm list.rel_mono_strong[no_vars]} + +\item[@{text "t."}\hthm{rel_cong} @{text "[fundef_cong]"}\rm:] ~ \\ +@{thm list.rel_cong[no_vars]} + +\item[@{text "t."}\hthm{rel_cong_simp}\rm:] ~ \\ +@{thm list.rel_cong_simp[no_vars]} + \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\ @{thm list.rel_refl[no_vars]} +\item[@{text "t."}\hthm{rel_refl_strong}\rm:] ~ \\ +@{thm list.rel_refl_strong[no_vars]} + +\item[@{text "t."}\hthm{rel_reflp}\rm:] ~ \\ +@{thm list.rel_reflp[no_vars]} + +\item[@{text "t."}\hthm{rel_symp}\rm:] ~ \\ +@{thm list.rel_symp[no_vars]} + +\item[@{text "t."}\hthm{rel_transp}\rm:] ~ \\ +@{thm list.rel_transp[no_vars]} + \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.rel_transfer[no_vars]} \\ The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
--- a/src/HOL/BNF_Def.thy Thu Sep 24 14:29:08 2015 +0200 +++ b/src/HOL/BNF_Def.thy Thu Sep 24 15:21:12 2015 +0200 @@ -234,6 +234,18 @@ lemma ge_eq_refl: "op = \<le> R \<Longrightarrow> R x x" by auto +lemma reflp_eq: "reflp R = (op = \<le> R)" + by (auto simp: reflp_def fun_eq_iff) + +lemma transp_relcompp: "transp r \<longleftrightarrow> r OO r \<le> r" + by (auto simp: transp_def) + +lemma symp_conversep: "symp R = (R\<inverse>\<inverse> \<le> R)" + by (auto simp: symp_def fun_eq_iff) + +lemma diag_imp_eq_le: "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> \<forall>x y. x \<in> A \<longrightarrow> y \<in> A \<longrightarrow> x = y \<longrightarrow> R x y" + by blast + ML_file "Tools/BNF/bnf_util.ML" ML_file "Tools/BNF/bnf_tactics.ML" ML_file "Tools/BNF/bnf_def_tactics.ML"
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Thu Sep 24 14:29:08 2015 +0200 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Thu Sep 24 15:21:12 2015 +0200 @@ -22,8 +22,8 @@ lemma shift_prefix_cases: assumes "xl @- xs = yl @- ys" shows "prefixeq xl yl \<or> prefixeq yl xl" -using shift_prefix[OF assms] apply(cases "length xl \<le> length yl") -by (metis, metis assms nat_le_linear shift_prefix) +using shift_prefix[OF assms] +by (cases "length xl \<le> length yl") (metis, metis assms nat_le_linear shift_prefix) section\<open>Linear temporal logic\<close> @@ -111,12 +111,12 @@ lemma ev_mono: assumes ev: "ev \<phi> xs" and 0: "\<And> xs. \<phi> xs \<Longrightarrow> \<psi> xs" shows "ev \<psi> xs" -using ev by induct (auto intro: ev.intros simp: 0) +using ev by induct (auto simp: 0) lemma alw_mono: assumes alw: "alw \<phi> xs" and 0: "\<And> xs. \<phi> xs \<Longrightarrow> \<psi> xs" shows "alw \<psi> xs" -using alw by coinduct (auto elim: alw.cases simp: 0) +using alw by coinduct (auto simp: 0) lemma until_monoL: assumes until: "(\<phi>1 until \<psi>) xs" and 0: "\<And> xs. \<phi>1 xs \<Longrightarrow> \<phi>2 xs" @@ -137,55 +137,55 @@ lemma until_false: "\<phi> until false = alw \<phi>" proof- {fix xs assume "(\<phi> until false) xs" hence "alw \<phi> xs" - apply coinduct by (auto elim: UNTIL.cases) + by coinduct (auto elim: UNTIL.cases) } moreover {fix xs assume "alw \<phi> xs" hence "(\<phi> until false) xs" - apply coinduct by (auto elim: alw.cases) + by coinduct auto } ultimately show ?thesis by blast qed lemma ev_nxt: "ev \<phi> = (\<phi> or nxt (ev \<phi>))" -apply(rule ext) by (metis ev.simps nxt.simps) +by (rule ext) (metis ev.simps nxt.simps) lemma alw_nxt: "alw \<phi> = (\<phi> aand nxt (alw \<phi>))" -apply(rule ext) by (metis alw.simps nxt.simps) +by (rule ext) (metis alw.simps nxt.simps) lemma ev_ev[simp]: "ev (ev \<phi>) = ev \<phi>" proof- {fix xs assume "ev (ev \<phi>) xs" hence "ev \<phi> xs" - by induct (auto intro: ev.intros) + by induct auto } - thus ?thesis by (auto intro: ev.intros) + thus ?thesis by auto qed lemma alw_alw[simp]: "alw (alw \<phi>) = alw \<phi>" proof- {fix xs assume "alw \<phi> xs" hence "alw (alw \<phi>) xs" - by coinduct (auto elim: alw.cases) + by coinduct auto } - thus ?thesis by (auto elim: alw.cases) + thus ?thesis by auto qed lemma ev_shift: assumes "ev \<phi> xs" shows "ev \<phi> (xl @- xs)" -using assms by (induct xl) (auto intro: ev.intros) +using assms by (induct xl) auto lemma ev_imp_shift: assumes "ev \<phi> xs" shows "\<exists> xl xs2. xs = xl @- xs2 \<and> \<phi> xs2" using assms by induct (metis shift.simps(1), metis shift.simps(2) stream.collapse)+ lemma alw_ev_shift: "alw \<phi> xs1 \<Longrightarrow> ev (alw \<phi>) (xl @- xs1)" -by (auto intro: ev_shift ev.intros) +by (auto intro: ev_shift) lemma alw_shift: assumes "alw \<phi> (xl @- xs)" shows "alw \<phi> xs" -using assms by (induct xl) (auto elim: alw.cases) +using assms by (induct xl) auto lemma ev_ex_nxt: assumes "ev \<phi> xs" @@ -224,15 +224,15 @@ using assms nxt_wait_least unfolding nxt_sdrop by auto lemma nxt_ev: "(nxt ^^ n) \<phi> xs \<Longrightarrow> ev \<phi> xs" -by (induct n arbitrary: xs) (auto intro: ev.intros) +by (induct n arbitrary: xs) auto lemma not_ev: "not (ev \<phi>) = alw (not \<phi>)" proof(rule ext, safe) fix xs assume "not (ev \<phi>) xs" thus "alw (not \<phi>) xs" - by (coinduct) (auto intro: ev.intros) + by (coinduct) auto next fix xs assume "ev \<phi> xs" and "alw (not \<phi>) xs" thus False - by (induct) (auto elim: alw.cases) + by (induct) auto qed lemma not_alw: "not (alw \<phi>) = ev (not \<phi>)" @@ -256,9 +256,7 @@ lemma ev_alw_imp_alw_ev: assumes "ev (alw \<phi>) xs" shows "alw (ev \<phi>) xs" -using assms apply induct - apply (metis (full_types) alw_mono ev.base) - by (metis alw alw_nxt ev.step) +using assms by induct (metis (full_types) alw_mono ev.base, metis alw alw_nxt ev.step) lemma alw_aand: "alw (\<phi> aand \<psi>) = alw \<phi> aand alw \<psi>" proof- @@ -267,7 +265,7 @@ } moreover {fix xs assume "(alw \<phi> aand alw \<psi>) xs" hence "alw (\<phi> aand \<psi>) xs" - by coinduct (auto elim: alw.cases) + by coinduct auto } ultimately show ?thesis by blast qed @@ -279,7 +277,7 @@ } moreover {fix xs assume "ev (\<phi> or \<psi>) xs" hence "(ev \<phi> or ev \<psi>) xs" - by induct (auto intro: ev.intros) + by induct auto } ultimately show ?thesis by blast qed @@ -314,7 +312,7 @@ lemma ev_alw_alw_impl: assumes "ev (alw \<phi>) xs" and "alw (alw \<phi> impl ev \<psi>) xs" shows "ev \<psi> xs" -using assms by induct (auto intro: ev.intros elim: alw.cases) +using assms by induct auto lemma ev_alw_stl[simp]: "ev (alw \<phi>) (stl x) \<longleftrightarrow> ev (alw \<phi>) x" by (metis (full_types) alw_nxt ev_nxt nxt.simps) @@ -323,18 +321,18 @@ "alw (alw \<phi> impl ev \<psi>) = (ev (alw \<phi>) impl alw (ev \<psi>))" (is "?A = ?B") proof- {fix xs assume "?A xs \<and> ev (alw \<phi>) xs" hence "alw (ev \<psi>) xs" - apply coinduct using ev_nxt by (auto elim: ev_alw_alw_impl alw.cases intro: ev.intros) + by coinduct (auto elim: ev_alw_alw_impl) } moreover {fix xs assume "?B xs" hence "?A xs" - apply coinduct by (auto elim: alw.cases intro: ev.intros) + by coinduct auto } ultimately show ?thesis by blast qed lemma ev_alw_impl: assumes "ev \<phi> xs" and "alw (\<phi> impl \<psi>) xs" shows "ev \<psi> xs" -using assms by induct (auto intro: ev.intros elim: alw.cases) +using assms by induct auto lemma ev_alw_impl_ev: assumes "ev \<phi> xs" and "alw (\<phi> impl ev \<psi>) xs" shows "ev \<psi> xs" @@ -345,7 +343,7 @@ shows "alw \<psi> xs" proof- {assume "alw \<phi> xs \<and> alw (\<phi> impl \<psi>) xs" hence ?thesis - apply coinduct by (auto elim: alw.cases) + by coinduct auto } thus ?thesis using assms by auto qed @@ -362,7 +360,7 @@ lemma alw_impl_ev_alw: assumes "alw (\<phi> impl ev \<psi>) xs" shows "alw (ev \<phi> impl ev \<psi>) xs" -using assms by coinduct (auto elim: alw.cases dest: ev_alw_impl intro: ev.intros) +using assms by coinduct (auto dest: ev_alw_impl) lemma ev_holds_sset: "ev (holds P) xs \<longleftrightarrow> (\<exists> x \<in> sset xs. P x)" (is "?L \<longleftrightarrow> ?R") @@ -379,7 +377,7 @@ shows "alw \<phi> xs" proof- {assume "\<phi> xs \<and> alw (\<phi> impl nxt \<phi>) xs" hence ?thesis - apply coinduct by(auto elim: alw.cases) + by coinduct auto } thus ?thesis using assms by auto qed @@ -390,7 +388,7 @@ proof- {assume "\<not> ev \<psi> xs" hence "alw (not \<psi>) xs" unfolding not_ev[symmetric] . moreover have "alw (not \<psi> impl (\<phi> impl nxt \<phi>)) xs" - using 2 by coinduct (auto elim: alw.cases) + using 2 by coinduct auto ultimately have "alw (\<phi> impl nxt \<phi>) xs" by(auto dest: alw_mp) with 1 have "alw \<phi> xs" by(rule alw_invar) } @@ -404,7 +402,7 @@ obtain xl xs1 where xs: "xs = xl @- xs1" and \<phi>: "\<phi> xs1" using e by (metis ev_imp_shift) have "\<phi> xs1 \<and> alw (\<phi> impl (nxt \<phi>)) xs1" using a \<phi> unfolding xs by (metis alw_shift) - hence "alw \<phi> xs1" by(coinduct xs1 rule: alw.coinduct) (auto elim: alw.cases) + hence "alw \<phi> xs1" by(coinduct xs1 rule: alw.coinduct) auto thus ?thesis unfolding xs by (auto intro: alw_ev_shift) qed @@ -602,7 +600,7 @@ using suntil.induct[of \<phi> \<psi> x P] by blast lemma ev_suntil: "(\<phi> suntil \<psi>) \<omega> \<Longrightarrow> ev \<psi> \<omega>" - by (induct rule: suntil.induct) (auto intro: ev.intros) + by (induct rule: suntil.induct) auto lemma suntil_inv: assumes stl: "\<And>s. f (stl s) = stl (f s)"
--- a/src/HOL/Tools/BNF/bnf_comp.ML Thu Sep 24 14:29:08 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Thu Sep 24 15:21:12 2015 +0200 @@ -325,13 +325,12 @@ fun rel_OO_Grp_tac ctxt = let val outer_rel_Grp = rel_Grp_of_bnf outer RS sym; - val outer_rel_cong = rel_cong_of_bnf outer; val thm = (trans OF [in_alt_thm RS @{thm OO_Grp_cong}, trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]}, rel_conversep_of_bnf outer RS sym], outer_rel_Grp], - trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF + trans OF [rel_OO_of_bnf outer RS sym, rel_cong0_of_bnf outer OF (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym); in unfold_thms_tac ctxt set'_eq_sets THEN rtac ctxt thm 1 @@ -441,7 +440,7 @@ trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]}, rel_conversep_of_bnf bnf RS sym], rel_Grp], - trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF + trans OF [rel_OO_of_bnf bnf RS sym, rel_cong0_of_bnf bnf OF (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @ replicate (live - n) @{thm Grp_fst_snd})]]] RS sym); in
--- a/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 24 14:29:08 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 24 15:21:12 2015 +0200 @@ -76,12 +76,18 @@ val rel_Grp_of_bnf: bnf -> thm val rel_OO_of_bnf: bnf -> thm val rel_OO_Grp_of_bnf: bnf -> thm + val rel_cong0_of_bnf: bnf -> thm val rel_cong_of_bnf: bnf -> thm + val rel_cong_simp_of_bnf: bnf -> thm val rel_conversep_of_bnf: bnf -> thm val rel_mono_of_bnf: bnf -> thm val rel_mono_strong0_of_bnf: bnf -> thm val rel_mono_strong_of_bnf: bnf -> thm val rel_refl_of_bnf: bnf -> thm + val rel_refl_strong_of_bnf: bnf -> thm + val rel_reflp_of_bnf: bnf -> thm + val rel_symp_of_bnf: bnf -> thm + val rel_transp_of_bnf: bnf -> thm val rel_map_of_bnf: bnf -> thm list val rel_transfer_of_bnf: bnf -> thm val rel_eq_of_bnf: bnf -> thm @@ -244,7 +250,9 @@ rel_eq: thm lazy, rel_flip: thm lazy, set_map: thm lazy list, + rel_cong0: thm lazy, rel_cong: thm lazy, + rel_cong_simp: thm lazy, rel_map: thm list lazy, rel_mono: thm lazy, rel_mono_strong0: thm lazy, @@ -254,13 +262,18 @@ rel_conversep: thm lazy, rel_OO: thm lazy, rel_refl: thm lazy, + rel_refl_strong: thm lazy, + rel_reflp: thm lazy, + rel_symp: thm lazy, + rel_transp: thm lazy, rel_transfer: thm lazy }; fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel - inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident - map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong - set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer = { + inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident map_transfer + rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono rel_mono_strong0 + rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp + rel_symp rel_transp rel_transfer = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, bd_Cnotzero = bd_Cnotzero, @@ -281,7 +294,9 @@ rel_eq = rel_eq, rel_flip = rel_flip, set_map = set_map, + rel_cong0 = rel_cong0, rel_cong = rel_cong, + rel_cong_simp = rel_cong_simp, rel_map = rel_map, rel_mono = rel_mono, rel_mono_strong0 = rel_mono_strong0, @@ -291,6 +306,10 @@ rel_conversep = rel_conversep, rel_OO = rel_OO, rel_refl = rel_refl, + rel_refl_strong = rel_refl_strong, + rel_reflp = rel_reflp, + rel_symp = rel_symp, + rel_transp = rel_transp, set_transfer = set_transfer}; fun map_facts f { @@ -314,7 +333,9 @@ rel_eq, rel_flip, set_map, + rel_cong0, rel_cong, + rel_cong_simp, rel_map, rel_mono, rel_mono_strong0, @@ -324,6 +345,10 @@ rel_conversep, rel_OO, rel_refl, + rel_refl_strong, + rel_reflp, + rel_symp, + rel_transp, set_transfer} = {bd_Card_order = f bd_Card_order, bd_Cinfinite = f bd_Cinfinite, @@ -345,7 +370,9 @@ rel_eq = Lazy.map f rel_eq, rel_flip = Lazy.map f rel_flip, set_map = map (Lazy.map f) set_map, + rel_cong0 = Lazy.map f rel_cong0, rel_cong = Lazy.map f rel_cong, + rel_cong_simp = Lazy.map f rel_cong_simp, rel_map = Lazy.map (map f) rel_map, rel_mono = Lazy.map f rel_mono, rel_mono_strong0 = Lazy.map f rel_mono_strong0, @@ -355,6 +382,10 @@ rel_conversep = Lazy.map f rel_conversep, rel_OO = Lazy.map f rel_OO, rel_refl = Lazy.map f rel_refl, + rel_refl_strong = Lazy.map f rel_refl_strong, + rel_reflp = Lazy.map f rel_reflp, + rel_symp = Lazy.map f rel_symp, + rel_transp = Lazy.map f rel_transp, set_transfer = Lazy.map (map f) set_transfer}; val morph_facts = map_facts o Morphism.thm; @@ -482,11 +513,17 @@ val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf; val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf; val set_transfer_of_bnf = Lazy.force o #set_transfer o #facts o rep_bnf; +val rel_cong0_of_bnf = Lazy.force o #rel_cong0 o #facts o rep_bnf; val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf; +val rel_cong_simp_of_bnf = Lazy.force o #rel_cong_simp o #facts o rep_bnf; val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf; val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf; val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf; val rel_refl_of_bnf = Lazy.force o #rel_refl o #facts o rep_bnf; +val rel_refl_strong_of_bnf = Lazy.force o #rel_refl_strong o #facts o rep_bnf; +val rel_reflp_of_bnf = Lazy.force o #rel_reflp o #facts o rep_bnf; +val rel_symp_of_bnf = Lazy.force o #rel_symp o #facts o rep_bnf; +val rel_transp_of_bnf = Lazy.force o #rel_transp o #facts o rep_bnf; val rel_map_of_bnf = Lazy.force o #rel_map o #facts o rep_bnf; val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf; val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf; @@ -670,7 +707,13 @@ val rel_monoN = "rel_mono"; val rel_mono_strong0N = "rel_mono_strong0"; val rel_mono_strongN = "rel_mono_strong"; +val rel_congN = "rel_cong"; +val rel_cong_simpN = "rel_cong_simp"; val rel_reflN = "rel_refl"; +val rel_refl_strongN = "rel_refl_strong"; +val rel_reflpN = "rel_reflp"; +val rel_sympN = "rel_symp"; +val rel_transpN = "rel_transp"; val rel_transferN = "rel_transfer"; val rel_comppN = "rel_compp"; val rel_compp_GrpN = "rel_compp_Grp"; @@ -742,7 +785,13 @@ (rel_mapN, Lazy.force (#rel_map facts), []), (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs), (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []), + (rel_congN, [Lazy.force (#rel_cong facts)], fundefcong_attrs), + (rel_cong_simpN, [Lazy.force (#rel_cong_simp facts)], []), (rel_reflN, [Lazy.force (#rel_refl facts)], []), + (rel_refl_strongN, [Lazy.force (#rel_refl_strong facts)], []), + (rel_reflpN, [Lazy.force (#rel_reflp facts)], []), + (rel_sympN, [Lazy.force (#rel_symp facts)], []), + (rel_transpN, [Lazy.force (#rel_transp facts)], []), (rel_transferN, [Lazy.force (#rel_transfer facts)], []), (set_mapN, map Lazy.force (#set_map facts), []), (set_transferN, Lazy.force (#set_transfer facts), [])] @@ -784,7 +833,7 @@ let val live = length set_rhss; - val def_qualify = Binding.concealed o Binding.qualify false (Binding.name_of bnf_b); + val def_qualify = Binding.qualify false (Binding.name_of bnf_b); fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b; @@ -804,7 +853,7 @@ let val b = b () in apfst (apsnd snd) ((if internal then Local_Theory.define_internal else Local_Theory.define) - ((b, NoSyn), ((Thm.def_binding b, []), rhs)) lthy) + ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), rhs)) lthy) end end; @@ -1033,7 +1082,7 @@ fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel; val pre_names_lthy = lthy; - val ((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), zs), zs'), ys), As), + val (((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), y'), zs), zs'), ys), As), As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs), S_BsEs), transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy |> mk_Frees "f" (map2 (curry op -->) As' Bs') @@ -1044,6 +1093,7 @@ ||>> yield_singleton (mk_Frees "x") CA' ||>> yield_singleton (mk_Frees "x") CA' ||>> yield_singleton (mk_Frees "y") CB' + ||>> yield_singleton (mk_Frees "y") CB' ||>> mk_Frees "z" As' ||>> mk_Frees "z" As' ||>> mk_Frees "y" Bs' @@ -1060,7 +1110,8 @@ ||>> mk_Frees "S" transfer_ranRTs; val fs_copy = map2 (retype_const_or_free o fastype_of) fs gs; - val x_copy = retype_const_or_free CA' y; + val x_copy = retype_const_or_free CA' y'; + val y_copy = retype_const_or_free CB' x'; val rel = mk_bnf_rel pred2RTs CA' CB'; val relCsEs = mk_bnf_rel pred2RTsCsEs CC' CE'; @@ -1289,7 +1340,7 @@ val rel_Grp = Lazy.lazy mk_rel_Grp; - fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy + fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy; fun mk_rel_concl f = HOLogic.mk_Trueprop (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy))); @@ -1305,7 +1356,7 @@ |> Thm.close_derivation end; - fun mk_rel_cong () = + fun mk_rel_cong0 () = let val cong_prems = mk_rel_prems (curry HOLogic.mk_eq); val cong_concl = mk_rel_concl HOLogic.mk_eq; @@ -1317,14 +1368,14 @@ end; val rel_mono = Lazy.lazy mk_rel_mono; - val rel_cong = Lazy.lazy mk_rel_cong; + val rel_cong0 = Lazy.lazy mk_rel_cong0; fun mk_rel_eq () = Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'), HOLogic.eq_const CA')) (fn {context = ctxt, prems = _} => - mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id0 axioms)) + mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong0) (#map_id0 axioms)) |> Thm.close_derivation; val rel_eq = Lazy.lazy mk_rel_eq; @@ -1400,6 +1451,30 @@ val rel_mono_strong = Lazy.lazy mk_rel_mono_strong; + fun mk_rel_cong_prem mk_implies x x' z z' set set' R R_copy = + Logic.all z (Logic.all z' + (mk_implies (mk_Trueprop_mem (z, set $ x), mk_implies (mk_Trueprop_mem (z', set' $ x'), + mk_Trueprop_eq (R $ z $ z', R_copy $ z $ z'))))); + + fun mk_rel_cong mk_implies () = + let + val prem0 = mk_Trueprop_eq (x, x_copy); + val prem1 = mk_Trueprop_eq (y, y_copy); + val prems = @{map 6} (mk_rel_cong_prem mk_implies x_copy y_copy) + zs ys bnf_sets_As bnf_sets_Bs Rs Rs_copy; + val eq = mk_Trueprop_eq (Term.list_comb (rel, Rs) $ x $ y, + Term.list_comb (rel, Rs_copy) $ x_copy $ y_copy); + in + Goal.prove_sorry lthy [] (prem0 :: prem1 :: prems) eq + (fn {context = ctxt, prems} => + mk_rel_cong_tac ctxt (chop 2 prems) (Lazy.force rel_mono_strong)) + |> Thm.close_derivation + |> singleton (Proof_Context.export names_lthy lthy) + end; + + val rel_cong = Lazy.lazy (mk_rel_cong Logic.mk_implies); + val rel_cong_simp = Lazy.lazy (mk_rel_cong (fn (a, b) => @{term simp_implies} $ a $ b)); + fun mk_rel_map () = let fun mk_goal lhs rhs = @@ -1432,6 +1507,33 @@ val rel_refl = Lazy.lazy mk_rel_refl; + fun mk_rel_refl_strong () = + (rule_by_tactic lthy (ALLGOALS (Object_Logic.full_atomize_tac lthy)) + ((Lazy.force rel_eq RS @{thm predicate2_eqD}) RS @{thm iffD2[OF _ refl]} RS + Lazy.force rel_mono_strong)) OF + (replicate live @{thm diag_imp_eq_le}) + + val rel_refl_strong = Lazy.lazy mk_rel_refl_strong; + + fun mk_rel_preserves mk_prop prop_conv_thm thm () = + let + val Rs = map2 retype_const_or_free self_pred2RTs Rs; + val prems = map (HOLogic.mk_Trueprop o mk_prop) Rs; + val goal = HOLogic.mk_Trueprop (mk_prop (Term.list_comb (relAsAs, Rs))); + in + Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal)) + (fn {context = ctxt, prems = _} => + unfold_thms_tac ctxt [prop_conv_thm] THEN + HEADGOAL (rtac ctxt (Lazy.force thm RS sym RS @{thm ord_eq_le_trans}) + THEN' rtac ctxt (Lazy.force rel_mono) THEN_ALL_NEW assume_tac ctxt)) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation + end; + + val rel_reflp = Lazy.lazy (mk_rel_preserves mk_reflp @{thm reflp_eq} rel_eq); + val rel_symp = Lazy.lazy (mk_rel_preserves mk_symp @{thm symp_conversep} rel_conversep); + val rel_transp = Lazy.lazy (mk_rel_preserves mk_transp @{thm transp_relcompp} rel_OO); + fun mk_map_transfer () = let val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs; @@ -1519,8 +1621,9 @@ val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 - map_ident map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 - rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer; + map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map + rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO + rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer; val wits = map2 mk_witness bnf_wits wit_thms;
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Sep 24 14:29:08 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Sep 24 15:21:12 2015 +0200 @@ -28,6 +28,7 @@ val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic + val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic @@ -356,4 +357,15 @@ REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN' rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps); +fun mk_rel_cong_tac ctxt (eqs, prems) mono = + let + fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt; + fun mk_tacs iffD = etac ctxt mono :: + map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD) + |> Drule.rotate_prems ~1 |> mk_tac) prems; + in + unfold_thms_tac ctxt eqs THEN + HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2)) + end; + end;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 24 14:29:08 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 24 15:21:12 2015 +0200 @@ -219,7 +219,7 @@ val map_ids = map map_id_of_bnf bnfs; val set_bdss = map set_bd_of_bnf bnfs; val set_mapss = map set_map_of_bnf bnfs; - val rel_congs = map rel_cong_of_bnf bnfs; + val rel_congs = map rel_cong0_of_bnf bnfs; val rel_converseps = map rel_conversep_of_bnf bnfs; val rel_Grps = map rel_Grp_of_bnf bnfs; val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 24 14:29:08 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 24 15:21:12 2015 +0200 @@ -61,6 +61,9 @@ val mk_rel_comp: term * term -> term val mk_rel_compp: term * term -> term val mk_vimage2p: term -> term -> term + val mk_reflp: term -> term + val mk_symp: term -> term + val mk_transp: term -> term (*parameterized terms*) val mk_nthN: int -> term -> int -> term @@ -348,6 +351,12 @@ (T1 --> T2) --> (U1 --> U2) --> mk_pred2T T2 U2 --> mk_pred2T T1 U1) $ f $ g end; +fun mk_pred name R = + Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R; +val mk_reflp = mk_pred @{const_name reflp}; +val mk_symp = mk_pred @{const_name symp}; +val mk_transp = mk_pred @{const_name transp}; + fun mk_trans thm1 thm2 = trans OF [thm1, thm2]; fun mk_sym thm = thm RS sym;