1open HolKernel Parse boolLib bossLib 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