fun-op-sem/cbv-lc/logrelScript.sml

54  rw [] >>
56  rw [] >>
78  rw [] >>
136      rw [] >>
139      rw [] >>
152      rw [] >>
163  rw [LIST_REL_EL_EQN] >>
171  rw [LIST_REL_EL_EQN] >>
179  rw [exp_rel_def] >>
180  rw [exec_rel_rw, sem_def] >>
181  rw [res_rel_def, val_rel_rw] >>
188  rw [exp_rel_def, sem_def, exec_rel_rw] >>
193  rw [val_rel_rw, res_rel_def]
200 local val rw = srw_tac[] val fs = fsrw_tac[] in
207  rw [exp_rel_def, sem_def] >>
211  rw [] >>
216  rw [] >>
218  rw [LET_THM] >>
232  rw [] >>
234  rw [] >>
239  rw [] >>
241  rw []
259  rw [exp_rel_def, sem_def] >>
260  rw [exec_rel_rw] >>
262  rw [val_rel_rw, res_rel_def]
266  rw [] >>
275  rw [exp_rel_def, sem_def] >>
276  rw [exec_rel_rw] >>
280  rw [res_rel_rw]
288  rw [] >>
291  rw [LET_THM]);
296  rw [] >>
303  rw [val_rel_rw] >>
307  rw [] >>
313  rw [state_rel_rw, LIST_REL_EL_EQN] >>
324  rw [ctxt_rel_def, ctxt_to_exp_def]);
328  rw [ctxt_rel_def, ctxt_to_exp_def] >>
333  rw [ctxt_rel_def, ctxt_to_exp_def] >>
338  rw [ctxt_rel_def, ctxt_to_exp_def] >>
343  rw [ctxt_rel_def, ctxt_to_exp_def] >>
349  rw [] >>
354  rw [ctxt_approx_def] >>
362  rw [] >>
367             by rw [state_rel_rw] >>
368      `LIST_REL (val_rel c) [] []` by rw [] >>
372      rw [] >>
393             by rw [state_rel_rw] >>
394      `LIST_REL (val_rel c) [] []` by rw [] >>
398      rw [] >>
401      rw [] >>
415  rw [] >>
419 local val rw = srw_tac[] val fs = fsrw_tac[] in
427  rw [exec_rel_rw] >>
429  rw [LET_THM] >>
444  rw [exec_rel_rw] >>
446  rw [LET_THM] >>
460  rw [val_rel_rw]);
464  rw [state_rel_rw, LIST_REL_EL_EQN] >>
472  rw [val_rel_rw]
475      rw [] >>
480      rw [] >>
482      rw [] >>
487      rw [exec_rel_rw, LET_THM] >>
489      rw [] >>
491      rw [res_rel_rw]
493          rw [exec_rel_rw] >>
495          rw [LET_THM] >>
502          rw [] >>
504          rw [LET_THM] >>
514          rw [exec_rel_rw] >>
516          rw [LET_THM] >>
523          rw [] >>
525          rw [LET_THM] >>
536  rw [exp_rel_def] >>
564  `s2 = s2 with clock := s2.clock` by rw [] >>
576  rw [] >>
579  rw [] >>
596  rw [] >>
605  rw [] >>
608  reverse (rw [])
611      rw [] >>
612      rw []) >>
618      rw [] >>
619      rw [] >>
622  rw [] >>