equal
deleted
inserted
replaced
1 (* Authors: Klaus Aehlig, Tobias Nipkow *) |
1 (* Authors: Klaus Aehlig, Tobias Nipkow *) |
2 |
2 |
3 section \<open>Testing implementation of normalization by evaluation\<close> |
3 section \<open>Testing implementation of normalization by evaluation\<close> |
4 |
4 |
5 theory Normalization_by_Evaluation |
5 theory Normalization_by_Evaluation |
6 imports Complex_Main |
6 imports Complex_Main "HOL-Library.Word" |
7 begin |
7 begin |
8 |
8 |
9 lemma "True" by normalization |
9 lemma "True" by normalization |
10 lemma "p \<longrightarrow> True" by normalization |
10 lemma "p \<longrightarrow> True" by normalization |
11 declare disj_assoc [code nbe] |
11 declare disj_assoc [code nbe] |
106 lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization |
106 lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization |
107 lemma "max (Suc 0) 0 = Suc 0" by normalization |
107 lemma "max (Suc 0) 0 = Suc 0" by normalization |
108 lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization |
108 lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization |
109 value [nbe] "Suc 0 \<in> set ms" |
109 value [nbe] "Suc 0 \<in> set ms" |
110 |
110 |
|
111 lemma "4 - 42 * 3 - 7 = (256 + 35) - (164 :: 8 word)" |
|
112 by normalization |
|
113 |
111 (* non-left-linear patterns, equality by extensionality *) |
114 (* non-left-linear patterns, equality by extensionality *) |
112 |
115 |
113 lemma "f = f" by normalization |
116 lemma "f = f" by normalization |
114 lemma "f x = f x" by normalization |
117 lemma "f x = f x" by normalization |
115 lemma "(f o g) x = f (g x)" by normalization |
118 lemma "(f o g) x = f (g x)" by normalization |