# HG changeset patch # User traytel # Date 1346687742 -7200 # Node ID ce2ef34eb82822ca61c78d1a076030d3f47f2682 # Parent 8ab9fb2483a909075c88d829fafcc4838b1ca5fe added examples for testing of coinductive witnesses diff -r 8ab9fb2483a9 -r ce2ef34eb828 src/HOL/Codatatype/Examples/Misc_Codata.thy --- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Mon Sep 03 15:50:41 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Mon Sep 03 17:55:42 2012 +0200 @@ -74,6 +74,16 @@ codata_raw less_killing: 'a = "'b \ 'c" +codata_raw + wit3_F1: 'b1 = "'a1 \ 'b1 \ 'b2" +and wit3_F2: 'b2 = "'a2 \ 'b2" +and wit3_F3: 'b3 = "'a1 \ 'a2 \ 'b1 + 'a3 \ 'a1 \ 'a2 \ 'b1" + +codata_raw + coind_wit1: 'a = "'c \ 'a \ 'b \ 'd" +and coind_wit2: 'd = "'d \ 'e + 'c \ 'g" +and ind_wit: 'b = "unit + 'c" + (* SLOW, MEMORY-HUNGRY codata_raw K1': 'K1 = "'K2 + 'a list" and K2': 'K2 = "'K3 + 'c fset"