1open HolKernel boolLib bossLib Parse finite_mapTheory termTheory ramanaLib pred_setTheory substTheory walkTheory walkstarTheory;
2
3val _ = new_theory "collapse";
4
5(* NB: collapsing a substitution means it's not triangular any more. The
6 * intended method for applying triangular substitutions is to use walk*. The
7 * relationship to directly applying a collapsed substitution proved here is
8 * not intended as an implementation strategy, because it would destroy the
9 * shared-tails benefits of using triangular substutions. *)
10
11val collapse_def = Define`
12  collapse s = FUN_FMAP (\v.walkstar s (Var v)) (FDOM s)`;
13
14val collapse_APPLY_eq_walkstar = Q.store_thm(
15"collapse_APPLY_eq_walkstar",
16`wfs s ==> !t.(collapse s ��� t = walkstar s t)`,
17STRIP_TAC THEN HO_MATCH_MP_TAC walkstar_ind THEN
18SRW_TAC [][] THEN
19Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
20SRW_TAC [][collapse_def,FLOOKUP_DEF,FUN_FMAP_DEF] THEN
21Cases_on `vwalk s n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
22METIS_TAC [NOT_FDOM_vwalk,term_11,term_distinct]);
23
24val collapse_FAPPLY_eq_walkstar = Q.store_thm(
25"collapse_FAPPLY_eq_walkstar",
26`wfs s ==> !v.v IN FDOM s ==> (collapse s ' v = walkstar s (Var v))`,
27SRW_TAC [][collapse_def,FUN_FMAP_DEF]);
28
29val walkstar_unchanged = Q.store_thm(
30"walkstar_unchanged",
31`wfs s ==> !t.DISJOINT (vars t) (FDOM s) ==>
32   (walkstar s t = t)`,
33STRIP_TAC THEN HO_MATCH_MP_TAC walkstar_ind THEN
34SRW_TAC [][] THEN
35Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
36SRW_TAC [][NOT_FDOM_vwalk]);
37
38val collapse_idempotent = Q.store_thm(
39"collapse_idempotent",
40`wfs s ==> idempotent (collapse s)`,
41METIS_TAC [walkstar_idempotent,idempotent_def,collapse_APPLY_eq_walkstar]);
42
43val idempotent_collapse = Q.store_thm(
44"idempotent_collapse",
45`idempotent s ��� noids s ==> (collapse s = s)`,
46STRIP_TAC THEN
47`wfs s` by METIS_TAC [wfs_idempotent] THEN
48`FDOM s = FDOM (collapse s)` by SRW_TAC [][collapse_def,FUN_FMAP_DEF] THEN
49SRW_TAC [][GSYM fmap_EQ,FUN_EQ_THM] THEN
50REVERSE (Cases_on `x IN FDOM s`) THEN1
51  METIS_TAC [NOT_FDOM_FAPPLY_FEMPTY] THEN
52`DISJOINT (FDOM s) (rangevars s)`
53  by ((idempotent_rangevars |> EQ_IMP_RULE |> fst |> MATCH_MP_TAC) THEN
54      SRW_TAC [][noids_def,FLOOKUP_DEF] THEN
55      Cases_on `v IN FDOM (collapse s)` THEN SRW_TAC [][] THEN
56      MATCH_MP_TAC (UNDISCH wfs_FAPPLY_var) THEN
57      METIS_TAC []) THEN
58`DISJOINT (FDOM s) (vars (s ' x))`
59  by (FULL_SIMP_TAC (srw_ss()) [FRANGE_DEF,rangevars_def] THEN
60      METIS_TAC []) THEN
61`walkstar s (s ' x) = (s ' x)`
62  by METIS_TAC [walkstar_unchanged,DISJOINT_SYM] THEN
63Q_TAC SUFF_TAC `walkstar s (Var x) = walkstar s (s ' x)` THEN1
64  METIS_TAC [collapse_FAPPLY_eq_walkstar] THEN
65Q.PAT_X_ASSUM `walkstar X Y = Z` (fn th => ALL_TAC) THEN
66SRW_TAC [][Once vwalk_def,FLOOKUP_DEF] THEN
67Cases_on `s ' x` THEN SRW_TAC [][]);
68
69val walkstar_eq_idem_APPLY = Q.store_thm(
70"walkstar_eq_idem_APPLY",
71`wfs s ==> (idempotent s <=> (walkstar s = subst_APPLY s))`,
72STRIP_TAC THEN EQ_TAC THEN1
73METIS_TAC [wfs_noids,idempotent_collapse,collapse_APPLY_eq_walkstar] THEN
74STRIP_TAC THEN
75Q_TAC SUFF_TAC `s = collapse s`
76  THEN1 METIS_TAC [collapse_idempotent] THEN
77`FDOM s = FDOM (collapse s)`
78  by SRW_TAC [][collapse_def,FUN_FMAP_DEF] THEN
79SRW_TAC [][GSYM fmap_EQ,FUN_EQ_THM] THEN
80REVERSE (Cases_on `x IN FDOM s`) THEN1
81  METIS_TAC [NOT_FDOM_FAPPLY_FEMPTY] THEN
82METIS_TAC [collapse_APPLY_eq_walkstar,subst_APPLY_FAPPLY]);
83
84val subst_APPLY_walkstar = Q.store_thm(
85"subst_APPLY_walkstar",
86`wfs s ��� ���t. s ��� (walk* s t) = (walk* s t)`,
87STRIP_TAC THEN HO_MATCH_MP_TAC apply_ts_ind THEN
88SRW_TAC [][apply_ts_thm] THEN
89Cases_on `FLOOKUP s t` THEN SRW_TAC [][] );
90
91val collapse_noids = store_thm("collapse_noids",
92  ``wfs s ==> noids (collapse s)``,
93  rw[noids_def,FLOOKUP_DEF] >>
94  spose_not_then strip_assume_tac >>
95  `v ��� FDOM s` by fs[collapse_def] >>
96  imp_res_tac collapse_FAPPLY_eq_walkstar >>
97  rfs[] >>
98  Cases_on`vwalk s v` >> rfs[] >> rw[] >>
99  metis_tac[vwalk_no_cycles])
100
101val wfs_collapse = store_thm("wfs_collapse",
102  ``wfs s ==> wfs (collapse s)``,
103  metis_tac[collapse_idempotent,collapse_noids,wfs_idempotent])
104
105val _ = export_theory ();
106