theory Ex13_Tut_Sol imports "HOL-IMP.Small_Step" "HOL-IMP.Sem_Equiv" "HOL-IMP.Vars" begin datatype sign = None | Neg | Pos0 | Any fun \ :: "sign \ val set" where "\ None = {}" | "\ Neg = {i. i < 0}" | "\ Pos0 = {i. i \ 0}" | "\ Any = UNIV" fun inv_plus' :: "sign \ sign \ sign \ sign * sign" where "inv_plus' Any a1 a2 = (a1,a2)" | "inv_plus' None a1 a2 = (None,None)" | "inv_plus' a None a2 = (None,None)" | "inv_plus' a a1 None = (None,None)" | "inv_plus' Pos0 Neg Any = (Neg,Pos0)" | "inv_plus' Pos0 Any Neg = (Pos0,Neg)" | "inv_plus' Pos0 Neg Neg = (None,None)" | "inv_plus' Pos0 a1 a2 = (a1,a2)" | "inv_plus' Neg Pos0 Any = (Pos0,Neg)" | "inv_plus' Neg Any Pos0 = (Neg,Pos0)" | "inv_plus' Neg Pos0 Pos0 = (None,None)" | "inv_plus' Neg a1 a2 = (a1,a2)" lemma "\ inv_plus' a a1 a2 = (a1',a2'); i1 \ \ a1; i2 \ \ a2; i1+i2 \ \ a \ \ i1 \ \ a1' \ i2 \ \ a2' " by (induction a a1 a2 rule: inv_plus'.induct) auto fun inv_less' :: "bool \ sign \ sign \ sign * sign" where "inv_less' _ None _ = (None,None)" | "inv_less' _ _ None = (None,None)" | "inv_less' True Pos0 Neg = (None,None)" | "inv_less' True Pos0 Any = (Pos0,Pos0)" | "inv_less' True Any Neg = (Neg,Neg)" | "inv_less' True a1 a2 = (a1,a2)" | "inv_less' False Neg Pos0 = (None,None)" | "inv_less' False Any Pos0 = (Pos0,Pos0)" | "inv_less' False Neg Any = (Neg,Neg)" | "inv_less' False a1 a2 = (a1,a2)" lemma "\ inv_less' bv a1 a2 = (a1',a2'); i1 \ \ a1; i2 \ \ a2; (i1 \ i1 \ \ a1' \ i2 \ \ a2'" by (induction bv a1 a2 rule: inv_less'.induct) auto end