1structure Conversion :> Conversion = 2struct 3 4open HolKernel Parse boolLib 5 6(* 7val _ = load "stringLib"; 8val _ = load "listTheory"; 9val _ = load "pairTheory"; 10val _ = load "arithmeticTheory"; 11*) 12local 13open bossLib; 14open boolTheory; 15open stringLib; 16open Conv; 17open Parse; 18open listTheory; 19open pairTheory; 20open arithmeticTheory; 21open STETheory; 22open Lib; 23open Drule; 24in 25 26 27val base_defn_list = [DefTraj_def, DefSeq_def, leq_def, 28 lub_def, Zero_def, 29 One_def, X_def, FST, 30 SND, Depth_def, 31 Nodes_def, APPEND, MAX_def, 32 MEM]; 33 34val CONV = SIMP_CONV arith_ss [DISJ_IMP_THM, FORALL_AND_THM, 35 UNWIND_FORALL_THM1]; 36 37 38 39fun STE_CONV_RULE theorem thm_list = 40 41 let 42 val TrajConv = computeLib.CBV_CONV (computeLib.new_compset thm_list) 43 val NC = computeLib.CBV_CONV (reduceLib.num_compset()) 44 val BC = computeLib.CBV_CONV (computeLib.bool_compset()) 45 in 46 CONV_RULE(EVERY_CONV [TrajConv, NC, TrajConv, BC]) theorem 47 end; 48 49 50(* Some user-interface functions *) 51fun add_next start term = 52 if start = 0 then term 53 else 54 let val newstart = start - 1 55 in 56 add_next newstart (``NEXT ^term``) 57 end; 58 59fun add_next_upto_depth start depth term = 60 if (start = (depth-1)) then 61 add_next start term 62 else 63 ``^(add_next start term) AND 64 ^(add_next_upto_depth (start+1) depth term)``; 65 66fun TrajForm (guard:term, n:string, value:term, START, END) = 67 let val node = stringLib.fromMLstring n 68 val atom = 69 ``((Is_1 ^node) WHEN (^value/\ ^guard)) 70 AND 71 ((Is_0 ^node) WHEN ~(^value /\ ^guard))``; 72 in 73 add_next_upto_depth START END atom 74 end; 75 76fun TF [x] = TrajForm x 77| TF (x::xs) = ``^(TrajForm x) AND ^(TF xs)``; 78 79fun extract_constr theorem = fst(boolSyntax.dest_imp(Thm.concl theorem)); 80 81 82(* STE Simulator over lattice models *) 83(* verbose switches the print options *) 84fun STE A C Y comp_list verbose = 85if verbose then 86let 87val clock = start_time(); 88val thm_list = comp_list @ base_defn_list; 89val _ = print ("\nSpecialising the STE Implementation definition..."); 90val iter0 = SPECL [A, C, Y] STE_Impl_def; 91val _ = print ("done\n"); 92val _ = print ("Calculating the depth of the formula..."); 93val iter1 = RIGHT_CONV_RULE(SIMP_CONV arith_ss [Depth_def, MAX_def]) iter0; 94val _ = print ("done\n"); 95val _ = print("Rewriting for less than or equal..."); 96val iter2 = RIGHT_CONV_RULE(SIMP_CONV std_ss [LESS_OR_EQ]) iter1; 97val _ = print("done\n"); 98val _ = print("Rewriting for less than..."); 99val iter3 = RIGHT_CONV_RULE(SIMP_CONV arith_ss [LESS_EQ]) iter2; 100val _ = print("done\n"); 101val _ = print("Calculating the nodes in the antecedent and consequent..."); 102val iter4 = RIGHT_CONV_RULE(STRIP_QUANT_CONV(RAND_CONV(EVAL))) iter3; 103val _ = print("done\n"); 104val _ = print ("Rewriting with DISJ_IMP_THM..."); 105val iter5a = RIGHT_CONV_RULE(SIMP_CONV std_ss [DISJ_IMP_THM]) iter4; 106val _ = print("done\n"); 107val _ = print ("Rewriting with FORALL_AND_THM..."); 108val iter5b = RIGHT_CONV_RULE(SIMP_CONV std_ss [FORALL_AND_THM]) iter5a; 109val _ = print("done\n"); 110val _ = print ("Rewriting with UNWINDFORALL_THM1..."); 111val iter5 = RIGHT_CONV_RULE(SIMP_CONV std_ss [UNWIND_FORALL_THM1]) iter5b; 112val _ = print ("done\n"); 113val _ = print("Running STE..."); 114val iter6 = STE_CONV_RULE iter5 thm_list; 115val iter7 = RIGHT_CONV_RULE(TOP_DEPTH_CONV(stringLib.string_EQ_CONV) 116 THENC (TOP_DEPTH_CONV(COND_CONV))) iter6; 117val _ = print("done\n"); 118val _ = print ("Canonicalising booleans..."); 119val iter8 = RIGHT_CONV_RULE(EVAL) iter7; 120val _ = print ("done\n"); 121val _ = end_time clock 122in 123iter8 124end 125else 126let 127val clock = start_time(); 128val thm_list = comp_list @ base_defn_list; 129val iter0 = SPECL [A, C, Y] STE_Impl_def; 130val iter1 = RIGHT_CONV_RULE(SIMP_CONV arith_ss [Depth_def, MAX_def]) iter0; 131val iter2 = RIGHT_CONV_RULE(SIMP_CONV std_ss [LESS_OR_EQ]) iter1; 132val iter3 = RIGHT_CONV_RULE(SIMP_CONV arith_ss [LESS_EQ]) iter2; 133val iter4 = RIGHT_CONV_RULE(STRIP_QUANT_CONV(RAND_CONV(EVAL))) iter3; 134val iter5a = RIGHT_CONV_RULE(SIMP_CONV std_ss [DISJ_IMP_THM]) iter4; 135val iter5b = RIGHT_CONV_RULE(SIMP_CONV std_ss [FORALL_AND_THM]) iter5a; 136val iter5 = RIGHT_CONV_RULE(SIMP_CONV std_ss [UNWIND_FORALL_THM1]) iter5b; 137val iter6 = STE_CONV_RULE iter5 thm_list; 138val iter7 = RIGHT_CONV_RULE(TOP_DEPTH_CONV(stringLib.string_EQ_CONV) 139 THENC (TOP_DEPTH_CONV(COND_CONV))) iter6; 140val iter8 = RIGHT_CONV_RULE(EVAL) iter7; 141val _ = end_time clock 142in 143iter8 144end; 145 146 147 148(* From STE World to the Boolean World *) 149fun STE_TO_BOOL A C Y Yb ok_thm monotonic_thm ste_impl_result = 150 let val iter1 = SPECL [A, C, Y, Yb] BRIDGETHEOREM2; 151 val iter2 = CONV_RULE(SIMP_CONV arith_ss [ok_thm]) iter1; 152 val iter3 = CONV_RULE(SIMP_CONV arith_ss [monotonic_thm]) iter2; 153 val iter4 = 154 CONV_RULE(SIMP_CONV bool_ss [DE_MORGAN_THM]) ste_impl_result; 155 val iter5 = CONV_RULE(SIMP_CONV std_ss [iter4]) iter3 156in 157 iter5 158 end; 159 160end 161 162end (* struct *) 163