equal
deleted
inserted
replaced
60 |
60 |
61 is_prophecy_relation_def: |
61 is_prophecy_relation_def: |
62 "is_prophecy_relation R C A == is_backward_simulation R C A & |
62 "is_prophecy_relation R C A == is_backward_simulation R C A & |
63 is_ref_map (%x.(@y. (x,y):(R^-1))) A C" |
63 is_ref_map (%x.(@y. (x,y):(R^-1))) A C" |
64 |
64 |
65 ML {* use_legacy_bindings (the_context ()) *} |
65 |
|
66 lemma set_non_empty: "(A~={}) = (? x. x:A)" |
|
67 apply auto |
|
68 done |
|
69 |
|
70 lemma Int_non_empty: "(A Int B ~= {}) = (? x. x: A & x:B)" |
|
71 apply (simp add: set_non_empty) |
|
72 done |
|
73 |
|
74 |
|
75 lemma Sim_start_convert: |
|
76 "(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)" |
|
77 apply (unfold Image_def) |
|
78 apply (simp add: Int_non_empty) |
|
79 done |
|
80 |
|
81 declare Sim_start_convert [simp] |
|
82 |
|
83 |
|
84 lemma ref_map_is_simulation: |
|
85 "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A" |
|
86 |
|
87 apply (unfold is_ref_map_def is_simulation_def) |
|
88 apply simp |
|
89 done |
66 |
90 |
67 end |
91 end |