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