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