equal
deleted
inserted
replaced
12 auto(); |
12 auto(); |
13 qed"compatibility_consequence3"; |
13 qed"compatibility_consequence3"; |
14 |
14 |
15 |
15 |
16 goal thy |
16 goal thy |
17 "!! A B. [| compat_ioas A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \ |
17 "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \ |
18 \ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
18 \ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
19 br ForallPFilterQR 1; |
19 br ForallPFilterQR 1; |
20 ba 2; |
20 ba 2; |
21 br compatibility_consequence3 1; |
21 br compatibility_consequence3 1; |
22 by (REPEAT (asm_full_simp_tac (!simpset |
22 by (REPEAT (asm_full_simp_tac (!simpset |
30 goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA"; |
30 goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA"; |
31 auto(); |
31 auto(); |
32 qed"compatibility_consequence4"; |
32 qed"compatibility_consequence4"; |
33 |
33 |
34 goal thy |
34 goal thy |
35 "!! A B. [| compat_ioas A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \ |
35 "!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \ |
36 \ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
36 \ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
37 br ForallPFilterQR 1; |
37 br ForallPFilterQR 1; |
38 ba 2; |
38 ba 2; |
39 br compatibility_consequence4 1; |
39 br compatibility_consequence4 1; |
40 by (REPEAT (asm_full_simp_tac (!simpset |
40 by (REPEAT (asm_full_simp_tac (!simpset |
50 |
50 |
51 goal thy "!! A1 A2 B1 B2. \ |
51 goal thy "!! A1 A2 B1 B2. \ |
52 \ [| IOA A1; IOA A2; IOA B1; IOA B2;\ |
52 \ [| IOA A1; IOA A2; IOA B1; IOA B2;\ |
53 \ is_asig (asig_of A1); is_asig (asig_of A2); \ |
53 \ is_asig (asig_of A1); is_asig (asig_of A2); \ |
54 \ is_asig (asig_of B1); is_asig (asig_of B2); \ |
54 \ is_asig (asig_of B1); is_asig (asig_of B2); \ |
55 \ compat_ioas A1 B1; compat_ioas A2 B2; \ |
55 \ compatible A1 B1; compatible A2 B2; \ |
56 \ A1 =<| A2; \ |
56 \ A1 =<| A2; \ |
57 \ B1 =<| B2 |] \ |
57 \ B1 =<| B2 |] \ |
58 \ ==> (A1 || B1) =<| (A2 || B2)"; |
58 \ ==> (A1 || B1) =<| (A2 || B2)"; |
59 |
59 |
60 by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1); |
60 by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1); |