(* Title: HOL/Library/BNF_Corec.thy
Author: Jasmin Blanchette, Inria, LORIA, MPII
Author: Aymeric Bouzy, Ecole polytechnique
Author: Dmitriy Traytel, ETH Zurich
Copyright 2015, 2016
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 case_sum_Inl_Inr_L: "case_sum (f \ Inl) (f \ Inr) = f"
by (metis case_sum_expand_Inr')
lemma eq_o_InrI: "\g \ Inl = h; case_sum h f = g\ \ f = g \ Inr"
by (auto simp: fun_eq_iff split: sum.splits)
lemma id_bnf_o: "BNF_Composition.id_bnf \ f = f"
unfolding BNF_Composition.id_bnf_def by (rule o_def)
lemma o_id_bnf: "f \ BNF_Composition.id_bnf = f"
unfolding BNF_Composition.id_bnf_def by (rule o_def)
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
lemmas imp_gen_cong[intro] = predicate2D[OF leq_gen_cong]
lemma gen_cong_minimal: "\R \ R'; cong R'\ \ gen_cong R \ R'"
unfolding gen_cong_def[abs_def] by (rule predicate2I) metis
lemma congdd_base_gen_congdd_base_aux:
"rel (gen_cong R) x y \ R \ R' \ cong R' \ R' (eval x) (eval y)"
by (force simp: rel_fun_def gen_cong_def cong_def dest: spec[of _ R'] predicate2D[OF rel_mono, rotated -1, of _ _ _ R'])
lemma cong_gen_cong: "cong (gen_cong R)"
proof -
{ fix R' x y
have "rel (gen_cong R) x y \ R \ R' \ cong R' \ R' (eval x) (eval y)"
by (force simp: rel_fun_def gen_cong_def cong_def dest: spec[of _ R']
predicate2D[OF rel_mono, rotated -1, of _ _ _ R'])
}
then show "cong (gen_cong R)" by (auto simp: equivp_gen_cong rel_fun_def gen_cong_def cong_def)
qed
lemma gen_cong_eval_rel_fun:
"(rel_fun (rel (gen_cong R)) (gen_cong R)) eval eval"
using cong_gen_cong[of R] unfolding cong_def by simp
lemma gen_cong_eval:
"rel (gen_cong R) x y \ gen_cong R (eval x) (eval y)"
by (erule rel_funD[OF gen_cong_eval_rel_fun])
lemma gen_cong_idem: "gen_cong (gen_cong R) = gen_cong R"
by (simp add: antisym cong_gen_cong gen_cong_minimal leq_gen_cong)
lemma gen_cong_rho:
"\ = eval \ f \ rel (gen_cong R) (f x) (f y) \ gen_cong R (\ x) (\ y)"
by (simp add: gen_cong_eval)
lemma coinduction:
assumes coind: "\R. R \ retr R \ R \ (=)"
assumes cih: "R \ retr (gen_cong R)"
shows "R \ (=)"
apply (rule order_trans[OF leq_gen_cong mp[OF spec[OF coind]]])
apply (rule self_bounded_weaken_left[OF gen_cong_minimal])
apply (rule inf_greatest[OF leq_gen_cong cih])
apply (rule cong_retr[OF cong_gen_cong])
done
end
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
then show "base.cong (step.gen_cong R)"
by (auto simp: base.cong_def step.equivp_gen_cong)
qed
end
named_theorems friend_of_corec_simps
ML_file \<open>../Tools/BNF/bnf_gfp_grec_tactics.ML\<close>
ML_file \<open>../Tools/BNF/bnf_gfp_grec.ML\<close>
ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar_util.ML\<close>
ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML\<close>
ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar.ML\<close>
ML_file \<open>../Tools/BNF/bnf_gfp_grec_unique_sugar.ML\<close>
method_setup transfer_prover_eq = \<open>
Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
\<close> "apply transfer_prover after folding relator_eq"
method_setup corec_unique = \<open>
Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Unique_Sugar.corec_unique_tac)
\<close> "prove uniqueness of corecursive equation"
end
¤ Dauer der Verarbeitung: 0.76 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
