1(*---------------------------------------------------------------------------*) 2(* Tricky recursive definition of list reversal. Doesn't use any other *) 3(* functions, nor extra arguments. Suggested by Joe Hurd. See nest in this *) 4(* directory to see a different approach. *) 5(*---------------------------------------------------------------------------*) 6 7quietdec := true; 8open TotalDefn listTheory prim_recTheory; 9quietdec := false; 10 11val measure_length = Q.prove 12(`measure LENGTH t (h::t)`, RW_TAC list_ss [measure_thm]) 13 14(*---------------------------------------------------------------------------*) 15(* The definition *) 16(*---------------------------------------------------------------------------*) 17 18val rev_defn = Hol_defn 19 "rev" 20 `(rev [] = []) /\ 21 (rev (x::xs) = 22 case rev xs 23 of [] -> [x] 24 || y::ys -> y :: rev (x::rev ys))`; 25 26(*---------------------------------------------------------------------------*) 27(* Fetch and simplify the auxiliary eqns *) 28(*---------------------------------------------------------------------------*) 29 30val rev_defn1 = Defn.set_reln rev_defn ``measure LENGTH``; 31val SOME rev_aux_defn = Defn.aux_defn rev_defn1; 32val [e1,e2] = Defn.eqns_of rev_aux_defn; 33val rev_empty = SIMP_RULE std_ss [WF_measure] (DISCH_ALL e1); 34val rev_cons = 35 SIMP_RULE std_ss [WF_measure,measure_length] (DISCH_ALL e2); 36 37(*---------------------------------------------------------------------------*) 38(* Fetch and simplify the auxiliary induction theorem *) 39(*---------------------------------------------------------------------------*) 40 41val SOME rev_aux_ind = Defn.ind_of rev_aux_defn; 42val ind = SIMP_RULE std_ss [WF_measure,measure_length] (DISCH_ALL rev_aux_ind); 43 44(*---------------------------------------------------------------------------*) 45(* Useful invariant *) 46(*---------------------------------------------------------------------------*) 47 48val REV_AUX_LENGTH = Q.prove 49(`!l. LENGTH (rev_aux (measure LENGTH) l) = LENGTH l`, 50 recInduct ind 51 THEN RW_TAC list_ss [rev_empty] 52 THEN MP_TAC rev_cons 53 THEN Q.ABBREV_TAC `Rev = rev_aux (measure LENGTH)` 54 THEN CASE_TAC 55 THEN FULL_SIMP_TAC list_ss [measure_thm]); 56 57(*---------------------------------------------------------------------------*) 58(* val rev_def = *) 59(* |- (rev [] = []) /\ *) 60(* (rev (x::xs) = *) 61(* case rev xs of [] -> [x] || y::ys -> y::rev (x::rev ys)) : thm *) 62(* *) 63(* val rev_ind = *) 64(* |- !P. *) 65(* P [] /\ *) 66(* (!x xs. *) 67(* (!y ys. (rev xs = y::ys) ==> P ys) /\ *) 68(* (!y ys. (rev xs = y::ys) ==> P (x::rev ys)) /\ P xs ==> *) 69(* P (x::xs)) ==> *) 70(* !v. P v : thm *) 71(*---------------------------------------------------------------------------*) 72 73val (rev_def, rev_ind) = Defn.tprove 74(rev_defn1, 75 REPEAT CONJ_TAC THENL 76 [METIS_TAC [WF_measure], ALL_TAC, ALL_TAC, RW_TAC list_ss [measure_thm]] 77 THEN Q.ABBREV_TAC `Rev = rev_aux (measure LENGTH)` 78 THEN RW_TAC list_ss [measure_thm] 79 THEN `(LENGTH (Rev xs) = LENGTH xs) /\ (LENGTH (Rev xs) = LENGTH (y::ys))` 80 by METIS_TAC [REV_AUX_LENGTH] 81 THENL [ALL_TAC, `LENGTH (Rev ys) = LENGTH ys` by METIS_TAC [REV_AUX_LENGTH]] 82 THEN FULL_SIMP_TAC list_ss []); 83 84 85(*---------------------------------------------------------------------------*) 86(* rev = REVERSE *) 87(*---------------------------------------------------------------------------*) 88 89val rev_REVERSE = Q.prove 90(`rev = REVERSE`, 91 REWRITE_TAC [FUN_EQ_THM] THEN recInduct rev_ind THEN CONJ_TAC THENL 92 [METIS_TAC [rev_def, REVERSE_DEF], 93 REPEAT STRIP_TAC THEN RW_TAC list_ss [Once rev_def] 94 THEN CASE_TAC THEN RW_TAC list_ss []]); 95 96