Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: BNF_Corec.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.