equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 subsection "Abstract Interpretation" |
2 |
4 |
3 theory Abs_Int0 |
5 theory Abs_Int0 |
4 imports Abs_Int_init |
6 imports Abs_Int_init |
5 begin |
7 begin |
6 |
8 |
7 subsection "Orderings" |
9 subsubsection "Orderings" |
8 |
10 |
9 text\<open>The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are |
11 text\<open>The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are |
10 defined in @{theory Main}, more precisely in theories @{theory HOL.Orderings} and @{theory HOL.Lattices}. |
12 defined in @{theory Main}, more precisely in theories @{theory HOL.Orderings} and @{theory HOL.Lattices}. |
11 If you view this theory with jedit, just click on the names to get there.\<close> |
13 If you view this theory with jedit, just click on the names to get there.\<close> |
12 |
14 |
137 lemma strip_pfp: |
139 lemma strip_pfp: |
138 assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0" |
140 assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0" |
139 using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp |
141 using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp |
140 |
142 |
141 |
143 |
142 subsection "Abstract Interpretation" |
144 subsubsection "Abstract Interpretation" |
143 |
145 |
144 definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where |
146 definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where |
145 "\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}" |
147 "\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}" |
146 |
148 |
147 fun \<gamma>_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where |
149 fun \<gamma>_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where |