(* generated by Ott 0.10.17 from: common.ott common_type.ott common_simple_typing.ott bool.ott bool_type.ott bool_simple_typing.ott nat.ott nat_type.ott nat_simple_typing.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.

Inductive type : Set := 
 | TyBool : type
 | TyNat : type.


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.



(** We use the special scope [ty_scope] for the types in our object
language. This allows us to write [Bool%ty] instead of [TyBool]. **)

Delimit Scope ty_scope with ty.
Bind Scope ty_scope with type.


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 "'Bool'" := TyBool (at level 0, no associativity) : ty_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.



Notation "'Nat'" := TyNat (at level 0, no associativity) : ty_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').

(* defns Jtype *)
Inductive typing : term -> type -> Prop :=    (* defn typing *)
 | T_True : 
     typing TmTrue TyBool
 | T_False : 
     typing TmFalse TyBool
 | T_If : forall (t1 t2 t3:term) (T:type),
     typing t1 TyBool ->
     typing t2 T ->
     typing t3 T ->
     typing (TmIf t1 t2 t3) T
 | T_Zero : 
     typing TmZero TyNat
 | T_Succ : forall (t1:term),
     typing t1 TyNat ->
     typing (TmSucc t1) TyNat
 | T_Pred : forall (t1:term),
     typing t1 TyNat ->
     typing (TmPred t1) TyNat
 | T_IsZero : forall (t1:term),
     typing t1 TyNat ->
     typing (TmIszero t1) TyBool.

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



(** We define some syntactic sugar for expressing the typing
judgements at Coq level. The notation [t : T] is already used by Coq
internally, so we use [|- t : T] as sugar for the proposition [typing
t T]. **)

Notation "|-  t : T" := (typing t T) : type_scope.