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