1open HolKernel boolLib bossLib Parse
2
3open termTheory sttTheory contextlistsTheory NEWLib nomsetTheory
4
5val _ = new_theory "sttVariants"
6
7(* prove a cofinite version of the induction principle *)
8val hastype_cofin_ind = store_thm(
9  "hastype_cofin_ind",
10  ``!P.
11       (!G s A. valid_ctxt G /\ MEM (s,A) G ==> P G (VAR s) A) /\
12       (!G m n A B.
13            P G m (A --> B) /\ P G n A ==>
14            P G (m @@ n) B) /\
15       (!G v m A B X.
16            FINITE X /\
17            (!y. ~(y IN X) ==> P ((y,A)::G) ([VAR y/v]m) B) ==>
18            P G (LAM v m) (A --> B)) ==>
19       !G m A. G |- m -: A ==> P G m A``,
20  GEN_TAC THEN STRIP_TAC THEN
21  Q_TAC SUFF_TAC `!G m A. G |- m -: A ==> !pi. P (ctxtswap pi G) (tpm pi m) A`
22        THEN1 METIS_TAC [pmact_nil] THEN
23  HO_MATCH_MP_TAC hastype_strongind THEN
24  SRW_TAC [][] THEN1 METIS_TAC [] THEN
25  Q_TAC (NEW_TAC "z") `FV (tpm pi m) UNION ctxtFV (ctxtswap pi G) UNION
26                       {x;lswapstr pi x} UNION FV m UNION ctxtFV G` THEN
27  `LAM (lswapstr pi x) (tpm pi m) = LAM z (tpm [(z,lswapstr pi x)] (tpm pi m))`
28     by SRW_TAC [][tpm_ALPHA] THEN
29  SRW_TAC [][] THEN
30  FIRST_X_ASSUM MATCH_MP_TAC THEN
31  Q.EXISTS_TAC `ctxtFV (ctxtswap pi G) UNION FV (tpm pi m) UNION
32                {x; z; lswapstr pi x} UNION FV m UNION ctxtFV G` THEN
33  SRW_TAC [][] THEN
34  FIRST_X_ASSUM (Q.SPEC_THEN `(y, lswapstr pi x) :: pi` MP_TAC) THEN
35  ASM_SIMP_TAC (srw_ss()) [] THEN
36  `~(x IN ctxtFV G)`
37     by (`valid_ctxt ((x,A)::G)` by METIS_TAC [hastype_valid_ctxt] THEN
38         FULL_SIMP_TAC (srw_ss()) []) THEN
39  `ctxtswap ((y,lswapstr pi x)::pi) G =
40      ctxtswap [(y,lswapstr pi x)] (ctxtswap pi G)`
41     by SRW_TAC [][GSYM pmact_decompose] THEN
42  `_ = ctxtswap pi G` by SRW_TAC [][ctxtswap_fresh] THEN
43  `[VAR y/z] (tpm [(z,lswapstr pi x)] (tpm pi m)) =
44     tpm [(y,z)] (tpm [(z,lswapstr pi x)] (tpm pi m))`
45       by SRW_TAC [][fresh_tpm_subst] THEN
46  `_ = tpm [(lswapstr [(y,z)] z, lswapstr [(y,z)] (lswapstr pi x))]
47           (tpm [(y,z)] (tpm pi m))`
48       by SRW_TAC [][Once (GSYM pmact_sing_to_back)] THEN
49  `_ = tpm [(y,lswapstr pi x)] (tpm pi m)`
50       by SRW_TAC [][tpm_fresh, nomsetTheory.supp_apart] THEN
51  SRW_TAC [][GSYM pmact_decompose]);
52
53(* and a "cofinite" introduction rule for the abstraction case *)
54val cofin_hastype_abs_I = store_thm(
55  "cofin_hastype_abs_I",
56  ``!X v M A B G.
57         FINITE X /\
58         (!u. ~(u IN X) ==> (u,A)::G |- [VAR u/v]M -: B)
59       ==>
60         G |- LAM v M -: (A --> B)``,
61  REPEAT STRIP_TAC THEN
62  Q_TAC (NEW_TAC "z") `X UNION FV M` THEN
63  `LAM v M = LAM z ([VAR z/v] M)` by SRW_TAC [][SIMPLE_ALPHA] THEN
64  SRW_TAC [][hastype_rules]);
65
66(* this then allows a nice, renaming free proof of weakening *)
67val weakening_cofin = prove(
68  ``!G m A. G |- m -: A ==> !D. G ��� D /\ valid_ctxt D ==> D |- m -: A``,
69  HO_MATCH_MP_TAC hastype_cofin_ind THEN
70  SRW_TAC [][] THENL [
71    METIS_TAC [hastype_rules, subctxt_def],
72    METIS_TAC [hastype_rules],
73    MATCH_MP_TAC cofin_hastype_abs_I THEN
74    Q.EXISTS_TAC `X UNION ctxtFV D` THEN SRW_TAC [][] THEN
75    `valid_ctxt ((u,A)::D)` by FULL_SIMP_TAC (srw_ss()) [] THEN
76    `((u,A)::G) ��� ((u,A)::D)`
77       by FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [subctxt_def] THEN
78    SRW_TAC [][]
79  ]);
80
81
82(* ----------------------------------------------------------------------
83    A more involved way of doing a similar "universal in the hypothesis"
84    thing.
85   ---------------------------------------------------------------------- *)
86
87(* now a slightly different typing relation, with different syntax: "||-"
88   instead of "|-".  Underlying name of constant is "hastype2".  *)
89val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)),
90                  fixity = Infix(NONASSOC, 425),
91                  paren_style = OnlyIfNecessary,
92                  pp_elements = [HardSpace 1, TOK "||-", BreakSpace(1, 0),
93                                 BeginFinalBlock(PP.INCONSISTENT, 2),
94                                 TM, HardSpace 1, TOK "-:", BreakSpace(1,0)],
95                  term_name = "hastype2"}
96
97val (hastype2_rules, hastype2_ind, hastype2_cases) = Hol_reln`
98  (!Gamma s A. valid_ctxt Gamma /\ MEM (s,A) Gamma ==>
99               Gamma ||- VAR s -: A) /\
100  (!Gamma m n A B. Gamma ||- m -: A --> B /\ Gamma ||- n -: A ==>
101                   Gamma ||- m @@ n -: B) /\
102  (!Gamma m x A B. (!v. ~(v IN ctxtFV Gamma) ==>
103                        (v,A) :: Gamma ||- [VAR v/x]m -: B) ���
104                   ~(x ��� ctxtFV Gamma) ==>
105                   Gamma ||- LAM x m -: A --> B)
106`;
107
108val hastype2_swap = store_thm(
109  "hastype2_swap",
110  ``!G m A. G ||- m -: A ==> !pi. ctxtswap pi G ||- tpm pi m -: A``,
111  HO_MATCH_MP_TAC hastype2_ind THEN SRW_TAC [][] THENL [
112    METIS_TAC [hastype2_rules, MEM_ctxtswap, valid_ctxt_swap],
113    METIS_TAC [hastype2_rules],
114    MATCH_MP_TAC (last (CONJUNCTS hastype2_rules)) THEN
115    SRW_TAC [][tpm_subst_out] THEN
116    METIS_TAC [pmact_inverse]
117  ]);
118
119val hastype2_bvc_ind = store_thm(
120  "hastype2_bvc_ind",
121  ``!P fv.
122      (!x. FINITE (fv x)) /\
123      (!G s A x.
124         valid_ctxt G /\ MEM (s,A) G ==> P G (VAR s) A x)
125         /\
126      (!G m n A B x.
127          (!y. P G m (A --> B) y) /\
128          (!y. P G n A y) ==>
129             P G (m @@ n) B x) /\
130
131      (!G m u A B x.
132          (!v y. ~(v IN ctxtFV G) ==> P ((v,A)::G) ([VAR v/u] m) B y) /\
133          ~(u IN ctxtFV G) /\ ~(u IN fv x)
134        ==>
135          P G (LAM u m) (A --> B) x)
136    ==>
137      !G m ty. G ||- m -: ty ==> !x. P G m ty x``,
138  REPEAT GEN_TAC THEN STRIP_TAC THEN
139  Q_TAC SUFF_TAC `!G m ty. G ||- m -: ty ==>
140                           !pi x. P (ctxtswap pi G) (tpm pi m) ty x`
141        THEN1 METIS_TAC [pmact_nil] THEN
142  HO_MATCH_MP_TAC hastype2_ind THEN
143  SRW_TAC [][] THEN1 METIS_TAC [] THEN
144  Q.MATCH_ABBREV_TAC `P GG (LAM vv MM) (A --> B) xx` THEN
145  Q_TAC (NEW_TAC "z") `{vv} UNION FV MM UNION ctxtFV GG UNION fv xx` THEN
146  `LAM vv MM = LAM z (tpm [(z,vv)] MM)`
147     by SRW_TAC [][tpm_ALPHA] THEN
148  SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
149  SRW_TAC [][] THEN
150  FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [tpm_subst] THEN
151  FIRST_X_ASSUM (Q.SPECL_THEN [`lswapstr (REVERSE ((z,vv)::pi)) v`,
152                               `(z,vv)::pi`, `y`]
153                 MP_TAC) THEN
154  ASM_SIMP_TAC (srw_ss()) [pmact_decompose] THEN
155  `~(vv IN ctxtFV GG)` by SRW_TAC [][Abbr`vv`, Abbr`GG`] THEN
156  `ctxtswap ((z,vv)::pi) G = ctxtswap [(z,vv)] GG`
157     by SRW_TAC [][Abbr`GG`, GSYM pmact_decompose] THEN
158  ` _ = GG` by SRW_TAC [][ctxtswap_fresh] THEN
159  `tpm ((z,vv)::pi) m = tpm [(z,vv)] MM`
160     by SRW_TAC [][Abbr`MM`, GSYM pmact_decompose] THEN
161  SRW_TAC [][] THEN
162  FIRST_X_ASSUM MATCH_MP_TAC THEN
163  FULL_SIMP_TAC (srw_ss()) [pmact_decompose]);
164
165val hastype2_bvc_ind0 = save_thm(
166  "hastype2_bvc_ind0",
167  (Q.GEN `P` o Q.GEN `X` o
168   SIMP_RULE bool_ss [] o
169   Q.SPECL [`\G m ty x. P G m ty`, `\x. X`]) hastype2_bvc_ind)
170
171val hastype2_valid_ctxt = store_thm(
172  "hastype2_valid_ctxt",
173  ``!G m A. G ||- m -: A ==> valid_ctxt G``,
174  HO_MATCH_MP_TAC hastype2_ind THEN SRW_TAC [][] THEN METIS_TAC []);
175
176val hastype2_swap_eqn = store_thm(
177  "hastype2_swap_eqn",
178  ``G ||- tpm pi m -: A <=> ctxtswap (REVERSE pi) G ||- m -: A``,
179  METIS_TAC [hastype2_swap, pmact_inverse]);
180
181val hastype2_hastype = prove(
182  ``!G m A. G ||- m -: A ==> G |- m -: A``,
183  HO_MATCH_MP_TAC hastype2_ind THEN REPEAT CONJ_TAC THENL [
184    (* var case *) SRW_TAC [][hastype_rules],
185    (* app case *) METIS_TAC [hastype_rules],
186    (* abs case *) METIS_TAC [hastype_rules, lemma14a]
187  ]);
188
189val hastype_hastype2 = prove(
190  ``!G m A. G |- m -: A ==> G ||- m -: A``,
191  HO_MATCH_MP_TAC hastype_indX THEN Q.EXISTS_TAC `{}` THEN
192  SRW_TAC [][hastype2_rules] THENL [
193    (* app case *) METIS_TAC [hastype2_rules],
194    (* abs case; goal with IH is: *)
195    MATCH_MP_TAC (last (CONJUNCTS hastype2_rules)) THEN
196    SRW_TAC [][] THEN
197    Cases_on `v = v'` THEN1 SRW_TAC [][lemma14a] THEN
198    (* if v' = v, proof is trivial; rest of tactic is for other case *)
199    `v' ��� ctxtFV ((v,A)::G)` by SRW_TAC [][] THEN
200    `~(v' IN FV m)` by METIS_TAC [hastype_FV] THEN
201    `[VAR v'/v] m = tpm [(v',v)] m` by SRW_TAC [][fresh_tpm_subst] THEN
202    SRW_TAC [][hastype2_swap_eqn, ctxtswap_fresh]
203  ]);
204
205val hastype_hastype2_eqn = store_thm(
206  "hastype_hastype2_eqn",
207  ``G |- m -: A <=> G ||- m -: A``,
208  METIS_TAC [hastype2_hastype, hastype_hastype2]);
209
210val _ = export_theory ()
211