[Hol-checkins] SF.net SVN: hol:[6770] HOL/examples

[<mic...@us...>]

Revision: 6770
          http://hol.svn.sourceforge.net/hol/?rev=6770&view=rev
Author:   michaeln
Date:     2009-05-11 02:23:34 +0000 (Mon, 11 May 2009)

Log Message:
-----------
Symbolic Trajectory Evaluation example from Ashish Darbari.

Added Paths:
-----------
    HOL/examples/STE/
    HOL/examples/STE/Conversion.sml
    HOL/examples/STE/Examples/
    HOL/examples/STE/Examples/And.sml
    HOL/examples/STE/Examples/Comparator-for-STE-Reduction.sml
    HOL/examples/STE/Examples/Comparator.sml
    HOL/examples/STE/Examples/Mux.sml
    HOL/examples/STE/Examples/Nand.sml
    HOL/examples/STE/Examples/Not.sml
    HOL/examples/STE/Examples/Or.sml
    HOL/examples/STE/README
    HOL/examples/STE/RunScript
    HOL/examples/STE/STEScript.sml
    HOL/examples/STE/doc/
    HOL/examples/STE/doc/STEHOL.ps.gz
    HOL/examples/STE/doc/SegerBryant.ps.gz
    HOL/examples/STE/doc/Xs.ps.gz

Added: HOL/examples/STE/Conversion.sml
===================================================================
--- HOL/examples/STE/Conversion.sml	                        (rev 0)
+++ HOL/examples/STE/Conversion.sml	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,156 @@
+
+(*
+val _ = load "stringLib";
+val _ = load "listTheory";
+val _ = load "pairTheory";
+val _ = load "arithmeticTheory";
+*)
+local 
+open bossLib;
+open boolTheory;
+open stringLib;
+open Conv;
+open Parse;
+open listTheory;
+open pairTheory;
+open arithmeticTheory;
+open STETheory;
+open Lib;
+open Drule;
+in
+
+
+val base_defn_list = [DefTraj_def, DefSeq_def, leq_def, 
+		      lub_def, Zero_def, 
+		      One_def, X_def, FST, 
+		      SND, Depth_def, 
+		      Nodes_def, APPEND, MAX_def,  
+		      MEM];
+
+val CONV = SIMP_CONV arith_ss [DISJ_IMP_THM, FORALL_AND_THM, 
+			       UNWIND_FORALL_THM1];
+
+
+
+fun STE_CONV_RULE theorem thm_list = 
+
+    let  
+	val TrajConv = computeLib.CBV_CONV (computeLib.new_compset thm_list)
+	val NC = computeLib.CBV_CONV (reduceLib.num_compset())
+	val BC = computeLib.CBV_CONV (computeLib.bool_compset())
+    in
+	CONV_RULE(EVERY_CONV [TrajConv, NC, TrajConv, BC]) theorem 
+    end;
+
+
+(* Some user-interface functions *)
+fun add_next start term = 
+    if start = 0 then term 
+    else
+	let val newstart = start - 1
+	in
+	    add_next newstart (``NEXT ^term``)
+	end;
+
+fun add_next_upto_depth start depth term = 
+	if (start  = (depth-1)) then
+	    add_next start term 
+	else
+	    ``^(add_next start term) AND 
+	    ^(add_next_upto_depth (start+1) depth term)``;
+	
+fun TrajForm (guard:term, n:string, value:term, START, END) = 
+     let val node = stringLib.fromMLstring n
+	 val atom = 
+	     ``((Is_1 ^node) WHEN (^value/\ ^guard))
+	     AND 
+	     ((Is_0 ^node) WHEN ~(^value /\ ^guard))``;
+     in
+	 add_next_upto_depth START END atom
+     end;
+
+fun TF [x] = TrajForm x 
+| TF (x::xs) = ``^(TrajForm x) AND ^(TF xs)``;
+
+fun extract_constr theorem = fst(boolSyntax.dest_imp(Thm.concl theorem));
+
+
+(* STE Simulator over lattice models *)
+(* verbose switches the print options *)
+fun STE A C Y comp_list verbose =
+if verbose then
+let
+val clock = start_time();
+val thm_list = comp_list @ base_defn_list;
+val _ = print ("\nSpecialising the STE Implementation definition...");
+val iter0 = SPECL [A, C, Y] STE_Impl_def;
+val _ = print ("done\n");
+val _ = print ("Calculating the depth of the formula...");
+val iter1 =  RIGHT_CONV_RULE(SIMP_CONV arith_ss [Depth_def, MAX_def]) iter0;
+val _ = print ("done\n");
+val _ = print("Rewriting for less than or equal...");
+val iter2 = RIGHT_CONV_RULE(SIMP_CONV std_ss [LESS_OR_EQ]) iter1;
+val _ = print("done\n");
+val _ = print("Rewriting for less than...");
+val iter3 = RIGHT_CONV_RULE(SIMP_CONV arith_ss [LESS_EQ]) iter2;
+val _ = print("done\n");
+val _ = print("Calculating the nodes in the antecedent and consequent...");
+val iter4 = RIGHT_CONV_RULE(STRIP_QUANT_CONV(RAND_CONV(EVAL))) iter3;
+val _ = print("done\n");
+val _ = print ("Rewriting with DISJ_IMP_THM...");
+val iter5a = RIGHT_CONV_RULE(SIMP_CONV std_ss [DISJ_IMP_THM]) iter4;
+val _ = print("done\n");
+val _ = print ("Rewriting with FORALL_AND_THM...");
+val iter5b = RIGHT_CONV_RULE(SIMP_CONV std_ss [FORALL_AND_THM]) iter5a;
+val _ = print("done\n");
+val _ = print ("Rewriting with UNWINDFORALL_THM1...");
+val iter5 = RIGHT_CONV_RULE(SIMP_CONV std_ss [UNWIND_FORALL_THM1]) iter5b;
+val _ = print ("done\n");
+val _ = print("Running STE...");
+val iter6 = STE_CONV_RULE iter5 thm_list;
+val iter7 = RIGHT_CONV_RULE(TOP_DEPTH_CONV(stringLib.string_EQ_CONV) 
+		THENC (TOP_DEPTH_CONV(COND_CONV))) iter6;
+val _ = print("done\n");
+val _ = print ("Canonicalising booleans...");
+val iter8 = RIGHT_CONV_RULE(EVAL) iter7;
+val _ = print ("done\n");
+val _ = end_time clock
+in
+iter8
+end
+else
+let
+val clock = start_time();
+val thm_list = comp_list @ base_defn_list;
+val iter0 = SPECL [A, C, Y] STE_Impl_def;
+val iter1 =  RIGHT_CONV_RULE(SIMP_CONV arith_ss [Depth_def, MAX_def]) iter0;
+val iter2 = RIGHT_CONV_RULE(SIMP_CONV std_ss [LESS_OR_EQ]) iter1;
+val iter3 = RIGHT_CONV_RULE(SIMP_CONV arith_ss [LESS_EQ]) iter2;
+val iter4 = RIGHT_CONV_RULE(STRIP_QUANT_CONV(RAND_CONV(EVAL))) iter3;
+val iter5a = RIGHT_CONV_RULE(SIMP_CONV std_ss [DISJ_IMP_THM]) iter4;
+val iter5b = RIGHT_CONV_RULE(SIMP_CONV std_ss [FORALL_AND_THM]) iter5a;
+val iter5 = RIGHT_CONV_RULE(SIMP_CONV std_ss [UNWIND_FORALL_THM1]) iter5b;
+val iter6 = STE_CONV_RULE iter5 thm_list;
+val iter7 = RIGHT_CONV_RULE(TOP_DEPTH_CONV(stringLib.string_EQ_CONV) 
+		THENC (TOP_DEPTH_CONV(COND_CONV))) iter6;
+val iter8 = RIGHT_CONV_RULE(EVAL) iter7;
+val _ = end_time clock
+in
+iter8
+end;
+
+
+
+(* From STE World to the Boolean World *)
+fun STE_TO_BOOL A C Y Yb ok_thm monotonic_thm ste_impl_result =
+    let val iter1 = SPECL [A, C, Y, Yb] BRIDGETHEOREM2;
+	val iter2 = CONV_RULE(SIMP_CONV arith_ss [ok_thm]) iter1;
+	val iter3 = CONV_RULE(SIMP_CONV arith_ss [monotonic_thm]) iter2;
+	val iter4 = 
+	    CONV_RULE(SIMP_CONV bool_ss [DE_MORGAN_THM]) ste_impl_result;
+    	val iter5 = CONV_RULE(SIMP_CONV std_ss [iter4]) iter3
+in
+    iter5
+    end;
+
+end;


Property changes on: HOL/examples/STE/Conversion.sml
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-styl
   + native
Added: svn:eol-style
   + native

Added: HOL/examples/STE/Examples/And.sml
===================================================================
--- HOL/examples/STE/Examples/And.sml	                        (rev 0)
+++ HOL/examples/STE/Examples/And.sml	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,55 @@
+
+(* And Delay *)
+
+val And_def = Define  `And (a, b) (c, d) = (a/\c, b\/d)`;;
+
+val And_bool_def =  Define `And_bool s_b s_b' = 
+    !node. ((node = "out") ==> 
+	    (s_b' node = ((s_b "i0") /\ (s_b "i1"))))`;
+
+val And_lattice_def = Define `(And_lattice s node = 
+			    if (node = "i0")
+				then X 
+			    else if (node = "i1") then X
+			    else if (node = "out") 
+				     then 
+					 And (s "i0")(s "i1")
+				 else
+				     X)`;
+
+val comp_list = [And_lattice_def, And_bool_def];
+
+val a1 = (T, "i0", ``v1:bool``, 0, 1);
+val a2 = (T, "i1", ``v2:bool``, 0, 1);
+val c  =  (T, "out", ``(v1/\v2):bool``, 1, 2) ;
+val A  =  TF [a1, a2];
+val C  =  TF [c];
+
+(* Running the STE Simulator *)	      
+val AND_STE_IMPL1 = STE A C ``And_lattice`` comp_list true;
+
+(* when you expect a low output at the AND gate *)
+
+ (* under specification works okay *)
+val a1 = (T, "i0", ``v1:bool``, 0, 1);
+val c  =  (T, "out", ``F:bool``, 1, 2) ;
+val A  =  TF [a1];
+val C  =  TF [c];
+
+(* Running the STE Simulator *)	      
+val AND_STE_IMPL1 = STE A C ``And_lattice`` comp_list true;
+
+
+(* when you expect a high output at the AND gate *)
+val a1 = (T, "i0", ``v1:bool``, 0, 1);
+val a2 = (T, "i1", ``v2:bool``, 0, 1);
+val c  = (T, "out", ``T:bool``, 1, 2) ;
+val A  =  TF [a1,a2];
+val C  =  TF [c];
+
+(* Running the STE Simulator *)	      
+val AND_STE_IMPL1 = STE A C ``And_lattice`` comp_list true;
+val residue = rhs(concl AND_STE_IMPL1);
+
+set_goal([], ``v1/\v2 ==> ^residue``);
+


