equal
deleted
inserted
replaced
6 imports Abs_Int_init |
6 imports Abs_Int_init |
7 begin |
7 begin |
8 |
8 |
9 subsubsection "Orderings" |
9 subsubsection "Orderings" |
10 |
10 |
11 text\<open>The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are |
11 text\<open>The basic type classes \<^class>\<open>order\<close>, \<^class>\<open>semilattice_sup\<close> and \<^class>\<open>order_top\<close> are |
12 defined in @{theory Main}, more precisely in theories @{theory HOL.Orderings} and @{theory HOL.Lattices}. |
12 defined in \<^theory>\<open>Main\<close>, more precisely in theories \<^theory>\<open>HOL.Orderings\<close> and \<^theory>\<open>HOL.Lattices\<close>. |
13 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> |
14 |
14 |
15 class semilattice_sup_top = semilattice_sup + order_top |
15 class semilattice_sup_top = semilattice_sup + order_top |
16 |
16 |
17 |
17 |
162 and gamma_plus': "i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1+i2 \<in> \<gamma>(plus' a1 a2)" |
162 and gamma_plus': "i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1+i2 \<in> \<gamma>(plus' a1 a2)" |
163 |
163 |
164 type_synonym 'av st = "(vname \<Rightarrow> 'av)" |
164 type_synonym 'av st = "(vname \<Rightarrow> 'av)" |
165 |
165 |
166 text\<open>The for-clause (here and elsewhere) only serves the purpose of fixing |
166 text\<open>The for-clause (here and elsewhere) only serves the purpose of fixing |
167 the name of the type parameter @{typ 'av} which would otherwise be renamed to |
167 the name of the type parameter \<^typ>\<open>'av\<close> which would otherwise be renamed to |
168 @{typ 'a}.\<close> |
168 \<^typ>\<open>'a\<close>.\<close> |
169 |
169 |
170 locale Abs_Int_fun = Val_semilattice where \<gamma>=\<gamma> |
170 locale Abs_Int_fun = Val_semilattice where \<gamma>=\<gamma> |
171 for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set" |
171 for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set" |
172 begin |
172 begin |
173 |
173 |
352 for m :: "'av::semilattice_sup_top \<Rightarrow> nat" + |
352 for m :: "'av::semilattice_sup_top \<Rightarrow> nat" + |
353 assumes m2: "x < y \<Longrightarrow> m x > m y" |
353 assumes m2: "x < y \<Longrightarrow> m x > m y" |
354 begin |
354 begin |
355 |
355 |
356 text\<open>The predicates \<open>top_on_ty a X\<close> that follow describe that any abstract |
356 text\<open>The predicates \<open>top_on_ty a X\<close> that follow describe that any abstract |
357 state in \<open>a\<close> maps all variables in \<open>X\<close> to @{term \<top>}. |
357 state in \<open>a\<close> maps all variables in \<open>X\<close> to \<^term>\<open>\<top>\<close>. |
358 This is an important invariant for the termination proof where we argue that only |
358 This is an important invariant for the termination proof where we argue that only |
359 the finitely many variables in the program change. That the others do not change |
359 the finitely many variables in the program change. That the others do not change |
360 follows because they remain @{term \<top>}.\<close> |
360 follows because they remain \<^term>\<open>\<top>\<close>.\<close> |
361 |
361 |
362 fun top_on_st :: "'av st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>s") where |
362 fun top_on_st :: "'av st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>s") where |
363 "top_on_st S X = (\<forall>x\<in>X. S x = \<top>)" |
363 "top_on_st S X = (\<forall>x\<in>X. S x = \<top>)" |
364 |
364 |
365 fun top_on_opt :: "'av st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>o") where |
365 fun top_on_opt :: "'av st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>o") where |