src/HOL/Library/BNF_Corec.thy
 author Manuel Eberl Mon Mar 26 16:14:16 2018 +0200 (18 months ago) changeset 67951 655aa11359dc parent 67613 ce654b0e6d69 child 69605 a96320074298 permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
```     1 (*  Title:      HOL/Library/BNF_Corec.thy
```
```     2     Author:     Jasmin Blanchette, Inria, LORIA, MPII
```
```     3     Author:     Aymeric Bouzy, Ecole polytechnique
```
```     4     Author:     Dmitriy Traytel, ETH Zurich
```
```     5     Copyright   2015, 2016
```
```     6
```
```     7 Generalized corecursor sugar ("corec" and friends).
```
```     8 *)
```
```     9
```
```    10 section \<open>Generalized Corecursor Sugar (corec and friends)\<close>
```
```    11
```
```    12 theory BNF_Corec
```
```    13 imports Main
```
```    14 keywords
```
```    15   "corec" :: thy_decl and
```
```    16   "corecursive" :: thy_goal and
```
```    17   "friend_of_corec" :: thy_goal and
```
```    18   "coinduction_upto" :: thy_decl
```
```    19 begin
```
```    20
```
```    21 lemma obj_distinct_prems: "P \<longrightarrow> P \<longrightarrow> Q \<Longrightarrow> P \<Longrightarrow> Q"
```
```    22   by auto
```
```    23
```
```    24 lemma inject_refine: "g (f x) = x \<Longrightarrow> g (f y) = y \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
```
```    25   by (metis (no_types))
```
```    26
```
```    27 lemma convol_apply: "BNF_Def.convol f g x = (f x, g x)"
```
```    28   unfolding convol_def ..
```
```    29
```
```    30 lemma Grp_UNIV_id: "BNF_Def.Grp UNIV id = (=)"
```
```    31   unfolding BNF_Def.Grp_def by auto
```
```    32
```
```    33 lemma sum_comp_cases:
```
```    34   assumes "f \<circ> Inl = g \<circ> Inl" and "f \<circ> Inr = g \<circ> Inr"
```
```    35   shows "f = g"
```
```    36 proof (rule ext)
```
```    37   fix a show "f a = g a"
```
```    38     using assms unfolding comp_def fun_eq_iff by (cases a) auto
```
```    39 qed
```
```    40
```
```    41 lemma case_sum_Inl_Inr_L: "case_sum (f \<circ> Inl) (f \<circ> Inr) = f"
```
```    42   by (metis case_sum_expand_Inr')
```
```    43
```
```    44 lemma eq_o_InrI: "\<lbrakk>g \<circ> Inl = h; case_sum h f = g\<rbrakk> \<Longrightarrow> f = g \<circ> Inr"
```
```    45   by (auto simp: fun_eq_iff split: sum.splits)
```
```    46
```
```    47 lemma id_bnf_o: "BNF_Composition.id_bnf \<circ> f = f"
```
```    48   unfolding BNF_Composition.id_bnf_def by (rule o_def)
```
```    49
```
```    50 lemma o_id_bnf: "f \<circ> BNF_Composition.id_bnf = f"
```
```    51   unfolding BNF_Composition.id_bnf_def by (rule o_def)
```
```    52
```
```    53 lemma if_True_False:
```
```    54   "(if P then True else Q) \<longleftrightarrow> P \<or> Q"
```
```    55   "(if P then False else Q) \<longleftrightarrow> \<not> P \<and> Q"
```
```    56   "(if P then Q else True) \<longleftrightarrow> \<not> P \<or> Q"
```
```    57   "(if P then Q else False) \<longleftrightarrow> P \<and> Q"
```
```    58   by auto
```
```    59
```
```    60 lemma if_distrib_fun: "(if c then f else g) x = (if c then f x else g x)"
```
```    61   by simp
```
```    62
```
```    63
```
```    64 subsection \<open>Coinduction\<close>
```
```    65
```
```    66 lemma eq_comp_compI: "a \<circ> b = f \<circ> x \<Longrightarrow> x \<circ> c = id \<Longrightarrow> f = a \<circ> (b \<circ> c)"
```
```    67   unfolding fun_eq_iff by simp
```
```    68
```
```    69 lemma self_bounded_weaken_left: "(a :: 'a :: semilattice_inf) \<le> inf a b \<Longrightarrow> a \<le> b"
```
```    70   by (erule le_infE)
```
```    71
```
```    72 lemma self_bounded_weaken_right: "(a :: 'a :: semilattice_inf) \<le> inf b a \<Longrightarrow> a \<le> b"
```
```    73   by (erule le_infE)
```
```    74
```
```    75 lemma symp_iff: "symp R \<longleftrightarrow> R = R\<inverse>\<inverse>"
```
```    76   by (metis antisym conversep.cases conversep_le_swap predicate2I symp_def)
```
```    77
```
```    78 lemma equivp_inf: "\<lbrakk>equivp R; equivp S\<rbrakk> \<Longrightarrow> equivp (inf R S)"
```
```    79   unfolding equivp_def inf_fun_def inf_bool_def by metis
```
```    80
```
```    81 lemma vimage2p_rel_prod:
```
```    82   "(\<lambda>x y. rel_prod R S (BNF_Def.convol f1 g1 x) (BNF_Def.convol f2 g2 y)) =
```
```    83    (inf (BNF_Def.vimage2p f1 f2 R) (BNF_Def.vimage2p g1 g2 S))"
```
```    84   unfolding vimage2p_def rel_prod.simps convol_def by auto
```
```    85
```
```    86 lemma predicate2I_obj: "(\<forall>x y. P x y \<longrightarrow> Q x y) \<Longrightarrow> P \<le> Q"
```
```    87   by auto
```
```    88
```
```    89 lemma predicate2D_obj: "P \<le> Q \<Longrightarrow> P x y \<longrightarrow> Q x y"
```
```    90   by auto
```
```    91
```
```    92 locale cong =
```
```    93   fixes rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool)"
```
```    94     and eval :: "'b \<Rightarrow> 'a"
```
```    95     and retr :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
```
```    96   assumes rel_mono: "\<And>R S. R \<le> S \<Longrightarrow> rel R \<le> rel S"
```
```    97     and equivp_retr: "\<And>R. equivp R \<Longrightarrow> equivp (retr R)"
```
```    98     and retr_eval: "\<And>R x y. \<lbrakk>(rel_fun (rel R) R) eval eval; rel (inf R (retr R)) x y\<rbrakk> \<Longrightarrow>
```
```    99       retr R (eval x) (eval y)"
```
```   100 begin
```
```   101
```
```   102 definition cong :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
```
```   103   "cong R \<equiv> equivp R \<and> (rel_fun (rel R) R) eval eval"
```
```   104
```
```   105 lemma cong_retr: "cong R \<Longrightarrow> cong (inf R (retr R))"
```
```   106   unfolding cong_def
```
```   107   by (auto simp: rel_fun_def dest: predicate2D[OF rel_mono, rotated]
```
```   108     intro: equivp_inf equivp_retr retr_eval)
```
```   109
```
```   110 lemma cong_equivp: "cong R \<Longrightarrow> equivp R"
```
```   111   unfolding cong_def by simp
```
```   112
```
```   113 definition gen_cong :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
```
```   114   "gen_cong R j1 j2 \<equiv> \<forall>R'. R \<le> R' \<and> cong R' \<longrightarrow> R' j1 j2"
```
```   115
```
```   116 lemma gen_cong_reflp[intro, simp]: "x = y \<Longrightarrow> gen_cong R x y"
```
```   117   unfolding gen_cong_def by (auto dest: cong_equivp equivp_reflp)
```
```   118
```
```   119 lemma gen_cong_symp[intro]: "gen_cong R x y \<Longrightarrow> gen_cong R y x"
```
```   120   unfolding gen_cong_def by (auto dest: cong_equivp equivp_symp)
```
```   121
```
```   122 lemma gen_cong_transp[intro]: "gen_cong R x y \<Longrightarrow> gen_cong R y z \<Longrightarrow> gen_cong R x z"
```
```   123   unfolding gen_cong_def by (auto dest: cong_equivp equivp_transp)
```
```   124
```
```   125 lemma equivp_gen_cong: "equivp (gen_cong R)"
```
```   126   by (intro equivpI reflpI sympI transpI) auto
```
```   127
```
```   128 lemma leq_gen_cong: "R \<le> gen_cong R"
```
```   129   unfolding gen_cong_def[abs_def] by auto
```
```   130
```
```   131 lemmas imp_gen_cong[intro] = predicate2D[OF leq_gen_cong]
```
```   132
```
```   133 lemma gen_cong_minimal: "\<lbrakk>R \<le> R'; cong R'\<rbrakk> \<Longrightarrow> gen_cong R \<le> R'"
```
```   134   unfolding gen_cong_def[abs_def] by (rule predicate2I) metis
```
```   135
```
```   136 lemma congdd_base_gen_congdd_base_aux:
```
```   137   "rel (gen_cong R) x y \<Longrightarrow> R \<le> R' \<Longrightarrow> cong R' \<Longrightarrow> R' (eval x) (eval y)"
```
```   138    by (force simp: rel_fun_def gen_cong_def cong_def dest: spec[of _ R'] predicate2D[OF rel_mono, rotated -1, of _ _ _ R'])
```
```   139
```
```   140 lemma cong_gen_cong: "cong (gen_cong R)"
```
```   141 proof -
```
```   142   { fix R' x y
```
```   143     have "rel (gen_cong R) x y \<Longrightarrow> R \<le> R' \<Longrightarrow> cong R' \<Longrightarrow> R' (eval x) (eval y)"
```
```   144       by (force simp: rel_fun_def gen_cong_def cong_def dest: spec[of _ R']
```
```   145         predicate2D[OF rel_mono, rotated -1, of _ _ _ R'])
```
```   146   }
```
```   147   then show "cong (gen_cong R)" by (auto simp: equivp_gen_cong rel_fun_def gen_cong_def cong_def)
```
```   148 qed
```
```   149
```
```   150 lemma gen_cong_eval_rel_fun:
```
```   151   "(rel_fun (rel (gen_cong R)) (gen_cong R)) eval eval"
```
```   152   using cong_gen_cong[of R] unfolding cong_def by simp
```
```   153
```
```   154 lemma gen_cong_eval:
```
```   155   "rel (gen_cong R) x y \<Longrightarrow> gen_cong R (eval x) (eval y)"
```
```   156   by (erule rel_funD[OF gen_cong_eval_rel_fun])
```
```   157
```
```   158 lemma gen_cong_idem: "gen_cong (gen_cong R) = gen_cong R"
```
```   159   by (simp add: antisym cong_gen_cong gen_cong_minimal leq_gen_cong)
```
```   160
```
```   161 lemma gen_cong_rho:
```
```   162   "\<rho> = eval \<circ> f \<Longrightarrow> rel (gen_cong R) (f x) (f y) \<Longrightarrow> gen_cong R (\<rho> x) (\<rho> y)"
```
```   163   by (simp add: gen_cong_eval)
```
```   164 lemma coinduction:
```
```   165   assumes coind: "\<forall>R. R \<le> retr R \<longrightarrow> R \<le> (=)"
```
```   166   assumes cih: "R \<le> retr (gen_cong R)"
```
```   167   shows "R \<le> (=)"
```
```   168   apply (rule order_trans[OF leq_gen_cong mp[OF spec[OF coind]]])
```
```   169   apply (rule self_bounded_weaken_left[OF gen_cong_minimal])
```
```   170    apply (rule inf_greatest[OF leq_gen_cong cih])
```
```   171   apply (rule cong_retr[OF cong_gen_cong])
```
```   172   done
```
```   173
```
```   174 end
```
```   175
```
```   176 lemma rel_sum_case_sum:
```
```   177   "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)"
```
```   178   by (auto simp: rel_fun_def rel_sum.simps split: sum.splits)
```
```   179
```
```   180 context
```
```   181   fixes rel eval rel' eval' retr emb
```
```   182   assumes base: "cong rel eval retr"
```
```   183   and step: "cong rel' eval' retr"
```
```   184   and emb: "eval' \<circ> emb = eval"
```
```   185   and emb_transfer: "rel_fun (rel R) (rel' R) emb emb"
```
```   186 begin
```
```   187
```
```   188 interpretation base: cong rel eval retr by (rule base)
```
```   189 interpretation step: cong rel' eval' retr by (rule step)
```
```   190
```
```   191 lemma gen_cong_emb: "base.gen_cong R \<le> step.gen_cong R"
```
```   192 proof (rule base.gen_cong_minimal[OF step.leq_gen_cong])
```
```   193   note step.gen_cong_eval_rel_fun[transfer_rule] emb_transfer[transfer_rule]
```
```   194   have "(rel_fun (rel (step.gen_cong R)) (step.gen_cong R)) eval eval"
```
```   195     unfolding emb[symmetric] by transfer_prover
```
```   196   then show "base.cong (step.gen_cong R)"
```
```   197     by (auto simp: base.cong_def step.equivp_gen_cong)
```
```   198 qed
```
```   199
```
```   200 end
```
```   201
```
```   202 named_theorems friend_of_corec_simps
```
```   203
```
```   204 ML_file "../Tools/BNF/bnf_gfp_grec_tactics.ML"
```
```   205 ML_file "../Tools/BNF/bnf_gfp_grec.ML"
```
```   206 ML_file "../Tools/BNF/bnf_gfp_grec_sugar_util.ML"
```
```   207 ML_file "../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
```
```   208 ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML"
```
```   209 ML_file "../Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
```
```   210
```
```   211 method_setup transfer_prover_eq = \<open>
```
```   212   Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
```
```   213 \<close> "apply transfer_prover after folding relator_eq"
```
```   214
```
```   215 method_setup corec_unique = \<open>
```
```   216   Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Unique_Sugar.corec_unique_tac)
```
```   217 \<close> "prove uniqueness of corecursive equation"
```
```   218
```
```   219 end
```