equal
deleted
inserted
replaced
5 |
5 |
6 Extending of state sets |
6 Extending of state sets |
7 function f (forget) maps the extended state to the original state |
7 function f (forget) maps the extended state to the original state |
8 function g (forgotten) maps the extended state to the "extending part" |
8 function g (forgotten) maps the extended state to the "extending part" |
9 *) |
9 *) |
10 |
|
11 Goal "inj f ==> (f a : f``A) = (a : A)"; |
|
12 by (blast_tac (claset() addDs [injD]) 1); |
|
13 qed "inj_image_mem_iff"; |
|
14 |
|
15 |
|
16 Goal "inj f ==> (f``A = f``B) = (A = B)"; |
|
17 by (blast_tac (claset() addSEs [equalityE] |
|
18 addDs [injD]) 1); |
|
19 qed "inj_image_eq_iff"; |
|
20 |
|
21 |
|
22 val rinst = read_instantiate_sg (sign_of thy); |
|
23 |
|
24 (*** General lemmas ***) |
|
25 |
10 |
26 Open_locale "Extend"; |
11 Open_locale "Extend"; |
27 |
12 |
28 val slice_def = thm "slice_def"; |
13 val slice_def = thm "slice_def"; |
29 val f_act_def = thm "f_act_def"; |
14 val f_act_def = thm "f_act_def"; |