1open HolKernel Parse boolLib 2 3open bossLib simpLib 4 5val _ = new_theory "cl"; 6 7val _ = (hide "S"; hide "K") 8val _ = Datatype `cl = S | K | # cl cl`; 9 10val _ = set_fixity "#" (Infixl 1100); 11 12val _ = set_mapped_fixity {tok = "-->", fixity = Infix(NONASSOC, 450), 13 term_name = "redn"} 14 15val (redn_rules, _, _) = Hol_reln ` 16 (!x y f. x --> y ==> f # x --> f # y) /\ 17 (!f g x. f --> g ==> f # x --> g # x) /\ 18 (!x y. K # x # y --> x) /\ 19 (!f g x. S # f # g # x --> (f # x) # (g # x))`; 20 21val _ = hide "RTC"; 22 23val (RTC_rules, _, RTC_cases) = Hol_reln ` 24 (!x. RTC R x x) /\ 25 (!x y z. R x y /\ RTC R y z ==> RTC R x z)`; 26 27val confluent_def = Define` 28 confluent R = 29 !x y z. RTC R x y /\ RTC R x z ==> 30 ?u. RTC R y u /\ RTC R z u`; 31 32val normform_def = Define `normform R x = !y. ~R x y`; 33 34 35val confluent_normforms_unique = store_thm( 36 "confluent_normforms_unique", 37 ``!R. confluent R ==> 38 !x y z. RTC R x y /\ normform R y /\ RTC R x z /\ normform R z 39 ==> 40 (y = z)``, 41 rw[confluent_def] >> 42 `?u. RTC R y u /\ RTC R z u` by metis_tac [] >> 43 metis_tac [normform_def, RTC_cases]); 44 45val diamond_def = Define 46 `diamond R = !x y z. R x y /\ R x z ==> ?u. R y u /\ R z u`; 47 48val confluent_diamond_RTC = store_thm( 49 "confluent_diamond_RTC", 50 ``!R. confluent R = diamond (RTC R)``, 51 rw[confluent_def, diamond_def]); 52 53val R_RTC_diamond = store_thm( 54 "R_RTC_diamond", 55 ``!R. diamond R ==> 56 !x p. RTC R x p ==> 57 !z. R x z ==> 58 ?u. RTC R p u /\ RTC R z u``, 59 GEN_TAC >> STRIP_TAC >> Induct_on `RTC` >> 60 metis_tac [diamond_def,RTC_rules]); 61 62val RTC_RTC = store_thm( 63 "RTC_RTC", 64 ``!R x y z. RTC R x y /\ RTC R y z ==> RTC R x z``, 65 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] >> 66 GEN_TAC >> Induct_on `RTC` >> metis_tac [RTC_rules]); 67 68val diamond_RTC_lemma = prove( 69 ``!R. 70 diamond R ==> 71 !x y. RTC R x y ==> !z. RTC R x z ==> 72 ?u. RTC R y u /\ RTC R z u``, 73 GEN_TAC >> STRIP_TAC >> Induct_on `RTC` >> rw[] >| [ 74 metis_tac[RTC_rules], 75 `?v. RTC R x' v /\ RTC R z v` by metis_tac[R_RTC_diamond] >> 76 metis_tac [RTC_RTC, RTC_rules] 77 ]); 78 79val diamond_RTC = store_thm( 80 "diamond_RTC", 81 ``!R. diamond R ==> diamond (RTC R)``, 82 metis_tac [diamond_def,diamond_RTC_lemma]); 83 84val _ = set_mapped_fixity {tok = "-||->", fixity = Infix(NONASSOC, 450), 85 term_name = "predn"} 86val (predn_rules, predn_ind, predn_cases) = Hol_reln ` 87 (!x. x -||-> x) /\ 88 (!x y u v. x -||-> y /\ u -||-> v ==> x # u -||-> y # v) /\ 89 (!x y. K # x # y -||-> x) /\ 90 (!f g x. S # f # g # x -||-> (f # x) # (g # x)) 91`; 92 93val RTC_monotone = store_thm( 94 "RTC_monotone", 95 ``!R1 R2. (!x y. R1 x y ==> R2 x y) ==> 96 (!x y. RTC R1 x y ==> RTC R2 x y)``, 97 rpt GEN_TAC >> STRIP_TAC >> Induct_on `RTC` >> 98 rpt STRIP_TAC >> metis_tac [RTC_rules]); 99 100val _ = set_fixity "-->*" (Infix(NONASSOC, 450)); 101val _ = overload_on ("-->*", ``RTC redn``) 102 103val _ = set_fixity "-||->*" (Infix(NONASSOC, 450)); 104val _ = overload_on ("-||->*", ``RTC predn``) 105 106val RTCredn_RTCpredn = store_thm( 107 "RTCredn_RTCpredn", 108 ``!x y. x -->* y ==> x -||->* y``, 109 HO_MATCH_MP_TAC RTC_monotone >> Induct_on `x --> y` >> 110 metis_tac [predn_rules]); 111 112val RTCredn_ap_congruence = store_thm( 113 "RTCredn_ap_congruence", 114 ``!x y. x -->* y ==> !z. x # z -->* y # z /\ z # x -->* z # y``, 115 Induct_on `RTC` >> metis_tac [RTC_rules, redn_rules]); 116 117val predn_RTCredn = store_thm( 118 "predn_RTCredn", 119 ``!x y. x -||-> y ==> x -->* y``, 120 Induct_on `x -||-> y` >> 121 metis_tac [RTC_rules,redn_rules,RTC_RTC,RTCredn_ap_congruence]); 122 123val RTCpredn_RTCredn = store_thm( 124 "RTCpredn_RTCredn", 125 ``!x y. x -||->* y ==> x -->* y``, 126 Induct_on `RTC` >> metis_tac [predn_RTCredn, RTC_RTC, RTC_rules]); 127 128val RTCpredn_EQ_RTCredn = store_thm( 129 "RTCpredn_EQ_RTCredn", 130 ``$-||->* = $-->*``, 131 SIMP_TAC std_ss [FUN_EQ_THM] >> 132 metis_tac [RTCpredn_RTCredn, RTCredn_RTCpredn]); 133 134fun characterise t = SIMP_RULE (srw_ss()) [] (SPEC t predn_cases); 135 136val K_predn = characterise ``K``; 137val S_predn = characterise ``S``; 138val Sx_predn0 = characterise ``S # x``; 139 140val Sx_predn = prove( 141 ``!x y. S # x -||-> y = ?z. (y = S # z) /\ (x -||-> z)``, 142 rw[Sx_predn0, predn_rules, S_predn, EQ_IMP_THM]); 143 144val Kx_predn = prove( 145 ``!x y. K # x -||-> y = ?z. (y = K # z) /\ (x -||-> z)``, 146 rw[characterise ``K # x``, predn_rules, K_predn, EQ_IMP_THM]); 147 148val Kxy_predn = prove( 149 ``!x y z. K # x # y -||-> z = 150 (?u v. (z = K # u # v) /\ (x -||-> u) /\ (y -||-> v)) \/ 151 (z = x)``, 152 rw[characterise ``K # x # y``, predn_rules, Kx_predn, EQ_IMP_THM]); 153 154 155val Sxy_predn = prove( 156 ``!x y z. S # x # y -||-> z = 157 ?u v. (z = S # u # v) /\ (x -||-> u) /\ (y -||-> v)``, 158 rw[characterise ``S # x # y``, predn_rules, EQ_IMP_THM, 159 S_predn, Sx_predn]); 160 161val Sxyz_predn = prove( 162 ``!w x y z. S # w # x # y -||-> z = 163 (?p q r. (z = S # p # q # r) /\ 164 w -||-> p /\ x -||-> q /\ y -||-> r) \/ 165 (z = (w # y) # (x # y))``, 166 rw[characterise ``S # w # x # y``, predn_rules, Sxy_predn, EQ_IMP_THM]); 167 168val x_ap_y_predn = characterise ``x # y``; 169 170val predn_diamond_lemma = prove( 171 ``!x y. x -||-> y ==> 172 !z. x -||-> z ==> ?u. y -||-> u /\ z -||-> u``, 173 Induct_on `x -||-> y` >> rpt conj_tac >| [ 174 metis_tac [predn_rules], 175 rw[] >> 176 qpat_x_assum `_ # _ -||-> _` 177 (strip_assume_tac o SIMP_RULE std_ss [x_ap_y_predn]) >> 178 rw[] >| [ 179 metis_tac[predn_rules], 180 metis_tac[predn_rules], 181 `?w. (y = K # w) /\ (z -||-> w)` by metis_tac [Kx_predn] >> 182 rw[] >> metis_tac [predn_rules], 183 `?p q. (y = S # p # q) /\ (f -||-> p) /\ (g -||-> q)` by 184 metis_tac [Sxy_predn] >> 185 rw[] >> metis_tac [predn_rules] 186 ], 187 rw[Kxy_predn] >> metis_tac [predn_rules], 188 rw[Sxyz_predn] >> metis_tac [predn_rules] 189 ]); 190 191val predn_diamond = store_thm( 192 "predn_diamond", 193 ``diamond predn``, 194 metis_tac [diamond_def, predn_diamond_lemma]); 195 196val confluent_redn = store_thm( 197 "confluent_redn", 198 ``confluent redn``, 199 metis_tac [predn_diamond, confluent_diamond_RTC, 200 RTCpredn_EQ_RTCredn, diamond_RTC]); 201 202 203val _ = export_theory(); 204