Theory BNF_Corec

(*  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 ‹Generalized Corecursor Sugar (corec and friends)›

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 ‹Coinduction›

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 ‹../Tools/BNF/bnf_gfp_grec_tactics.ML›
ML_file ‹../Tools/BNF/bnf_gfp_grec.ML›
ML_file ‹../Tools/BNF/bnf_gfp_grec_sugar_util.ML›
ML_file ‹../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML›
ML_file ‹../Tools/BNF/bnf_gfp_grec_sugar.ML›
ML_file ‹../Tools/BNF/bnf_gfp_grec_unique_sugar.ML›

method_setup transfer_prover_eq = ‹
  Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
› "apply transfer_prover after folding relator_eq"

method_setup corec_unique = ‹
  Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Unique_Sugar.corec_unique_tac)
› "prove uniqueness of corecursive equation"

end