equal
deleted
inserted
replaced
82 |
82 |
83 subsubsection \<open>Narrowing's basic operations\<close> |
83 subsubsection \<open>Narrowing's basic operations\<close> |
84 |
84 |
85 type_synonym 'a narrowing = "integer => 'a narrowing_cons" |
85 type_synonym 'a narrowing = "integer => 'a narrowing_cons" |
86 |
86 |
87 definition empty :: "'a narrowing" |
|
88 where |
|
89 "empty d = Narrowing_cons (Narrowing_sum_of_products []) []" |
|
90 |
|
91 definition cons :: "'a => 'a narrowing" |
87 definition cons :: "'a => 'a narrowing" |
92 where |
88 where |
93 "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])" |
89 "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])" |
94 |
90 |
95 fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a" |
91 fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a" |