equal
deleted
inserted
replaced
64 |
64 |
65 Goal "G component F ==> F Join G = F"; |
65 Goal "G component F ==> F Join G = F"; |
66 by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def])); |
66 by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def])); |
67 qed "Join_absorb2"; |
67 qed "Join_absorb2"; |
68 |
68 |
69 Goal |
69 Goal "H:program==>(JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)"; |
70 "H:program==>(JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)"; |
|
71 by (case_tac "I=0" 1); |
70 by (case_tac "I=0" 1); |
72 by (Force_tac 1); |
71 by (Force_tac 1); |
73 by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
72 by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
74 by Auto_tac; |
73 by Auto_tac; |
75 by (dres_inst_tac [("c", "xb"), ("A", "AllowedActs(H)")] subsetD 2); |
74 by (dres_inst_tac [("c", "xb"), ("A", "AllowedActs(H)")] subsetD 2); |