Property changes on: HOL/examples/STE/Examples/And.sml
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-style
   + native

Added: HOL/examples/STE/Examples/Comparator-for-STE-Reduction.sml
===================================================================
--- HOL/examples/STE/Examples/Comparator-for-STE-Reduction.sml	                        (rev 0)
+++ HOL/examples/STE/Examples/Comparator-for-STE-Reduction.sml	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,179 @@
+(* Two bit comparator *)
+val _ = load "combinTheory";
+val _ = load "stringLib";
+val _ = load "pairTheory";
+val _ = load "arithmeticTheory";
+val _ = load " listTheory";
+open combinTheory stringLib pairTheory arithmeticTheory listTheory;
+
+fun SUC_ELIM n = 
+    let val thm =
+	RIGHT_CONV_RULE(TOP_DEPTH_CONV numLib.num_CONV)(numLib.num_CONV n)
+	in thm end;
+
+
+(* Basic circuit functions defined on a domain of lattice values *)
+val Or_def = Define `Or (a, b) (c, d) = (a\/c, b/\d)`;; 
+
+val Not_def = Define `Not (a:bool, b:bool) = (b, a)`;;
+
+val And_def = Define `And (a, b) (c, d) = (a/\c, b\/d)`;; 
+
+val Xnor_def = Define `Xnor a b = Or (And a b)(And (Not a)(Not b))`;
+
+(* Unit delay two bit comparator circuit for equality testing - lattice model*)
+val Comparison_def = Define `(Comparison s node =
+    if (node = "a0") then X
+    else if (node = "a1") then X
+	 else if (node = "b0") then X
+	      else if (node = "b1") then X
+		  else if (node = "i0") 
+			   then 
+			       Xnor (s "a0")(s "b0")
+		       else if (node = "i1") 
+				then 
+				    Xnor (s "a1")(s "b1")
+			    else if (node = "out") 
+				     then
+					 And 
+					 (Xnor (s "a0")(s "b0"))
+					 (Xnor (s "a1")(s "b1"))
+				 else X)`;
+
+val And_lattice_def = Define `(And_lattice s node = 
+			    if (node = "i0")
+				then X
+			    else if (node = "i1") then 
+				X
+				 else if (node = "out") 
+					  then 
+					      And (s "i0")(s "i1")
+				      else
+					  X)`;
+
+val Bitwise_comparison_def = Define `(Bitwise_comparison s node =
+    if (node = "a0") then X
+    else if (node = "a1") then X
+	 else if (node = "b0") then X
+	      else if (node = "b1") then X
+		  else if (node = "i0") then Xnor (s "a0")(s "b0")
+		       else if (node = "i1") then Xnor (s "a1")(s "b1")
+			   else X)`;
+
+
+val Comparator_lattice_def = Define `(Comparator_lattice  = 
+				      And_lattice o Bitwise_comparison)`;
+
+val xnor_def = Define `xnor a b = (a /\ b) \/ (~a /\ ~b)`;    
+val comp_list = [Comparison_def, Bitwise_comparison_def, 
+		 Comparator_lattice_def,
+		 Xnor_def, xnor_def, Or_def, o_DEF,
+		 And_def, And_lattice_def, Not_def, FST, SND];
+
+
+
+val MEM_CONV = SIMP_CONV list_ss [DISJ_IMP_THM, MAP, MEM, LESS_OR_EQ, LESS_EQ,
+				FORALL_AND_THM, UNWIND_FORALL_THM1, 
+				LENGTH, HD, TL, FOLDR, MAP2];
+
+(*********************** E X A M P L E S *******************************)
+
+(* Example I *)
+
+val a0 = (T, "a0", ``a0:bool``, 0, 1);
+val a1 = (T, "a1", ``a1:bool``, 0, 1);
+val b0 = (T, "b0", ``b0:bool``, 0, 1);
+val b1 = (T, "b1", ``b1:bool``, 0, 1);
+val out = (T, "out", ``xnor a0 b0 /\ xnor a1 b1``, 1, 2);
+val A  =  TF [a0,a1,b0,b1] ;
+val C  =  TF [out] ;
+
+(* Running the STE Simulator *)	      
+val COMPARATOR_STE_IMPL1 = STE A C ``Comparator_lattice`` comp_list true;
+
+(******* using symmetry  ****************************************************)
+(*
+The detailed solution
+----------------------
+
+Equality
+--------
+
+The goal is to show that 
+
+Comp |= ("a0" is a0) and ("b0" is b0) and
+        ("a1" is a1) and ("b1" is b1) 
+         ==>> ("out" is 1) when (xnor a0 b0 /\ xnor a1 b1)
+
+A1 = ("a0" is a0) and ("b0" is b0) from 0 to 1
+A2 = ("a1" is a1) and ("b1" is b1) from 0 to 1
+B1 = ("i0" is 1)  from 1 to 2
+B2 = ("i1" is 1) from 1 to 2
+G1 = (a0=b0) 
+G2 = (a1=b1)
+C = "out" is 1 from 2 to 3
+*)
+
+val A1 = TF [(T, "a0", ``a0:bool``, 0, 1), (T, "b0", ``b0:bool``, 0, 1)];
+val G1 = ``xnor a0 b0``;
+val B1 = (T, "i0", T, 1, 2);
+
+(* B1 when G1*)
+val NewB1 = TF [(G1, "i0", T, 1, 2)];
+
+(* Comp |= A1 ==>> B1 when G1  (STE run) *)
+
+STE A1 NewB1 ``Bitwise_comparison`` comp_list true;
+
+(*
+From symmetry we conclude
+
+Comp |= A2 ==>> B2 when G2  (Symmetry)
+
+By Constr Impl1 we get
+
+G1 ==> (Comp |= A1 ==>> B1)
+
+G2 ==> (Comp |= A2 ==>> B2)
+
+From GUARD CONJUNCTION we get
+
+(G1 /\ G2) ==> (Comp|= (A1 and A2) ==>> (B1 and B2))
+
+*)
+
+(* Comp |= (B1 and B2) ==>> C (STE run) *)
+
+val B1 = (T, "i0", T, 0, 1);
+val B2 = (T, "i1", T, 0, 1);
+val C = (T, "out", T, 1, 2);
+
+STE (TF [B1, B2]) (TF [C]) ``And_lattice`` comp_list true;
+
+By time shift lemma it will be true that for the following formulas
+
+val B1 = (T, "i0", T, 1, 2);
+val B2 = (T, "i1", T, 1, 2);
+val C = (T, "out", T, 2, 3);
+
+ the following lemma will hold
+
+|- STE (TF [B1, B2]) (TF [C]) ``And_lattice`` comp_list true;
+
+
+By SPECIALISED CUT 1  we get
+
+(G1 /\ G2) ==> (Comp |= A1 and A2 ==>> C)
+
+By Constr Impl 2 we get
+
+Comp |= (A1 and A2) ==>> (C when (G1 /\ G2))
+
+Replacing the values of A1, A2, C, G1 and G2 we get
+
+Comp |= ("a0" is a0) and ("b0" is b0) and
+        ("a1" is a1) and ("b1" is b1) 
+         ==>> ("out" is 1) when ((a0=b0) /\ (a1=b1))
+
+Similarly we can do the Inequality case by following the flow in this file
+../../TypeSystem/Examples/Comparator.sml


Property changes on: HOL/examples/STE/Examples/Comparator-for-STE-Reduction.sml
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-style
   + native

