(*------------------------------------------------------------
         The following examples provide HOL-90 equivalents 
       for the HOL-88 examples in Chapter 3 of the Tutorial.
    (HOL90 responses are shown as comments for some of them.)
-------------------------------------------------------------*)

term_pp_prefix := "";  term_pp_suffix := "";

val men_are_mortal = 
             string_to_term "!(x:ind). Man x ==> Mortal x";

val socrates_is_a_man = 
             string_to_term "(Man:ind->bool) Socrates";

val th1 = ASSUME  men_are_mortal;

val th2 = ASSUME  socrates_is_a_man;

MATCH_MP th1 th2;          
  (* val it = .. |- Mortal Socrates : thm *)

(*------------------------------------------------------------*)

"x ==> y";                   (* val it = "x ==> y" : string *)

string_to_term("x ==> y");  (* val it = (--`x ==> y`--):term *)

  (***IN HOL90, STRINGS ARE EXPLICITLY CONVERTED INTO TERMS.***)

dest_imp it;

  (*
  val it = {ant=`x`,conseq=`y`} : {ant:term, conseq:term}
val it = {ant=(--`x`--),conseq=(--`y`--)}:{ant:term, conseq:term}
  *)

  (*** HOL90 USES RECORD STRUCTURES AS OPPOSED TO PAIR. ***)
 
#ant(it);          (* val it = `x` : term *)

  (*** ACCESSING FIELDS OF A RECORD IN SML. ***)

  (*++ string_to_term("x /\ y ==> z");    *ERROR* ++*)

string_to_term("x \\/ y");       (* val it = `x \/ y` : term *)

dest_conj(string_to_term("x /\\ y"));       
   (* val it = {conj1=`x`,conj2=`y`}:{conj1:term, conj2:term} *)

   (*** HOL90 NEEDS "\\" TO REPRESENT "\" IN STRINGS. ***)

#conj1(dest_conj(string_to_term("(1 = 2) /\\ (y ==> z)")));       
   (* val it = `1 = 2` : term *)

(*----------------------------------------------------------- 
 ----------------------- ML vs HOL TYPES---------------------
 -----------------------------------------------------------*)

1 = 2;                     (* val it = false : bool *)
"1 = 2";                   (* val it = "1 = 2" : string *)
string_to_term("(1 = 2)"); (* val it = `1 = 2` : term *)

type_of;                   (* val it = fn : term -> hol_type *)

type_of (string_to_term("(1 = 2)")) ; 
    (* val it = (==`:bool`==) : hol_type *)

type_of string_to_term("2"); 
    (* val it = (==`:num`==) : hol_type *)

type_of (string_to_term("==>"));
    (* val it = (==`:bool -> bool -> bool`==) : hol_type *)

type_of (string_to_term("+"));
    (* val it = (==`:num -> num -> num`==) : hol_type *)

type_of (string_to_term("!(x:num). ~(p x)"));
    (* val it = (==`:bool`==) : hol_type *)

type_of (string_to_term("\\x. x+1"));
    (* val it = (==`:num -> num`==) : hol_type *)


(*----------------------------------------------------------
 ------------------ DEFINING A THEORY-----------------------
 ----------------------------------------------------------*)
current_theory();

new_theory "p_peano";   (* Peano's Postulates *)

new_type;            
    (* val it = fn : {Arity:int, Name:string} -> unit *)

new_type {Arity=0, Name="nat"};
    (*** nat is a 0-ary type-operator (i.e., type constant).***)

new_constant;       
    (* val it = fn : {Name:string, Ty:hol_type} -> unit *)

new_constant {Name="O", Ty=(==`:nat`==)}; 
    (* using letter O, not zero 0 *)

new_constant {Name="Succ", Ty=(==`:nat -> nat`==)};

    (*** TO GET HELP ON NEW_AXIOM USE: help("new_axiom"); ***)

new_open_axiom ("P3",(--`!n. ~(O = Succ n)`--));
    (* val it = |- !n. ~(O = Succ n) : thm *)

new_open_axiom ("P4",(--`!m n. (Succ m = Succ n)==>(m=n)`--));

new_open_axiom ("P5",(--`!P. (((P O) /\
                       (!n. (P n) ==> (P (Succ n))) ) ==> 
                                      (!n. (P n)) )`--));
print_theory "p_peano";  
  
close_theory();
    (* Theory "p_peano" closed BUT NOT SAVED.*)

(*-----------------------------------------------------------*)

extend_theory("p_peano");      (*** TO EXTEND THE THEORY ***)  

new_infix ;
     (* val it = fn:{Name:string,Prec:int,Ty:hol_type}->unit*)

new_infix{Name="p_add",Ty=(==`:nat -> nat -> nat`==),Prec=600};
     (*** This yields an ERROR if the current mode is
          not DRAFT MODE (after calling "close_theory()") ***)

new_open_axiom ("p_add_def", 
          (--`(!n. O p_add n = n) /\ 
              (!m n. (Succ m) p_add n = Succ (m p_add n))`--) );

new_definition("double", (--`double x = x p_add x`--));

(*-----------------------------------------------------------*)

export_theory ();           
     (*** SAVES THE THEORY IN CURRENT DIR ***)

close ();                   
     (*** SAVES THE THEORY ON DISK AND QUITS ***)

load_theory "p_peano";      
     (*** LOADS THE THEORY FROM THE DISK ***)

(*-----------------------------------------------------------*)