21 (* Equality rules for union *) |
21 (* Equality rules for union *) |
22 (* ------------------------------------------------------------------------- *) |
22 (* ------------------------------------------------------------------------- *) |
23 |
23 |
24 goalw SubUnion.thy [union_def] |
24 goalw SubUnion.thy [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 redexes_ss 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 val union_Var = result(); |
28 val union_Var = result(); |
29 |
29 |
30 goalw SubUnion.thy [union_def] |
30 goalw SubUnion.thy [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 redexes_ss 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 val union_Fun = result(); |
34 val union_Fun = result(); |
35 |
35 |
36 goalw SubUnion.thy [union_def] |
36 goalw SubUnion.thy [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 redexes_ss 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 val union_App = result(); |
41 val union_App = result(); |
42 |
42 |
43 val union_ss = redexes_ss addsimps |
43 Addsimps (Ssub.intrs@bool_typechecks@ |
44 (Ssub.intrs@bool_simps@bool_typechecks@ |
44 Sreg.intrs@Scomp.intrs@ |
45 Sreg.intrs@Scomp.intrs@ |
45 [or_1 RSN (3,or_commute RS trans), |
46 [or_1 RSN (3,or_commute RS trans), |
46 or_0 RSN (3,or_commute RS trans), |
47 or_0 RSN (3,or_commute RS trans), |
47 union_App,union_Fun,union_Var,compD2,compD1,regD]); |
48 union_App,union_Fun,union_Var,compD2,compD1,regD]); |
|
49 |
48 |
50 val union_cs = (ZF_cs addIs Scomp.intrs addSEs |
49 AddIs Scomp.intrs; |
51 [Sreg.mk_cases redexes.con_defs "regular(App(b,f,a))", |
50 AddSEs [Sreg.mk_cases redexes.con_defs "regular(App(b,f,a))", |
52 Sreg.mk_cases redexes.con_defs "regular(Fun(b))", |
51 Sreg.mk_cases redexes.con_defs "regular(Fun(b))", |
53 Sreg.mk_cases redexes.con_defs "regular(Var(b))", |
52 Sreg.mk_cases redexes.con_defs "regular(Var(b))", |
54 Scomp.mk_cases redexes.con_defs "Fun(u) ~ Fun(t)", |
53 Scomp.mk_cases redexes.con_defs "Fun(u) ~ Fun(t)", |
55 Scomp.mk_cases redexes.con_defs "u ~ Fun(t)", |
54 Scomp.mk_cases redexes.con_defs "u ~ Fun(t)", |
56 Scomp.mk_cases redexes.con_defs "u ~ Var(n)", |
55 Scomp.mk_cases redexes.con_defs "u ~ Var(n)", |
57 Scomp.mk_cases redexes.con_defs "u ~ App(b,t,a)", |
56 Scomp.mk_cases redexes.con_defs "u ~ App(b,t,a)", |
58 Scomp.mk_cases redexes.con_defs "Fun(t) ~ v", |
57 Scomp.mk_cases redexes.con_defs "Fun(t) ~ v", |
59 Scomp.mk_cases redexes.con_defs "App(b,f,a) ~ v", |
58 Scomp.mk_cases redexes.con_defs "App(b,f,a) ~ v", |
60 Scomp.mk_cases redexes.con_defs "Var(n) ~ u" |
59 Scomp.mk_cases redexes.con_defs "Var(n) ~ u" |
61 ]); |
60 ]; |
62 |
61 |
63 |
62 |
64 |
63 |
65 (* ------------------------------------------------------------------------- *) |
64 (* ------------------------------------------------------------------------- *) |
66 (* comp proofs *) |
65 (* comp proofs *) |
67 (* ------------------------------------------------------------------------- *) |
66 (* ------------------------------------------------------------------------- *) |
68 |
67 |
69 goal SubUnion.thy "!!u.u:redexes ==> u ~ u"; |
68 goal SubUnion.thy "!!u.u:redexes ==> u ~ u"; |
70 by (eresolve_tac [redexes.induct] 1); |
69 by (eresolve_tac [redexes.induct] 1); |
71 by (ALLGOALS(fast_tac union_cs)); |
70 by (ALLGOALS Fast_tac); |
72 val comp_refl = result(); |
71 val comp_refl = result(); |
73 |
72 |
74 goal SubUnion.thy |
73 goal SubUnion.thy |
75 "!!u.u ~ v ==> v ~ u"; |
74 "!!u.u ~ v ==> v ~ u"; |
76 by (etac Scomp.induct 1); |
75 by (etac Scomp.induct 1); |
77 by (ALLGOALS(fast_tac union_cs)); |
76 by (ALLGOALS Fast_tac); |
78 val comp_sym = result(); |
77 val comp_sym = result(); |
79 |
78 |
80 goal SubUnion.thy |
79 goal SubUnion.thy |
81 "u ~ v <-> v ~ u"; |
80 "u ~ v <-> v ~ u"; |
82 by (fast_tac (ZF_cs addIs [comp_sym]) 1); |
81 by (fast_tac (!claset addIs [comp_sym]) 1); |
83 val comp_sym_iff = result(); |
82 val comp_sym_iff = result(); |
84 |
83 |
85 |
84 |
86 goal SubUnion.thy |
85 goal SubUnion.thy |
87 "!!u.u ~ v ==> ALL w.v ~ w-->u ~ w"; |
86 "!!u.u ~ v ==> ALL w.v ~ w-->u ~ w"; |
88 by (etac Scomp.induct 1); |
87 by (etac Scomp.induct 1); |
89 by (ALLGOALS(fast_tac union_cs)); |
88 by (ALLGOALS Fast_tac); |
90 val comp_trans1 = result(); |
89 val comp_trans1 = result(); |
91 |
90 |
92 val comp_trans = comp_trans1 RS spec RS mp; |
91 val comp_trans = comp_trans1 RS spec RS mp; |
93 |
92 |
94 (* ------------------------------------------------------------------------- *) |
93 (* ------------------------------------------------------------------------- *) |
97 |
96 |
98 goal SubUnion.thy |
97 goal SubUnion.thy |
99 "!!u.u ~ v ==> u <== (u un v)"; |
98 "!!u.u ~ v ==> u <== (u un v)"; |
100 by (etac Scomp.induct 1); |
99 by (etac Scomp.induct 1); |
101 by (etac boolE 3); |
100 by (etac boolE 3); |
102 by (ALLGOALS(asm_full_simp_tac union_ss)); |
101 by (ALLGOALS Asm_full_simp_tac); |
103 val union_l = result(); |
102 val union_l = result(); |
104 |
103 |
105 goal SubUnion.thy |
104 goal SubUnion.thy |
106 "!!u.u ~ v ==> v <== (u un v)"; |
105 "!!u.u ~ v ==> v <== (u un v)"; |
107 by (etac Scomp.induct 1); |
106 by (etac Scomp.induct 1); |
108 by (eres_inst_tac [("c","b2")] boolE 3); |
107 by (eres_inst_tac [("c","b2")] boolE 3); |
109 by (ALLGOALS(asm_full_simp_tac union_ss)); |
108 by (ALLGOALS Asm_full_simp_tac); |
110 val union_r = result(); |
109 val union_r = result(); |
111 |
110 |
112 goal SubUnion.thy |
111 goal SubUnion.thy |
113 "!!u.u ~ v ==> u un v = v un u"; |
112 "!!u.u ~ v ==> u un v = v un u"; |
114 by (etac Scomp.induct 1); |
113 by (etac Scomp.induct 1); |
115 by (ALLGOALS(asm_simp_tac (union_ss addsimps [or_commute]))); |
114 by (ALLGOALS(asm_simp_tac (!simpset addsimps [or_commute]))); |
116 val union_sym = result(); |
115 val union_sym = result(); |
117 |
116 |
118 (* ------------------------------------------------------------------------- *) |
117 (* ------------------------------------------------------------------------- *) |
119 (* regular proofs *) |
118 (* regular proofs *) |
120 (* ------------------------------------------------------------------------- *) |
119 (* ------------------------------------------------------------------------- *) |
121 |
120 |
122 goal SubUnion.thy |
121 goal SubUnion.thy |
123 "!!u.u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"; |
122 "!!u.u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"; |
124 by (etac Scomp.induct 1); |
123 by (etac Scomp.induct 1); |
125 by (ALLGOALS(asm_full_simp_tac |
124 by (ALLGOALS(asm_full_simp_tac |
126 (union_ss setloop(SELECT_GOAL (safe_tac union_cs))))); |
125 (!simpset setloop(SELECT_GOAL (safe_tac (!claset)))))); |
127 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1); |
126 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1); |
128 by (asm_full_simp_tac union_ss 1); |
127 by (Asm_full_simp_tac 1); |
129 val union_preserve_regular = result(); |
128 val union_preserve_regular = result(); |