src/HOL/IMP/AExp.thy
changeset 45238 ed2bb3b58cc4
parent 45216 a51a70687517
child 45246 4fbeabee6487
equal deleted inserted replaced
45223:62ca94616539 45238:ed2bb3b58cc4
    58 "asimp_const (Plus a1 a2) =
    58 "asimp_const (Plus a1 a2) =
    59   (case (asimp_const a1, asimp_const a2) of
    59   (case (asimp_const a1, asimp_const a2) of
    60     (N n1, N n2) \<Rightarrow> N(n1+n2) |
    60     (N n1, N n2) \<Rightarrow> N(n1+n2) |
    61     (a1',a2') \<Rightarrow> Plus a1' a2')"
    61     (a1',a2') \<Rightarrow> Plus a1' a2')"
    62 
    62 
    63 theorem aval_asimp_const[simp]:
    63 theorem aval_asimp_const:
    64   "aval (asimp_const a) s = aval a s"
    64   "aval (asimp_const a) s = aval a s"
    65 apply(induction a)
    65 apply(induction a)
    66 apply (auto split: aexp.split)
    66 apply (auto split: aexp.split)
    67 done
    67 done
    68 
    68