theory Exercise14 imports Main "HOL-IMP.Small_Step" "HOL-IMP.Sem_Equiv" "HOL-IMP.Vars" begin section "Inverse Analysis" 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' a b c = (b, c)" lemma "\ inv_plus' a a1 a2 = (a1',a2'); i1 \ \ a1; i2 \ \ a2; i1+i2 \ \ a \ \ i1 \ \ a1' \ i2 \ \ a2' " by simp fun inv_less' :: "bool \ sign \ sign \ sign * sign" where "inv_less' a b c = (b, c)" lemma "\ inv_less' bv a1 a2 = (a1',a2'); i1 \ \ a1; i2 \ \ a2; (i1 \ i1 \ \ a1' \ i2 \ \ a2'" by simp section "Command Equivalence" fun is_SKIP where "is_SKIP c = False" lemma "is_SKIP c \ c \ SKIP" sorry end