author | paulson |
Wed, 15 Jul 1998 14:13:18 +0200 | |
changeset 5147 | 825877190618 |
parent 5068 | fb28eaa07e01 |
child 5268 | 59ef39008514 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: Residuals.ML |
1048 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Ole Rasmussen |
1048 | 4 |
Copyright 1995 University of Cambridge |
5 |
Logic Image: ZF |
|
6 |
*) |
|
7 |
||
8 |
open Residuals; |
|
9 |
||
10 |
(* ------------------------------------------------------------------------- *) |
|
11 |
(* Setting up rule lists *) |
|
12 |
(* ------------------------------------------------------------------------- *) |
|
13 |
||
2469 | 14 |
AddIs (Sres.intrs@redexes.intrs@Sreg.intrs@ |
15 |
[subst_type]@nat_typechecks); |
|
16 |
AddSEs (redexes.free_SEs @ |
|
17 |
(map (Sres.mk_cases redexes.con_defs) |
|
18 |
["residuals(Var(n),Var(n),v)", |
|
19 |
"residuals(Fun(t),Fun(u),v)", |
|
20 |
"residuals(App(b, u1, u2), App(0, v1, v2),v)", |
|
21 |
"residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)", |
|
22 |
"residuals(Var(n),u,v)", |
|
23 |
"residuals(Fun(t),u,v)", |
|
24 |
"residuals(App(b, u1, u2), w,v)", |
|
25 |
"residuals(u,Var(n),v)", |
|
26 |
"residuals(u,Fun(t),v)", |
|
27 |
"residuals(w,App(b, u1, u2),v)"]) @ |
|
28 |
(map (Ssub.mk_cases redexes.con_defs) |
|
29 |
["Var(n) <== u", |
|
30 |
"Fun(n) <== u", |
|
31 |
"u <== Fun(n)", |
|
32 |
"App(1,Fun(t),a) <== u", |
|
33 |
"App(0,t,a) <== u"]) @ |
|
34 |
[redexes.mk_cases redexes.con_defs "Fun(t):redexes"]); |
|
1048 | 35 |
|
2469 | 36 |
Addsimps Sres.intrs; |
1048 | 37 |
val resD1 =Sres.dom_subset RS subsetD RS SigmaD1; |
38 |
val resD2 =Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1; |
|
39 |
val resD3 =Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2; |
|
40 |
||
41 |
||
42 |
(* ------------------------------------------------------------------------- *) |
|
43 |
(* residuals is a partial function *) |
|
44 |
(* ------------------------------------------------------------------------- *) |
|
45 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
46 |
Goal "residuals(u,v,w) ==> ALL w1. residuals(u,v,w1) --> w1 = w"; |
1732 | 47 |
by (etac Sres.induct 1); |
2469 | 48 |
by (ALLGOALS Fast_tac); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
49 |
qed_spec_mp "residuals_function"; |
1048 | 50 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
51 |
Goal "u~v ==> regular(v) --> (EX w. residuals(u,v,w))"; |
1732 | 52 |
by (etac Scomp.induct 1); |
2469 | 53 |
by (ALLGOALS Fast_tac); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
54 |
qed "residuals_intro"; |
1048 | 55 |
|
56 |
val prems = goal Residuals.thy |
|
57 |
"[|u~v; residuals(u,v,THE w. residuals(u, v, w))==> R; \ |
|
58 |
\ regular(v)|] ==> R"; |
|
59 |
by (cut_facts_tac prems 1); |
|
60 |
by (resolve_tac prems 1); |
|
61 |
by (resolve_tac [residuals_intro RS mp RS exE] 1); |
|
62 |
by (resolve_tac [the_equality RS ssubst] 3); |
|
4091 | 63 |
by (ALLGOALS (fast_tac (claset() addIs [residuals_function]))); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
64 |
qed "comp_resfuncE"; |
1048 | 65 |
|
66 |
||
67 |
(* ------------------------------------------------------------------------- *) |
|
68 |
(* Residual function *) |
|
69 |
(* ------------------------------------------------------------------------- *) |
|
70 |
||
4091 | 71 |
val resfunc_cs = (claset() addIs [the_equality,residuals_function] |
2469 | 72 |
addSEs [comp_resfuncE]); |
1048 | 73 |
|
5068 | 74 |
Goalw [res_func_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
75 |
"n:nat ==> Var(n) |> Var(n) = Var(n)"; |
1048 | 76 |
by (fast_tac resfunc_cs 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
77 |
qed "res_Var"; |
1048 | 78 |
|
5068 | 79 |
Goalw [res_func_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
80 |
"[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"; |
1048 | 81 |
by (fast_tac resfunc_cs 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
82 |
qed "res_Fun"; |
1048 | 83 |
|
5068 | 84 |
Goalw [res_func_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
85 |
"[|s~u; regular(u); t~v; regular(v); b:bool|]==> \ |
1048 | 86 |
\ App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"; |
87 |
by (fast_tac resfunc_cs 1); |
|
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
88 |
qed "res_App"; |
1048 | 89 |
|
5068 | 90 |
Goalw [res_func_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
91 |
"[|s~u; regular(u); t~v; regular(v); b:bool|]==> \ |
1048 | 92 |
\ App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"; |
93 |
by (fast_tac resfunc_cs 1); |
|
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
94 |
qed "res_redex"; |
1048 | 95 |
|
5068 | 96 |
Goal |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
97 |
"[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes"; |
1732 | 98 |
by (etac Scomp.induct 1); |
1048 | 99 |
by (ALLGOALS (asm_full_simp_tac |
4091 | 100 |
(simpset() addsimps [res_Var,res_Fun,res_App,res_redex] |
4152 | 101 |
setloop (SELECT_GOAL Safe_tac)))); |
1048 | 102 |
by (dres_inst_tac [("psi", "Fun(?u) |> ?v : redexes")] asm_rl 1); |
103 |
by (asm_full_simp_tac |
|
4091 | 104 |
(simpset() addsimps [res_Fun] |
4152 | 105 |
setloop (SELECT_GOAL Safe_tac)) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
106 |
qed "resfunc_type"; |
1048 | 107 |
|
2469 | 108 |
Addsimps ([res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp, |
109 |
lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type, |
|
110 |
subst_rec_preserve_reg] @ |
|
111 |
redexes.free_iffs); |
|
1048 | 112 |
|
4152 | 113 |
val res1L_ss = simpset() setloop (SELECT_GOAL Safe_tac); |
1048 | 114 |
|
115 |
(* ------------------------------------------------------------------------- *) |
|
116 |
(* Commutation theorem *) |
|
117 |
(* ------------------------------------------------------------------------- *) |
|
118 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
119 |
Goal "u<==v ==> u~v"; |
1732 | 120 |
by (etac Ssub.induct 1); |
2469 | 121 |
by (ALLGOALS Asm_simp_tac); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
122 |
qed "sub_comp"; |
1048 | 123 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
124 |
Goal "u<==v ==> regular(v) --> regular(u)"; |
1732 | 125 |
by (etac Ssub.induct 1); |
1048 | 126 |
by (ALLGOALS (asm_simp_tac res1L_ss)); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
127 |
qed "sub_preserve_reg"; |
1048 | 128 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
129 |
Goal "[|u~v; k:nat|]==> regular(v)--> (ALL n:nat. \ |
1048 | 130 |
\ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"; |
1732 | 131 |
by (etac Scomp.induct 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
132 |
by Safe_tac; |
4091 | 133 |
by (ALLGOALS (asm_full_simp_tac ((addsplit (simpset())) addsimps [lift_subst]))); |
3840 | 134 |
by (dres_inst_tac [("psi", "ALL x:nat. Fun(?u(x)) |> ?v(x) = ?w(x)")] asm_rl 1); |
2469 | 135 |
by (Asm_full_simp_tac 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
136 |
qed "residuals_lift_rec"; |
1048 | 137 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
138 |
Goal "u1~u2 ==> ALL v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\ |
3840 | 139 |
\ (ALL n:nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \ |
1048 | 140 |
\ subst_rec(v1 |> v2, u1 |> u2,n))"; |
1732 | 141 |
by (etac Scomp.induct 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
142 |
by Safe_tac; |
1048 | 143 |
by (ALLGOALS |
4091 | 144 |
(asm_full_simp_tac ((addsplit (simpset())) addsimps ([residuals_lift_rec])))); |
1048 | 145 |
by (dres_inst_tac [("psi", "ALL x.?P(x)")] asm_rl 1); |
4091 | 146 |
by (asm_full_simp_tac (simpset() addsimps ([substitution])) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
147 |
qed "residuals_subst_rec"; |
1048 | 148 |
|
149 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
150 |
Goal "[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\ |
1048 | 151 |
\ (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"; |
4091 | 152 |
by (asm_simp_tac (simpset() addsimps ([residuals_subst_rec])) 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
153 |
qed "commutation"; |
1048 | 154 |
|
155 |
(* ------------------------------------------------------------------------- *) |
|
156 |
(* Residuals are comp and regular *) |
|
157 |
(* ------------------------------------------------------------------------- *) |
|
158 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
159 |
Goal "u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)"; |
1732 | 160 |
by (etac Scomp.induct 1); |
2469 | 161 |
by (ALLGOALS (asm_simp_tac res1L_ss)); |
1048 | 162 |
by (dresolve_tac [spec RS mp RS mp RS mp] 1 |
163 |
THEN resolve_tac Scomp.intrs 1 THEN resolve_tac Scomp.intrs 2 |
|
164 |
THEN resolve_tac Sreg.intrs 3); |
|
165 |
by (REPEAT(assume_tac 1)); |
|
166 |
by (asm_full_simp_tac res1L_ss 1); |
|
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
167 |
qed_spec_mp "residuals_preserve_comp"; |
1048 | 168 |
|
169 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
170 |
Goal "u~v ==> regular(u) --> regular(v) --> regular(u|>v)"; |
1732 | 171 |
by (etac Scomp.induct 1); |
4152 | 172 |
by Safe_tac; |
1048 | 173 |
by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl)); |
174 |
by (ALLGOALS (asm_full_simp_tac res1L_ss)); |
|
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
175 |
qed "residuals_preserve_reg"; |
1048 | 176 |
|
177 |
(* ------------------------------------------------------------------------- *) |
|
178 |
(* Preservation lemma *) |
|
179 |
(* ------------------------------------------------------------------------- *) |
|
180 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
181 |
Goal "u~v ==> v ~ (u un v)"; |
1732 | 182 |
by (etac Scomp.induct 1); |
2469 | 183 |
by (ALLGOALS Asm_full_simp_tac); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
184 |
qed "union_preserve_comp"; |
1048 | 185 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
186 |
Goal "u ~ v ==> regular(v) --> u|>v = (u un v)|>v"; |
1732 | 187 |
by (etac Scomp.induct 1); |
4152 | 188 |
by Safe_tac; |
1048 | 189 |
by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3); |
190 |
by (ALLGOALS (asm_full_simp_tac (res1L_ss addsimps |
|
1461 | 191 |
[union_preserve_comp,comp_sym_iff]))); |
4091 | 192 |
by (asm_full_simp_tac (simpset() addsimps |
1461 | 193 |
[union_preserve_comp RS comp_sym, |
194 |
comp_sym RS union_preserve_comp RS comp_sym]) 1); |
|
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2469
diff
changeset
|
195 |
qed_spec_mp "preservation"; |