equal
deleted
inserted
replaced
131 |
131 |
132 definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)" |
132 definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)" |
133 |
133 |
134 interpretation Abs_Int_measure |
134 interpretation Abs_Int_measure |
135 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
135 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
136 and m = m_const and h = "2" |
136 and m = m_const and h = "1" |
137 proof |
137 proof |
138 case goal1 thus ?case by(auto simp: m_const_def split: const.splits) |
138 case goal1 thus ?case by(auto simp: m_const_def split: const.splits) |
139 next |
139 next |
140 case goal2 thus ?case by(auto simp: m_const_def split: const.splits) |
140 case goal2 thus ?case by(auto simp: m_const_def split: const.splits) |
141 next |
141 next |