Generalized corecursor sugar ("corec" and friends).
*)
section \<open>Generalized Corecursor Sugar (corec and friends)\<close>
theory BNF_Corec imports Main
keywords "corec" :: thy_defn and "corecursive" :: thy_goal_defn and "friend_of_corec" :: thy_goal_defn and "coinduction_upto" :: thy_decl begin
lemma obj_distinct_prems: "P \ P \ Q \ P \ Q" by auto
lemma inject_refine: "g (f x) = x \ g (f y) = y \ f x = f y \ x = y" by (metis (no_types))
lemma convol_apply: "BNF_Def.convol f g x = (f x, g x)" unfolding convol_def ..
lemma Grp_UNIV_id: "BNF_Def.Grp UNIV id = (=)" unfolding BNF_Def.Grp_def by auto
lemma sum_comp_cases: assumes"f \ Inl = g \ Inl" and "f \ Inr = g \ Inr" shows"f = g" proof (rule ext) fix a show"f a = g a" using assms unfolding comp_def fun_eq_iff by (cases a) auto qed
lemma if_True_False: "(if P then True else Q) \ P \ Q" "(if P then False else Q) \ \ P \ Q" "(if P then Q else True) \ \ P \ Q" "(if P then Q else False) \ P \ Q" by auto
lemma if_distrib_fun: "(if c then f else g) x = (if c then f x else g x)" by simp
subsection \<open>Coinduction\<close>
lemma eq_comp_compI: "a \ b = f \ x \ x \ c = id \ f = a \ (b \ c)" unfolding fun_eq_iff by simp
lemma self_bounded_weaken_left: "(a :: 'a :: semilattice_inf) \ inf a b \ a \ b" by (erule le_infE)
lemma self_bounded_weaken_right: "(a :: 'a :: semilattice_inf) \ inf b a \ a \ b" by (erule le_infE)
lemma symp_iff: "symp R \ R = R\\" by (metis antisym conversep.cases conversep_le_swap predicate2I symp_def)
lemma equivp_inf: "\equivp R; equivp S\ \ equivp (inf R S)" unfolding equivp_def inf_fun_def inf_bool_def by metis
lemma vimage2p_rel_prod: "(\x y. rel_prod R S (BNF_Def.convol f1 g1 x) (BNF_Def.convol f2 g2 y)) =
(inf (BNF_Def.vimage2p f1 f2 R) (BNF_Def.vimage2p g1 g2 S))" unfolding vimage2p_def rel_prod.simps convol_def by auto
lemma predicate2I_obj: "(\x y. P x y \ Q x y) \ P \ Q" by auto
lemma predicate2D_obj: "P \ Q \ P x y \ Q x y" by auto
locale cong = fixes rel :: "('a \ 'a \ bool) \ ('b \ 'b \ bool)" and eval :: "'b \ 'a" and retr :: "('a \ 'a \ bool) \ ('a \ 'a \ bool)" assumes rel_mono: "\R S. R \ S \ rel R \ rel S" and equivp_retr: "\R. equivp R \ equivp (retr R)" and retr_eval: "\R x y. \(rel_fun (rel R) R) eval eval; rel (inf R (retr R)) x y\\
retr R (eval x) (eval y)" begin
definition cong :: "('a \ 'a \ bool) \ bool" where "cong R \ equivp R \ (rel_fun (rel R) R) eval eval"
lemma cong_retr: "cong R \ cong (inf R (retr R))" unfolding cong_def by (auto simp: rel_fun_def dest: predicate2D[OF rel_mono, rotated]
intro: equivp_inf equivp_retr retr_eval)
lemma cong_equivp: "cong R \ equivp R" unfolding cong_def by simp
definition gen_cong :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" where "gen_cong R j1 j2 \ \R'. R \ R' \ cong R' \ R' j1 j2"
lemma gen_cong_reflp[intro, simp]: "x = y \ gen_cong R x y" unfolding gen_cong_def by (auto dest: cong_equivp equivp_reflp)
lemma gen_cong_symp[intro]: "gen_cong R x y \ gen_cong R y x" unfolding gen_cong_def by (auto dest: cong_equivp equivp_symp)
lemma gen_cong_transp[intro]: "gen_cong R x y \ gen_cong R y z \ gen_cong R x z" unfolding gen_cong_def by (auto dest: cong_equivp equivp_transp)
lemma equivp_gen_cong: "equivp (gen_cong R)" by (intro equivpI reflpI sympI transpI) auto
lemma leq_gen_cong: "R \ gen_cong R" unfolding gen_cong_def[abs_def] by auto
lemma rel_sum_case_sum: "rel_fun (rel_sum R S) T (case_sum f1 g1) (case_sum f2 g2) = (rel_fun R T f1 f2 \ rel_fun S T g1 g2)" by (auto simp: rel_fun_def rel_sum.simps split: sum.splits)
context fixes rel eval rel' eval' retr emb assumes base: "cong rel eval retr" and step: "cong rel' eval' retr" and emb: "eval' \ emb = eval" and emb_transfer: "rel_fun (rel R) (rel' R) emb emb" begin
interpretation base: cong rel eval retr by (rule base) interpretation step: cong rel' eval' retr by (rule step)
lemma gen_cong_emb: "base.gen_cong R \ step.gen_cong R" proof (rule base.gen_cong_minimal[OF step.leq_gen_cong]) note step.gen_cong_eval_rel_fun[transfer_rule] emb_transfer[transfer_rule] have"(rel_fun (rel (step.gen_cong R)) (step.gen_cong R)) eval eval" unfolding emb[symmetric] by transfer_prover thenshow"base.cong (step.gen_cong R)" by (auto simp: base.cong_def step.equivp_gen_cong) qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
