| author | wenzelm |
| Wed, 04 Oct 2017 12:00:53 +0200 | |
| changeset 66787 | 64b47495676d |
| parent 66453 | cc19f7ca2ed6 |
| permissions | -rw-r--r-- |
| 62696 | 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 |
||
6 |
Tests theory merges. |
|
7 |
*) |
|
8 |
||
| 62726 | 9 |
section \<open>Tests Theory Merges\<close> |
| 62696 | 10 |
|
11 |
theory Merge_A |
|
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
62726
diff
changeset
|
12 |
imports "HOL-Library.BNF_Corec" |
| 62696 | 13 |
begin |
14 |
||
15 |
codatatype 'a ta = Ca (sa1: 'a) (sa2: "'a ta") |
|
16 |
||
17 |
consts gb :: "'a ta \<Rightarrow> 'a ta" |
|
18 |
||
19 |
corec fa where |
|
20 |
"fa = Ca (Suc 0) fa" |
|
21 |
||
22 |
corec ga :: "'a ta \<Rightarrow> 'a ta" where |
|
23 |
"ga t = Ca (sa1 t) (sa2 t)" |
|
24 |
||
25 |
friend_of_corec ga :: "'a ta \<Rightarrow> 'a ta" where |
|
26 |
"ga t = Ca (sa1 t) (Ca (sa1 t) (sa2 t))" |
|
27 |
sorry |
|
28 |
||
29 |
thm ta.coinduct_upto |
|
30 |
thm ta.cong_refl |
|
31 |
||
32 |
end |