theory ex12 imports "HOL-IMP.Small_Step" "HOL-IMP.Sem_Equiv" "HOL-IMP.Vars" "HOL-IMP.Abs_Int1" begin datatype sign = Pos | Zero | Neg | Any instantiation sign :: semilattice_sup_top begin definition less_eq_sign where "x \ y = (y = Any \ x=y)" definition less_sign where "x < y = (x \ y \ \ y \ (x::sign))" definition sup_sign where "x \ y = (if x = y then x else Any)" definition top_sign where "\ = Any" instance by standard (auto simp: less_eq_sign_def less_sign_def sup_sign_def top_sign_def) end fun \_sign :: "sign \ val set" where "\_sign Neg = {i. i < 0}" | "\_sign Pos = {i. i > 0}" | "\_sign Zero = {0}" | "\_sign Any = UNIV" fun num_sign :: "val \ sign" where "num_sign i = (if i = 0 then Zero else if i > 0 then Pos else Neg)" fun plus_sign :: "sign \ sign \ sign" where "plus_sign y Zero = y" | "plus_sign Zero y = y" | "plus_sign x y = (if x = y then x else Any)" global_interpretation Val_semilattice where \ = \_sign and num' = num_sign and plus' = plus_sign proof (standard, goal_cases) case (4 _ a1 _ a2) thus ?case by (induction a1 a2 rule: plus_sign.induct) (auto simp add:mod_add_eq) qed (auto simp: less_eq_sign_def top_sign_def) global_interpretation Abs_Int where \ = \_sign and num' = num_sign and plus' = plus_sign defines aval_sign = aval' and step_sign = step' and AI_sign = AI .. abbreviation h_sign :: nat fun m_sign :: "sign \ nat" where "m_sign _ = undefined" global_interpretation Abs_Int_mono where \ = \_sign and num' = num_sign and plus' = plus_sign sorry global_interpretation Abs_Int_measure where \ = \_sign and num' = num_sign and plus' = plus_sign and m = m_sign and h = h_sign sorry datatype sign0 = None | Neg | Pos0 | Any fun \_0 :: "sign0 \ val set" where "\_0 None = {}" | "\_0 Neg = {i. i < 0}" | "\_0 Pos0 = {i. i \ 0}" | "\_0 Any = UNIV" fun inv_plus' :: "sign0 \ sign0 \ sign0 \ sign0 * sign0" where "inv_plus' _ = undefined" lemma "\ inv_plus' a a1 a2 = (a1',a2'); i1 \ \_0 a1; i2 \ \_0 a2; i1+i2 \ \_0 a \ \ i1 \ \_0 a1' \ i2 \ \_0 a2' " sorry fun inv_less' :: "bool \ sign0 \ sign0 \ sign0 * sign0" where "inv_less' _ = undefined" lemma "\ inv_less' bv a1 a2 = (a1',a2'); i1 \ \_0 a1; i2 \ \_0 a2; (i1 \ i1 \ \_0 a1' \ i2 \ \_0 a2'" sorry end