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