theory Arith

imports Main

begin

datatype arith =
  Z
| Succ "arith"
| Pred "arith"

(*
datatype val = 
  V_Z
| V_Succ "val"
*)

value "Z"
value "Pred Z"
value "Succ (Pred Z)"

inductive isvalue :: "arith \<Rightarrow> bool" where
v_z : "isvalue Z" |
v_s : "isvalue M ==> isvalue (Succ M)"

inductive step :: "arith \<Rightarrow> arith \<Rightarrow> bool" ("_\<down>_") where

s_succ : "m \<down> m' ==> (Succ m) \<down>  (Succ m')" |
s_pred_zero : "(Pred Z) \<down> Z" |
s_pred : "m \<down> m' ==> (Pred m) \<down> (Pred m')" |
s_pred_succ : "isvalue v ==> (Pred(Succ v)) \<down> v" |

(* I add these rules because I don't know how to
  proove the theorem that values don't step, so
  values have to step to themselves *)
s_z [simp] : "Z \<down> Z"
(* s_val : "isvalue v ==> v \<down> v" *)

theorem det: shows "(step m n_1) \<and> (step m n_2) ==> (n_1 = n_2)"
(* apply (rule step.induct) \<leftarrow> this doesn't do what I expected *)
sorry

end