Changeset 3047 for src/correctness.ma


Ignore:
Timestamp:
Mar 31, 2013, 10:01:42 PM (6 years ago)
Author:
campbell
Message:

Switch removal and labelling combined.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r3030 r3047  
    33
    44include "ASM/Interpret2.ma".
    5 
    6 include "Clight/labelSimulation.ma".
    75
    86include "Clight/Clight_classified_system.ma".
     
    7472include "common/ExtraMonads.ma".
    7573
     74include "Clight/SwitchAndLabel.ma".
     75
    7676theorem correct :
    7777  ∀observe.
     
    110110
    111111#NOT_WRONG %
    112 [ cases daemon (* TODO *)
     112[ whd in EQ_front_end:(??%%); destruct
     113  cut (labelled = \fst (clight_label cl_switch_removed))
     114  [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
     115  #E >E
     116  @switch_and_labelling_sim @NOT_WRONG
    113117| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
    114118
Note: See TracChangeset for help on using the changeset viewer.