While studying chapter 3 of Concrete Semantics my instructor mentionned that some of the functions there were built using the smart constructor pattern and stated that this pattern was beneficial for theorem proving.
I googled smart constructors and they seem to be used in languages like Haskell with which I'm not familiar with. Furthermore, there are not that many references of smart constructors in theorem proving.
So, what is smart constructor pattern in Isabelle and how can it help theorem proving? Maybe you can even explain it with chapter 3 of the book...
So the pattern basically consists in defining and proving difficult subcases of functions in separate functions and then combining them into the main function. This will of course ease the proof.
You can see an example of this behaviour in the AExp.thy from the tutorial. The simplified function is:
fun plus :: "aexp ⇒ aexp ⇒ aexp" where
"plus (N i1) (N i2) = N(i1+i2)" |
"plus (N i) a = (if i = 0 then a else Plus (N i) a)" |
"plus a (N i) = (if i = 0 then a else Plus a (N i))" |
"plus a1 a2 = Plus a1 a2"
Some theorems about the simple function are:
lemma aval_plus [simp]:
"aval (plus a1 a2) s = aval a1 s + aval a2 s"
apply(induction a1 a2 rule: plus.induct)
apply auto
done
The combination of the facts is found in:
fun asimp :: "aexp ⇒ aexp" where
"asimp (N n) = N n" |
"asimp (V x) = V x" |
"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"
and the final proof is simpler:
theorem aval_asimp[simp]:
"aval (asimp a) s = aval a s"
apply(induction a)
apply (auto)
done