equal
deleted
inserted
replaced
94 "asimp (N n) = N n" | |
94 "asimp (N n) = N n" | |
95 "asimp (V x) = V x" | |
95 "asimp (V x) = V x" | |
96 "asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)" |
96 "asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)" |
97 text_raw\<open>}%endsnip\<close> |
97 text_raw\<open>}%endsnip\<close> |
98 |
98 |
99 text\<open>Note that in @{const asimp_const} the optimized constructor was |
99 text\<open>Note that in \<^const>\<open>asimp_const\<close> the optimized constructor was |
100 inlined. Making it a separate function @{const plus} improves modularity of |
100 inlined. Making it a separate function \<^const>\<open>plus\<close> improves modularity of |
101 the code and the proofs.\<close> |
101 the code and the proofs.\<close> |
102 |
102 |
103 value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))" |
103 value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))" |
104 |
104 |
105 theorem aval_asimp[simp]: |
105 theorem aval_asimp[simp]: |