aspengasil.blogg.se

• #Jedit x plus plus#

#Jedit x plus plus#

First one is to prove that initial condition for Zero, second is to prove recursive case while having access to inductive hypothesis plus x (plus y z) = plus (plus x y) z. Plus (Suc x) (plus y z) = plus (plus (Suc x) y) z plus Zero (plus y z) = plus (plus Zero y) zĢ. Now the state of the proof becomes proof (prove)ġ. theorem add_associativity : "plus x (plus y z) = plus (plus x y) z"

This is done with apply(induct_tac x) tactic. When dealing with inductive types a good idea is to prove theorems by induction. Primitive recursive functions are very limiting and not Turing-complete, therefore, if primrec is not enough, we can use fun but we may have to provide our own proof that the recursion always ends ( fun will be shown later). This means that the size of first argument always decreases and because it is finite and non-negative it must eventually reach 0 and end. f a) on constructor parameters but not on the original input (e.g. Which means that they consider all cases ( X1 a, X1 b, … Xn c) of some inductive type x and can only perform recursion (e.g.

Those functions must be of the form datatype x = X1 a | X2 b |. To avoid such problems primrec must be a primitive recursive function. The reason why we don’t want that is because it would allow us to prove any statement about f to be true (proofs by induction will be shown soon). For example the following is illegal primrec f :: "nat ⇒ nat" whereīecause the evaluation of f would never end. In Isabelle all functions must terminate.