Added: HOL/examples/STE/Examples/Comparator.sml
===================================================================
--- HOL/examples/STE/Examples/Comparator.sml	                        (rev 0)
+++ HOL/examples/STE/Examples/Comparator.sml	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,256 @@
+(* Two bit comparator *)
+
+val fs = FULL_SIMP_TAC std_ss;
+
+(* Basic circuit functions defined on a domain of lattice values *)
+val Or_def = Define `Or (a, b) (c, d) = (a\/c, b/\d)`;; 
+
+val Not_def = Define `Not (a:bool, b:bool) = (b, a)`;;
+
+val And_def = Define `And (a, b) (c, d) = (a/\c, b\/d)`;; 
+
+val Xnor_def = Define `Xnor a b = Or (And a b)(And (Not a)(Not b))`;
+
+(* Unit delay two bit comparator circuit for equality testing - lattice model*)
+val Comparator_lattice_def = Define `(Comparator_lattice s node = 
+			      if (node = "a0") then X
+				  else if (node = "a1") then X
+				      else if (node = "b0") then X
+					  else if (node = "b1") then X
+					      else if (node = "out") then
+						  And (Xnor (s "a0")(s "b0"))
+						  (Xnor (s "a1")(s "b1"))
+						      else X)`;
+    
+
+(* Unit delay two bit comparator circuit for equality testing - Boolean model*)
+val Comparator_bool_def = Define `Comparator_bool (s_b:string->bool) s_b' =
+    !node. (node = "out") ==> 
+    (s_b' node = (s_b "a0" = s_b "b0") /\ (s_b "a1" = s_b "b1"))`;
+
+
+val comp_list = [Comparator_lattice_def, Xnor_def, Or_def, 
+		 And_def, Not_def];
+
+(* prove that it is okay to relate the two models for comparator *)    
+val COMPARATOR_OK = 
+    store_thm ("COMPARATOR_OK",
+	       ``Okay (Comparator_lattice, Comparator_bool)``,
+	       FULL_SIMP_TAC std_ss [Okay_def, 
+				     Comparator_lattice_def, Xnor_def, Or_def,
+				     Comparator_bool_def, And_def, Not_def,
+				     extended_drop_state_def, 
+				     leq_state_def]
+	       THEN REPEAT STRIP_TAC 
+	       THEN REPEAT COND_CASES_TAC 
+	       THEN fs [lattice_X1_lemma, leq_def] 
+	       THENL [PROVE_TAC [lattice_X1_lemma],
+		      PROVE_TAC [lattice_X1_lemma],
+		      PROVE_TAC [lattice_X1_lemma],
+		      PROVE_TAC [lattice_X1_lemma],
+		      Cases_on `s_b "a0"`
+		      THEN Cases_on `s_b "b0"` 
+		      THEN Cases_on `s_b "a1"` 
+		      THEN Cases_on `s_b "b1"`
+		      THEN fs [drop_def, 
+			       One_def,
+			       Zero_def, 
+			       X_def,
+			       Top_def,
+			       lub_def, 
+			       Or_def,
+			       And_def,
+			       Not_def],
+		      PROVE_TAC [lattice_X1_lemma]]);
+
+(* prove that the comparator circuit is monotonic *)    
+val COMPARATOR_MONOTONIC = 
+    store_thm("COMPARATOR_MONOTONIC",
+	      ``Monotonic Comparator_lattice``,
+	      FULL_SIMP_TAC std_ss [Monotonic_def, 
+		      Comparator_lattice_def,
+		      Xnor_def, Or_def,
+		      And_def, Not_def,
+		      extended_drop_state_def, 
+		      leq_state_def] 
+	      THEN REPEAT STRIP_TAC 
+	      THEN REPEAT COND_CASES_TAC 
+	      THEN fs [leq_def, lub_def, X_def]
+	      THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a0"``)
+	      THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a1"``)
+	      THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"b0"``)
+	      THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"b1"``)
+	      THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"out"``)
+	      THEN Cases_on `s "a0"` THEN Cases_on `s' "a0"`
+	      THEN Cases_on `s "b0"` THEN Cases_on `s' "b0"`
+	      THEN Cases_on `s "a1"` THEN Cases_on `s' "a1"`
+	      THEN Cases_on `s "b1"` THEN Cases_on `s' "b1"`
+	      THEN Cases_on `s "out"` THEN Cases_on `s' "out"`
+	      THEN fs [Not_def, And_def, Or_def, lub_def] 
+	      THEN RW_TAC std_ss [] 
+	      THENL [EQ_TAC THEN REPEAT STRIP_TAC THEN fs [],
+		     EQ_TAC THEN REPEAT STRIP_TAC THEN fs []]);
+
+
+
+(*********************** E X A M P L E S *******************************)
+
+(* Example I *)
+
+val a0 = (T, "a0", ``a0:bool``, 0, 1);
+val a1 = (T, "a1", ``a1:bool``, 0, 1);
+val b0 = (T, "b0", ``b0:bool``, 0, 1);
+val b1 = (T, "b1", ``b1:bool``, 0, 1);
+val out = (T, "out", ``(a0:bool=b0)/\(a1=b1)``, 1, 2);
+val A  =  TF [a0,a1,b0,b1] ;
+val C  =  TF [out] ;
+
+(* Running the STE Simulator *)	      
+val COMPARATOR_STE_IMPL1 = STE A C ``Comparator_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val COMPARATOR_STE_BOOL1 = 
+    STE_TO_BOOL A C ``Comparator_lattice`` ``Comparator_bool`` 
+    COMPARATOR_OK COMPARATOR_MONOTONIC COMPARATOR_STE_IMPL1;
+
+CONV_RULE(EVAL) COMPARATOR_STE_BOOL1;
+
+(* Example II *)
+
+val a0 = (T, "a0", ``T:bool``, 0, 1);
+val a1 = (T, "a1", ``T:bool``, 0, 1);
+val b0 = (T, "b0", ``T:bool``, 0, 1);
+val b1 = (T, "b1", ``T:bool``, 0, 1);
+val out = (T, "out", ``T``, 1, 2);
+val A  =  TF [a0, a1, b0, b1] ;
+val C  =  TF [out] ;
+
+(* Running the STE Simulator *)	      
+val COMPARATOR_STE_IMPL2 = STE A C ``Comparator_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val COMPARATOR_STE_BOOL2 = 
+    STE_TO_BOOL A C ``Comparator_lattice`` ``Comparator_bool`` 
+    COMPARATOR_OK COMPARATOR_MONOTONIC COMPARATOR_STE_IMPL2;
+
+CONV_RULE(EVAL) COMPARATOR_STE_BOOL2;
+
+(* Example III *)
+
+val a0 = (T, "a0", ``a0:bool``, 0, 1);
+val a1 = (T, "a1", ``a1:bool``, 0, 1);
+val b0 = (T, "b0", ``b0:bool``, 0, 1);
+val b1 = (T, "b1", ``b1:bool``, 0, 1);
+val out = (T, "out", ``(a0:bool=b0)/\(a1=b1)``, 1, 2);
+val A  =  TF [a0,a1,b0,b1] ;
+val C  =  TF [out] ;
+
+(* Running the STE Simulator *)	      
+val COMPARATOR_STE_IMPL3 = STE A C ``Comparator_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val COMPARATOR_STE_BOOL3 = 
+    STE_TO_BOOL A C ``Comparator_lattice`` ``Comparator_bool`` 
+    COMPARATOR_OK COMPARATOR_MONOTONIC COMPARATOR_STE_IMPL3;
+
+CONV_RULE(EVAL) COMPARATOR_STE_BOOL3;
+
+(* Example IV *)
+
+val a0 = (T, "a0", ``v0:bool``, 0, 1);
+val a1 = (T, "a1", ``v1:bool``, 0, 1);
+val b0 = (T, "b0", ``v0:bool``, 0, 1);
+val b1 = (T, "b1", ``v1:bool``, 0, 1);
+val out = (T, "out", ``T``, 1, 2);
+val A  =  TF [a0,a1,b0,b1] ;
+val C  =  TF [out] ;
+
+(* Running the STE Simulator *)	      
+val COMPARATOR_STE_IMPL4 = STE A C ``Comparator_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val COMPARATOR_STE_BOOL4 = 
+    STE_TO_BOOL A C ``Comparator_lattice`` ``Comparator_bool`` 
+    COMPARATOR_OK COMPARATOR_MONOTONIC COMPARATOR_STE_IMPL4;
+
+CONV_RULE(EVAL) COMPARATOR_STE_BOOL4;
+
+(* Example V *)
+
+val a0 = (T, "a0", ``T:bool``, 0, 1);
+val a1 = (T, "a1", ``T:bool``, 0, 1);
+val b0 = (T, "b0", ``T:bool``, 0, 1);
+val b1 = (T, "b1", ``T:bool``, 0, 1);
+val out = (T, "out", ``T``, 1, 2);
+val A  =  TF [a0, a1, b0, b1] ;
+val C  =  TF [out] ;
+
+(* Running the STE Simulator *)	
+val COMPARATOR_STE_IMPL5 = STE A C ``Comparator_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val COMPARATOR_STE_BOOL5 = 
+    STE_TO_BOOL A C ``Comparator_lattice`` ``Comparator_bool`` 
+    COMPARATOR_OK COMPARATOR_MONOTONIC COMPARATOR_STE_IMPL5;
+
+CONV_RULE(EVAL) COMPARATOR_STE_BOOL5;
+
+(* Example VI *)
+
+val a0 = (T, "a0", ``T:bool``, 0, 1);
+val a1 = (T, "a1", ``F:bool``, 0, 1);
+val b0 = (T, "b0", ``T:bool``, 0, 1);
+val b1 = (T, "b1", ``F:bool``, 0, 1);
+val out = (T, "out", ``T``, 1, 2);
+val A  =  TF [a0,a1,b0,b1] ;
+val C  =  TF [out];
+
+(* Running the STE Simulator *)	
+val COMPARATOR_STE_IMPL6 = STE A C ``Comparator_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val COMPARATOR_STE_BOOL6 = 
+    STE_TO_BOOL A C ``Comparator_lattice`` ``Comparator_bool`` 
+    COMPARATOR_OK COMPARATOR_MONOTONIC COMPARATOR_STE_IMPL6;
+
+CONV_RULE(EVAL) COMPARATOR_STE_BOOL6;
+
+(* Example VII *)
+
+val a0 = (T, "a0", ``T:bool``, 0, 1);
+val a1 = (T, "a1", ``F:bool``, 0, 1);
+val b0 = (T, "b0", ``T:bool``, 0, 1);
+val b1 = (T, "b1", ``T:bool``, 0, 1);
+val out = (T, "out", ``T``, 1, 2);
+val A  =  TF [a0,a1,b0,b1] ;
+val C  =  TF [out] ;
+
+(* Running the STE Simulator *)	
+val COMPARATOR_STE_IMPL7 = STE A C ``Comparator_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val COMPARATOR_STE_BOOL7 = 
+STE_TO_BOOL A C ``Comparator_lattice`` ``Comparator_bool`` 
+COMPARATOR_OK COMPARATOR_MONOTONIC COMPARATOR_STE_IMPL7;
+
+CONV_RULE(EVAL) COMPARATOR_STE_BOOL7;
+
+(* Example VIII *)
+
+val a0 = (T, "a0", ``T:bool``, 0, 1);
+val a1 = (T, "a1", ``F:bool``, 0, 1);
+val b0 = (T, "b0", ``T:bool``, 0, 1);
+val b1 = (T, "b1", ``T:bool``, 0, 1);
+val out = (T, "out", ``F``, 1, 2);
+val A  =  TF [a0,a1,b0,b1] ;
+val C  =  TF [out] ;
+
+(* Running the STE Simulator *)
+val COMPARATOR_STE_IMPL8 = STE A C ``Comparator_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val COMPARATOR_STE_BOOL8 = 
+    STE_TO_BOOL A C ``Comparator_lattice`` ``Comparator_bool`` 
+    COMPARATOR_OK COMPARATOR_MONOTONIC COMPARATOR_STE_IMPL8;
+
+CONV_RULE(EVAL) COMPARATOR_STE_BOOL8;


