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