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