1 2open HolKernel Parse boolLib bossLib 3 4val _ = new_theory("env") 5 6 7open bossLib 8open pairTheory 9open pairLib 10open pairTools 11open pairSyntax 12open pred_setTheory 13open pred_setLib 14open listTheory 15open stringTheory 16open sumTheory 17open simpLib 18open stringLib 19open numLib 20open metisLib 21open setLemmasTheory 22 23(* defns about environments *) 24 25val ENV_UPDATE_def = save_thm("ENV_UPDATE_def",Define 26 `ENV_UPDATE (e:string -> 'state -> bool) (Q:string) (s:'state -> bool) = \q. if (q=Q) then s else e q`) 27 28val _ = add_rule {term_name = "ENV_UPDATE", fixity = Suffix 2503, 29 pp_elements = [TOK "[[[", TM, TOK "<--",TM, TOK "]]]"], 30 paren_style = OnlyIfNecessary, 31 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))} 32 33(* initially had BOTTOMSET instead of {} but that causes problems when evaluating concrete environments where I would like all empty 34environments to evaluate to the same thing, rather than not evaluate at all. Using {} is not as satisfactory theoretically but more 35practical *) 36val EMPTY_ENV = Define `EMPTY_ENV = \(s:string). {}` 37 38 39(* thms about environments *) 40 41val env1a = prove(``!x Q Q'. ~(Q=Q') ==> (!e X X'. e[[[Q<--X]]][[[Q'<--X']]]x = e[[[Q'<--X']]][[[Q<--X]]]x)``,RW_TAC std_ss [ENV_UPDATE_def] THEN ASSUM_LIST PROVE_TAC) 42 43val ENV_SWAP = save_thm("ENV_SWAP",prove (``!e Q Q' X X'. ~(Q=Q') ==> (e[[[Q<--X]]][[[Q'<--X']]] = e[[[Q'<--X']]][[[Q<--X]]])``, 44 RW_TAC std_ss [ENV_UPDATE_def,EXTENSION,SET_SPEC] 45 THEN RW_TAC std_ss [FUN_EQ_CONV ``(\q. (if q = Q' then X' else (if q = Q then X else e q))) = 46 (\q. (if q = Q then X else (if q = Q' then X' else e q)))``,env1a,ENV_UPDATE_def] 47 THEN ASSUM_LIST PROVE_TAC)) 48 49val ENV_UPDATE = save_thm("ENV_UPDATE",prove(``!Q e X Y. e[[[Q<--X]]][[[Q<--Y]]] = e[[[Q<--Y]]]``,RW_TAC std_ss [ENV_UPDATE_def])) 50 51val ENV_EVAL = save_thm("ENV_EVAL",prove(``!e Q X. e[[[Q<--X]]] Q = X``,SIMP_TAC std_ss [ENV_UPDATE_def])) 52 53val ENV_UPDATE_INV = save_thm("ENV_UPDATE_INV",prove(``!e Q Q' X. ~(Q=Q') ==> (e[[[Q'<--X]]] Q = e Q)``,SIMP_TAC std_ss [ENV_UPDATE_def])) 54 55val ENV_EVAL_EQ_INV = save_thm("ENV_EVAL_EQ_INV",prove(``!e e' Q P X. (Q=P) ==> (e[[[Q<--X]]] P = e'[[[Q<--X]]] P)``, 56 SIMP_TAC std_ss [ENV_UPDATE_def])) 57 58val ENV_EVAL_NEQ_INV = save_thm("ENV_EVAL_NEQ_INV",prove(``!e e' Q P X. ~(Q=P) ==> ((e[[[Q<--X]]] P = e'[[[Q<--X]]] P) = (e P = e' P))``, 59 SIMP_TAC std_ss [ENV_UPDATE_def])) 60 61val EMPTY_ENV_MAP = save_thm("EMPTY_ENV_MAP",prove(``!x y. EMPTY_ENV x = EMPTY_ENV y``,SIMP_TAC std_ss [EMPTY_ENV])) 62 63val ENV_UPDATE_BOTH_INV = save_thm("ENV_UPDATE_BOTH_INV",prove(``!e Q Q' X Y. ~(Q=Q') ==> (e[[[Q'<--X]]] Q = e[[[Q'<--Y]]] Q)``,SIMP_TAC std_ss [ENV_UPDATE_def])) 64 65val ENV_CASES = save_thm("ENV_CASES",prove(``!e e' P Q X Y. e[[[P<--X]]] Q SUBSET e'[[[P<--Y]]] Q = if (Q=P) then X SUBSET Y else e Q SUBSET e' Q``,REPEAT STRIP_TAC THEN SIMP_TAC std_ss [ENV_UPDATE_def,SUBSET_DEF] THEN REPEAT COND_CASES_TAC THEN SIMP_TAC std_ss [])) 66 67val _ = export_theory() 68