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