Re: Skip termination proofs

[Chris Warburton]

Here's an example of before/after for skipping a termination proof:

Before:

  function (sequential) exp :: "Nat => Nat => Nat" where
  "exp x (Z) = S Z"
  | "exp x (S y2) = times x (exp x (S y2))"
  by pat_completeness auto
  termination by size_change

After:

  function (sequential) exp :: "Nat => Nat => Nat" where
  "exp x (Z) = S Z"
  | "exp x (S y2) = times x (exp x (S y2))"
  by pat_completeness auto
  termination sorry

Note that we don't use 'by'; probably some object/meta distinction
between proofs and tactics or something...

Note that we should *also* use 'sorry' for the completeness proof as
well, since things like destructor functions are partial:

  function (sequential) exp :: "Nat => Nat => Nat" where
  "exp x (Z) = S Z"
  | "exp x (S y2) = times x (exp x (S y2))"
  sorry
  termination sorry