1open HolKernel boolLib bossLib Parse pred_setTheory relationTheory finite_mapTheory termTheory ramanaLib pairTheory bagTheory prim_recTheory substTheory walkTheory walkstarTheory
2
3val _ = new_theory "redUnif"
4val _ = metisTools.limit :=  { time = NONE, infs = SOME 5000 }
5
6val istep_def = Define`
7  istep (sl,bl) (sr,br) =
8  (���t. (br + {|(t, t)|} = bl) ���
9       (sr = sl)) ���
10  (���t1a t1d t2a t2d.
11    (br + {|(Pair t1a t1d, Pair t2a t2d)|} = {|(t1a,t2a); (t1d,t2d)|} + bl) ���
12    (sr = sl)) ���
13  (���v t bi.
14    ((bi + {|(Var v, t)|} = bl) ���
15     (bi + {|(t, Var v)|} = bl)) ���
16    v ��� vars t ���
17    (br = BAG_IMAGE (��(t1,t2). ((FEMPTY|+(v,t)) ��� t1, (FEMPTY|+(v,t)) ��� t2)) bi) ���
18    (sr = sl |+ (v,t)))`;
19
20val tstep_def = Define`
21  tstep (sl,bl) (sr,br) =
22  (���t1 t2.
23    (walk sl t1 = walk sl t2) ���
24    (br + {|(t1,t2)|} = bl) ���
25    (sr = sl)) ���
26  (���t1 t2 t1a t1d t2a t2d.
27    (walk sl t1 = Pair t1a t1d) ��� (walk sl t2 = Pair t2a t2d) ���
28    (br + {|(t1,t2)|} = {|(t1a,t2a); (t1d,t2d)|} + bl) ���
29    (sr = sl)) ���
30  (���t1 t2 v t.
31    ((walk sl t1 = Var v) ��� (walk sl t2 = t) ���
32     (walk sl t1 = t) ��� (walk sl t2 = Var v)) ���
33    �� oc sl t v ���
34    (br + {|(t1,t2)|} = bl) ���
35    (sr = sl |+ (v,t)))`;
36
37open unifDefTheory unifPropsTheory;
38
39val wfs_tstep = Q.store_thm(
40"wfs_tstep",
41`wfs sl ��� tstep (sl,bl) (sr,br) ��� wfs sr`,
42SRW_TAC [][tstep_def] THEN SRW_TAC [][] THEN
43IMP_RES_TAC walk_to_var THEN
44Q.PAT_ASSUM `wfs s` ASSUME_TAC THEN
45FULL_SIMP_TAC (srw_ss()) [oc_eq_vars_walkstar,walkstar_walk] THEN
46MATCH_MP_TAC wfs_extend THEN
47METIS_TAC [IN_DEF,walkstar_walk])
48
49val walks_equal = Q.store_thm(
50"walks_equal",
51`wfs s ��� (walk s t1 = walk s t2) ��� (t1 = t2) ��� ���v. (t1 = Var v) ��� (t2 = Var v)`,
52Cases_on `t1 = t2` THEN ASM_SIMP_TAC (srw_ss()) [] THEN
53SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN STRIP_TAC THEN
54MAP_EVERY Cases_on [`t1`,`t2`] THEN SRW_TAC [][] THEN
55METIS_TAC []);
56
57val NOTIN_vars_walk = Q.store_thm(
58"NOTIN_vars_walk",
59`wfs s ��� (vwalk s v = walk s t) ��� (t ��� Var v) ��� v ��� vars t`,
60Cases_on `t` THEN SRW_TAC [][] THEN
61SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
62`v ��� vars (vwalk s v)` by SRW_TAC [][] THEN
63IMP_RES_TAC vwalk_vR THEN
64Q.PAT_ASSUM `vwalk s v = X` ASSUME_TAC THEN
65FULL_SIMP_TAC (srw_ss()) [wfs_no_cycles] THEN
66RES_TAC);
67
68(*
69val istep_if_tstep = Q.store_thm(
70"istep_if_tstep", (* no! the substitutions won't be equal, they will be equivalent. istep gives an idempotent substitution whereas tstep gives a triangular one! *)
71`wfs sl ��� tstep^* (sl,bl) (sr,br) ��� ���br'. tstep^* (sl,bl) (sr,br')`,
72Q_TAC SUFF_TAC
73`���x y. RTC tstep x y ��� wfs (FST x) ��� ���br. RTC istep x (FST y,br)`
74THEN1 ( SRW_TAC [][] THEN RES_TAC THEN
75        FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [] ) THEN
76HO_MATCH_MP_TAC RTC_INDUCT THEN
77SRW_TAC [][] THEN1 (
78  Q.EXISTS_TAC `SND x` THEN SRW_TAC [][] ) THEN
79Q.MATCH_ASSUM_RENAME_TAC `tstep a b` THEN
80MAP_EVERY Cases_on [`a`,`b`] THEN
81Q.MATCH_ASSUM_RENAME_TAC `tstep (sl,bl) (si,bi)` THEN
82FULL_SIMP_TAC (srw_ss()) [] THEN
83IMP_RES_TAC wfs_tstep THEN
84FULL_SIMP_TAC (srw_ss()) [] THEN
85Q.MATCH_ASSUM_RENAME_TAC `istep^* (si,bi) (FST sr,br)` THEN
86
87FULL_SIMP_TAC (srw_ss()) [tstep_def] THEN
88SRW_TAC [][] THEN1 (
89  `(t1 = t2) ��� (t1 ��� t2) ��� ���v. (t1 = Var v) ��� (t2 = Var v)`
90  by METIS_TAC [walks_equal] THEN
91  SRW_TAC [][] THEN1 (
92    Q.EXISTS_TAC `br` THEN
93    Q.MATCH_ABBREV_TAC `RTC istep pi pr` THEN
94    Q_TAC SUFF_TAC `istep pi (si,bi)`
95    THEN1 METIS_TAC [RTC_RULES] THEN
96    SRW_TAC [][istep_def,Abbr`pi`] ) THEN
97  FULL_SIMP_TAC (srw_ss()) [] THEN
98  SRW_TAC [][] THEN
99  TRY (Q.PAT_ASSUM `Var v ��� t2` (ASSUME_TAC o GSYM)) THEN
100  IMP_RES_TAC NOTIN_vars_walk THEN
101
102val tstep_if_istep = Q.store_thm(
103"tstep_if_istep", (* need/want idempotent sl instead? *)
104`wfs sl ��� istep^* (sl,bl) (sr,br) ��� ���br'. tstep^* (sl,bl) (sr,br')`,
105Q_TAC SUFF_TAC
106`���x y. RTC istep x y ��� wfs (FST x) ��� ���br. RTC tstep x (FST y,br)`
107THEN1 ( SRW_TAC [][] THEN RES_TAC THEN
108        FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [] ) THEN
109HO_MATCH_MP_TAC RTC_INDUCT THEN
110SRW_TAC [][] THEN1 (
111  Q.EXISTS_TAC `SND x` THEN SRW_TAC [][] ) THEN
112Q.MATCH_ASSUM_RENAME_TAC `istep a b` THEN
113MAP_EVERY Cases_on [`a`,`b`] THEN
114Q.MATCH_ASSUM_RENAME_TAC `istep (sl,bl) (si,bi)` THEN
115Q.MATCH_ASSUM_RENAME_TAC `tstep^* (si,bi) (FST sr,br)` THEN
116FULL_SIMP_TAC (srw_ss()) [istep_def] THEN
117SRW_TAC [][] THEN1 (
118  Q.EXISTS_TAC `br` THEN
119  Q.MATCH_ABBREV_TAC `RTC tstep pi pr` THEN
120  Q_TAC SUFF_TAC `tstep pi (si,bi)`
121  THEN1 METIS_TAC [RTC_RULES] THEN
122  SRW_TAC [][tstep_def,Abbr`pi`] )
123THEN1 (
124  Q.EXISTS_TAC `br` THEN
125  Q.MATCH_ABBREV_TAC `RTC tstep pi pr` THEN
126  Q_TAC SUFF_TAC `tstep pi (si,bi)`
127  THEN1 METIS_TAC [RTC_RULES] THEN
128  SRW_TAC [][tstep_def,Abbr`pi`] THEN
129  DISJ2_TAC THEN DISJ1_TAC THEN
130  MAP_EVERY Q.EXISTS_TAC [`Pair t1a t1d`,`Pair t2a t2d`,`t1a`,`t1d`,`t2a`,`t2d`] THEN
131
132val tstep_if_unify = Q.store_thm(
133"tstep_if_unify",
134`wfs s ��� (unify s t1 t2 = SOME sx) ��� tstep^+ (s,b+{|(t1,t2)|}) (sx,b)`,
135MAP_EVERY Q.ID_SPEC_TAC [`b`,`sx`,`t2`,`t1`,`s`] THEN
136HO_MATCH_MP_TAC unify_ind THEN
137SRW_TAC [][] THEN
138POP_ASSUM MP_TAC THEN
139ASM_SIMP_TAC (srw_ss()) [Once unify_def] THEN
140Cases_on `walk s t1` THEN Cases_on `walk s t2` THEN SRW_TAC [][]
141THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def])
142THEN1 (
143  MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def] THEN
144  DISJ2_TAC THEN
145  MAP_EVERY Q.EXISTS_TAC [`n`,`Var n'`] THEN
146  SRW_TAC [][] THEN
147  Q.PAT_ASSUM `walk s X = Var n'` MP_TAC THEN
148  Cases_on `t2` THEN SRW_TAC [][] THEN
149  IMP_RES_TAC vwalk_to_var THEN
150  SRW_TAC [][NOT_FDOM_vwalk])
151THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def])
152THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def])
153THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def])
154THEN1 (
155  Q.PAT_ASSUM `X = SOME sx` ASSUME_TAC THEN
156  Q.PAT_ASSUM `wfs s` ASSUME_TAC THEN
157  Cases_on `unify s t t'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
158  `wfs x` by METIS_TAC [unify_uP,uP_def] THEN
159  FULL_SIMP_TAC (srw_ss()) [] THEN
160  FIRST_X_ASSUM (Q.SPEC_THEN `b+{|(t0,t0')|}` STRIP_ASSUME_TAC) THEN
161  FIRST_X_ASSUM (Q.SPEC_THEN `b` STRIP_ASSUME_TAC) THEN
162  Q.PAT_ASSUM `TC tstep X (x,Y)` MP_TAC THEN
163  Q.MATCH_ABBREV_TAC `TC tstep p2 (x,Y) ��� TC tstep p1 (sx,b)` THEN
164  STRIP_TAC THEN Q_TAC SUFF_TAC `tstep p1 p2`
165  THEN1 METIS_TAC [TC_RULES] THEN
166  SRW_TAC [][tstep_def,Abbr`p2`,Abbr`p1`,Abbr`Y`] THEN
167  DISJ2_TAC THEN DISJ1_TAC THEN
168  MAP_EVERY Q.EXISTS_TAC [`t1`,`t2`,`t`,`t0`,`t'`,`t0'`] THEN
169  SRW_TAC [][ASSOC_BAG_UNION,BAG_INSERT_UNION] THEN
170  METIS_TAC [COMM_BAG_UNION,ASSOC_BAG_UNION] )
171THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def])
172THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def])
173);
174*)
175
176(*
177"unify_if_tstep",
178`tstep^+ (s,{|(t1,t2)|}) (sx,{||}) ��� ���su. (unify s t1 t2 = SOME su) ��� relate sx and su`
179*)
180
181(* The above is more like Urban's paper. The below is following "Term rewriting
182and all that" by Baader and Nipkow. It's messier because of the explicit orient
183step and because the idempotent substitution is supposed to be read off the
184solved form of the state when no reductions are possible.
185val istep_def = Define`
186  istep f el er =
187  (���c. er + {|(Const c, Const c)|} = el) ���
188  (���t1a t1d t2a t2d.
189    er + {|(Pair t1a t1d, Pair t2a t2d)|} = {|(t1a,t2a); (t1d,t2d)|} + el) ���
190  (���v t.
191    (���u. t ��� Var u) ���
192    (er + {|(t,Var v)|} = {|(Var v,t)|} + el)) ���
193  (���v t.
194    (Var v, t) <: el ���
195    v ��� vars t ���
196    �� BAG_EVERY el (��(t1,t2) v ��� vars t1 ��� v ��� vars t2) ���
197    (er = {|(Var v, t)|} + BAG_IMAGE (el - (Var v, t)) (��(t1,t2). ((FEMPTY|+(v,t)) ��� t1, (FEMPTY|+(v,t)) ��� t2))))`;
198
199val tstep_def = Define`
200  tstep f (sl,el) (sr,er) =
201  (���t1 t2 c.
202    (walk sl t1 = Const c) ���
203    (walk sl t2 = Const c) ���
204    (er + {|(t1,t2)|} = el) ���
205    (sr = sl)) ���
206  (���t1 t2 t1a t1d t2a t2d.
207    (walk sl t1 = Pair t1a t1d) ���
208    (walk sl t2 = Pair t2a t2d) ���
209    (er + {|(t1,t2)|} = {|(t1a,t2a); (t1d,t2d)|} + el) ���
210    (sr = sl)) ���
211  (���t1 t2 v t.
212    (walk sl t1 = t) ���
213    (walk sl t2 = Var v) ���
214    (���u. t ��� Var u) ���
215    (er + {|(t1,t2)|} = {|(Var v,t)|} + el) ���
216    (sr = sl)) ���
217  (���t1 t2 v t.
218    (walk sl t1 = Var v) ���
219    (walk sl t2 = t) ���
220    �� oc sl v t ���
221    (er + {|(t1,t2)|} = el) ���
222    (sr = sl |+ (v,t)))`;
223*)
224
225val _ = export_theory ();
226