1open HolKernel boolLib bossLib Parse stringTheory nomsetTheory listTheory ramanaLib relationTheory quotientLib pairTheory bagTheory commonUnifTheory; 2 3val _ = new_theory "nterm"; 4val _ = metisTools.limit := { time = NONE, infs = SOME 5000 }; 5 6val permeq_exists = RWstore_thm( 7"permeq_exists", 8`(���x. p == x) ��� (���x. x == p)`, 9METIS_TAC [permeq_refl]); 10 11val _ = Hol_datatype` 12 Cterm = CNom of string 13 | CSus of (string # string) list => num 14 | CTie of string => Cterm 15 | CnPair of Cterm => Cterm 16 | CnConst of 'a`; 17 18val Ctermeq_def = RWDefine` 19 (Ctermeq (CNom a1) (CNom a2) = (a1 = a2)) ��� 20 (Ctermeq (CSus p1 v1) (CSus p2 v2) = (p1 == p2) ��� (v1 = v2)) ��� 21 (Ctermeq (CTie a1 t1) (CTie a2 t2) = (a1 = a2) ��� Ctermeq t1 t2) ��� 22 (Ctermeq (CnPair t1a t1d) (CnPair t2a t2d) = Ctermeq t1a t2a ��� Ctermeq t1d t2d) ��� 23 (Ctermeq (CnConst c1) (CnConst c2) = (c1 = c2)) ��� 24 (Ctermeq t1 t2 = F)`; 25 26val Ctermeq_refl = RWstore_thm( 27"Ctermeq_refl", 28`���t. Ctermeq t t`, 29Induct THEN SRW_TAC [][permeq_refl]); 30 31val Ctermeq_sym = Q.store_thm( 32"Ctermeq_sym", 33`���t1 t2. Ctermeq t1 t2 = Ctermeq t2 t1`, 34Induct THEN 35Cases_on `t2` THEN SRW_TAC [][] THEN 36METIS_TAC [permeq_sym]); 37 38val Ctermeq_trans = Q.store_thm( 39"Ctermeq_trans", 40`���t1 t2 t3. Ctermeq t1 t2 ��� Ctermeq t2 t3 ��� Ctermeq t1 t3`, 41Induct THEN Cases_on `t2` THEN Cases_on `t3` THEN SRW_TAC [][] THEN 42METIS_TAC [permeq_trans]); 43 44val Ctermeq_equiv = Q.store_thm( 45"Ctermeq_equiv", 46`���t1 t2. Ctermeq t1 t2 ��� (Ctermeq t1 = Ctermeq t2)`, 47METIS_TAC [equivalence_def,symmetric_def,reflexive_def,transitive_def, 48 ALT_equivalence,Ctermeq_refl,Ctermeq_sym,Ctermeq_trans]); 49 50val CTie_rsp = Q.store_thm( 51"CTie_rsp", 52`���t1 t2 a1 a2. (a1 = a2) ��� Ctermeq t1 t2 ��� Ctermeq (CTie a1 t1) (CTie a2 t2)`, 53Induct THEN SRW_TAC [][]); 54 55val CnPair_rsp = Q.store_thm( 56"CnPair_rsp", 57`���t1a t1d t2a t2d. Ctermeq t1a t2a ��� Ctermeq t1d t2d ��� Ctermeq (CnPair t1a t1d) (CnPair t2a t2d)`, 58Induct THEN SRW_TAC [][]); 59 60fun mk_def(t) = 61let val s = (String.extract(term_to_string t,1,NONE)) in 62 {def_name = s ^ "_def", fixity = NONE, fname = s, func = t} 63end; 64 65val [nterm_induction,nterm_nchotomy,ntermeq_thm] 66= define_equivalence_type { 67 name = "nterm", 68 equiv = Ctermeq_equiv, 69 defs = map mk_def [``CNom``,``CSus``,``CTie``,``CnPair``,``CnConst``], 70 welldefs = [CTie_rsp,CnPair_rsp], 71 old_thms = map theorem ["Cterm_induction","Cterm_nchotomy"] @ [Ctermeq_def] 72}; 73 74val _ = save_thm("nterm_induction",nterm_induction); 75val _ = save_thm("nterm_nchotomy",nterm_nchotomy); 76val _ = RWsave_thm("ntermeq_thm",ntermeq_thm); 77 78val (nterm_rec_rules,nterm_rec_ind,nterm_rec_cases) = Hol_reln ` 79 nterm_rec Nf Sf Tf Pf Cf (Nom a) (Nf a) ��� 80 nterm_rec Nf Sf Tf Pf Cf (Sus p v) (Sf p v) ��� 81 (nterm_rec Nf Sf Tf Pf Cf t r ��� 82 nterm_rec Nf Sf Tf Pf Cf (Tie a t) (Tf a t r)) ��� 83 (nterm_rec Nf Sf Tf Pf Cf t1 r1 ��� 84 nterm_rec Nf Sf Tf Pf Cf t2 r2 ��� 85 nterm_rec Nf Sf Tf Pf Cf (nPair t1 t2) (Pf t1 t2 r1 r2)) ��� 86 nterm_rec Nf Sf Tf Pf Cf (nConst c) (Cf c)`; 87 88val nterm_rec_total = Q.store_thm( 89"nterm_rec_total", 90`���t. ���r. nterm_rec Nf Sf Tf Pf Cf t r`, 91HO_MATCH_MP_TAC nterm_induction THEN 92METIS_TAC [nterm_rec_rules]); 93 94val nterm_rec_unique = Q.store_thm( 95"nterm_rec_unique", 96`(���p1 p2 v. p1 == p2 ��� (Sf p1 v = Sf p2 v)) ��� 97 ���t r. nterm_rec Nf Sf Tf Pf Cf t r ��� 98 ���r'. nterm_rec Nf Sf Tf Pf Cf t r' ��� (r' = r)`, 99STRIP_TAC THEN HO_MATCH_MP_TAC nterm_rec_ind THEN 100SRW_TAC [][] THENL [ 101 FULL_SIMP_TAC (srw_ss()) [Once nterm_rec_cases], 102 FULL_SIMP_TAC (srw_ss()) [Once nterm_rec_cases], 103 POP_ASSUM MP_TAC THEN 104 SRW_TAC [][Once nterm_rec_cases] THEN 105 METIS_TAC [], 106 POP_ASSUM MP_TAC THEN 107 SRW_TAC [][Once nterm_rec_cases] THEN 108 METIS_TAC [], 109 FULL_SIMP_TAC (srw_ss()) [Once nterm_rec_cases] 110]); 111 112val nterm_rec_exists = Q.store_thm( 113"nterm_rec_exists", 114`���Nf Sf Tf Pf Cf. 115 (���p1 p2 v. p1 == p2 ��� (Sf p1 v = Sf p2 v)) ��� 116 ���f. (���a. f (Nom a) = Nf a) ��� 117 (���p v. f (Sus p v) = Sf p v) ��� 118 (���a t. f (Tie a t) = Tf a t (f t)) ��� 119 (���t1 t2. f (nPair t1 t2) = Pf t1 t2 (f t1) (f t2)) ��� 120 (���c. f (nConst c) = (Cf c))`, 121REPEAT STRIP_TAC THEN Q.EXISTS_TAC `��t. @r. nterm_rec Nf Sf Tf Pf Cf t r` THEN 122SRW_TAC [][] THENL [ 123 SELECT_ELIM_TAC THEN 124 METIS_TAC [nterm_rec_unique,nterm_rec_rules], 125 SELECT_ELIM_TAC THEN 126 METIS_TAC [nterm_rec_unique,nterm_rec_rules], 127 NTAC 2 SELECT_ELIM_TAC THEN 128 SRW_TAC [][] THENL [ 129 METIS_TAC [nterm_rec_total], 130 METIS_TAC [nterm_rec_rules], 131 POP_ASSUM MP_TAC THEN 132 SRW_TAC [][Once nterm_rec_cases] THEN 133 METIS_TAC [nterm_rec_unique] 134 ], 135 NTAC 3 SELECT_ELIM_TAC THEN 136 SRW_TAC [][] THENL [ 137 METIS_TAC [nterm_rec_total], 138 METIS_TAC [nterm_rec_total], 139 METIS_TAC [nterm_rec_rules], 140 POP_ASSUM MP_TAC THEN 141 SRW_TAC [][Once nterm_rec_cases] THEN 142 METIS_TAC [nterm_rec_unique] 143 ], 144 SELECT_ELIM_TAC THEN 145 METIS_TAC [nterm_rec_unique,nterm_rec_rules] 146]); 147 148val is_Nom_def = Define`is_Nom t = ?a. (t = Nom a)`; 149val is_Sus_def = Define`is_Sus t = ?p v. (t = Sus p v)`; 150val is_Tie_def = Define`is_Tie t = ?t' a. (t = Tie a t')`; 151val is_nPair_def = Define`is_nPair t = ?t1 t2. (t = nPair t1 t2)`; 152val _ = export_rewrites["is_Nom_def","is_Sus_def","is_Tie_def","is_nPair_def"]; 153 154val dest_Nom_def = Define `dest_Nom t = @a. t = Nom a`; 155val dest_Sus_def = Define `dest_Sus t = ((@p.���v. t = Sus p v),(@v.���p.t = Sus 156p v))`; 157val dest_Tie_def = Define `dest_Tie t = @p. Tie (FST p) (SND p) = t`; 158val dest_nPair_def = Define `dest_nPair t = @p. nPair (FST p) (SND p) = t`; 159val dest_nConst_def = Define `dest_nConst t = @c. nConst c = t`; 160val dest_Nom_thm = 161RWstore_thm("dest_Nom_thm", `dest_Nom (Nom a) = a`, 162SRW_TAC [][dest_Nom_def]); 163val dest_Sus = 164RWstore_thm("dest_Sus_thm", `dest_Sus (Sus p v) = ((@p'. p' == p),v)`, 165SRW_TAC [][dest_Sus_def] THEN1 166(AP_TERM_TAC THEN SRW_TAC [][FUN_EQ_THM] THEN METIS_TAC [permeq_sym]) THEN 167SELECT_ELIM_TAC THEN SRW_TAC [][] THEN METIS_TAC [permeq_refl]); 168val dest_Tie = 169RWstore_thm("dest_Tie_thm", `dest_Tie (Tie a t) = (a,t)`, 170SRW_TAC [][dest_Tie_def] THEN SELECT_ELIM_TAC THEN 171REPEAT (SRW_TAC [][EXISTS_PROD,PAIR])); 172val dest_nPair_thm = 173RWstore_thm("dest_nPair_thm", `dest_nPair (nPair t1 t2) = (t1,t2)`, 174SRW_TAC [][dest_nPair_def] THEN SELECT_ELIM_TAC THEN 175REPEAT (SRW_TAC [][EXISTS_PROD,PAIR])); 176val dest_nConst_thm = 177RWstore_thm("dest_nConst_thm", `dest_nConst (nConst a) = a`, 178SRW_TAC [][dest_nConst_def]); 179 180val nterm_case_def = Define` 181 nterm_CASE t Nf Sf Tf Pf Cf = 182 if is_Nom t then Nf (dest_Nom t) else 183 if is_Sus t then UNCURRY Sf (dest_Sus t) else 184 if is_Tie t then UNCURRY Tf (dest_Tie t) else 185 if is_nPair t then UNCURRY Pf (dest_nPair t) else Cf (dest_nConst t)`; 186 187val nterm_case_cong = Q.store_thm( 188"nterm_case_cong", 189`���t t' Nf Sf Tf Pf Cf. 190 (t = t') ��� 191 (���a. (t' = Nom a) ��� (Nf a = Nf' a)) ��� 192 (���p v. (t' = Sus p v) ��� (Sf p v = Sf' p v)) ��� 193 (���a t. (t' = Tie a t) ��� (Tf a t = Tf' a t)) ��� 194 (���t1 t2. (t' = nPair t1 t2) ��� (Pf t1 t2 = Pf' t1 t2)) ��� 195 (���c. (t' = nConst c) ��� (Cf c = Cf' c)) ��� 196 (nterm_CASE t Nf Sf Tf Pf Cf = nterm_CASE t' Nf' Sf' Tf' Pf' Cf')`, 197REPEAT GEN_TAC THEN 198Q.SPEC_THEN `t'` STRUCT_CASES_TAC nterm_nchotomy THEN 199SIMP_TAC (srw_ss()) 200[nterm_case_def] THEN 201SRW_TAC [][] THEN1 202(FIRST_X_ASSUM MATCH_MP_TAC THEN SELECT_ELIM_TAC THEN 203 SRW_TAC [][permeq_sym] THEN METIS_TAC [permeq_refl]) THEN 204METIS_TAC [permeq_refl]); 205 206val nterm_case_rewrites = RWstore_thm( 207"nterm_case_rewrites", 208`(nterm_CASE (Nom a) Nf Sf Tf Pf Cf = Nf a) ��� 209 (nterm_CASE (Tie a t) Nf Sf Tf Pf Cf = Tf a t) ��� 210 (nterm_CASE (nPair t1 t2) Nf Sf Tf Pf Cf = Pf t1 t2) ��� 211 (nterm_CASE (nConst c) Nf Sf Tf Pf Cf = Cf c)`, 212SIMP_TAC (srw_ss()) [nterm_case_def]); 213 214val Sus_case1 = Q.store_thm( 215"Sus_case1", 216`nterm_CASE (Sus p v) Nf Sf Tf Pf Cf = Sf (@p'. p' == p) v`, 217SRW_TAC [] [nterm_case_def]); 218 219(* Unfortunately this theorem is wasted when using Define, since only 220 Sus_case1 goes into the case theorem given to the TypeBase *) 221val Sus_case2 = Q.store_thm( 222"Sus_case2", 223`(���p1 p2. (p1 == p2) ��� (Sf p1 v = Sf p2 v)) ��� 224 (nterm_CASE (Sus p v) Nf Sf Tf Pf Cf = Sf p v)`, 225SRW_TAC [] [nterm_case_def] THEN 226FIRST_X_ASSUM MATCH_MP_TAC THEN 227SELECT_ELIM_TAC THEN SRW_TAC [][]); 228 229val nterm_size_def = RWnew_specification ("nterm_size_def", 230 ["nterm_size"], 231 nterm_rec_exists |> 232 Q.INST_TYPE [`:'a`|->`:num`] |> 233 Q.SPECL [ 234 `��a. 0`, 235 `��p v. 0`, 236 `��a t r. 1 + r`, 237 `��t1 t2 r1 r2. 1 + r1 + r2`, 238 `��c. 0`] |> 239 SIMP_RULE (srw_ss()) [] |> 240 GEN ``g:'b -> num`` |> 241 CONV_RULE SKOLEM_CONV |> 242 SIMP_RULE (srw_ss()) [FORALL_AND_THM]); 243 244val nterm_case_eq = Q.store_thm( 245 "nterm_case_eq", 246 ���(nterm_CASE n nmf sf tf pf cf = v) ��� 247 (���a. (n = Nom a) ��� (nmf a = v)) ��� 248 (���p w. (n = Sus p w) ��� (sf (@p'. p' == p) w = v)) ��� 249 (���a t. (n = Tie a t) ��� (tf a t = v)) ��� 250 (���t1 t2. (n = nPair t1 t2) ��� (pf t1 t2 = v)) ��� 251 (���c. (n = nConst c) ��� (cf c = v))���, 252 Q.ISPEC_THEN ���n��� STRUCT_CASES_TAC nterm_nchotomy >> 253 simp[nterm_case_rewrites, Sus_case1] >> eq_tac >> rw[] 254 >- (rename [���(c == _) /\ (_ = _)���] >> qexists_tac ���c��� >> simp[permeq_refl]) >> 255 rename [���_ (@p'. p' == c1) _ = _ (@p'. p' == c2) _���] >> 256 ������p. p == c2 <=> p == c1��� suffices_by simp[] >> 257 metis_tac[permeq_def]); 258 259local open TypeBase open TypeBasePure open Drule in 260val _ = write [mk_datatype_info { 261 ax = ORIG nterm_rec_exists, 262 induction = ORIG nterm_induction, 263 case_def = LIST_CONJ 264 (let val (n::rest) = CONJUNCTS nterm_case_rewrites 265 in n::Sus_case1::rest end), 266 case_cong = nterm_case_cong, 267 case_eq = nterm_case_eq, 268 nchotomy = nterm_nchotomy, 269 size = SOME (``nterm_size``,ORIG nterm_size_def), 270 encode = NONE, 271 lift = NONE, 272 one_one = NONE, 273 distinct = NONE (* SOME ntermeq_thm *), 274 fields = [], 275 accessors = [], 276 updates = [], 277 destructors = [], 278 recognizers = [] 279}] end 280 281val _ = adjoin_to_theory { 282 sig_ps = NONE, 283 struct_ps = SOME (fn _ => PP.add_string 284"local open TypeBase open TypeBasePure open Drule in\ 285\ val _ = write [mk_datatype_info {\ 286\ ax = ORIG nterm_rec_exists,\ 287\ induction = ORIG nterm_induction,\ 288\ case_def = LIST_CONJ\ 289\ (let val (n::rest) = CONJUNCTS nterm_case_rewrites\ 290\ in n::Sus_case1::rest end),\ 291\ case_cong = nterm_case_cong,\n\ 292\ case_eq = nterm_case_eq,\n\ 293\ nchotomy = nterm_nchotomy,\ 294\ size = SOME (``nterm_size``,ORIG nterm_size_def),\ 295\ encode = NONE,\ 296\ lift = NONE,\ 297\ one_one = NONE,\ 298\ distinct = NONE,\ 299\ fields = [],\ 300\ accessors = [],\ 301\ destructors = [],\ 302\ recognizers = [],\ 303\ updates = []\ 304\}] end\n")} 305 306val SELECT_permeq_REFL = RWstore_thm( 307"SELECT_permeq_REFL", 308`(@p.p==l)==l`, 309SELECT_ELIM_TAC THEN SRW_TAC [][]) 310 311val Sus_eq_perms = Q.store_thm( 312"Sus_eq_perms", 313`p1 == p2 ��� (Sus p1 v = Sus p2 v)`, 314SRW_TAC [][]) 315 316val nvars_def = RWDefine` 317 (nvars (Sus p v) = {v}) ��� 318 (nvars (Tie a t) = nvars t) ��� 319 (nvars (nPair t1 t2) = nvars t1 ��� nvars t2) ��� 320 (nvars _ = {})` 321 322val FINITE_nvars = RWstore_thm( 323"FINITE_nvars", 324`FINITE (nvars t)`, 325Induct_on `t` THEN SRW_TAC [][]) 326 327val nvarb_def = RWDefine` 328 (nvarb (Sus p v) = {|v|}) ��� 329 (nvarb (Tie a t) = nvarb t) ��� 330 (nvarb (nPair t1 t2) = nvarb t1 + nvarb t2) ��� 331 (nvarb _ = {||})` 332 333val FINITE_nvarb = RWstore_thm( 334 "FINITE_nvarb", 335 `���t. FINITE_BAG (nvarb t)`, 336 Induct THEN SRW_TAC [][]); 337 338val IN_nvarb_nvars = RWstore_thm( 339 "IN_nvarb_nvars", 340 `���t. BAG_IN e (nvarb t) <=> e IN nvars t`, 341 Induct THEN SRW_TAC [][]); 342 343val _ = export_theory (); 344