Property changes on: HOL/examples/STE/Examples/Comparator.sml
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-style
   + native

Added: HOL/examples/STE/Examples/Mux.sml
===================================================================
--- HOL/examples/STE/Examples/Mux.sml	                        (rev 0)
+++ HOL/examples/STE/Examples/Mux.sml	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,224 @@
+(* Unit delay 2-to-1 two bit MUX *)
+
+val fs = FULL_SIMP_TAC std_ss;
+val fl = FULL_SIMP_TAC list_ss;
+
+(* Basic circuit functions defined on a domain of lattice values *)
+val Or_def = Define `Or (a, b) (c, d) = (a\/c, b/\d)`;; 
+
+val Not_def = Define `Not (a:bool, b:bool) = (b, a)`;;
+
+val And_def = Define `And (a, b) (c, d) = (a/\c, b\/d)`;; 
+
+(* Unit delay 2-to-1 two bit MUX ---  lattice model *)
+val Mux_lattice_def = 
+    Define `(Mux_lattice s node = 
+	     if (node = "a0") then X
+	     else if (node = "a1") then X
+		  else if (node = "b0") then X
+		       else if (node = "b1") then X
+			    else if (node = "ctrl") then X
+				 else 
+				     if (node = "out0") 
+					 then
+					     Or 
+					     (And (s "a0")(s "ctrl"))
+					     (And (s "b0")(Not(s "ctrl")))
+				     else 
+					 if (node = "out1")
+					     then 
+						 Or 
+						 (And (s "a1")(s "ctrl"))
+						 (And (s "b1")(Not(s "ctrl")))
+					 else X)`;
+
+(* Unit delay 2-to-1 MUX Boolean model *)    
+val Mux_bool_def = Define `Mux_bool s_b s_b' =
+    !node.
+    (if (node = "out0") then 
+	 if (s_b "ctrl") then 
+	     (s_b' "out0" = s_b "a0")
+	 else (s_b' "out0" = s_b "b0")
+     else if (node = "out1") then
+	 if (s_b "ctrl") then 
+	     (s_b' "out1" = s_b "a1")
+	 else (s_b' "out1" = s_b "b1")
+	  else T)`;
+	 
+	 
+val comp_list = [Mux_lattice_def, Or_def, And_def, Not_def];
+
+(* prove that it is okay to relate the two models for MUX *)    
+val MUX_OK = 
+    store_thm("MUX_OK", 
+	      ``Okay (Mux_lattice, Mux_bool)``,
+	      FULL_SIMP_TAC std_ss [Okay_def, Mux_lattice_def, Or_def,
+				    Mux_bool_def, And_def, Not_def,
+				    extended_drop_state_def, leq_def, 
+				    leq_state_def]
+	      THEN REPEAT STRIP_TAC 
+	      THEN REPEAT COND_CASES_TAC 
+	      THENL [PROVE_TAC [lattice_X1_lemma],
+		     PROVE_TAC [lattice_X1_lemma],
+		     PROVE_TAC [lattice_X1_lemma],
+		     PROVE_TAC [lattice_X1_lemma],
+		     PROVE_TAC [lattice_X1_lemma],
+		     FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"out0"``) 
+		     THEN fl []
+		     THENL [POP_ASSUM MP_TAC THEN COND_CASES_TAC 
+			    THENL [REPEAT (POP_ASSUM MP_TAC) 
+				   THEN CONV_TAC
+				   (TOP_DEPTH_CONV(stringLib.string_EQ_CONV)) 
+				   THEN RW_TAC std_ss [], 
+				   REPEAT (POP_ASSUM MP_TAC) 
+				   THEN CONV_TAC
+				   (TOP_DEPTH_CONV(stringLib.string_EQ_CONV)) 
+				   THEN RW_TAC std_ss []],
+			    POP_ASSUM MP_TAC 
+			    THEN COND_CASES_TAC
+			    THENL [fl [] THEN Cases_on `s_b "a0"`
+				   THEN Cases_on `s_b "b0"` 
+				   THEN Cases_on `s_b' "out0"` 
+				   THEN fs [drop_def, One_def, Zero_def,
+					    X_def, Top_def, lub_def,
+					    Or_def, And_def, Not_def],
+				   Cases_on `s_b "a0"`
+				   THEN Cases_on `s_b "b0"` 
+				   THEN Cases_on `s_b' "out0"` 
+				   THEN fs [drop_def, One_def, Zero_def,
+					    X_def, Top_def, lub_def,
+					    Or_def, And_def, Not_def]]],
+		     FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"out1"``) THEN fl []
+		     THEN POP_ASSUM MP_TAC THEN (REPEAT COND_CASES_TAC) 
+		     THENL [REPEAT (POP_ASSUM MP_TAC) 
+			    THEN CONV_TAC
+			    (TOP_DEPTH_CONV(stringLib.string_EQ_CONV)) 
+			    THEN RW_TAC std_ss [],
+			    REPEAT (POP_ASSUM MP_TAC) 
+			    THEN CONV_TAC
+			    (TOP_DEPTH_CONV(stringLib.string_EQ_CONV)) 
+			    THEN RW_TAC std_ss [],
+			    fl [] THEN Cases_on `s_b "a1"`
+			    THEN Cases_on `s_b "b1"` 
+			    THEN Cases_on `s_b' "out1"` 
+			    THEN fs [drop_def, One_def, Zero_def,
+				     X_def, Top_def, lub_def,
+				     Or_def, And_def, Not_def],
+			    fl [] THEN Cases_on `s_b "a1"`
+			    THEN Cases_on `s_b "b1"` 
+			    THEN Cases_on `s_b' "out1"` 
+			    THEN fs [drop_def, One_def, Zero_def,
+				     X_def, Top_def, lub_def,
+				     Or_def, And_def, Not_def]],
+		     PROVE_TAC [lattice_X1_lemma]]);
+    
+(* prove that the MUX circuit is monotonic *)
+val MUX_MONOTONIC = 
+    store_thm("MUX_MONOTONIC", ``Monotonic Mux_lattice``,
+	      FULL_SIMP_TAC std_ss [Monotonic_def, 
+				    Mux_lattice_def,
+				    Or_def,
+				    And_def, Not_def,
+				    extended_drop_state_def, 
+				    leq_state_def] 
+	      THEN REPEAT STRIP_TAC 
+	      THEN REPEAT COND_CASES_TAC 
+	      THEN fs [leq_def, lub_def, X_def]
+	      THENL [REPEAT (POP_ASSUM MP_TAC) 
+		     THEN CONV_TAC(TOP_DEPTH_CONV(stringLib.string_EQ_CONV)) 
+		     THEN RW_TAC std_ss [],
+		     FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a0"``)
+		     THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"ctrl"``)
+		     THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"b0"``)
+		     THEN Cases_on `s "a0"` THEN Cases_on `s' "a0"`
+		     THEN Cases_on `s "b0"` THEN Cases_on `s' "b0"`
+		     THEN Cases_on `s "ctrl"` THEN Cases_on `s' "ctrl"`
+		     THEN fs [Not_def, And_def, Or_def, lub_def] 
+		     THEN RW_TAC std_ss [] THEN 
+		     EQ_TAC THEN REPEAT STRIP_TAC THEN fs [],
+		     FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a1"``)
+		     THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"ctrl"``)
+		     THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"b1"``)
+		     THEN Cases_on `s "a1"` THEN Cases_on `s' "a1"`
+		     THEN Cases_on `s "b1"` THEN Cases_on `s' "b1"`
+		     THEN Cases_on `s "ctrl"` THEN Cases_on `s' "ctrl"`
+		     THEN fs [Not_def, And_def, Or_def, lub_def] 
+		     THEN RW_TAC std_ss [] THEN 
+		     EQ_TAC THEN REPEAT STRIP_TAC THEN fs []]);
+
+
+
+(*********************** E X A M P L E S *******************************)
+
+
+(* Example I *)
+val a0 = (T, "a0", T, 0, 1);
+val a1 = (T, "a1", T, 0, 1);
+val b0 = (T, "b0", F, 0, 1);
+val b1 = (T, "b1", F, 0, 1);
+
+val ctrl = (T, "ctrl", T, 0, 1);
+
+val out0 = (T, "out0", T, 1, 2);
+val out1 = (T, "out1", T, 1, 2);
+
+val A  =  TF [ctrl, a0, a1, b0, b1];
+val C  =  TF [out0, out1] ;
+
+(* Running the STE simulator *)
+val MUX_STE_IMPL1 = STE A C ``Mux_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val MUX_STE_BOOL1 = 
+    STE_TO_BOOL A C ``Mux_lattice`` ``Mux_bool`` 
+    MUX_OK MUX_MONOTONIC MUX_STE_IMPL1;
+
+CONV_RULE(EVAL) MUX_STE_BOOL1;
+
+(* Example II *)
+
+val a0 = (T, "a0", ``va0:bool``, 0, 1);
+val a1 = (T, "a1", ``va1:bool``, 0, 1);
+val b0 = (T, "b0", ``vb0:bool``, 0, 1);
+val b1 = (T, "b1", ``vb1:bool``, 0, 1);
+val ctrl = (T, "ctrl", T, 0, 1);
+val out0 = (T, "out0", ``va0:bool``, 1, 2);
+val out1 = (T, "out1", ``va1:bool``, 1, 2);
+val A  =  TF [ctrl,a0,a1,b0,b1];
+val C  =  TF [out0, out1] ;
+
+(* Running the STE simulator *)
+val MUX_STE_IMPL2 = STE A C ``Mux_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val MUX_STE_BOOL2 = 
+    STE_TO_BOOL A C ``Mux_lattice`` ``Mux_bool`` 
+    MUX_OK MUX_MONOTONIC MUX_STE_IMPL2;
+
+CONV_RULE(EVAL) MUX_STE_BOOL2;
+
+
+(* Example III *)
+
+val a0 = (T, "a0", ``va0:bool``, 0, 1);
+val a1 = (T, "a1", ``va1:bool``, 0, 1);
+val b0 = (T, "b0", ``vb0:bool``, 0, 1);
+val b1 = (T, "b1", ``vb1:bool``, 0, 1);
+val ctrl = (T, "ctrl", ``ctrl:bool``, 0, 1);
+
+val out0 = (T, "out0", ``(va0 /\ ctrl) \/ (vb0 /\ (~ctrl))``, 1, 2);
+val out1 = (T, "out1", ``(va1 /\ ctrl) \/ (vb1 /\ (~ctrl))``, 1, 2);
+val A  =  TF [ctrl,a0,a1,b0,b1] ;
+val C  =  TF [out0, out1];
+val A  =  TF [ctrl,a0,a1,b0,b1];
+val C  =  TF [out0, out1] ;
+
+(* Running the STE simulator *)
+val MUX_STE_IMPL3 = STE A C ``Mux_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val MUX_STE_BOOL3 = 
+    STE_TO_BOOL A C ``Mux_lattice`` ``Mux_bool`` 
+    MUX_OK MUX_MONOTONIC MUX_STE_IMPL3;
+
+CONV_RULE(EVAL) MUX_STE_BOOL3;


