1(*  Title:      HOL/Corec_Examples/Tests/Merge_A.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_A
12imports "HOL-Library.BNF_Corec"
13begin
14
15codatatype 'a ta = Ca (sa1: 'a) (sa2: "'a ta")
16
17consts gb :: "'a ta \<Rightarrow> 'a ta"
18
19corec fa where
20  "fa = Ca (Suc 0) fa"
21
22corec ga :: "'a ta \<Rightarrow> 'a ta" where
23  "ga t = Ca (sa1 t) (sa2 t)"
24
25friend_of_corec ga :: "'a ta \<Rightarrow> 'a ta" where
26  "ga t = Ca (sa1 t) (Ca (sa1 t) (sa2 t))"
27  sorry
28
29thm ta.coinduct_upto
30thm ta.cong_refl
31
32end
33