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