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