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