Property changes on: HOL/examples/STE/Examples/Mux.sml
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-style
   + native

Added: HOL/examples/STE/Examples/Nand.sml
===================================================================
--- HOL/examples/STE/Examples/Nand.sml	                        (rev 0)
+++ HOL/examples/STE/Examples/Nand.sml	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,98 @@
+(* Nand Delay *)
+val Not_def = Define `Not (a:bool, b:bool) = (b, a)`;;
+
+val And_def = Define `And (a, b) (c, d) = (a/\c, b\/d)`;; 
+
+val Nand_def = Define `Nand a b = Not(And a b)`;
+			       
+val Nand_bool_def =  Define `Nand_bool s_b s_b' = 
+    !node. ((node = "out") ==> 
+	    (s_b' node = ~((s_b "in") /\ (s_b node))))`;
+
+val Nand_lattice_def = Define `(Nand_lattice s node = 
+			    if (node = "in")
+				then X 
+			    else if (node = "out") 
+				     then 
+					 Nand (s "in")(s node)
+				 else
+				     X)`;
+
+val comp_list = [Nand_lattice_def, Nand_def, And_def, Not_def];
+
+(* Its okay to relate Nand_lattice and Nand_bool *)
+val NAND_OK = 
+    store_thm ("NAND_OK", 
+	       ``Okay (Nand_lattice, Nand_bool)``,
+	       FULL_SIMP_TAC std_ss [Okay_def, 
+				     Nand_lattice_def, Nand_def,
+				     Nand_bool_def, And_def, Not_def,
+				     extended_drop_state_def, 
+				     leq_state_def] 
+	       THEN REPEAT STRIP_TAC 
+	       THEN REPEAT COND_CASES_TAC 
+	       THEN fs [lattice_X1_lemma, leq_def] 
+	       THENL [PROVE_TAC [lattice_X1_lemma],
+		      Cases_on `s_b "in"` THEN fs [drop_def, 
+						   One_def,
+						   Zero_def, 
+						   X_def,
+						   Top_def,
+						   lub_def, 
+						   Nand_def, 
+						   And_def,
+						   Not_def],
+		      PROVE_TAC [lattice_X1_lemma]]
+	       THEN Cases_on `s_b "out"` THEN fs [drop_def, 
+						  One_def,
+						  Zero_def, 
+						  X_def,
+						  Top_def,
+						  lub_def, 
+						  Nand_def,
+						  And_def,
+						  Not_def]);
+    
+
+(* Nand lattice is monotonic *)
+val NAND_MONOTONIC = 
+    store_thm("NAND_MONOTONIC", 
+	      ``Monotonic Nand_lattice``,
+	      FULL_SIMP_TAC std_ss [Monotonic_def, 
+				    Nand_lattice_def,
+				    Nand_def,
+				    Nand_bool_def, And_def, Not_def,
+				    extended_drop_state_def, 
+				    leq_state_def] 
+	      THEN REPEAT STRIP_TAC 
+	      THEN REPEAT COND_CASES_TAC 
+	      THEN fs [leq_def, lub_def, X_def]
+	      THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"in"``)
+	      THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"out"``)
+	      THEN Cases_on `s "in"` THEN Cases_on `s' "in"`
+	      THEN Cases_on `s "out"` THEN Cases_on `s' "out"`
+	      THEN fs [Not_def, And_def, lub_def] 
+	      THEN Cases_on `q` 
+	      THEN Cases_on `r` 
+	      THEN Cases_on `q'` 
+	      THEN Cases_on `r'` THEN PROVE_TAC []);
+
+(* Example *)    
+	
+(* STE assertions *)
+
+val a1 = (T, "in", ``v1:bool``, 0, 1);
+val a2 = (T, "out", ``v2:bool``, 0, 1);
+val c  =  (T, "out", ``~(v1/\v2):bool``, 1, 2) ;
+val A  =  TF [a1, a2];
+val C  =  TF [c];
+
+(* Running the STE Simulator *)	      
+val NAND_STE_IMPL1 = STE A C ``Nand_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val NAND_STE_BOOL1 = STE_TO_BOOL A C ``Nand_lattice`` ``Nand_bool`` 
+    NAND_OK NAND_MONOTONIC NAND_STE_IMPL1;
+
+
+


Property changes on: HOL/examples/STE/Examples/Nand.sml
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-style
   + native

Added: HOL/examples/STE/Examples/Not.sml
===================================================================
--- HOL/examples/STE/Examples/Not.sml	                        (rev 0)
+++ HOL/examples/STE/Examples/Not.sml	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,96 @@
+(* Unit delay inverter -- lattice model *)
+
+val fs = FULL_SIMP_TAC std_ss;
+val Not_def = Define `Not (a:bool, b:bool) = (b, a)`;;
+
+val Not_lattice_def = Define `Not_lattice s node = 
+    if (node = "in") then X
+    else if (node = "out") then Not (s "in") 
+	 else X`;
+
+(* Unit delay inverter -- Boolean model *)
+
+val Not_bool_def =  Define `Not_bool s_b s_b' = 
+    !node. ((node = "out") ==> (s_b' node = ~(s_b "in")))`;
+
+
+val comp_list = [Not_lattice_def, Not_def, Not_def];
+
+
+val NOT_OK = store_thm("NOT_OK", ``Okay (Not_lattice, Not_bool)``,
+		       FULL_SIMP_TAC std_ss [Okay_def, 
+					     Not_lattice_def, 
+					     Not_bool_def, Not_def,
+					     extended_drop_state_def, 
+					     leq_state_def]
+		       THEN REPEAT STRIP_TAC 
+		       THEN REPEAT COND_CASES_TAC
+		       THEN fs [lattice_X1_lemma, leq_def] 
+		       THENL [PROVE_TAC [lattice_X1_lemma],
+			      Cases_on `s_b "in"` 
+			      THEN Cases_on `s_b' "out"` 
+			      THEN fs [drop_def, One_def, Zero_def, 
+				       X_def, Top_def, lub_def, 
+				       Not_def, 
+				       Not_bool_def],
+			      PROVE_TAC [lattice_X1_lemma]]);
+
+
+
+val NOT_MONOTONIC = 
+    store_thm ("NOT_MONOTONIC",
+	       ``Monotonic Not_lattice``,
+	       FULL_SIMP_TAC std_ss [Monotonic_def, 
+				     Not_lattice_def,
+				     Not_def,
+				     extended_drop_state_def, 
+				     leq_state_def] 
+	       THEN REPEAT STRIP_TAC 
+	       THEN REPEAT COND_CASES_TAC 
+	       THEN fs [leq_def, lub_def, X_def]
+	       THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"in"``)
+	       THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"out"``)
+	       THEN Cases_on `s "in"` 
+	       THEN Cases_on `s' "in"`
+	       THEN Cases_on `q` 
+	       THEN Cases_on `r` 
+	       THEN Cases_on `q'` 
+	       THEN Cases_on `r'` 
+	       THEN PROVE_TAC [Not_def, lub_def]);
+    
+(* Example I *)
+
+val a =  (T, "in", ``v1:bool``, 0, 1);
+val c  =  (T, "out", ``~v1:bool``, 1, 2) ;
+val A  =  TF [a] ;
+val C  =  TF [c] ;
+
+(* Running the STE simulator *)
+val NOT_STE_IMPL1 = STE A C ``Not_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val NOT_STE_BOOL1 = 
+    STE_TO_BOOL A C ``Not_lattice`` ``Not_bool`` 
+    NOT_OK NOT_MONOTONIC NOT_STE_IMPL1;
+
+CONV_RULE (EVAL) NOT_STE_BOOL1;
+
+
+(* Example II *)
+
+val a = (T, "in", ``v1:bool``, 0, 1);
+val c  =  (T, "out", ``v1:bool``, 1, 2) ;
+val A  =  TF [a] ;
+val C  =  TF [c] ;
+
+(* Running the STE simulator *)
+val NOT_STE_IMPL2 = STE A C ``Not_lattice`` comp_list true;
+
+(* STE TO BOOL *)
+val NOT_STE_BOOL2 = 
+    STE_TO_BOOL A C ``Not_lattice`` ``Not_bool`` 
+    NOT_OK NOT_MONOTONIC NOT_STE_IMPL2;
+
+CONV_RULE(EVAL) NOT_STE_BOOL2;;
+
+


Property changes on: HOL/examples/STE/Examples/Not.sml
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-style
   + native

