1open HolKernel Parse boolLib bossLib lcsymtacs
2open binderLib
3
4open termTheory chap3Theory
5
6val _ = new_theory "takahashi"
7
8val redAPP_exists =
9    parameter_tm_recursion
10        |> INST_TYPE [alpha |-> ``:term``, ``:��`` |-> ``:term``]
11        |> Q.INST [`ap` |-> `\rt ru t u p. t @@ u @@ p`,
12                   `lm` |-> `\rt v t p. [p/v]t`,
13                   `vr` |-> `\s p. VAR s @@ p`,
14                   `apm` |-> `term_pmact`, `ppm` |-> `term_pmact`,
15                   `A` |-> `{}`]
16        |> SIMP_RULE (srw_ss()) [tpm_subst]
17        |> SIMP_RULE (srw_ss()) [fresh_tpm_subst, lemma15a]
18
19val redAPP_def = new_specification("redAPP_def", ["redAPP"], redAPP_exists)
20
21val redAPP_LAM = prove(
22  ``redAPP (LAM v M) N = [N/v]M``,
23  Q_TAC (NEW_TAC "z") `{v} ��� FV M ��� FV N` >>
24  `LAM v M = LAM z ([VAR z/v]M)` by rw[SIMPLE_ALPHA] >>
25  simp[redAPP_def, lemma15a]);
26
27(*
28
29redAPP applies term 1 to term 2, unless term 2 is an abstraction, in
30which case it performs a ��-reduction:
31
32   redAPP (VAR s) P = VAR s @@ p
33   redAPP (M @@ N) P = M @@ N @@ P
34   redAPP (LAM v M) N = [N/v]M
35*)
36
37val redAPP_thm = save_thm(
38  "redAPP_thm",
39  redAPP_def
40      |> CONJ_PAIR
41      |> apfst
42           (fn th1 => th1 |> CONJUNCTS |> front_last |> #1
43                          |> (fn l => l @ [GEN_ALL redAPP_LAM]) |> LIST_CONJ)
44      |> uncurry CONJ)
45val _ = export_rewrites ["redAPP_thm"]
46
47val pmact_COND = prove(
48  ``pmact a pi (COND p q r) = COND p (pmact a pi q) (pmact a pi r)``,
49  rw[]);
50
51(* Takahashi's superscript star operator *)
52val (tstar_thm, tpm_tstar) = define_recursive_term_function'
53  (SIMP_CONV (srw_ss()) [tpm_ALPHA,pmact_COND])
54`
55  (tstar (VAR s) = VAR s) ���
56  (tstar (APP M N) = if is_abs M then redAPP (tstar M) (tstar N)
57                     else tstar M @@ tstar N) ���
58  (tstar (LAM v M) = LAM v (tstar M))
59`;
60
61(* tstar (LAM v M @@ N) = [tstar N/v] (tstar M) *)
62val tstar_redex =
63    tstar_thm |> CONJUNCTS |> el 2
64              |> Q.INST [`M` |-> `LAM v M`]
65              |> SIMP_RULE (srw_ss()) [last (CONJUNCTS tstar_thm)]
66
67val _ = overload_on("RTC", ``tstar``)
68
69val varreflind_refl = prove(
70  ``���P X. (���s. P (VAR s) (VAR s)) ���
71          (���v M1 M2. v ��� X ��� P M1 M2 ��� P (LAM v M1) (LAM v M2)) ���
72          (���M1 M2 N1 N2. P M1 M2 ��� P N1 N2 ���
73                         P (M1 @@ N1) (M2 @@ N2)) ���
74          (���M1 M2 N1 N2 v.
75             v ��� X ��� v ��� FV N1 ��� v ��� FV N2 ��� P M1 M2 ��� P N1 N2 ���
76             P (LAM v M1 @@ N1) ([N2/v]M2)) ��� FINITE X ���
77    ���M. P M M``,
78  rpt gen_tac >> strip_tac >>
79  ho_match_mp_tac nc_INDUCTION2 >> qexists_tac `X` >> simp[])
80
81val varreflind0 = prove(
82  ``���P X. (���s. P (VAR s) (VAR s)) ���
83          (���v M1 M2. v ��� X ��� P M1 M2 ��� P (LAM v M1) (LAM v M2)) ���
84          (���M1 M2 N1 N2. P M1 M2 ��� P N1 N2 ���
85                         P (M1 @@ N1) (M2 @@ N2)) ���
86          (���M1 M2 N1 N2 v.
87             v ��� X ��� v ��� FV N1 ��� v ��� FV N2 ��� P M1 M2 ��� P N1 N2 ���
88             P (LAM v M1 @@ N1) ([N2/v]M2)) ��� FINITE X ���
89    ���M N. M =��=> N ��� P M N``,
90  rpt gen_tac >> strip_tac >> ho_match_mp_tac grandbeta_bvc_ind >>
91  qexists_tac `X` >> simp[] >>
92  match_mp_tac varreflind_refl >> qexists_tac `X` >> simp[])
93
94val varreflind =
95    varreflind0
96        |> Q.SPEC `��M N. P M N ��� M =��=> N`
97        |> SIMP_RULE (srw_ss()) [grandbeta_rules, GSYM CONJ_ASSOC]
98
99val grandbeta_refl = store_thm(
100  "grandbeta_refl",
101  ``M =��=> M``,
102  simp[grandbeta_rules]);
103val _ = export_rewrites ["grandbeta_refl"]
104
105val takahashi_5 = store_thm(
106  "takahashi_5",
107  ``���M N. M =��=> N ��� N =��=> M^*``,
108  ho_match_mp_tac varreflind >> qexists_tac `{}` >>
109  simp[tstar_thm, grandbeta_rules] >>
110  rpt conj_tac
111  >- (map_every qx_gen_tac [`M1`, `M2`, `N1`, `N2`] >> strip_tac >>
112      Tactical.REVERSE (Cases_on `is_abs M1`) >- simp[grandbeta_rules] >>
113      `���v M0. M1 = LAM v M0`
114         by (qspec_then `M1` FULL_STRUCT_CASES_TAC term_CASES >> fs[] >>
115             metis_tac[]) >>
116      fs[tstar_thm, abs_grandbeta] >> fs[abs_grandbeta, grandbeta_rules]) >>
117  simp[grandbeta_subst])
118
119val grandbeta_diamond = store_thm(
120  "grandbeta_diamond",
121  ``diamond_property $=b=>``,
122  metis_tac [takahashi_5, diamond_property_def]);
123
124val _ = export_theory()
125