1(*  Title:      HOL/Corec_Examples/Tests/Merge_D.thy
2    Author:     Aymeric Bouzy, Ecole polytechnique
3    Author:     Jasmin Blanchette, Inria, LORIA, MPII
4    Copyright   2015, 2016
5
6Tests theory merges.
7*)
8
9section \<open>Tests Theory Merges\<close>
10
11theory Merge_D
12imports Merge_B Merge_C
13begin
14
15thm ta.coinduct_upto
16
17(* Merges files having defined their own friends and uses these friends to
18define another corecursive function. *)
19
20corec gd where
21  "gd = fc (gc (gb (fb (ga (Ca 0 gd)))))"
22
23thm gd_def
24
25term fc
26
27corec hd :: "('a::zero) ta \<Rightarrow> 'a ta" where
28  "hd s = fc (gc (gb (fb (ga (Ca 0 (hd s))))))"
29
30friend_of_corec hd where
31  "hd s = Ca 0 (fc (gc (gb (fb (ga (Ca 0 (hd s)))))))"
32  sorry
33
34corecursive (friend) ff :: "'a ta \<Rightarrow> 'a ta" where
35  "ff x = Ca undefined (ff x)"
36  sorry
37
38thm ta.cong_intros
39thm ta.cong_gb
40
41end
42