1open HolKernel bossLib boolLib Parse 2 3open nomsetTheory 4 5val _ = new_theory "contextlists" 6 7val _ = type_abbrev("ctxt", ``:(string # 'a) list``) 8 9(* permutation over contexts swaps the strings and leaves the types alone *) 10val _ = overload_on 11 ("ctxtswap", ``listpm (pair_pmact string_pmact discrete_pmact)``) 12 13(* the free variables of a context *) 14val _ = overload_on 15 ("ctxtFV", 16 ``supp (list_pmact (pair_pmact string_pmact discrete_pmact))``) 17 18(* A context is valid if the strings 19 are all disjoint. Here's the primitive recursive defn. *) 20val valid_ctxt_def = Define` 21 (valid_ctxt [] ��� T) ��� 22 (valid_ctxt ((x,A) :: G) ��� x ��� ctxtFV G ��� valid_ctxt G) 23`; 24val _ = export_rewrites ["valid_ctxt_def"] 25 26(* here's the alternative characterisation in terms of the standard 27 ALL_DISTINCT constant *) 28val valid_ctxt_ALL_DISTINCT = store_thm( 29 "valid_ctxt_ALL_DISTINCT", 30 ``���G. valid_ctxt G = ALL_DISTINCT (MAP FST G)``, 31 Induct THEN 32 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, NOT_IN_supp_listpm, 33 listTheory.MEM_MAP]); 34 35val valid_ctxt_APPEND = store_thm( 36 "valid_ctxt_APPEND", 37 ``valid_ctxt (G1 ++ G2) ==> valid_ctxt G1 ��� valid_ctxt G2``, 38 Induct_on `G1` THEN 39 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 40 41(* context membership "respects" permutation *) 42val MEM_ctxtswap = store_thm( 43 "MEM_ctxtswap", 44 ``!G pi x A. MEM (lswapstr pi x, A) (ctxtswap pi G) = MEM (x,A) G``, 45 SRW_TAC [][MEM_listpm]) 46val _ = export_rewrites ["MEM_ctxtswap"] 47 48val ctxtFV_ctxtswap = store_thm( 49 "ctxtFV_ctxtswap", 50 ``ctxtFV (ctxtswap pi G) = setpm string_pmact pi (ctxtFV G)``, 51 MATCH_ACCEPT_TAC perm_supp); 52val _ = export_rewrites ["ctxtFV_ctxtswap"] 53 54(* valid_ctxt also respects permutation *) 55val valid_ctxt_swap0 = prove( 56 ``!G. valid_ctxt G ==> !x y. valid_ctxt (ctxtswap pi G)``, 57 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 58 59val valid_ctxt_swap = store_thm( 60 "valid_ctxt_swap", 61 ``valid_ctxt (ctxtswap pi G) = valid_ctxt G``, 62 METIS_TAC [valid_ctxt_swap0, pmact_inverse]); 63val _ = export_rewrites ["valid_ctxt_swap"] 64 65(* contexts have finitely many free variables *) 66val FINITE_ctxtFV = store_thm( 67 "FINITE_ctxtFV", 68 ``FINITE (ctxtFV G)``, 69 Induct_on `G` THEN 70 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, supp_pairpm]); 71val _ = export_rewrites ["FINITE_ctxtFV"] 72 73val ctxtswap_fresh = store_thm( 74 "ctxtswap_fresh", 75 ``��(x ��� ctxtFV G) /\ ��(y ��� ctxtFV G) ==> (ctxtswap [(x,y)] G = G)``, 76 MATCH_ACCEPT_TAC supp_fresh) 77 78(* sub-context relation, overloaded to use SUBSET *) 79val subctxt_def = Define` 80 subctxt �� �� = ���x A. MEM (x,A) �� ==> MEM (x,A) �� 81`; 82val _ = overload_on("SUBSET", ``subctxt``) 83 84val subctxt_nil = store_thm( 85 "subctxt_nil", 86 ``[] ��� ��``, 87 SRW_TAC [][subctxt_def]); 88val _ = export_rewrites ["subctxt_nil"] 89 90val subctxt_refl = store_thm( 91 "subctxt_refl", 92 ``G : 'a ctxt ��� G``, 93 SRW_TAC [][subctxt_def]); 94val _ = export_rewrites ["subctxt_refl"] 95 96(* cute, but unnecessary *) 97val subctxt_ctxtFV = store_thm( 98 "subctxt_ctxtFV", 99 ``C1 ��� C2 ==> ctxtFV C1 ��� ctxtFV C2``, 100 SIMP_TAC (srw_ss()) [pred_setTheory.SUBSET_DEF, subctxt_def, 101 IN_supp_listpm, pairTheory.EXISTS_PROD] THEN 102 METIS_TAC []); 103 104open sortingTheory 105val PERM_RULES = LIST_CONJ [Q.SPEC `[]` PERM_REFL, 106 prove(``���x l1 l2. PERM l1 l2 ==> 107 PERM (x::l1) (x::l2)``, 108 SRW_TAC [][]), 109 prove(``���x y l1 l2. PERM l1 l2 ==> 110 PERM (x::y::l1) (y::x::l2)``, 111 SRW_TAC [][PERM_SWAP_AT_FRONT]), 112 PERM_TRANS] 113val strong_perm_ind = IndDefLib.derive_strong_induction (PERM_RULES, PERM_IND) 114 115val valid_ctxt_PERM = store_thm( 116 "valid_ctxt_PERM", 117 ``!G1 G2. PERM G1 G2 ==> (valid_ctxt G1 = valid_ctxt G2)``, 118 HO_MATCH_MP_TAC strong_perm_ind THEN 119 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, NOT_IN_supp_listpm] THEN 120 SRW_TAC [][] THEN METIS_TAC [PERM_MEM_EQ]); 121 122val valid_ctxt_FILTER = store_thm( 123 "valid_ctxt_FILTER", 124 ``valid_ctxt G ==> valid_ctxt (FILTER P G)``, 125 Induct_on `G` THEN 126 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, NOT_IN_supp_listpm] THEN 127 SRW_TAC [][IN_supp_listpm, pairTheory.EXISTS_PROD, listTheory.MEM_FILTER]); 128val domfilter_def = Define` 129 domfilter (G:'a ctxt) P = FILTER (��(x,ty). x ��� P) G 130`; 131val _ = overload_on ("INTER", ``domfilter``) 132 133val domfilter_thm = store_thm( 134 "domfilter_thm", 135 ``([] ��� P = []) ��� 136 ((h :: G) ��� P = if FST h ��� P then h :: (G ��� P) else G ��� P)``, 137 Cases_on `h` THEN SRW_TAC [][domfilter_def]) 138val _ = export_rewrites ["domfilter_thm"] 139 140val valid_ctxt_domfilter = store_thm( 141 "valid_ctxt_domfilter", 142 ``valid_ctxt G ==> valid_ctxt (G ��� P)``, 143 SRW_TAC [][domfilter_def, valid_ctxt_FILTER]); 144 145val IN_ctxtFV_domfilter = store_thm( 146 "IN_ctxtFV_domfilter", 147 ``x ��� ctxtFV (G ��� P) ��� x ��� ctxtFV G ��� x ��� P``, 148 Induct_on `G` THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 149 SRW_TAC [][] THEN METIS_TAC []); 150val _ = export_rewrites ["IN_ctxtFV_domfilter"] 151 152Theorem MEM_domfilter[simp]: 153 MEM (x,ty) (G ��� P) ��� x ��� P ��� MEM (x,ty) G 154Proof 155 SRW_TAC [][domfilter_def, listTheory.MEM_FILTER] 156QED 157 158val subctxt_domfilter = store_thm( 159 "subctxt_domfilter", 160 ``(G:'a ctxt) ��� P ��� G``, 161 SRW_TAC [][subctxt_def, domfilter_def, listTheory.MEM_FILTER]); 162 163val domfilter_delete = store_thm( 164 "domfilter_delete", 165 ``��(v ��� ctxtFV G) ==> (G ��� (s DELETE v) = G ��� s)``, 166 Induct_on `G` THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 167 168val _ = export_theory() 169