Added: HOL/examples/STE/Examples/Or.sml
===================================================================
--- HOL/examples/STE/Examples/Or.sml	                        (rev 0)
+++ HOL/examples/STE/Examples/Or.sml	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,54 @@
+(* Or Delay *)
+
+val Or_def = Define  `Or (a, b) (c, d) = (a\/c, b/\d)`;;
+
+val Or_bool_def =  Define `Or_bool s_b s_b' = 
+    !node. ((node = "out") ==> 
+	    (s_b' node = ((s_b "i0") \/ (s_b "i1"))))`;
+
+val Or_lattice_def = Define `(Or_lattice s node = 
+			    if (node = "i0")
+				then X 
+			    else if (node = "i1") then X
+			    else if (node = "out") 
+				     then 
+					 Or (s "i0")(s "i1")
+				 else
+				     X)`;
+
+val comp_list = [Or_lattice_def, Or_bool_def, Or_lattice_def];
+
+val a1 = (T, "i0", ``v1:bool``, 0, 1);
+val a2 = (T, "i1", ``v2:bool``, 0, 1);
+val c  =  (T, "out", ``(v1\/v2):bool``, 1, 2) ;
+val A  =  TF [a1, a2];
+val C  =  TF [c];
+
+(* Running the STE Simulator *)	      
+val OR_STE_IMPL1 = STE A C ``Or_lattice`` comp_list true;
+
+
+val comp_list = [Or_lattice_def, Or_bool_def, Or_lattice_def];
+
+(* under specified assertion *)
+val a1 = (T, "i0", ``v1:bool``, 0, 1);
+val c  =  (``v1:bool``, "out", ``T:bool``, 1, 2) ;
+val A  =  TF [a1];
+val C  =  TF [c];
+
+(* Running the STE Simulator *)	      
+val OR_STE_IMPL1 = STE A C ``Or_lattice`` comp_list true;
+val residue = rhs(concl OR_STE_IMPL1);
+
+set_goal([], ``v1 ==> ^residue``);
+
+(* for the case when the output of the or gate is low *)
+
+val a1 = (T, "i0", ``v1:bool``, 0, 1);
+val a2 = (T, "i1", ``v2:bool``, 0, 1);
+val c  = (T, "out", ``F:bool``, 1, 2) ;
+val A  =  TF [a1,a2];
+val C  =  TF [c];
+
+(* Running the STE Simulator *)	      
+val OR_STE_IMPL1 = STE A C ``Or_lattice`` comp_list true;


Property changes on: HOL/examples/STE/Examples/Or.sml
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-style
   + native

Added: HOL/examples/STE/README
===================================================================
--- HOL/examples/STE/README	                        (rev 0)
+++ HOL/examples/STE/README	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,77 @@
+ README File for executing the STE simulator in HOL
+ --------------------------------------------------
+
+An implementation of STE simulator in HOL is presented. Because we
+have done a deep embedding of STE one is able to reason about the STE
+logic. While reasoning about the STE logic is one useful aspect about
+this implementation, one can use an STE simulator from the HOL-ML
+prompt to see STE model checking in action. This is particularly
+useful for anyone learning STE model checking. Some example circuit
+verification and relevant papers on STE (on which this work is built)
+are also provided.
+
+------------------------------------------------------------------------------
+An early version of this work appeared in the Emerging Trends
+Proceedings of TPHOLs 2003. The title of the paper is "Formalization
+and Execution of STE in HOL". The theory that is formalized here
+appeared in the paper titled Xs are for Trajectory Evaluation,
+Booleans are for Theorem Proving by Mark Aagaard, Tom Melham and John
+O' Leary.
+
+The execution part of STE relies on implementing several lemmas and
+results from the original paper on STE by Carl Seger and Randy Bryant
+titled "Formal verification by symbolic evaluation of
+partially-ordered trajectories"
+
+-----------------------------------------------------------------------------
+
+Software Requirements
+---------------------
+
+Make sure you have Moscow ML 2.01 and HOL4 installed on your
+machine. You can obtain Moscow ML at
+http://www.dina.dk/~sestoft/mosml.html and HOL4 from
+http://hol.sourceforge.net.
+
+
+How to install Moscow ML 2.0 and HOL 4 Kananaskis 2
+---------------------------------------------------
+Useful documentation is available on
+http://hol.sourceforge.net/InstallKananaskis.html
+
+
+STEScript.sml: Contains the definition of STE Theory, relation to the
+               Boolean world, and the implementation function STE_Impl.
+               It also contains all the lemmas and theorems presented
+               in the paper.
+
+Conversion.sml:
+              Contains the ML functions and conversions for running
+              the STE simulator and obtaining the equivalent theorem
+              in HOL.
+
+
+Examples/:    Contains some illustrative examples.
+
+
+The script file and the example have been tested under HOL 4
+Kananaskis Release 2, on an Intel x86  machine running Red Hat 7.2
+Linux.
+
+How to use it?
+-------------
+
+Make sure you compile the script file by running Holmake. If Holmake
+is successful you should be able to see STETheory.sig, STETheory.ui and
+STETheory.uo in your directory where you've compiled STEScript.sml. Once
+you've the theory files ready, in an interactive session of HOL 4,
+simply *use* the RunScript file.
+
+
+A sample sesssion in HOL 4
+
+- use "RunScript";
+
+For feedback/questions: as...@co...
+
+-----------------------------------------------------------------------------


Property changes on: HOL/examples/STE/README
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-styl
   + native
Added: svn:eol-style
   + native

Added: HOL/examples/STE/RunScript
===================================================================
--- HOL/examples/STE/RunScript	                        (rev 0)
+++ HOL/examples/STE/RunScript	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,25 @@
+val _ = load "Conversion";
+val _ = load "STETheory";
+
+open Conversion;
+open STETheory;
+
+
+
+(* Inverter circuit with delay *)
+
+use "Examples/Not.sml";
+
+
+(* Nand circuit with a feedback *)
+
+use "Examples/Nand.sml";
+
+
+(* 2-bit comparator for equality testing *)
+
+use "Examples/Comparator.sml";
+
+(* 2-bit 2-to-1 MUX *)
+
+use "Examples/Mux.sml";


Property changes on: HOL/examples/STE/RunScript
___________________________________________________________________
Added: svn:mime-type
   + text/plain
Added: svn:eol-styl
   + native
Added: svn:eol-style
   + native

