author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 64379 | 71f42dcaa1df |
child 67399 | eab6ce8368fa |
permissions | -rw-r--r-- |
64379
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
1 |
theory Iterate_GPV imports |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
64379
diff
changeset
|
2 |
"HOL-Library.BNF_Axiomatization" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
64379
diff
changeset
|
3 |
"HOL-Library.BNF_Corec" |
64379
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
4 |
begin |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
5 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
6 |
declare [[typedef_overloaded]] |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
7 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
8 |
datatype 'a spmf = return_spmf 'a |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
9 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
10 |
primrec (transfer) bind_spmf where |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
11 |
"bind_spmf (return_spmf a) f = f a" |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
12 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
13 |
datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
14 |
= Pure (result: 'a) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
15 |
| IO ("output": 'b) (continuation: "'c") |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
16 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
17 |
codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
18 |
= GPV (the_gpv: "('a, 'out, 'in \<Rightarrow> ('a, 'out, 'in) gpv) generat spmf") |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
19 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
20 |
declare gpv.rel_eq [relator_eq] |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
21 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
22 |
primcorec bind_gpv :: "('a, 'out, 'in) gpv \<Rightarrow> ('a \<Rightarrow> ('b, 'out, 'in) gpv) \<Rightarrow> ('b, 'out, 'in) gpv" |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
23 |
where |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
24 |
"bind_gpv r f = GPV (map_spmf (map_generat id id (op \<circ> (case_sum id (\<lambda>r. bind_gpv r f)))) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
25 |
(bind_spmf (the_gpv r) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
26 |
(case_generat |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
27 |
(\<lambda>x. map_spmf (map_generat id id (op \<circ> Inl)) (the_gpv (f x))) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
28 |
(\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))" |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
29 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
30 |
context includes lifting_syntax begin |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
31 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
32 |
lemma bind_gpv_parametric [transfer_rule]: |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
33 |
"(rel_gpv A C ===> (A ===> rel_gpv B C) ===> rel_gpv B C) bind_gpv bind_gpv" |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
34 |
unfolding bind_gpv_def by transfer_prover |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
35 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
36 |
end |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
37 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
38 |
lemma [friend_of_corec_simps]: |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
39 |
"map_spmf f (bind_spmf x h) = bind_spmf x (map_spmf f o h)" |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
40 |
by (cases x) auto |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
41 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
42 |
lemma [friend_of_corec_simps]: |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
43 |
"bind_spmf (map_spmf f x) h = bind_spmf x (h o f)" |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
44 |
by (cases x) auto |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
45 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
46 |
friend_of_corec bind_gpv :: "('a, 'out, 'in) gpv \<Rightarrow> ('a \<Rightarrow> ('a, 'out, 'in) gpv) \<Rightarrow> ('a, 'out, 'in) gpv" |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
47 |
where "bind_gpv r f = GPV (map_spmf (map_generat id id (op \<circ> (case_sum id (\<lambda>r. bind_gpv r f)))) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
48 |
(bind_spmf (the_gpv r) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
49 |
(case_generat |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
50 |
(\<lambda>x. map_spmf (map_generat id id (op \<circ> Inl)) (the_gpv (f x))) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
51 |
(\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))" |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
52 |
apply(rule bind_gpv.ctr) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
53 |
apply transfer_prover |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
54 |
apply transfer_prover |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
55 |
done |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
56 |
|
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
diff
changeset
|
57 |
end |