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