Added: HOL/examples/STE/STEScript.sml
===================================================================
--- HOL/examples/STE/STEScript.sml	                        (rev 0)
+++ HOL/examples/STE/STEScript.sml	2009-05-11 02:23:34 UTC (rev 6770)
@@ -0,0 +1,1659 @@
+(* ===================================================================== *)
+(* FILE          : STEScript.sml                                         *)
+(* DESCRIPTION   : STE Embedding in HOL                                  *)
+(* AUTHOR        : Ashish Darbari                                        *) 
+(* ===================================================================== *)
+(*
+(* For interactive running uncomment this part *)
+   val _ = load "stringLib";
+   val _ = load "mesonLib";
+ *)
+
+local 
+open boolLib Parse bossLib HolKernel;
+open arithmeticTheory stringLib;
+open listTheory mesonLib pairTheory;
+
+in
+
+(* Creating a new theory that will be called STE *)
+
+val _ = new_theory "STE";
+
+infix THEN THENL;
+
+(* Creating abbreviations for FULL_SIMP_TAC and RW_TAC *)
+
+val fs = FULL_SIMP_TAC std_ss;
+val fl = FULL_SIMP_TAC list_ss;
+val ARW_TAC = RW_TAC std_ss;
+
+(* Dual Rail Encoding of Lattice Values *)
+ 
+val Top_def  = Define `Top  = (F, F)`;
+val One_def  = Define `One  = (T, F)`;
+val Zero_def = Define `Zero = (F, T)`;
+val X_def    = Define `X    = (T, T)`;
+
+(* Definition of least upper bound *)
+val _ = set_fixity "lub" (Infixl 510);
+val lub_def = Define `(a, b) lub (c, d) = (a /\ c, b /\ d)`;
+
+
+(* Definition of lub on states *)
+
+val lub_state_def = Define `lub_state state1 state2 node = 
+			     (state1 node) lub (state2 node)`;
+
+(* Defintion of ordering *)
+ (*              ---
+                | 
+                 ---
+                 ---  *)              
+
+val _ = set_fixity "leq" (Infixl 510);
+val leq_def = Define `(a leq b  = (b = a lub b))`;
+
+(* Ordering lifted over states *)
+
+val _ = set_fixity "leq_state" (Infixl 510);
+val leq_state_def = Define `state1 leq_state state2
+    = !node:string. (state1 node) leq (state2 node)`; 
+
+(* Ordering lifted over sequences *)
+
+val _ = set_fixity "leq_seq" (Infixl 510);
+val leq_seq_def = Define `sigma1 leq_seq sigma2 
+    = !node:string t:num. (sigma1 t node) leq (sigma2 t node)`; 
+
+(* Definition of suffix *)
+
+val Suffix_def = Define 
+    `Suffix i (sigma: num->string->(bool # bool)) 
+    = \t node.(sigma (t+i) node)`; 
+
+
+(* Dropping from Boolean to Lattice Values *)
+
+val drop_def = Define `(drop T = One) /\ (drop F = Zero)`; 
+
+(* Drop operation lifted over states *)
+
+val extended_drop_state_def = Define 
+    `extended_drop_state (s_b:string->bool) = \node. drop (s_b node)`;
+
+
+(* Drop operation lifted over sequences *)
+
+val extended_drop_seq_def = Define 
+    `extended_drop_seq (sigma_b:num->string->bool) = \t.
+    (extended_drop_state (sigma_b t))`;
+
+(* Next state function is monotonic *)
+
+val Monotonic_def = Define `Monotonic Y_ckt = 
+    !s s'.
+    s leq_state s' ==>
+	(Y_ckt s) leq_state (Y_ckt s')`;
+	
+ 
+(* Sequence is in the STE language of a circuit  *)
+
+val in_STE_lang_def = Define `
+    in_STE_lang sigma Y_ckt = 
+    !t. (Y_ckt (sigma t)) leq_state (sigma (t+1))`; 
+
+
+(* Defining the abstract type of Trajectory formulas *)
+
+val _ = Hol_datatype 
+    `TF = Is_0 of string 
+  | Is_1 of string 
+  | AND of TF => TF
+  | WHEN of TF => bool
+  | NEXT of TF`;
+
+(* Defining the operators WHEN and AND to be left infix *)
+
+val _ = set_fixity "WHEN" (Infixl 500);    
+val _ = set_fixity "AND" (Infixl 510);
+
+(* Semantics of trajectory formula - defined wrt a sequence *)
+
+val SAT_STE_def = Define `(SAT_STE (Is_0 n) = \sigma. 
+			   Zero leq (sigma 0 n))
+
+    /\ (SAT_STE (Is_1 n) = \sigma. 
+	One leq (sigma 0 n))
+    
+    /\ (SAT_STE (tf1 AND tf2) = \sigma.
+	((SAT_STE tf1 sigma) /\ (SAT_STE tf2 sigma)))
+    
+    /\ (SAT_STE (tf WHEN (P:bool)) = \sigma. 
+	(P ==> (SAT_STE tf sigma)))
+    
+    /\ (SAT_STE (NEXT tf) = \sigma. 
+	(SAT_STE tf (Suffix 1 sigma)))`; 
+
+(* Datatype of Assertions - leadsto operator *)
+    
+val _ = Hol_datatype `Assertion = ==>> of TF => TF`;
+
+(* leadsto is infix *)
+
+val _ = set_fixity "==>>" (Infixl 470);
+    
+    
+(* Defining Sequence of a trajectory formula *)
+
+val DefSeq_def = Define `(DefSeq (Is_0 m) = \t n. 
+			  (if ((n = m) /\ (t = 0)) then Zero else X))
+    
+    /\ (DefSeq (Is_1 m) = \t n. 
+	(if ((n = m) /\ (t = 0)) then One else X))
+    
+    /\ (DefSeq (tf1 AND tf2) = \t n. 
+	((DefSeq tf1 t n) lub (DefSeq tf2 t n)))
+    
+    /\ (DefSeq (tf WHEN (P:bool)) = \t n. 
+	(P ==> FST(DefSeq tf t n),  P ==> SND(DefSeq tf t n)))
+    
+    /\ (DefSeq (NEXT tf) = \t n. 
+	(if ~(t = 0) then (DefSeq tf (t-1) n) else X))`; 
+
+
+(* Collecting the nodes in the trajectory formula *)
+
+val Nodes_def = Define `(Nodes (Is_0 n) Acc = 
+			    if MEM n Acc then Acc else (n::Acc))
+    /\ (Nodes (Is_1 n) Acc = if MEM n Acc then Acc else (n::Acc))
+    /\ (Nodes (tf1 AND tf2) Acc =  Nodes tf2 (Nodes tf1 Acc))
+    /\ (Nodes (tf WHEN P) Acc = Nodes tf Acc)
+    /\ (Nodes (NEXT tf) Acc = Nodes tf Acc)`;
+
+
+(* Useful properties about node membership *)
+
+val MEM_NODES1 = store_thm("MEM_NODES1",``!tf acc node.
+         MEM node (Nodes tf []) \/ MEM node acc =
+         MEM node (Nodes tf acc)``,
+			      Induct THEN
+			      fl [Nodes_def] 
+			      THEN REPEAT STRIP_TAC 
+			      THEN REPEAT COND_CASES_TAC 
+			      THEN fl [] THEN PROVE_TAC []);
+
+
+
+val MEM_NODES2 = store_thm("MEM_NODES2", ``!tf tf'. 
+			      ~MEM node (Nodes tf' (Nodes tf [])) =
+			      ~MEM node (Nodes tf []) 
+			      /\ ~MEM node (Nodes tf' [])``,
+			      PROVE_TAC [MEM_NODES1]);
+
+
+val MAX_def = Define `MAX t1 t2 = (if t1 >= t2 then t1 else t2)`;;
+
+(* Depth of a trajectory formula *)
+
+val Depth_def = Define `(Depth (Is_0 n) = 0)
+    /\ (Depth (Is_1 n) = 0)
+    /\ (Depth (tf1 AND tf2) = MAX (Depth tf1)(Depth tf2))
+    /\ (Depth (tf WHEN P) = Depth tf)
+    /\ (Depth (NEXT tf) = SUC (Depth tf))`;
+
+
+(* Defining Trajectory *)
+
+val DefTraj_def = Define `(DefTraj tf Model 0 node = DefSeq tf 0 node)
+    /\ (DefTraj tf Model (SUC t) node  
+	= (DefSeq tf (SUC t) node) lub (Model (DefTraj tf Model t) node))`;
+
+(* The STE implementation *)
+
+val STE_Impl_def = Define `STE_Impl (Ant ==>> Cons) Y_ckt = 
+    !t. (t <= Depth Cons ==> 
+	 !n. MEM n 
+	 (APPEND(Nodes Ant [])(Nodes Cons [])) ==>
+	     (DefSeq Cons t n) leq (DefTraj Ant Y_ckt t n))`;
+
+(* Satisfiability of a Trajectory Assertion *)
+
+val SAT_CKT_def = Define `SAT_CKT (Ant ==>> Cons) Y_ckt 
+    = !sigma. (in_STE_lang sigma Y_ckt ) 
+    ==>  (SAT_STE Ant sigma)
+    ==> (SAT_STE Cons sigma)`;
+    
+(* Boolean valued world starts here *)
+    
+(* Definition of suffix of a Boolean valued sequence *)
+
+val Suffix_b_def = Define 
+    `Suffix_b i (sigma_b:num->string->bool) 
+    = \t node.(sigma_b (t+i) node)`; 
+           
+(* Boolean Valued Sequence is in the relational model of a circuit  *)
+    
+val in_BOOL_lang_def = Define `
+    in_BOOL_lang (sigma_b:num->string->bool) Yb_ckt 
+    = !t. Yb_ckt (sigma_b t) (sigma_b (t+1))`;
+    
+(* Boolean sequence satisfies a trajectory formula *)
+    
+val SAT_BOOL_def = Define `(SAT_BOOL (Is_0 n) = \sigma_b.
+			    ((sigma_b 0 n) = F)) 
+    
+    /\ (SAT_BOOL (Is_1 n)  = \sigma_b. 
+	((sigma_b 0 n) = T))
+    
+    /\ (SAT_BOOL (tf1 AND tf2)  = \sigma_b.
+	(SAT_BOOL tf1 sigma_b) /\ (SAT_BOOL tf2 sigma_b))
+    
+    /\ (SAT_BOOL (tf WHEN (P:bool))  = \sigma_b.
+	(P ==> (SAT_BOOL tf  sigma_b)))
+    
+    /\ (SAT_BOOL (NEXT(tf))  =  \sigma_b.
+	(SAT_BOOL tf (Suffix_b 1 sigma_b)))`; 
+
+
+
+(* Linking the lattice and the Boolean Models *)
+
+val Okay_def = Define `Okay (Y_ckt, Yb_ckt) = 
+    !s_b:string->bool s_b':string->bool.
+    (Yb_ckt s_b s_b') ==> ((Y_ckt (extended_drop_state s_b)) leq_state
+			 (extended_drop_state s_b'))`;
+
+ (* Lemmas and Theorems *)
+
+
+(* Here is the Big Picture *)
+(*
+-----------Top Level Picture : BridgeTheorem ---------------------------------
+
+	A ==>> C Y  Yb
+	   |     |   |
+	   |     |   |
+	  \|/   \|/ \|/
+	   |     |   |
+	   |     |   |
+   --STE---------------------------
+  |				   |
+  | - its Okay to relate Y and Yb  |	    --- BOOLEAN ----	
+  | - Y is Monotonic		   |  ---> |                |
+  |	                           |       | Theorem in HOL |
+  | - run STE simulator to see if  |       |                | 
+  |	                           |        ----------------
+  | - Y satisfies A ==>> C	   |
+  |				   |
+    -------------------------------
+
+BridgeTheorem: 
+|- !Ant Cons Y_ckt Yb_ckt.
+	       Okay (Y_ckt, Yb_ckt) ==>
+		   Monotonic Y_ckt 
+		   ==>  
+		   (
+		    
+		    (!t.
+		     t <= Depth Cons ==>
+			 !n.
+			 MEM n (Nodes Ant APPEND Nodes Cons) ==>
+			     leq (DefSeq Cons t n) (DefTraj Ant Y_ckt t n))
+		    
+		    ==>
+		    (
+		     !sigma_b.
+		     in_BOOL_lang sigma_b Yb_ckt ==>
+			 !t.
+			 SAT_BOOL Ant (Suffix_b t sigma_b) ==>
+			     SAT_BOOL Cons (Suffix_b t sigma_b))
+		    ) : thm
+
+Proof of BridgeTheorem:
+			
+			Relies on proving SAT_CKT_IFF_STE_IMPL and Theorem2
+------------------------------------------------------------------------------
+
+
+---------------SAT_CKT_IFF_STE_IMPL--------------------------------------------
+
+
+	A ==>> C Y  
+	   |     |  
+	   |     |  
+	  \|/   \|/ 
+	   |     |  
+	   |     |  
+  ----------------------------------- 	   	
+ |				     |		
+ | If Y is monotonic then	     |
+ | the jth suffix of the lattice     |
+ | valued sequence satisfies the     |
+ | STE assertion if and only if	     |
+ | the STE implementation (STE_Impl) |
+ | does.			     |
+  -----------------------------------
+
+STE_Impl is defined as:
+
+|- !Ant Cons Y_ckt.
+         STE_Impl (Ant ==>> Cons) Y_ckt =
+         !t.
+           t <= Depth Cons ==>
+           !n.
+             MEM n (Nodes Ant APPEND Nodes Cons) ==>
+             leq (DefSeq Cons t n) (DefTraj Ant Y_ckt t n) : thm
+
+SAT_CKT_IFF_STE_IMPL:
+
+ |- !Ant Cons Y_ckt.
+         Monotonic Y_ckt ==>
+         ((!sigma.
+             in_STE_lang sigma Y_ckt ==>
+             !j.
+               SAT_STE Ant (Suffix j sigma) ==>
+               SAT_STE Cons (Suffix j sigma)) =
+          !t.
+            t <= Depth Cons ==>
+            !n.
+              MEM n (Nodes Ant APPEND Nodes Cons) ==>
+              leq (DefSeq Cons t n) (DefTraj Ant Y_ckt t n)) : thm
+
+
+Proof of SAT_CKT_IFF_STE_IMPL:
+			Relies on SAT_CKT_IFF_TIME_SHIFT theorem and
+			AuxTheorem1 (relies on Y being monotonic)
+
+------------------------------------------------------------------------------
+
+-------------------Theorem2---------------------------------------------------
+
+	
+	 ----------------------------------
+	| If its Okay to relate Y and Yb,  |
+        | and Y is monotonic               |
+	| then if the lattice sequence	   |
+	| which is in the langauge of Y    |
+	| satisfies the STE assertion,     |
+	| the Boolean sequence which is	   |
+	| in the language of Yb also	   |
+	| satisfies the same STE assertion |
+         ---------------------------------
+
+
+Theorem2:
+
+|- !Ant Cons Y_ckt Yb_ckt.
+         Okay (Y_ckt,Yb_ckt) 
+	 ==> 
+         (!sigma.
+            in_STE_lang sigma Y_ckt ==>
+            !t.
+              SAT_STE Ant (Suffix t sigma) ==>
+              SAT_STE Cons (Suffix t sigma)) ==>
+         !sigma_b.
+           in_BOOL_lang sigma_b Yb_ckt ==>
+           !t.
+             SAT_BOOL Ant (Suffix_b t sigma_b) ==>
+             SAT_BOOL Cons (Suffix_b t sigma_b) : thm
+
+Proof of Theorem2:
+		  Relies on Lemma1, Lemma2 and Suffix_Lemma
+
+------------------------------------------------------------------------------
+
+*)
+
+
+(* If its Okay to relate Y and Yb then for all Boolean valued 
+   sequences which are in the language of the Boolean Model Yb,
+   the drop of the Boolean valued sequence is in the language
+   of the lattice model Y.
+       
+  Lemma1 is used in the proof of Theorem2
+
+*)
+
+val Lemma1 = 
+    store_thm ("Lemma1", 
+	       ``!Y_ckt Yb_ckt. Okay (Y_ckt, Yb_ckt) 
+	       ==> !sigma_b. 
+	       in_BOOL_lang sigma_b Yb_ckt
+	       ==>  in_STE_lang (extended_drop_seq sigma_b) Y_ckt``,
+	       STRIP_TAC THEN fs [Okay_def, in_BOOL_lang_def, 
+				  in_STE_lang_def, 
+				  extended_drop_seq_def]);
+
+(* Calculating the Suffix after calculating the
+   drop of the Boolean valued sequence, results 
+   in the sequence that one obtains by first calculating
+   the Suffix of the Boolean valued sequence and then 
+   dropping it
+   
+   Suffix_Lemma is used in the proof of Theorem2
+   
+*)   
+val Suffix_Lemma = TAC_PROOF(([], ``!t sigma_b. 
+   (Suffix t (extended_drop_seq sigma_b)) = 
+   (extended_drop_seq (Suffix_b t sigma_b))``), 
+
+			      (REPEAT STRIP_TAC
+			       THEN Induct_on `t` 
+			       THEN fs [Suffix_def, Suffix_b_def, 
+					extended_drop_seq_def,
+					extended_drop_state_def, drop_def])
+			      );
+
+
+(* Lemma2_1 is used in the proof of Lemma 2 *)
+
+val Lemma2_1 = prove (``!tf sigma_b. SAT_BOOL tf sigma_b
+		      ==> SAT_STE tf (extended_drop_seq sigma_b)``, 
+   
+		      STRIP_TAC 
+		      THEN Induct_on `tf` 
+		      THEN fs [SAT_BOOL_def, SAT_STE_def]
+		      THEN fs [extended_drop_seq_def, 
+			       extended_drop_state_def,
+			       drop_def, leq_def, Zero_def, 
+			       lub_def]
+		      THEN fs [extended_drop_seq_def, 
+			       extended_drop_state_def,
+			       drop_def, leq_def, One_def, lub_def]
+		      THEN fs [Suffix_def, Suffix_b_def, 
+			       extended_drop_seq_def,
+			       extended_drop_state_def]
+		      
+		      );
+
+
+(* Lemma2_2 is used in the proof of Lemma 2 *)
+
+val Lemma2_2 = prove (``!tf sigma_b. SAT_STE tf (extended_drop_seq sigma_b)
+		      ==> SAT_BOOL tf sigma_b``,
+		      
+		      STRIP_TAC THEN Induct_on `tf` 
+		      THEN fs [SAT_STE_def, SAT_BOOL_def, 
+			       extended_drop_seq_def, 
+			       extended_drop_state_def, drop_def]
+		      THEN REPEAT STRIP_TAC
+		      THEN fs [Zero_def, One_def, drop_def, leq_def, lub_def]
+		      
+		      
+		      THEN fs [SAT_STE_def, SAT_BOOL_def, 
+			       extended_drop_seq_def, 
+			       extended_drop_state_def, drop_def]
+		      THEN REPEAT STRIP_TAC
+		      THEN fs [Zero_def, One_def, drop_def, 
+			       leq_def, lub_def]
+		      THEN Induct_on `sigma_b 0 s = T`
+		      THEN fs [drop_def, lub_def, Zero_def, One_def]
+		      THEN fs [SAT_STE_def, SAT_BOOL_def, 
+			       extended_drop_seq_def, extended_drop_state_def, 
+			       Suffix_def, Suffix_b_def]
+		      );
+
+(* Trajectory formula is satisfiable by a Boolean valued sequence
+   if and only if the trajectory formula is satisfiable by the
+   drop of the Boolean valued sequence
+
+*)
+
+val Lemma2 = prove (``!tf sigma_b. SAT_BOOL tf sigma_b =
+		    SAT_STE tf (extended_drop_seq sigma_b)``,
+		    
+		    REPEAT STRIP_TAC THEN EQ_TAC 
+		    THEN fs [Lemma2_1, Lemma2_2]);
+
+
+(* Properties of drop operation 
+   An interesting property though these lemmas are not used anywhere
+*)
+
+
+val Lemma3_1 = prove(``!sigma_b:num->string->bool. 
+		      (sigma_b 0 node = F) 
+		      = (Zero leq ((extended_drop_seq sigma_b) 0 node))``,
+		      
+		      STRIP_TAC THEN EQ_TAC 
+		      THEN fs [extended_drop_seq_def, extended_drop_state_def, 
+			       drop_def, leq_def, lub_def]
+		      THEN fs [lub_def, Zero_def]
+		      THEN fs [extended_drop_seq_def, extended_drop_state_def, 
+			       drop_def, leq_def, lub_def]
+		      THEN STRIP_TAC
+		      THEN Induct_on `sigma_b 0 node = T` 
+		      THEN fs [drop_def, lub_def, Zero_def, One_def]
+		      THEN fs [drop_def, lub_def, Zero_def, One_def]);
+
+    
+val Lemma3_2 = prove(``!sigma_b:num->string->bool. (sigma_b 0 node = T) 
+		     = (One leq ((extended_drop_seq sigma_b) 0 node))``,
+		     
+		     STRIP_TAC THEN EQ_TAC 
+		     THEN fs [extended_drop_seq_def, extended_drop_state_def, 
+			      drop_def, leq_def, lub_def]
+		     THEN fs [lub_def, Zero_def]
+		     THEN fs [extended_drop_seq_def, extended_drop_state_def, 
+			      drop_def, leq_def, lub_def]
+		     THEN STRIP_TAC
+		     THEN Induct_on `sigma_b 0 node = T` 
+		     THEN fs [drop_def, lub_def, Zero_def, One_def]
+		     THEN fs [drop_def, lub_def, Zero_def, One_def]);
+
+(* lattice_X1_lemma and lattice_X2_lemma state the same thing -
+   that the lub of any lattice value and X is that lattice value.
+   We have two versions they get used as and when they are needed
+   in the proofs of other lemmas 
+       
+   Used in the proof of DEFSEQ_LE_THAN_SAT_STE1 and AuxTheorem1
+
+*)
+
+val lattice_X1_lemma = store_thm ("lattice_X1_lemma", 
+				  ``!elem. elem = X lub elem``, 
+				  STRIP_TAC THEN Cases_on `elem` 
+				  THEN fs [lub_def, X_def]);
+
+val lattice_X2_lemma = TAC_PROOF(([], ``!elem. elem = (T, T) lub elem``), 
+				STRIP_TAC THEN Cases_on `elem` 
+				 THEN fs [lub_def]);
+
+(* If a number is not zero, it must be either equal to 1 or greater than 1
+
+   Used in the proof of DEFSEQ_LE_THAN_SAT_STE1
+*)
+
+
+val NUM_LEMMA = TAC_PROOF(([], ``!t. ~(t = 0) ==> 1 <= t``), 
+			  Induct THEN DECIDE_TAC
+			  );
+
+(* Transitivity Lemma 
+  Used in the proof of SEQ_LESS_THAN_SAT_STE and 
+  DEFTRAJ_LESSTHAN_SEQ_IMP_SAT_STE_2
+ 
+*)
+val TRANS_LEMMA = 
+    TAC_PROOF(([],  ``!a c. (?b. a leq b /\ b leq c) ==> a leq c``),
+        REPEAT Cases THEN STRIP_TAC THEN Cases_on `b` THEN
+        fs [leq_def, lub_def] THEN PROVE_TAC[]);;
+
+
+
+(* A rather obvious but useful lemma that the 0th suffix of the se...
 
[truncated message content]