src/HOL/Library/BNF_Corec.thy
changeset 62692 0701f25fac39
child 62700 e3ca8dc01c4f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/BNF_Corec.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,213 @@
     1.4 +(*  Title:      HOL/Library/BNF_Corec.thy
     1.5 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
     1.6 +    Author:     Aymeric Bouzy, Ecole polytechnique
     1.7 +    Author:     Dmitriy Traytel, ETH Zurich
     1.8 +    Copyright   2015, 2016
     1.9 +
    1.10 +Generalized corecursor sugar ("corec" and friends).
    1.11 +*)
    1.12 +
    1.13 +chapter {* Generalized Corecursor Sugar (corec and friends) *}
    1.14 +
    1.15 +theory BNF_Corec
    1.16 +imports Main
    1.17 +keywords
    1.18 +  "corec" :: thy_decl and
    1.19 +  "corecursive" :: thy_goal and
    1.20 +  "friend_of_corec" :: thy_goal and
    1.21 +  "coinduction_upto" :: thy_decl
    1.22 +begin
    1.23 +
    1.24 +lemma obj_distinct_prems: "P \<longrightarrow> P \<longrightarrow> Q \<Longrightarrow> P \<Longrightarrow> Q"
    1.25 +  by auto
    1.26 +
    1.27 +lemma inject_refine: "g (f x) = x \<Longrightarrow> g (f y) = y \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
    1.28 +  by (metis (no_types))
    1.29 +
    1.30 +lemma convol_apply: "BNF_Def.convol f g x = (f x, g x)"
    1.31 +  unfolding convol_def ..
    1.32 +
    1.33 +lemma Grp_UNIV_id: "BNF_Def.Grp UNIV id = (op =)"
    1.34 +  unfolding BNF_Def.Grp_def by auto
    1.35 +
    1.36 +lemma sum_comp_cases:
    1.37 +  assumes "f o Inl = g o Inl" and "f o Inr = g o Inr"
    1.38 +  shows "f = g"
    1.39 +proof (rule ext)
    1.40 +  fix a show "f a = g a"
    1.41 +    using assms unfolding comp_def fun_eq_iff by (cases a) auto
    1.42 +qed
    1.43 +
    1.44 +lemma case_sum_Inl_Inr_L: "case_sum (f o Inl) (f o Inr) = f"
    1.45 +  by (metis case_sum_expand_Inr')
    1.46 +
    1.47 +lemma eq_o_InrI: "\<lbrakk>g o Inl = h; case_sum h f = g\<rbrakk> \<Longrightarrow> f = g o Inr"
    1.48 +  by (auto simp: fun_eq_iff split: sum.splits)
    1.49 +
    1.50 +lemma id_bnf_o: "BNF_Composition.id_bnf \<circ> f = f"
    1.51 +  unfolding BNF_Composition.id_bnf_def by (rule o_def)
    1.52 +
    1.53 +lemma o_id_bnf: "f \<circ> BNF_Composition.id_bnf = f"
    1.54 +  unfolding BNF_Composition.id_bnf_def by (rule o_def)
    1.55 +
    1.56 +lemma if_True_False:
    1.57 +  "(if P then True else Q) \<longleftrightarrow> P \<or> Q"
    1.58 +  "(if P then False else Q) \<longleftrightarrow> \<not> P \<and> Q"
    1.59 +  "(if P then Q else True) \<longleftrightarrow> \<not> P \<or> Q"
    1.60 +  "(if P then Q else False) \<longleftrightarrow> P \<and> Q"
    1.61 +  by auto
    1.62 +
    1.63 +lemma if_distrib_fun: "(if c then f else g) x = (if c then f x else g x)"
    1.64 +  by simp
    1.65 +
    1.66 +
    1.67 +section \<open>Coinduction\<close>
    1.68 +
    1.69 +lemma eq_comp_compI: "a o b = f o x \<Longrightarrow> x o c = id \<Longrightarrow> f = a o (b o c)"
    1.70 +  unfolding fun_eq_iff by simp
    1.71 +
    1.72 +lemma self_bounded_weaken_left: "(a :: 'a :: semilattice_inf) \<le> inf a b \<Longrightarrow> a \<le> b"
    1.73 +  by (erule le_infE)
    1.74 +
    1.75 +lemma self_bounded_weaken_right: "(a :: 'a :: semilattice_inf) \<le> inf b a \<Longrightarrow> a \<le> b"
    1.76 +  by (erule le_infE)
    1.77 +
    1.78 +lemma symp_iff: "symp R \<longleftrightarrow> R = R^--1"
    1.79 +  by (metis antisym conversep.cases conversep_le_swap predicate2I symp_def)
    1.80 +
    1.81 +lemma equivp_inf: "\<lbrakk>equivp R; equivp S\<rbrakk> \<Longrightarrow> equivp (inf R S)"
    1.82 +  unfolding equivp_def inf_fun_def inf_bool_def by metis
    1.83 +
    1.84 +lemma vimage2p_rel_prod:
    1.85 +  "(\<lambda>x y. rel_prod R S (BNF_Def.convol f1 g1 x) (BNF_Def.convol f2 g2 y)) =
    1.86 +   (inf (BNF_Def.vimage2p f1 f2 R) (BNF_Def.vimage2p g1 g2 S))"
    1.87 +  unfolding vimage2p_def rel_prod.simps convol_def by auto
    1.88 +
    1.89 +lemma predicate2I_obj: "(\<forall>x y. P x y \<longrightarrow> Q x y) \<Longrightarrow> P \<le> Q"
    1.90 +  by auto
    1.91 +
    1.92 +lemma predicate2D_obj: "P \<le> Q \<Longrightarrow> P x y \<longrightarrow> Q x y"
    1.93 +  by auto
    1.94 +
    1.95 +locale cong =
    1.96 +  fixes rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool)"
    1.97 +    and eval :: "'b \<Rightarrow> 'a"
    1.98 +    and retr :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
    1.99 +  assumes rel_mono: "\<And>R S. R \<le> S \<Longrightarrow> rel R \<le> rel S"
   1.100 +    and equivp_retr: "\<And>R. equivp R \<Longrightarrow> equivp (retr R)"
   1.101 +    and retr_eval: "\<And>R x y. \<lbrakk>(rel_fun (rel R) R) eval eval; rel (inf R (retr R)) x y\<rbrakk> \<Longrightarrow>
   1.102 +      retr R (eval x) (eval y)"
   1.103 +begin
   1.104 +
   1.105 +definition cong :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.106 +  "cong R \<equiv> equivp R \<and> (rel_fun (rel R) R) eval eval"
   1.107 +
   1.108 +lemma cong_retr: "cong R \<Longrightarrow> cong (inf R (retr R))"
   1.109 +  unfolding cong_def
   1.110 +  by (auto simp: rel_fun_def dest: predicate2D[OF rel_mono, rotated]
   1.111 +    intro: equivp_inf equivp_retr retr_eval)
   1.112 +
   1.113 +lemma cong_equivp: "cong R \<Longrightarrow> equivp R"
   1.114 +  unfolding cong_def by simp
   1.115 +
   1.116 +definition gen_cong :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
   1.117 +  "gen_cong R j1 j2 \<equiv> \<forall>R'. R \<le> R' \<and> cong R' \<longrightarrow> R' j1 j2"
   1.118 +
   1.119 +lemma gen_cong_reflp[intro, simp]: "x = y \<Longrightarrow> gen_cong R x y"
   1.120 +  unfolding gen_cong_def by (auto dest: cong_equivp equivp_reflp)
   1.121 +
   1.122 +lemma gen_cong_symp[intro]: "gen_cong R x y \<Longrightarrow> gen_cong R y x"
   1.123 +  unfolding gen_cong_def by (auto dest: cong_equivp equivp_symp)
   1.124 +
   1.125 +lemma gen_cong_transp[intro]: "gen_cong R x y \<Longrightarrow> gen_cong R y z \<Longrightarrow> gen_cong R x z"
   1.126 +  unfolding gen_cong_def by (auto dest: cong_equivp equivp_transp)
   1.127 +
   1.128 +lemma equivp_gen_cong: "equivp (gen_cong R)"
   1.129 +  by (intro equivpI reflpI sympI transpI) auto
   1.130 +
   1.131 +lemma leq_gen_cong: "R \<le> gen_cong R"
   1.132 +  unfolding gen_cong_def[abs_def] by auto
   1.133 +
   1.134 +lemmas imp_gen_cong[intro] = predicate2D[OF leq_gen_cong]
   1.135 +
   1.136 +lemma gen_cong_minimal: "\<lbrakk>R \<le> R'; cong R'\<rbrakk> \<Longrightarrow> gen_cong R \<le> R'"
   1.137 +  unfolding gen_cong_def[abs_def] by (rule predicate2I) metis
   1.138 +
   1.139 +lemma congdd_base_gen_congdd_base_aux:
   1.140 +  "rel (gen_cong R) x y \<Longrightarrow> R \<le> R' \<Longrightarrow> cong R' \<Longrightarrow> R' (eval x) (eval y)"
   1.141 +   by (force simp: rel_fun_def gen_cong_def cong_def dest: spec[of _ R'] predicate2D[OF rel_mono, rotated -1, of _ _ _ R'])
   1.142 +
   1.143 +lemma cong_gen_cong: "cong (gen_cong R)"
   1.144 +proof -
   1.145 +  { fix R' x y
   1.146 +    have "rel (gen_cong R) x y \<Longrightarrow> R \<le> R' \<Longrightarrow> cong R' \<Longrightarrow> R' (eval x) (eval y)"
   1.147 +      by (force simp: rel_fun_def gen_cong_def cong_def dest: spec[of _ R']
   1.148 +        predicate2D[OF rel_mono, rotated -1, of _ _ _ R'])
   1.149 +  }
   1.150 +  then show "cong (gen_cong R)" by (auto simp: equivp_gen_cong rel_fun_def gen_cong_def cong_def)
   1.151 +qed
   1.152 +
   1.153 +lemma gen_cong_eval_rel_fun:
   1.154 +  "(rel_fun (rel (gen_cong R)) (gen_cong R)) eval eval"
   1.155 +  using cong_gen_cong[of R] unfolding cong_def by simp
   1.156 +
   1.157 +lemma gen_cong_eval:
   1.158 +  "rel (gen_cong R) x y \<Longrightarrow> gen_cong R (eval x) (eval y)"
   1.159 +  by (erule rel_funD[OF gen_cong_eval_rel_fun])
   1.160 +
   1.161 +lemma gen_cong_idem: "gen_cong (gen_cong R) = gen_cong R"
   1.162 +  by (simp add: antisym cong_gen_cong gen_cong_minimal leq_gen_cong)
   1.163 +
   1.164 +lemma gen_cong_rho:
   1.165 +  "\<rho> = eval o f \<Longrightarrow> rel (gen_cong R) (f x) (f y) \<Longrightarrow> gen_cong R (\<rho> x) (\<rho> y)"
   1.166 +  by (simp add: gen_cong_eval)
   1.167 +lemma coinduction:
   1.168 +  assumes coind: "\<forall>R. R \<le> retr R \<longrightarrow> R \<le> op ="
   1.169 +  assumes cih: "R \<le> retr (gen_cong R)"
   1.170 +  shows "R \<le> op ="
   1.171 +  apply (rule order_trans[OF leq_gen_cong mp[OF spec[OF coind]]])
   1.172 +  apply (rule self_bounded_weaken_left[OF gen_cong_minimal])
   1.173 +   apply (rule inf_greatest[OF leq_gen_cong cih])
   1.174 +  apply (rule cong_retr[OF cong_gen_cong])
   1.175 +  done
   1.176 +
   1.177 +end
   1.178 +
   1.179 +lemma rel_sum_case_sum:
   1.180 +  "rel_fun (rel_sum R S) T (case_sum f1 g1) (case_sum f2 g2) = (rel_fun R T f1 f2 \<and> rel_fun S T g1 g2)"
   1.181 +  by (auto simp: rel_fun_def rel_sum.simps split: sum.splits)
   1.182 +
   1.183 +context
   1.184 +  fixes rel eval rel' eval' retr emb
   1.185 +  assumes base: "cong rel eval retr"
   1.186 +  and step: "cong rel' eval' retr"
   1.187 +  and emb: "eval' o emb = eval"
   1.188 +  and emb_transfer: "rel_fun (rel R) (rel' R) emb emb"
   1.189 +begin
   1.190 +
   1.191 +interpretation base: cong rel eval retr by (rule base)
   1.192 +interpretation step: cong rel' eval' retr by (rule step)
   1.193 +
   1.194 +lemma gen_cong_emb: "base.gen_cong R \<le> step.gen_cong R"
   1.195 +proof (rule base.gen_cong_minimal[OF step.leq_gen_cong])
   1.196 +  note step.gen_cong_eval_rel_fun[transfer_rule] emb_transfer[transfer_rule]
   1.197 +  have "(rel_fun (rel (step.gen_cong R)) (step.gen_cong R)) eval eval"
   1.198 +    unfolding emb[symmetric] by transfer_prover
   1.199 +  then show "base.cong (step.gen_cong R)"
   1.200 +    by (auto simp: base.cong_def step.equivp_gen_cong)
   1.201 +qed
   1.202 +
   1.203 +end
   1.204 +
   1.205 +ML_file "../Tools/BNF/bnf_gfp_grec_tactics.ML"
   1.206 +ML_file "../Tools/BNF/bnf_gfp_grec.ML"
   1.207 +ML_file "../Tools/BNF/bnf_gfp_grec_sugar_util.ML"
   1.208 +ML_file "../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
   1.209 +ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML"
   1.210 +ML_file "../Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
   1.211 +
   1.212 +method_setup corec_unique = \<open>
   1.213 +  Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Unique_Sugar.corec_unique_tac)
   1.214 +\<close> "prove uniqueness of corecursive equation"
   1.215 +
   1.216 +end