19 |
19 |
20 (* ------------------------------------------------------------------------- *) |
20 (* ------------------------------------------------------------------------- *) |
21 (* Equality rules for union *) |
21 (* Equality rules for union *) |
22 (* ------------------------------------------------------------------------- *) |
22 (* ------------------------------------------------------------------------- *) |
23 |
23 |
24 goalw SubUnion.thy [union_def] |
24 Goalw [union_def] |
25 "!!u. n:nat==>Var(n) un Var(n)=Var(n)"; |
25 "!!u. n:nat==>Var(n) un Var(n)=Var(n)"; |
26 by (Asm_simp_tac 1); |
26 by (Asm_simp_tac 1); |
27 by (simp_tac (rank_ss addsimps redexes.con_defs) 1); |
27 by (simp_tac (rank_ss addsimps redexes.con_defs) 1); |
28 qed "union_Var"; |
28 qed "union_Var"; |
29 |
29 |
30 goalw SubUnion.thy [union_def] |
30 Goalw [union_def] |
31 "!!u.[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)"; |
31 "!!u.[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)"; |
32 by (Asm_simp_tac 1); |
32 by (Asm_simp_tac 1); |
33 by (simp_tac (rank_ss addsimps redexes.con_defs) 1); |
33 by (simp_tac (rank_ss addsimps redexes.con_defs) 1); |
34 qed "union_Fun"; |
34 qed "union_Fun"; |
35 |
35 |
36 goalw SubUnion.thy [union_def] |
36 Goalw [union_def] |
37 "!!u.[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \ |
37 "!!u.[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \ |
38 \ App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)"; |
38 \ App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)"; |
39 by (Asm_simp_tac 1); |
39 by (Asm_simp_tac 1); |
40 by (simp_tac (rank_ss addsimps redexes.con_defs) 1); |
40 by (simp_tac (rank_ss addsimps redexes.con_defs) 1); |
41 qed "union_App"; |
41 qed "union_App"; |
63 |
63 |
64 (* ------------------------------------------------------------------------- *) |
64 (* ------------------------------------------------------------------------- *) |
65 (* comp proofs *) |
65 (* comp proofs *) |
66 (* ------------------------------------------------------------------------- *) |
66 (* ------------------------------------------------------------------------- *) |
67 |
67 |
68 goal SubUnion.thy "!!u. u:redexes ==> u ~ u"; |
68 Goal "!!u. u:redexes ==> u ~ u"; |
69 by (eresolve_tac [redexes.induct] 1); |
69 by (eresolve_tac [redexes.induct] 1); |
70 by (ALLGOALS Fast_tac); |
70 by (ALLGOALS Fast_tac); |
71 qed "comp_refl"; |
71 qed "comp_refl"; |
72 |
72 |
73 goal SubUnion.thy |
73 Goal |
74 "!!u. u ~ v ==> v ~ u"; |
74 "!!u. u ~ v ==> v ~ u"; |
75 by (etac Scomp.induct 1); |
75 by (etac Scomp.induct 1); |
76 by (ALLGOALS Fast_tac); |
76 by (ALLGOALS Fast_tac); |
77 qed "comp_sym"; |
77 qed "comp_sym"; |
78 |
78 |
79 goal SubUnion.thy |
79 Goal |
80 "u ~ v <-> v ~ u"; |
80 "u ~ v <-> v ~ u"; |
81 by (fast_tac (claset() addIs [comp_sym]) 1); |
81 by (fast_tac (claset() addIs [comp_sym]) 1); |
82 qed "comp_sym_iff"; |
82 qed "comp_sym_iff"; |
83 |
83 |
84 |
84 |
85 goal SubUnion.thy |
85 Goal |
86 "!!u. u ~ v ==> ALL w. v ~ w-->u ~ w"; |
86 "!!u. u ~ v ==> ALL w. v ~ w-->u ~ w"; |
87 by (etac Scomp.induct 1); |
87 by (etac Scomp.induct 1); |
88 by (ALLGOALS Fast_tac); |
88 by (ALLGOALS Fast_tac); |
89 qed_spec_mp "comp_trans"; |
89 qed_spec_mp "comp_trans"; |
90 |
90 |
91 (* ------------------------------------------------------------------------- *) |
91 (* ------------------------------------------------------------------------- *) |
92 (* union proofs *) |
92 (* union proofs *) |
93 (* ------------------------------------------------------------------------- *) |
93 (* ------------------------------------------------------------------------- *) |
94 |
94 |
95 goal SubUnion.thy |
95 Goal |
96 "!!u. u ~ v ==> u <== (u un v)"; |
96 "!!u. u ~ v ==> u <== (u un v)"; |
97 by (etac Scomp.induct 1); |
97 by (etac Scomp.induct 1); |
98 by (etac boolE 3); |
98 by (etac boolE 3); |
99 by (ALLGOALS Asm_full_simp_tac); |
99 by (ALLGOALS Asm_full_simp_tac); |
100 qed "union_l"; |
100 qed "union_l"; |
101 |
101 |
102 goal SubUnion.thy |
102 Goal |
103 "!!u. u ~ v ==> v <== (u un v)"; |
103 "!!u. u ~ v ==> v <== (u un v)"; |
104 by (etac Scomp.induct 1); |
104 by (etac Scomp.induct 1); |
105 by (eres_inst_tac [("c","b2")] boolE 3); |
105 by (eres_inst_tac [("c","b2")] boolE 3); |
106 by (ALLGOALS Asm_full_simp_tac); |
106 by (ALLGOALS Asm_full_simp_tac); |
107 qed "union_r"; |
107 qed "union_r"; |
108 |
108 |
109 goal SubUnion.thy |
109 Goal |
110 "!!u. u ~ v ==> u un v = v un u"; |
110 "!!u. u ~ v ==> u un v = v un u"; |
111 by (etac Scomp.induct 1); |
111 by (etac Scomp.induct 1); |
112 by (ALLGOALS(asm_simp_tac (simpset() addsimps [or_commute]))); |
112 by (ALLGOALS(asm_simp_tac (simpset() addsimps [or_commute]))); |
113 qed "union_sym"; |
113 qed "union_sym"; |
114 |
114 |
115 (* ------------------------------------------------------------------------- *) |
115 (* ------------------------------------------------------------------------- *) |
116 (* regular proofs *) |
116 (* regular proofs *) |
117 (* ------------------------------------------------------------------------- *) |
117 (* ------------------------------------------------------------------------- *) |
118 |
118 |
119 goal SubUnion.thy |
119 Goal |
120 "!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"; |
120 "!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"; |
121 by (etac Scomp.induct 1); |
121 by (etac Scomp.induct 1); |
122 by (ALLGOALS(asm_full_simp_tac |
122 by (ALLGOALS(asm_full_simp_tac |
123 (simpset() setloop(SELECT_GOAL Safe_tac)))); |
123 (simpset() setloop(SELECT_GOAL Safe_tac)))); |
124 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1); |
124 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1); |