equal
deleted
inserted
replaced
98 |
98 |
99 |
99 |
100 subsubsection "Termination" |
100 subsubsection "Termination" |
101 |
101 |
102 locale Measure1 = |
102 locale Measure1 = |
103 fixes m :: "'av::{order,top} \<Rightarrow> nat" |
103 fixes m :: "'av::{order,order_top} \<Rightarrow> nat" |
104 fixes h :: "nat" |
104 fixes h :: "nat" |
105 assumes h: "m x \<le> h" |
105 assumes h: "m x \<le> h" |
106 begin |
106 begin |
107 |
107 |
108 definition m_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^isub>s") where |
108 definition m_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^isub>s") where |
132 finally show ?thesis . |
132 finally show ?thesis . |
133 qed |
133 qed |
134 |
134 |
135 end |
135 end |
136 |
136 |
137 fun top_on_st :: "'a::top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where |
137 fun top_on_st :: "'a::order_top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where |
138 "top_on_st S X = (\<forall>x\<in>X. fun S x = \<top>)" |
138 "top_on_st S X = (\<forall>x\<in>X. fun S x = \<top>)" |
139 |
139 |
140 fun top_on_opt :: "'a::top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where |
140 fun top_on_opt :: "'a::order_top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where |
141 "top_on_opt (Some S) X = top_on_st S X" | |
141 "top_on_opt (Some S) X = top_on_st S X" | |
142 "top_on_opt None X = True" |
142 "top_on_opt None X = True" |
143 |
143 |
144 definition top_on_acom :: "'a::top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where |
144 definition top_on_acom :: "'a::order_top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where |
145 "top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)" |
145 "top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)" |
146 |
146 |
147 lemma top_on_top: "top_on_opt (\<top>::_ st option) X" |
147 lemma top_on_top: "top_on_opt (\<top>::_ st option) X" |
148 by(auto simp: top_option_def fun_top) |
148 by(auto simp: top_option_def fun_top) |
149 |
149 |