author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64379  71f42dcaa1df 
child 67091  1393c2340eec 
permissions  rwrr 
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

1 
(* Title: HOL/Library/BNF_Corec.thy 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, Inria, LORIA, MPII 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

3 
Author: Aymeric Bouzy, Ecole polytechnique 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

4 
Author: Dmitriy Traytel, ETH Zurich 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

5 
Copyright 2015, 2016 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

6 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

7 
Generalized corecursor sugar ("corec" and friends). 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

8 
*) 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

9 

62700  10 
section \<open>Generalized Corecursor Sugar (corec and friends)\<close> 
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

11 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

12 
theory BNF_Corec 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

13 
imports Main 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

14 
keywords 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

15 
"corec" :: thy_decl and 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

16 
"corecursive" :: thy_goal and 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

17 
"friend_of_corec" :: thy_goal and 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

18 
"coinduction_upto" :: thy_decl 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

19 
begin 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

20 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

22 
by auto 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

23 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

25 
by (metis (no_types)) 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

26 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

28 
unfolding convol_def .. 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

29 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

31 
unfolding BNF_Def.Grp_def by auto 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

32 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

33 
lemma sum_comp_cases: 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

35 
shows "f = g" 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

36 
proof (rule ext) 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

37 
fix a show "f a = g a" 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

39 
qed 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

40 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

42 
by (metis case_sum_expand_Inr') 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

43 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

46 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

49 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

52 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

53 
lemma if_True_False: 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

58 
by auto 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

59 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

61 
by simp 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

62 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

63 

62700  64 
subsection \<open>Coinduction\<close> 
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

65 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

67 
unfolding fun_eq_iff by simp 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

68 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

70 
by (erule le_infE) 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

71 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

73 
by (erule le_infE) 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

74 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

77 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

80 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

81 
lemma vimage2p_rel_prod: 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

85 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

87 
by auto 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

88 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

90 
by auto 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

91 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

92 
locale cong = 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

94 
and eval :: "'b \<Rightarrow> 'a" 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

99 
retr R (eval x) (eval y)" 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

100 
begin 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

101 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

104 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

106 
unfolding cong_def 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

108 
intro: equivp_inf equivp_retr retr_eval) 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

109 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

111 
unfolding cong_def by simp 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

112 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

115 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

118 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

121 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

124 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

126 
by (intro equivpI reflpI sympI transpI) auto 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

127 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

130 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

132 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

135 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

136 
lemma congdd_base_gen_congdd_base_aux: 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

139 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

141 
proof  
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

142 
{ fix R' x y 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

146 
} 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

148 
qed 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

149 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

150 
lemma gen_cong_eval_rel_fun: 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

153 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

154 
lemma gen_cong_eval: 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

157 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

160 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

161 
lemma gen_cong_rho: 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

163 
by (simp add: gen_cong_eval) 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

164 
lemma coinduction: 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

167 
shows "R \<le> op =" 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

172 
done 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

173 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

174 
end 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

175 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

176 
lemma rel_sum_case_sum: 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

179 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

180 
context 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

181 
fixes rel eval rel' eval' retr emb 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

182 
assumes base: "cong rel eval retr" 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

183 
and step: "cong rel' eval' retr" 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

184 
and emb: "eval' o emb = eval" 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

186 
begin 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

187 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

190 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

195 
unfolding emb[symmetric] by transfer_prover 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

198 
qed 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

199 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

200 
end 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

201 

64379
71f42dcaa1df
additional userspecified simp (naturality) rules used in friend_of_corec
traytel
parents:
64378
diff
changeset

202 
named_theorems friend_of_corec_simps 
71f42dcaa1df
additional userspecified 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

210 

64378  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 

62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

215 
method_setup corec_unique = \<open> 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec 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/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

217 
\<close> "prove uniqueness of corecursive equation" 
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

218 

0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprimcorec to Isabelle
blanchet
parents:
diff
changeset

219 
end 