1(*---------------------------------------------------------------------------*)
2(* Higher order recursion on N-ary trees.                                    *)
3(*---------------------------------------------------------------------------*)
4
5set_trace "Unicode" 0;
6set_trace "pp_annotations" 0;
7
8use (HOLDIR^"/src/pfl/defchoose");
9
10quietdec := true;
11open arithmeticTheory optionTheory;
12quietdec := false;
13
14(*---------------------------------------------------------------------------*)
15(* General purpose support.                                                  *)
16(*---------------------------------------------------------------------------*)
17
18val MAX_LE_THM = Q.prove
19(`!m n. m <= MAX m n /\ n <= MAX m n`,
20 RW_TAC arith_ss [MAX_DEF]);
21
22val IS_SOME_EXISTS = Q.prove
23(`!x. IS_SOME x = ?y. x = SOME y`,
24 Cases THEN METIS_TAC [optionTheory.IS_SOME_DEF]);
25
26(*---------------------------------------------------------------------------*)
27(* Declare tree type.                                                        *)
28(*---------------------------------------------------------------------------*)
29
30Hol_datatype `tree = Node of 'a => tree list`;
31
32(*---------------------------------------------------------------------------*)
33(* pEXISTS : ('a -> bool option) -> 'a list -> bool option                   *)
34(*                                                                           *)
35(* Since we are in a setting with no notion of evaluation order, we have to  *)
36(* imagine that any evaluation order will take place. Ugh. pEXISTS P l must  *)
37(* return NONE if an invocation of P on any list element returns NONE.       *)
38(* Otherwise, if there is an element x s.t. P x = SOME T, then return        *)
39(* SOME T. Otherwise, return SOME F.                                         *)
40(*---------------------------------------------------------------------------*)
41
42val pEXISTS_def =
43 Define
44   `(pEXISTS P [] = SOME F) /\
45    (pEXISTS P (h::t) =
46       case pEXISTS P t
47        of NONE -> NONE
48        || SOME b ->
49              case P h
50               of NONE -> NONE
51               || SOME F -> SOME b
52               || SOME T -> SOME T)`;
53
54val pEXISTS_CONG = Q.prove
55(`!l1 l2 P P'.
56     (l1 = l2) /\ (!x. MEM x l2 ==> (P x = P' x)) ==>
57     (pEXISTS P l1 = pEXISTS P' l2)`,
58 Induct THENL [ALL_TAC, GEN_TAC] THEN Induct
59   THEN RW_TAC list_ss [pEXISTS_def]
60   THEN FULL_SIMP_TAC list_ss [] THEN RW_TAC list_ss [] THEN
61   REPEAT CASE_TAC THEN METIS_TAC [NOT_SOME_NONE,SOME_11]);
62
63val pEXISTS_DEFINED_LIST = Q.prove
64(`!l t. MEM t l /\ IS_SOME (pEXISTS P l) ==> IS_SOME (P t)`,
65 Induct THEN SIMP_TAC list_ss [pEXISTS_def] THEN
66   REPEAT (GEN_TAC ORELSE CASE_TAC) THEN RW_TAC list_ss [] THEN
67   METIS_TAC [IS_SOME_EXISTS, IS_SOME_DEF]);
68
69val IS_SOME_PEXISTS_DISTRIB = Q.prove
70(`!l. IS_SOME (pEXISTS P l) <=> !t. MEM t l ==> IS_SOME(P t)`,
71Induct THEN SIMP_TAC list_ss [pEXISTS_def,EQ_IMP_THM] THEN
72  REPEAT (GEN_TAC ORELSE CASE_TAC) THEN RW_TAC list_ss [] THEN
73   METIS_TAC [IS_SOME_EXISTS, IS_SOME_DEF]);
74
75
76(*---------------------------------------------------------------------------*)
77(* Indexed function definition                                               *)
78(*---------------------------------------------------------------------------*)
79
80val iintree_def =
81 Define
82  `iintree d x tree =
83     if d=0 then NONE else
84     case tree
85      of Node y tlist -> if x=y then SOME T
86                         else pEXISTS (iintree (d-1) x) tlist`;
87
88(*---------------------------------------------------------------------------*)
89(* Domain of the function.                                                   *)
90(*---------------------------------------------------------------------------*)
91
92val dom_def = Define `dom x tree = ?d. IS_SOME(iintree d x tree)`;
93
94(*---------------------------------------------------------------------------*)
95(* Measure on recursion depth.                                               *)
96(*---------------------------------------------------------------------------*)
97
98val rdepth_thm =
99 MINCHOOSE ("rdepth_thm", "rdepth",
100            ``!x tree. ?d. IS_SOME (iintree d x tree)``);
101
102(*---------------------------------------------------------------------------*)
103(* Define intree                                                             *)
104(*---------------------------------------------------------------------------*)
105
106val intree_def =
107 Define
108   `intree x tree = THE (iintree (rdepth x tree) x tree)`;
109
110(*---------------------------------------------------------------------------*)
111(* Lemmas about izero and definedness                                        *)
112(*---------------------------------------------------------------------------*)
113
114val IS_SOME_IINTREE = Q.prove
115(`!d x tree. IS_SOME (iintree d x tree) ==> d <> 0`,
116 Cases THEN RW_TAC std_ss [Once iintree_def]);
117
118val IS_SOME_PEXISTS = Q.prove
119(`!l d x. IS_SOME (pEXISTS (iintree d x) l) ==> (l=[]) \/ d <> 0`,
120 Cases THEN RW_TAC list_ss [Once iintree_def,pEXISTS_def] THEN CASE_TAC);
121
122val iintree_dlem = Q.prove
123(`!d x tree.
124    IS_SOME (iintree d x tree) ==> (iintree d x tree = iintree (SUC d) x tree)`,
125Induct THENL [METIS_TAC [IS_SOME_IINTREE], ALL_TAC] THEN
126  REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [iintree_def] THEN
127  REPEAT CASE_TAC THEN FULL_SIMP_TAC arith_ss [] THEN
128  METIS_TAC[IS_SOME_EXISTS,SOME_11,IS_SOME_DEF,NOT_SOME_NONE]);
129
130val iintree_determ = Q.prove
131(`!d1 d2 x tree.
132    IS_SOME(iintree d1 x tree) /\
133    IS_SOME(iintree d2 x tree) ==> (iintree d1 x tree = iintree d2 x tree)`,
134 Induct THENL [METIS_TAC [IS_SOME_IINTREE,numTheory.NOT_SUC],
135 Induct THENL [METIS_TAC [IS_SOME_IINTREE,numTheory.NOT_SUC],
136   POP_ASSUM (K ALL_TAC) THEN REPEAT GEN_TAC THEN
137   ONCE_REWRITE_TAC [iintree_def] THEN SIMP_TAC arith_ss [] THEN
138   REPEAT CASE_TAC THEN RW_TAC std_ss [] THEN
139   MATCH_MP_TAC pEXISTS_CONG THEN RW_TAC list_ss [] THEN
140   FIRST_ASSUM MATCH_MP_TAC THEN METIS_TAC [IS_SOME_PEXISTS_DISTRIB]]]);
141
142val iintree_monotone_step = Q.prove
143(`!d x tree. IS_SOME(iintree d x tree) ==> IS_SOME(iintree (SUC d) x tree)`,
144e (Induct THENL [RW_TAC arith_ss [Once iintree_def],
145                 ONCE_REWRITE_TAC [iintree_def]]);
146e (SIMP_TAC arith_ss [] THEN REPEAT GEN_TAC THEN
147   REPEAT CASE_TAC THEN STRIP_TAC);
148e (`(l=[]) \/ d<>0` by METIS_TAC [IS_SOME_PEXISTS]);
149(*1*)
150e (RW_TAC list_ss [pEXISTS_def]);
151(*2*)
152e (`iintree (SUC d) x (Node a l) = pEXISTS (iintree d x) l`
153   by (RW_TAC list_ss [Once iintree_def] THEN METIS_TAC[]));
154e (RW_TAC list_ss [Once iintree_def]);
155e (`IS_SOME (iintree (SUC d) x (Node a l))` by METIS_TAC []);
156
157REPEAT STRIP_TAC THEN RW_TAC list_ss [Once iintree_def] THEN
158 CASE_TAC THEN RW_TAC list_ss [] THEN
159 `d<>0` by METIS_TAC [IS_SOME_IINTREE] THEN
160 Q.PAT_ASSUM `IS_SOME thing` MP_TAC THEN
161 ASM_SIMP_TAC list_ss [Once iintree_def] THEN CASE_TAC THEN RW_TAC list_ss []
162
163 METIS_TAC [IS_SOME_EXISTS,NOT_SOME_NONE,SOME_11,iintree_determ]);
164
165val iintree_monotone = Q.prove
166(`!d1 d2 x list.
167    IS_SOME(iintree d1 x list) /\ d1 <= d2 ==> IS_SOME(iintree d2 x list)`,
168 RW_TAC arith_ss [LESS_EQ_EXISTS] THEN
169 Induct_on `p` THEN METIS_TAC [ADD_CLAUSES,iintree_monotone_step]);
170
171val iintree_norm = Q.prove
172(`!d x list.
173    IS_SOME(iintree d x list) ==>
174    (iintree d n = iintree (rdepth x list) x list)`,
175  METIS_TAC [iintree_determ,rdepth_thm]);
176