(* generated by Ott 0.10.17 from: common.ott bool.ott nat.ott *)

Require Import Arith.
Require Import Bool.
Require Import List.

(** syntax *)
Definition label := nat.
Definition index := nat.

Inductive term : Set := 
 | TmTrue : term
 | TmFalse : term
 | TmIf : term -> term -> term -> term
 | TmZero : term
 | TmSucc : term -> term
 | TmPred : term -> term
 | TmIszero : term -> term.


Require Export notations.



(** We use Coq's notations so we can use the standard syntax of terms
even in Coq. However, since the syntax of the object languages is very
similar to the syntax of Coq, some confusion may easily arise. In
general, we use [true%tm] to denote an object language term
(represented as the constructor [TmTrue] in Coq) to avoid confusing it
with the ordinary boolean [true] that we use when programming directly
in Coq. **)

Delimit Scope term_scope with tm.
Bind Scope term_scope with term.


Arguments Scope TmIf [term_scope term_scope term_scope].

Notation "'true'" := (TmTrue)  : term_scope.
Notation "'false'" := (TmFalse) : term_scope.
Notation "'if' t1 'then' t2 'else' t3" := 
	 ((TmIf t1 t2 t3)) : term_scope.



Notation "'succ' t" := ((TmSucc t)) : term_scope.
Notation "'pred' t" := ((TmPred t)) : term_scope.
Notation "0" := (TmZero) : term_scope.
Notation "'iszero' t" := ((TmIszero t)) : term_scope.



(** definitions *)

(* defns Jop *)
Inductive nv : term -> Prop :=    (* defn nv *)
 | NV_Zero : 
     nv TmZero
 | NV_Succ : forall (t:term),
     nv t ->
     nv  (TmSucc t) 
with val : term -> Prop :=    (* defn val *)
 | Val_True : 
     val TmTrue
 | Val_False : 
     val TmFalse
 | Val_NV : forall (t:term),
     nv t ->
     val t
with eval : term -> term -> Prop :=    (* defn eval *)
 | E_IfTrue : forall (t2 t3:term),
     eval (TmIf TmTrue t2 t3) t2
 | E_IfFalse : forall (t2 t3:term),
     eval (TmIf TmFalse t2 t3) t3
 | E_If : forall (t1 t2 t3 t1':term),
     eval t1 t1' ->
     eval (TmIf t1 t2 t3) (TmIf t1' t2 t3)
 | E_Succ : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmSucc t1) (TmSucc t1')
 | E_PredZero : 
     eval (TmPred TmZero) TmZero
 | E_PredSucc : forall (t1:term),
     nv t1 ->
     eval (TmPred  (TmSucc t1) ) t1
 | E_Pred : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmPred t1) (TmPred t1')
 | E_IsZeroZero : 
     eval (TmIszero TmZero) TmTrue
 | E_IsZeroSucc : forall (t1:term),
     nv t1 ->
     eval (TmIszero  (TmSucc t1) ) TmFalse
 | E_IsZero : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmIszero t1) (TmIszero t1').

Notation "t1 --> t2" := (eval t1 t2) : type_scope.