inftreeScript.sml

1Theory inftree[bare]
2Ancestors
3  arithmetic list
4Libs
5  HolKernel boolLib Parse BasicProvers boolSimps simpLib
6  IndDefLib metisLib BasicProvers TypeBasePure[qualified]
7
8(* ----------------------------------------------------------------------
9    establish type of (possibly infinitely) branching tree
10   ---------------------------------------------------------------------- *)
11
12val (is_tree_rules, is_tree_ind, is_tree_cases) = Hol_reln`
13  (!a. is_tree (\p. INL (a:'a))) /\
14  (!f (b:'b). (!(d:'d). is_tree (f d)) ==>
15         is_tree (\p. if p = [] then INR b
16                      else f (HD p) (TL p)))
17`
18
19val inftree = new_type_definition(
20  "inftree",
21  prove(``?x : ('d list -> 'a + 'b). is_tree x``, METIS_TAC [is_tree_rules]))
22
23val inftree_bijections = define_new_type_bijections {
24  ABS = "to_inftree", REP = "from_inftree",
25  name = "inftree_bijections", tyax = inftree
26};
27
28Theorem fromto_id[local]:
29    is_tree f ==> (from_inftree (to_inftree f) = f)
30Proof
31  METIS_TAC [inftree_bijections]
32QED
33
34Theorem is_tree_from_inftree[local]:
35    is_tree (from_inftree x)
36Proof
37  METIS_TAC [inftree_bijections]
38QED
39val _ = augment_srw_ss [rewrites [is_tree_from_inftree]]
40
41Theorem from_inftree_11[local]:
42    (from_inftree t1 = from_inftree t2) = (t1 = t2)
43Proof
44  METIS_TAC [inftree_bijections]
45QED
46
47Definition iLf_def:
48  iLf a = to_inftree (\p. INL a)
49End
50
51Definition iNd_def:
52  iNd b f = to_inftree (\p. if p = [] then INR b
53                            else from_inftree (f (HD p)) (TL p))
54End
55
56Theorem iNd_is_tree:
57    !b f. is_tree (\p. if p = [] then INR b
58                       else from_inftree (f (HD p)) (TL p))
59Proof
60  REPEAT GEN_TAC THEN
61  Q_TAC SUFF_TAC `is_tree (\p. if p = [] then INR b
62                               else (from_inftree o f) (HD p) (TL p))`
63        THEN1 SRW_TAC [][] THEN
64  MATCH_MP_TAC (#2 (CONJ_PAIR is_tree_rules)) THEN
65  SRW_TAC [][]
66QED
67
68Theorem inftree_11[simp]:
69    ((iLf a1 = iLf a2 : ('a,'b,'c) inftree) <=> (a1 = a2)) /\
70    ((iNd b1 f1 = iNd b2 f2 : ('a,'b,'c)inftree) <=> (b1 = b2) /\ (f1 = f2))
71Proof
72  SRW_TAC [][iLf_def, iNd_def] THENL [
73    SRW_TAC [][EQ_IMP_THM] THEN
74    POP_ASSUM (MP_TAC o AP_TERM ``from_inftree``) THEN
75    SIMP_TAC (srw_ss()) [fromto_id, is_tree_rules, FUN_EQ_THM],
76
77    REVERSE EQ_TAC THEN1 SRW_TAC [][] THEN
78    DISCH_THEN (MP_TAC o AP_TERM ``from_inftree``) THEN
79    SRW_TAC [][fromto_id, FUN_EQ_THM, iNd_is_tree] THENL [
80      POP_ASSUM (Q.SPEC_THEN `[]` MP_TAC) THEN SRW_TAC [][],
81      POP_ASSUM (Q.SPEC_THEN `x::t` (MP_TAC o GEN ``t:'c list``)) THEN
82      SRW_TAC [][] THEN
83      Q_TAC SUFF_TAC `from_inftree (f1 x) = from_inftree (f2 x)`
84            THEN1 SRW_TAC [][from_inftree_11] THEN
85      ASM_SIMP_TAC bool_ss [FUN_EQ_THM]
86    ]
87  ]
88QED
89
90Theorem inftree_distinct[simp]:
91    ~(iLf a = iNd b f)
92Proof
93  SRW_TAC [][iLf_def, iNd_def] THEN
94  DISCH_THEN (MP_TAC o AP_TERM ``from_inftree``) THEN
95  SRW_TAC [][fromto_id, iNd_is_tree, is_tree_rules, FUN_EQ_THM] THEN
96  Q.EXISTS_TAC `[]` THEN SRW_TAC [][]
97QED
98
99val strong_ind =
100    SIMP_RULE bool_ss [is_tree_rules]
101              (Q.SPEC `\f. is_tree f /\ P f` is_tree_ind)
102
103Theorem forall_inftree[local]:
104    (!t. P t) = (!f. is_tree f ==> P (to_inftree f))
105Proof
106  METIS_TAC [inftree_bijections]
107QED
108
109Theorem inftree_ind:
110    !P.
111       (!a. P (iLf a)) /\
112       (!b f. (!d. P (f d)) ==> P (iNd b f)) ==>
113       !t. P t
114Proof
115  SIMP_TAC (srw_ss()) [forall_inftree, iNd_def, iLf_def] THEN
116  GEN_TAC THEN STRIP_TAC THEN
117  HO_MATCH_MP_TAC strong_ind THEN CONJ_TAC THEN1 SRW_TAC [][] THEN
118  REPEAT STRIP_TAC THEN
119  FIRST_X_ASSUM (MP_TAC o SPEC ``b:'b``) THEN
120  DISCH_THEN (Q.SPEC_THEN `to_inftree o f` MP_TAC) THEN
121  SRW_TAC [][fromto_id]
122QED
123
124val (relrec_rules, relrec_ind, relrec_cases) = Hol_reln`
125  (!lf nd a. relrec lf nd (iLf a) (lf a)) /\
126  (!lf nd b df g. (!d. relrec lf nd (df d) (g d)) ==>
127                  relrec lf nd (iNd b df) (nd b g))
128`
129
130Theorem relrec_fn[local]:
131    !lf nd t r1. relrec lf nd t r1 ==> !r2. relrec lf nd t r2 ==> (r1 = r2)
132Proof
133  HO_MATCH_MP_TAC relrec_ind THEN CONJ_TAC THEN REPEAT GEN_TAC THENL [
134    ONCE_REWRITE_TAC [relrec_cases] THEN SRW_TAC [][],
135    STRIP_TAC THEN ONCE_REWRITE_TAC [relrec_cases] THEN
136    SRW_TAC [][] THEN Q_TAC SUFF_TAC `g = g'` THEN1 SRW_TAC [][] THEN
137    SRW_TAC [][FUN_EQ_THM]
138  ]
139QED
140
141Theorem relrec_total[local]:
142    !t. ?r. relrec lf nd t r
143Proof
144  HO_MATCH_MP_TAC inftree_ind THEN REPEAT STRIP_TAC THEN
145  ONCE_REWRITE_TAC [relrec_cases] THEN SRW_TAC [][] THEN
146  METIS_TAC []
147QED
148
149Definition inftree_rec_def:
150  inftree_rec lf nd t = @r. relrec lf nd t r
151End
152
153Theorem inftree_rec_thm[local]:
154    (inftree_rec lf nd (iLf a) = lf a) /\
155    (inftree_rec lf nd (iNd b d) = nd b (inftree_rec lf nd o d))
156Proof
157  SRW_TAC [][inftree_rec_def] THEN
158  ONCE_REWRITE_TAC [relrec_cases] THEN SRW_TAC [][] THEN
159  Q.SUBGOAL_THEN `inftree_rec lf nd = \t. @r. relrec lf nd t r` ASSUME_TAC
160  THENL [
161     SRW_TAC [][inftree_rec_def, FUN_EQ_THM],
162     ALL_TAC
163  ] THEN
164  SRW_TAC [][combinTheory.o_DEF] THEN POP_ASSUM (K ALL_TAC) THEN
165  Q_TAC SUFF_TAC `!g. (!d'. relrec lf nd (d d') (g d')) =
166                      (g = \x. @r. relrec lf nd (d x) r)`
167        THEN1 SRW_TAC [][] THEN
168  SRW_TAC [][FUN_EQ_THM, EQ_IMP_THM] THENL [
169    SELECT_ELIM_TAC THEN METIS_TAC [relrec_total, relrec_fn],
170    POP_ASSUM (K ALL_TAC) THEN SELECT_ELIM_TAC THEN
171    METIS_TAC [relrec_total]
172  ]
173QED
174
175Theorem inftree_Axiom0[local]:
176    !lf nd. ?f : ('a,'b,'c) inftree -> 'd.
177       (!a. f (iLf a) = lf a) /\
178       (!b d. f (iNd b d) = nd b (f o d))
179Proof
180  REPEAT GEN_TAC THEN Q.EXISTS_TAC `inftree_rec lf nd` THEN
181  SRW_TAC [][inftree_rec_thm]
182QED
183
184Theorem inftree_Axiom:
185    !lf nd. ?f : ('a,'b,'c)inftree -> 'd.
186       (!a. f (iLf a) = lf a) /\
187       (!b d. f (iNd b d) = nd b d (f o d))
188Proof
189  REPEAT GEN_TAC THEN
190  Q.SPECL_THEN [`\a. (lf a, iLf a)`,
191                 `\b f. (nd b (SND o f) (FST o f), iNd b (SND o f))`]
192               STRIP_ASSUME_TAC
193               (INST_TYPE [delta |-> ``:'d # ('a,'b,'c)inftree``]
194                          inftree_Axiom0) THEN
195  Q.EXISTS_TAC `FST o f` THEN
196  SRW_TAC [][] THEN
197  Q_TAC SUFF_TAC `SND o f o d = d` THEN1 SRW_TAC [][] THEN
198  Q_TAC SUFF_TAC `!x. SND (f x) = x` THEN1 SRW_TAC [][FUN_EQ_THM] THEN
199  HO_MATCH_MP_TAC inftree_ind THEN SRW_TAC [][FUN_EQ_THM]
200QED
201
202
203val inftree_case_def = hd (Prim_rec.define_case_constant inftree_Axiom)
204val _ = export_rewrites ["inftree_case_def"]
205
206Theorem inftree_nchotomy:
207    !t. (?a. t = iLf a) \/ (?b d. t = iNd b d)
208Proof
209  HO_MATCH_MP_TAC inftree_ind THEN SRW_TAC [][]
210QED
211
212val _ = TypeBase.export (
213  TypeBasePure.gen_datatype_info {
214    ax = inftree_Axiom,
215    ind = inftree_ind,
216    case_defs = [inftree_case_def]
217  }
218)