-
Notifications
You must be signed in to change notification settings - Fork 1
/
reflectionLib.sml
2634 lines (2440 loc) · 93.6 KB
/
reflectionLib.sml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
structure reflectionLib :> reflectionLib = struct
open preamble listSimps stringSimps listLib optionLib pairLib
open numSyntax pairSyntax stringSyntax listSyntax holSyntaxSyntax
open setSpecTheory holSyntaxTheory holSyntaxExtraTheory holSemanticsTheory holSemanticsExtraTheory
open holBoolTheory holConstrainedExtensionTheory
open reflectionTheory basicReflectionLib
open holSyntaxLib holSyntaxLibTheory
local open finite_mapSyntax in end
(* TODO: miscLib.prove_hyps_by is wrong: it needs to call PROVE_HYP multiple times *)
val ERR = mk_HOL_ERR"reflectionLib"
fun VALID_TAC_PROOF (goal,tac) = TAC_PROOF(goal, VALID tac)
val bool_to_inner_tm = ``bool_to_inner``
val fun_to_inner_tm = ``fun_to_inner``
fun to_inner_tm ty =
mk_comb (
mk_const ("to_inner0", (universe_ty --> universe_ty --> bool)
--> type_ty --> ty --> universe_ty),
mk_var ("mem", universe_ty --> universe_ty --> bool)
)
fun mk_to_inner tyin ty =
let
val newty = type_subst tyin ty
in
if ty = newty then
case type_view ty of
Tyapp(thy, "bool", []) => bool_to_inner_tm
| Tyapp(thy, "fun", [ty1,ty2]) => mk_binop fun_to_inner_tm (mk_to_inner tyin ty1, mk_to_inner tyin ty2)
| _ => mk_monop (to_inner_tm ty) (type_to_deep ty)
else
mk_to_inner [] newty
end
fun to_inner_prop vti (ty : hol_type) : term =
``wf_to_inner ^(mk_to_inner vti ty)``
fun mk_range vti (ty : hol_type) : term =
``range ^(mk_to_inner vti ty)``
datatype any_type_view =
BoolType | FunType of hol_type * hol_type | BaseType of type_view
fun base_type_view (ty : hol_type) : type_view = case type_view ty of
Tyapp(thy, "bool", []) => raise ERR"base_type_view""called on bool"
| Tyapp(thy, "fun", [ty1,ty2]) => raise ERR"base_type_view""called on funtype"
| view => view
fun any_type_view (ty : hol_type) : any_type_view = case type_view ty of
Tyapp(thy, "bool", []) => BoolType
| Tyapp(thy, "fun", [ty1,ty2]) => FunType(ty1,ty2)
| view => BaseType view
fun base_types_of_type (ty : hol_type) : hol_type list = case any_type_view ty of
BoolType => []
| BaseType v => ty::(case v of Tyvar _ => []
| Tyapp(_,_,args) =>
flatten(map base_types_of_type args))
| FunType(ty1,ty2) => base_types_of_type ty1 @ base_types_of_type ty2
fun tysig_prop tysig ty =
let
val (name,args) = dest_type ty
in
``FLOOKUP ^tysig ^(string_to_inner name) =
SOME ^(term_of_int (length args))``
end
fun base_type_assums vti (ty : hol_type) : term list =
to_inner_prop vti ty ::
(case base_type_view ty of
Tyapp(thy, name, args) => [tysig_prop tysig ty,
``tyass ^(string_to_inner name)
^(mk_list(map (mk_range vti) args,universe_ty)) =
^(mk_range vti ty)``]
| Tyvar name => [``tyval ^(string_to_inner name) = ^(mk_range vti ty)``])
fun type_assums vti : hol_type -> term list =
flatten o map (base_type_assums vti) o base_types_of_type
fun typesem_prop vti (ty : hol_type) : term =
``typesem tyass tyval ^(type_to_deep ty) = ^(mk_range vti ty)``
val good_context_is_set_theory =
good_context_def |> SPEC_ALL |> EQ_IMP_RULE |> fst |> UNDISCH |> CONJUNCT1
val good_context_is_std_type_assignment =
good_context_def |> SPEC_ALL |> EQ_IMP_RULE |> fst |> UNDISCH
|> CONJUNCTS |> last |> REWRITE_RULE[is_std_interpretation_def]
|> CONJUNCT1
val good_context = hd(hyp good_context_is_set_theory)
val is_valuation = Abs_thm |> hyp |> el 2
val tyass_fun_simp =
tyass_fun_thm |> SIMP_RULE std_ss []
val [is_set_theory_mem, is_std_type_assignment] = hyp tyass_bool_thm
fun prim_typesem_cert vti ty =
let
val goal = (is_set_theory_mem::is_std_type_assignment::(type_assums vti ty), typesem_prop vti ty)
(* set_goal goal *)
in
VALID_TAC_PROOF(goal,
rpt(
(CHANGED_TAC(REWRITE_TAC[typesem_def,listTheory.MAP,ETA_AX]))
ORELSE
(CHANGED_TAC(ASM_SIMP_TAC std_ss
[tyass_bool_thm,
tyass_fun_simp,
wf_to_inner_bool_to_inner,
wf_to_inner_fun_to_inner]))
ORELSE match_mp_tac tyass_fun_thm))
end
fun typesem_cert vti ty =
PROVE_HYP good_context_is_std_type_assignment
(PROVE_HYP good_context_is_set_theory (prim_typesem_cert vti ty))
fun types_of_term (tm : term) : hol_type list = case dest_term tm of
VAR (name,ty) => [ty]
| CONST {Name,Thy,Ty} => [Ty]
| LAMB (var,body) => type_of var :: types_of_term body
| COMB (tm1,tm2) => types_of_term tm1 @ types_of_term tm2
val base_types_of_term : term -> hol_type list =
mk_set o flatten o (map base_types_of_type) o types_of_term
fun dest_base_term (tm : term) : lambda = case dest_term tm of
LAMB (var,body) => raise ERR"dest_base_term""called on lambda"
| COMB (tm1,tm2) => raise ERR"dest_base_term""called on combination"
| view => view
val generic_type = type_of o prim_mk_const
fun complete_match_type Ty0 Ty =
let
val tyin0 = match_type Ty0 Ty
val dom = map #redex tyin0
fun f x = {redex = assert (not o C Lib.mem dom) x,
residue = x}
in
mapfilter f (type_vars Ty0) @ tyin0
end
fun type_instance c =
let
val {Name,Thy,Ty} = dest_thy_const c
val Ty0 = generic_type {Name=Name,Thy=Thy}
in
complete_match_type Ty0 Ty
end
fun cmp_to_P c x y = c (x,y) <> GREATER
fun tyvar_to_str (x : hol_type) = tyvar_to_deep (dest_vartype x)
local
fun to_pair {redex,residue} = (tyvar_to_str redex, residue)
val le = cmp_to_P (inv_img_cmp fst String.compare)
in
val const_tyargs : term -> hol_type list =
map snd o sort le o map to_pair o type_instance
end
local
val s = HOLset.singleton Term.compare
fun f (tm : term) = case dest_term tm of
VAR (name,ty) => s tm
| CONST {Name,Thy,Ty} => s tm
| LAMB (var,body) => HOLset.difference(f body, s var)
| COMB (tm1,tm2) => HOLset.union(f tm1, f tm2)
in
val set_base_terms_of_term = f
end
val base_terms_of_term = HOLset.listItems o set_base_terms_of_term
fun tmsig_prop tmsig c =
let
val {Thy,Name,Ty} = dest_thy_const c
val Ty0 = type_of(prim_mk_const{Name=Name,Thy=Thy})
in
``FLOOKUP ^tmsig ^(string_to_inner Name) = SOME ^(type_to_deep Ty0)``
end
fun base_term_assums vti (tm : term) : term list = case dest_base_term tm of
VAR (name,ty) => [``tmval (^(string_to_inner name), ^(type_to_deep ty)) =
^(mk_to_inner vti ty) ^(inst vti tm)``]
| CONST {Thy,Name,Ty} =>
[tmsig_prop tmsig tm,
``tmass ^(string_to_inner Name)
^(mk_list (map (mk_range vti)
(const_tyargs tm),
universe_ty)) =
^(mk_to_inner vti Ty) ^(inst vti tm)``]
fun type_assums_of_term vti tm =
HOLset.addList(
Term.empty_tmset,
flatten (map (base_type_assums vti) (base_types_of_term tm)))
fun term_assums vti (tm : term) : term list =
HOLset.listItems(
HOLset.addList(type_assums_of_term vti tm,
flatten (map (base_term_assums vti) (base_terms_of_term tm))))
val instance_tm = Term.inst[alpha|->universe_ty]``instance``
fun mk_instance name ty =
list_mk_comb(instance_tm,[tmsig,interpretation,name,ty,tyval])
fun instance_prop vti (tm : term) : term = case dest_term tm of
CONST {Name,Thy,Ty} =>
mk_eq(mk_instance (string_to_inner Name) (type_to_deep Ty),
mk_comb(mk_to_inner vti Ty,inst vti tm))
| _ => raise ERR"instance_prop""called on non-constant"
local
fun to_deep {redex,residue} =
let
val k = redex |> dest_vartype |> tyvar_to_deep
|> string_to_inner |> mk_Tyvar
val v = type_to_deep residue
in
mk_pair(v,k)
end
in
fun tyin_to_deep tyin =
mk_list (map to_deep tyin,mk_prod(type_ty,type_ty))
end
val good_context_tyass_bool =
foldl (uncurry PROVE_HYP) tyass_bool_thm [good_context_is_set_theory,good_context_is_std_type_assignment]
val good_context_tyass_fun_simp =
foldl (uncurry PROVE_HYP) tyass_fun_simp [good_context_is_set_theory,good_context_is_std_type_assignment]
local
val instance_thm =
instance_def |> SIMP_RULE std_ss [GSYM AND_IMP_INTRO]
val ss = std_ss ++
simpLib.std_conv_ss{
name="string_EQ_CONV",
pats=[``a:string = b``],
conv=stringLib.string_EQ_CONV}
val rws = [TYPE_SUBST_def,
listTheory.MAP,
holSyntaxLibTheory.REV_ASSOCD,
mlstringTheory.implode_def,
typesem_def,
good_context_tyass_bool,
good_context_tyass_fun_simp,
MP wf_to_inner_bool_to_inner good_context_is_set_theory,
MP wf_to_inner_fun_to_inner good_context_is_set_theory,
type_11,mlstringTheory.mlstring_11]
in
fun instance_cert vti (tm : term) : thm =
let
val goal = (good_context::(term_assums vti tm),instance_prop vti tm)
val tyin = tyin_to_deep (type_instance tm)
(* set_goal goal *)
in
VALID_TAC_PROOF(goal,
first_assum(mp_tac o MATCH_MP instance_thm) >>
disch_then(
(CONV_TAC o LAND_CONV o RATOR_CONV o REWR_CONV) o
SIMP_RULE ss rws o
SPECL [interpretation,tyin]) >>
CONV_TAC(LAND_CONV(BETA_CONV)) >>
EVAL_STRING_SORT >>
REV_FULL_SIMP_TAC ss rws)
end
end
fun termsem_prop vti tm =
mk_eq(mk_termsem (term_to_deep tm),
mk_comb(mk_to_inner vti (type_of tm),inst vti tm))
(* TODO: assume good_context here, rather than using
good_context_is_set_theory wherever the return values of
wf_to_inner_mk_to_inner appear? *)
local
val bool_th = wf_to_inner_bool_to_inner |> UNDISCH
val fun_th = wf_to_inner_fun_to_inner |> UNDISCH
in
fun wf_to_inner_mk_to_inner vti =
let
fun f ty =
case any_type_view ty of
BoolType => bool_th
| FunType(x,y) =>
let
val th1 = f x
val th2 = f y
in
MATCH_MP fun_th (CONJ th1 th2)
end
| BaseType _ => ASSUME (to_inner_prop vti ty)
in f end
end
local
val varth = type_ok_def |> CONJUNCT1 |> SIMP_RULE bool_ss []
val appth = type_ok_def |> CONJUNCT2 |> SPEC_ALL |> EQ_IMP_RULE |> snd
|> REWRITE_RULE[ETA_AX,GSYM AND_IMP_INTRO] |> GEN_ALL |> SPEC tysig
val term_ok_clauses =
holSyntaxExtraTheory.term_ok_clauses
|> C MATCH_MP
(good_context_def |> SPEC_ALL |> EQ_IMP_RULE |> fst
|> UNDISCH |> CONJUNCT2 |> CONJUNCT1)
val boolth =
term_ok_clauses |> funpow 2 CONJUNCT2 |> CONJUNCT1 |> SIMP_RULE std_ss []
val funth =
term_ok_clauses |> funpow 3 CONJUNCT2 |> CONJUNCT1
|> EQ_IMP_RULE |> snd |> SIMP_RULE std_ss []
in
fun type_ok_type_to_deep ty = case any_type_view ty of
BoolType => boolth
(* val FunType(ty1,ty2) = it *)
(* val ty = ty2 *)
| FunType(ty1,ty2) =>
MATCH_MP funth
(CONJ (type_ok_type_to_deep ty1)
(type_ok_type_to_deep ty2))
| BaseType(Tyvar name) =>
varth |> SPECL [string_to_inner (tyvar_to_deep name), tysig]
(* val BaseType(Tyapp (thy,name,args)) = it *)
| BaseType(Tyapp (thy,name,args)) =>
let
val ths = map type_ok_type_to_deep args
val argsd = mk_list(map (rand o concl) ths, type_ty)
val th = SPECL [string_to_inner name, argsd] appth
|> CONV_RULE (LAND_CONV(
SIMP_CONV (bool_ss++listSimps.LIST_ss++numSimps.ARITH_ss)
[arithmeticTheory.ADD1]))
|> UNDISCH
|> CONV_RULE (LAND_CONV(
SIMP_CONV (bool_ss++listSimps.LIST_ss) []))
|> C MP (if null ths then TRUTH else LIST_CONJ ths)
in
th
end
end
local
val get_rule =
snd o EQ_IMP_RULE o SPEC_ALL o SIMP_RULE std_ss [] o SPEC signatur
val varth = term_ok_def |> CONJUNCT1 |> get_rule |> Q.GEN`x`
|> ADD_ASSUM good_context
val constth =
term_ok_def |> CONJUNCT2 |> CONJUNCT1 |> get_rule
|> SIMP_RULE std_ss [GSYM LEFT_FORALL_IMP_THM]
|> ONCE_REWRITE_RULE[CONJ_COMM]
|> ONCE_REWRITE_RULE[GSYM CONJ_ASSOC]
|> REWRITE_RULE[GSYM AND_IMP_INTRO]
|> Q.GEN`name`
|> ADD_ASSUM good_context
val combth = term_ok_def |> funpow 2 CONJUNCT2 |> CONJUNCT1 |> get_rule
|> SIMP_RULE std_ss [WELLTYPED_CLAUSES,GSYM AND_IMP_INTRO]
val absth =
term_ok_def |> funpow 3 CONJUNCT2 |> get_rule
|> SIMP_RULE std_ss [PULL_EXISTS]
in
fun term_ok_term_to_deep tm =
case dest_term tm of
(* val VAR (x,ty) = it *)
VAR (x,ty) =>
MATCH_MP varth (type_ok_type_to_deep ty)
|> SPEC (string_to_inner x)
| CONST {Name,Thy,Ty} =>
let
val th =
constth
|> C MATCH_MP (type_ok_type_to_deep Ty)
|> SPEC (string_to_inner Name)
|> SPEC (type_to_deep (generic_type {Name=Name,Thy=Thy}))
val goal:goal = ([],th |> concl |> dest_imp |> fst)
(* set_goal goal *)
val th1 = VALID_TAC_PROOF(goal,
exists_tac (tyin_to_deep (type_instance tm)) >>
EVAL_TAC)
in
UNDISCH (MP th th1)
end
(* val COMB (f,x) = it *)
| COMB (f,x) =>
let
val th1 = term_ok_term_to_deep f
val th2 = term_ok_term_to_deep x
val th =
combth
|> C MATCH_MP th1
|> C MATCH_MP th2
|> C MATCH_MP (MATCH_MP term_ok_welltyped th1)
|> C MATCH_MP (MATCH_MP term_ok_welltyped th2)
val th1 = th |> concl |> dest_imp |> fst
|> ((QUANT_CONV((LAND_CONV EVAL) THENC
(RAND_CONV EVAL))) THENC
(SIMP_CONV (std_ss++listSimps.LIST_ss) [type_11]))
|> EQT_ELIM
in
MP th th1
end
| LAMB (x,b) =>
let
val th1 = term_ok_term_to_deep x
val th2 = term_ok_term_to_deep b
in
MATCH_MP absth
(LIST_CONJ
[REFL(rand(concl th1)),
type_ok_type_to_deep(type_of x),
th2])
end
end
fun termsem_cert_unint vti =
let
fun f tm =
let
val goal = (good_context::is_valuation::(term_assums vti tm),termsem_prop vti tm)
(* set_goal goal *)
in
case dest_term tm of
VAR _ => VALID_TAC_PROOF(goal,ASM_SIMP_TAC std_ss [termsem_def])
| CONST _ => VALID_TAC_PROOF(goal,
SIMP_TAC std_ss [termsem_def] >>
ACCEPT_TAC(instance_cert vti tm))
(* val COMB(t1,t2) = it *)
(* val tm = t1 *)
(* val tm = t2 *)
| COMB(t1,t2) =>
let
val th1 = f t1
val th2 = f t2
val (dty,rty) = dom_rng (type_of t1)
val th = MATCH_MP Comb_thm (CONJ th1 th2)
|> C MATCH_MP (wf_to_inner_mk_to_inner vti dty)
|> C MATCH_MP (wf_to_inner_mk_to_inner vti rty)
|> PROVE_HYP good_context_is_set_theory
in
VALID_TAC_PROOF(goal, ACCEPT_TAC th)
end
(* val LAMB(x,b) = it *)
(* val tm = b *)
| LAMB(x,b) =>
let
val th =
MATCH_MP Abs_thm
(CONJ (typesem_cert vti (type_of x))
(typesem_cert vti (type_of b)))
val cb = f b
in
VALID_TAC_PROOF(goal,
match_mp_tac th >>
conj_tac >- (ACCEPT_TAC (term_ok_term_to_deep b)) >>
conj_tac >- EVAL_TAC >>
gen_tac >> strip_tac >>
CONV_TAC(RAND_CONV(RAND_CONV(BETA_CONV))) >>
match_mp_tac (MP_CANON (DISCH_ALL cb)) >>
ASM_SIMP_TAC (std_ss++LIST_ss++STRING_ss)
[combinTheory.APPLY_UPDATE_THM,
mlstringTheory.mlstring_11] >>
rpt conj_tac >>
TRY (
match_mp_tac (MP_CANON (GSYM wf_to_inner_finv_right)) >>
rpt conj_tac >>
TRY(first_assum ACCEPT_TAC) >>
imp_res_tac (DISCH_ALL good_context_is_set_theory) >>
rpt (
TRY(first_assum ACCEPT_TAC) >>
TRY(MATCH_ACCEPT_TAC (UNDISCH wf_to_inner_bool_to_inner)) >>
match_mp_tac (UNDISCH wf_to_inner_fun_to_inner) >>
rpt conj_tac )) >>
match_mp_tac is_valuation_extend >>
(conj_tac >- first_assum ACCEPT_TAC) >>
imp_res_tac (DISCH_ALL good_context_tyass_bool) >>
ASM_SIMP_TAC (std_ss++LIST_ss)
[typesem_def,
MP wf_to_inner_bool_to_inner good_context_is_set_theory,
MP wf_to_inner_fun_to_inner good_context_is_set_theory,
good_context_tyass_fun_simp])
end
end
in f end
(*
val tm = ``λx. K F``
val tm = ``λx. K (λy. F) 3``
val tm = ``let x = 5 in x + y``
val tm = ``[x;y;[2]]``
val tm = ``typesem tysig tyval Bool``
val tm = mem
val tm = good_context
val tm = ``map (λf. (λ(x,y). x) = f) []``
val tm = ``ARB``
val tm =
``(λ(p :α -> β -> bool).
∃(x :α) (y :β). p = (λ(a :α) (b :β). (a = x) ∧ (b = y)))
(r :α -> β -> bool) ⇔ (REP_prod (ABS_prod r) = r)``
termsem_cert_unint tyin tm
show_assums := true
*)
type update = {
sound_update_thm : thm, (* |- sound_update ctxt upd *)
constrainable_thm : thm, (* |- constrainable_update upd *)
updates_thm : thm, (* |- upd updates ctxt *)
extends_init_thm : thm, (* |- ctxt extends init_ctxt *)
tys : hol_type list,
consts : term list,
axs : thm list }
(* TODO: stolen from ml_translatorLib.sml *)
(* packers and unpackers for thms, terms and types *)
fun pack_type ty = REFL (mk_var("ty",ty));
fun unpack_type th = th |> concl |> dest_eq |> fst |> type_of;
fun pack_term tm = REFL tm;
fun unpack_term th = th |> concl |> dest_eq |> fst;
fun pack_thm th = PURE_ONCE_REWRITE_RULE [GSYM markerTheory.Abbrev_def] th |> DISCH_ALL;
fun unpack_thm th = th |> UNDISCH_ALL |> PURE_ONCE_REWRITE_RULE [markerTheory.Abbrev_def];
fun pack_list f xs = TRUTH :: map f xs |> LIST_CONJ |> PURE_ONCE_REWRITE_RULE [GSYM markerTheory.Abbrev_def];
fun unpack_list f th = th |> PURE_ONCE_REWRITE_RULE [markerTheory.Abbrev_def] |> CONJUNCTS |> tl |> map f;
(* -- *)
(* pack and unpack context *)
fun pack_update (upd:update) =
pack_list I [pack_thm (#sound_update_thm upd),
pack_thm (#constrainable_thm upd),
pack_thm (#updates_thm upd),
pack_thm (#extends_init_thm upd),
pack_list pack_type (#tys upd),
pack_list pack_term (#consts upd),
pack_list pack_thm (#axs upd)]
fun unpack_update th =
let
val ls = unpack_list I th
in
{sound_update_thm = unpack_thm (el 1 ls),
constrainable_thm = unpack_thm (el 2 ls),
updates_thm = unpack_thm (el 3 ls),
extends_init_thm = unpack_thm (el 4 ls),
tys = unpack_list unpack_type (el 5 ls),
consts = unpack_list unpack_term (el 6 ls),
axs = unpack_list unpack_thm (el 7 ls)}
end
val pack_ctxt = pack_list pack_update
val unpack_ctxt = unpack_list unpack_update
fun find_type_instances toconstrain fromupdate =
mk_set (
foldl
(fn (ty1,acc) =>
foldl (fn (ty2,acc) =>
case total (complete_match_type ty1) ty2 of NONE => acc
| SOME s => s::acc)
acc
toconstrain)
[]
fromupdate
)
(*
val fromupdate = #consts upd
*)
fun find_const_instances consts fromupdate =
let
val consts1 = filter (fn tm => exists (same_const tm) fromupdate) consts
in
mk_set(map type_instance consts1)
end
fun tyvar_variant tvs tv =
if List.exists (equal tv) tvs
then
mk_vartype((dest_vartype tv)^"_")
|> tyvar_variant tvs
else tv
local
val distinct_tag_bool_range = prove(
``is_set_theory ^mem ⇒
!x. wf_to_inner ((to_inner x):'a -> 'U) ⇒
range ((to_inner x):'a -> 'U) ≠ range bool_to_inner``,
rw[] >>
imp_res_tac is_extensional >>
fs[extensional_def] >>
qexists_tac`to_inner x ARB` >>
qmatch_abbrev_tac`a ≠ b` >>
qsuff_tac`~b`>-metis_tac[wf_to_inner_range_thm]>>
simp[Abbr`a`,Abbr`b`,to_inner_def,range_bool_to_inner] >>
simp[tag_def]) |> UNDISCH
val distinct_tag_fun_range = prove(
``is_set_theory ^mem ⇒
!x y z.
wf_to_inner ((to_inner x):'a -> 'U) ⇒
wf_to_inner y ⇒
wf_to_inner z ⇒
range ((to_inner x):'a -> 'U) ≠ range (fun_to_inner y z)``,
rw[] >>
imp_res_tac is_extensional >>
fs[extensional_def] >>
qexists_tac`to_inner x ARB` >>
qmatch_abbrev_tac`a ≠ b` >>
qsuff_tac`~b`>-metis_tac[wf_to_inner_range_thm]>>
simp[Abbr`a`,Abbr`b`,to_inner_def,range_fun_to_inner] >>
simp[tag_def]) |> UNDISCH
val distinct_tags = prove(
``is_set_theory ^mem ⇒
!x y.
wf_to_inner ((to_inner x):'a -> 'U) ⇒
wf_to_inner ((to_inner y):'b -> 'U) ⇒
x ≠ y ⇒
range ((to_inner x):'a -> 'U) ≠
range ((to_inner y):'b -> 'U)``,
rw[] >>
imp_res_tac is_extensional >>
fs[extensional_def] >>
qexists_tac`to_inner x ARB` >>
qmatch_abbrev_tac`a ≠ b` >>
qsuff_tac`~b`>-metis_tac[wf_to_inner_range_thm]>>
simp[Abbr`a`,Abbr`b`] >>
spose_not_then strip_assume_tac >>
imp_res_tac wf_to_inner_finv_right >>
fs[to_inner_def] >>
metis_tac[tag_def,pairTheory.PAIR_EQ]) |> UNDISCH
val distinct_bool_fun = prove(
``is_set_theory ^mem ⇒
!x y.
wf_to_inner x ⇒
wf_to_inner y ⇒
range bool_to_inner ≠ range (fun_to_inner x y )``,
rw[range_bool_to_inner,range_fun_to_inner] >>
imp_res_tac is_extensional >>
fs[extensional_def] >>
pop_assum kall_tac >>
rw[mem_boolset] >>
qexists_tac`True` >> rw[] >>
spose_not_then strip_assume_tac >>
imp_res_tac in_funspace_abstract >>
fs[abstract_def,true_def] >>
imp_res_tac is_extensional >>
fs[Once extensional_def] >> rfs[mem_empty] >>
pop_assum kall_tac >>
imp_res_tac wf_to_inner_range_thm >>
rfs[mem_sub,mem_product] >>
last_x_assum(qspec_then`(x ARB,f (x ARB))`mp_tac) >>
simp[pair_inj] >>
metis_tac[is_extensional,extensional_def]) |> UNDISCH
val unequal_suff = prove(
``is_set_theory ^mem ⇒
(∀x y a. a <: x ∧ ¬(a <: y) ⇒ P x y ∧ P y x) ⇒
(∀x y. x ≠ y ⇒ P x y)``,
rw[] >>
imp_res_tac is_extensional >>
fs[extensional_def] >>
pop_assum kall_tac >>
fs[EQ_IMP_THM] >>
metis_tac[]) |> UNDISCH
val distinct_fun_fun = prove(
``is_set_theory ^mem ⇒
!d1 r1 d2 r2.
wf_to_inner d1 ∧
wf_to_inner r1 ∧
wf_to_inner d2 ∧
wf_to_inner r2 ⇒
pair$, (range d1) (range r1) ≠ (range d2, range r2) ⇒
range (fun_to_inner d1 r1) ≠ range (fun_to_inner d2 r2)``,
rw[range_fun_to_inner] >>
imp_res_tac wf_to_inner_range_thm >>
rpt(qpat_x_assum`wf_to_inner X`kall_tac) >>
rpt(first_x_assum(qspec_then`ARB`mp_tac)) >>
pop_assum mp_tac >|[
map_every qspec_tac
[(`range r2`,`w`),(`range r1`,`z`),
(`r2 ARB`,`we`),(`r1 ARB`,`ze`),
(`d2 ARB`,`ye`),(`d1 ARB`,`xe`),
(`range d2`,`y`),(`range d1`,`x`)],
map_every qspec_tac
[(`range d2`,`w`),(`range d1`,`z`),
(`d2 ARB`,`we`),(`d1 ARB`,`ze`),
(`r2 ARB`,`ye`),(`r1 ARB`,`xe`),
(`range r2`,`y`),(`range r1`,`x`)]] >>
simp[RIGHT_FORALL_IMP_THM] >>
ho_match_mp_tac unequal_suff >>
rpt gen_tac >> strip_tac >>
(reverse conj_asm1_tac >- metis_tac[]) >>
rpt strip_tac>>
imp_res_tac is_extensional >>
fs[extensional_def] >>
pop_assum kall_tac >>
pop_assum mp_tac >>
simp[EQ_IMP_THM] >|[
qexists_tac`Abstract y z (K ze)`,
qexists_tac`Abstract z y (K a)`] >>
disj1_tac >>
(conj_tac >- (
match_mp_tac (UNDISCH abstract_in_funspace) >> rw[] )) >>
simp[funspace_def,relspace_def,mem_sub] >> disj1_tac >>
simp[mem_power,abstract_def,mem_sub,mem_product,PULL_EXISTS,pair_inj] >>
metis_tac[]) |> UNDISCH
val ERR = mk_HOL_ERR"reflectionLib""ranges_distinct"
val ERR_same = ERR"same_types"
in
fun ranges_distinct vti ty1 ty2 =
case (any_type_view ty1, any_type_view ty2) of
(BoolType, BoolType) => raise ERR_same
| (BoolType, FunType (x,y)) =>
distinct_bool_fun
|> ISPECL [mk_to_inner vti x, mk_to_inner vti y]
|> C MP (wf_to_inner_mk_to_inner vti x)
|> C MP (wf_to_inner_mk_to_inner vti y)
| (FunType _, BoolType) => GSYM (ranges_distinct vti ty2 ty1)
| (BaseType _, FunType(x,y)) =>
let
val tvs = type_varsl [ty1,ty2]
val b = tyvar_variant tvs beta
val c = tyvar_variant tvs gamma
in
distinct_tag_fun_range
|> INST_TYPE[alpha|->ty1,beta|->b,gamma|->c]
|> ISPECL [type_to_deep ty1, mk_to_inner vti x, mk_to_inner vti y]
|> UNDISCH
|> C MP (wf_to_inner_mk_to_inner vti x)
|> C MP (wf_to_inner_mk_to_inner vti y)
end
| (FunType _, BaseType _) => GSYM (ranges_distinct vti ty2 ty1)
(* val (FunType (x1,y1), FunType (x2,y2)) = it *)
| (FunType (x1,y1), FunType (x2,y2)) =>
let
val tys = [x1,y1,x2,y2]
val ranges = map (mk_range vti) tys
val th1 =
pairTheory.PAIR_EQ
|> EQ_IMP_RULE |> fst
|> CONTRAPOS
|> CONV_RULE(LAND_CONV(REWR_CONV(
CONJUNCT1 (SPEC_ALL DE_MORGAN_THM))))
|> Q.GENL(rev[`x`,`y`,`a`,`b`])
|> ISPECL ranges
val th2 =
if x1 = x2 then
if y1 = y2 then raise ERR_same
else
DISJ2
(th1|>concl|>dest_imp|>fst|>dest_disj|>fst)
(ranges_distinct vti y1 y2)
else
DISJ1
(ranges_distinct vti x1 x2)
(th1|>concl|>dest_imp|>fst|>dest_disj|>snd)
in
distinct_fun_fun
|> ISPECL (map (mk_to_inner vti) tys)
|> C MP (LIST_CONJ (map (wf_to_inner_mk_to_inner vti) tys))
|> C MP (MP th1 th2)
end
| (BaseType _, BoolType) =>
distinct_tag_bool_range
|> ISPEC (type_to_deep ty1)
|> INST_TYPE[alpha|->ty1]
|> UNDISCH
| (BoolType, BaseType _) => GSYM (ranges_distinct vti ty2 ty1)
| (BaseType _, BaseType _) =>
if ty1 = ty2 then raise ERR_same
else let
val tys = map type_to_deep [ty1, ty2]
(* TODO: purpose-built conversion rather than EVAL? *)
val th = EVAL(mk_eq(el 1 tys, el 2 tys)) |> EQF_ELIM
in
distinct_tags
|> ISPECL tys
|> INST_TYPE[alpha|->ty1,beta|->ty2]
|> funpow 2 UNDISCH
|> C MP th
end
end
local
val [if_T_thm,if_F_thm] = SPEC_ALL COND_CLAUSES |> CONJUNCTS
val TEST_CONV = RATOR_CONV o RATOR_CONV o RAND_CONV
val lists_unequal_th =
listTheory.LIST_EQ_REWRITE |> SPEC_ALL
|> EQ_IMP_RULE |> fst |> CONTRAPOS
|> SIMP_RULE (std_ss++boolSimps.DNF_ss) []
|> CONJUNCT2 |> Q.GENL[`l2`,`l1`]
val EVAL_LENGTH = computeLib.CBV_CONV (listSimps.list_compset())
val EVAL_EL = EVAL_LENGTH
in
fun cs_to_inner vti tys consts =
let
fun subst_to_cs s =
let
fun const_to_inner c =
let
val ic = inst s c
in
mk_comb(mk_to_inner vti (type_of ic), ic)
end
val inner_tys = map (mk_range vti o type_subst s) tys
val inner_consts = map const_to_inner consts
in
mk_pair(mk_list(inner_tys,universe_ty),
mk_list(inner_consts,universe_ty))
end
fun subst_to_sorted_types (s:(hol_type,hol_type)subst) =
let
val by_name =
cmp_to_P (inv_img_cmp (dest_vartype o #redex) String.compare)
val sorted_subst = sort by_name s
in
map #residue sorted_subst
end
fun foldthis (s,(f,ths)) =
let
val instance_tys = subst_to_sorted_types s
val instance = mk_list(map (mk_range vti) instance_tys,universe_ty)
val result = optionSyntax.mk_some (subst_to_cs s)
val new_map = combinSyntax.mk_update (instance, result)
val new_f = mk_icomb(new_map, f)
val th =
combinTheory.APPLY_UPDATE_THM
|> ISPECL [f,instance,result,instance]
|> CONV_RULE(RAND_CONV(
TEST_CONV(REWR_CONV(EQT_INTRO(REFL instance)))
THENC REWR_CONV if_T_thm))
(* val (instance_tys0,th0)::_ = ths *)
fun update (instance_tys0,th0) =
let
val notinstance = th0 |> concl |> lhs |> rand
val typairs = zip instance_tys instance_tys0
val i = index (not o op=) typairs
val rth = uncurry (ranges_distinct vti) (List.nth(typairs,i))
val notinstanceth =
lists_unequal_th
|> ISPECL [instance,notinstance,numSyntax.term_of_int i]
|> CONV_RULE(LAND_CONV(LAND_CONV EVAL_LENGTH THENC
RAND_CONV(EVAL_EL THENC
REWR_CONV(EQT_INTRO rth))))
|> C MP (CONJ TRUTH TRUTH)
val uth0 =
combinTheory.APPLY_UPDATE_THM
|> ISPECL [f,instance,result,notinstance]
|> CONV_RULE(RAND_CONV(
TEST_CONV(REWR_CONV(EQF_INTRO notinstanceth))
THENC REWR_CONV if_F_thm))
in
(instance_tys0,TRANS uth0 th0)
end
val updated_ths = map update ths
in
(new_f,((instance_tys,th)::updated_ths))
end
in
foldl foldthis (``K NONE : 'U constraints``,
[]:(hol_type list * thm) list)
end
end
(*
val tys = [mk_list_type alpha]
val consts = [cons_tm]
val substs = [[alpha|->numSyntax.num],[alpha|->bool]]
val (s::_) = substs
val (_::s::_) = substs
val (csi, ths) = cs_to_inner tys consts substs
val (ty1,th1) = hd ths
val (ty2,th2) = hd (tl ths)
rand(lhs (concl th1))
rand(lhs (concl th2))
aconv (rator (lhs (concl th2))) csi
aconv (rator (lhs (concl th1))) csi
val (f,ths) = it
val tys = [mk_prod(alpha,beta),finite_mapSyntax.mk_fmap_ty(alpha,beta)]
val consts = [comma_tm,finite_mapSyntax.fempty_t]
val substs = [[alpha|->numSyntax.num,beta|->bool],
[alpha|->bool,beta|->beta],
[alpha|->bool,beta|->bool]]
val (csi,ths) = cs_to_inner tys consts substs
val [(ty1,th1),(ty2,th2),(ty3,th3)] = ths
th2
val true =
rand(rator(rhs(concl(EVAL ``conexts_of_upd ^inner_upd``)))) =
term_to_deep(concl(combinTheory.K_DEF))
val substs =
[[alpha|->bool,beta|->bool],
[alpha|->``:'x``,beta|->``:'y``]]
val int0 = ``hol_model select ind_to_inner``
*)
fun update_to_inner (upd:update) = #constrainable_thm upd |> concl |> rand
local
val cons_lemma = last(CONJUNCTS listTheory.LIST_REL_def) |> EQ_IMP_RULE |> fst
val betarule = CONV_RULE (RATOR_CONV BETA_CONV THENC BETA_CONV)
in
fun split_LIST_REL th =
let
val (th1,th) = CONJ_PAIR(MATCH_MP cons_lemma th)
in
betarule th1::(split_LIST_REL th)
end handle HOL_ERR _ => []
end
(*
val substs = instances_to_constrain
*)
fun make_cs_assums vti upd substs theory_ok_thm jtm =
let
val tys = #tys upd val consts = #consts upd
val updates_thm = #updates_thm upd
val (csi,tysths) = cs_to_inner vti tys consts substs
val int = ``constrain_interpretation ^(update_to_inner upd) ^csi ^jtm``
val tya = ``tyaof ^int``
val tma = ``tmaof ^int``
(* val (instances,th) = hd tysths *)
fun mapthis (_,th) =
let
val lemma = MATCH_MP tmaof_constrain_interpretation_lemma th
val alldistinct = MATCH_MP updates_upd_ALL_DISTINCT updates_thm |> CONJUNCT1
val lem2 = MATCH_MP lemma alldistinct
(* TODO: finer conversions than the EVALs below *)
val lem3 = CONV_RULE(LAND_CONV EVAL) lem2 |> C MP TRUTH
val lem4 = lem3 |> CONV_RULE(RATOR_CONV(RAND_CONV EVAL))
val lem5 = lem4 |> Q.GEN`int0` |> SPEC jtm
val tmths = split_LIST_REL lem5
(* --- *)
val lemma = MATCH_MP tyaof_constrain_interpretation_lemma th
val alldistinct = MATCH_MP updates_upd_ALL_DISTINCT updates_thm |> CONJUNCT2
val lem2 = MATCH_MP lemma alldistinct
(* TODO: finer conversions than the EVALs below *)
val lem3 = CONV_RULE(LAND_CONV EVAL) lem2 |> C MP TRUTH
val lem4 = lem3 |> CONV_RULE(RATOR_CONV(RAND_CONV EVAL))
val lem5 = lem4 |> Q.GEN`int0` |> SPEC jtm
val tyths = split_LIST_REL lem5
in
tyths@tmths
end
in
(int, flatten (map mapthis tysths), map snd tysths)
end
fun get_int th = th |> concl |> rator |> rand
local
val base_case = prove(``∀z. (IS_SOME (K NONE z) ⇔ MEM z [])``,rw[])
val step_case = prove(``∀f z k v ls.
(IS_SOME (f z) ⇔ MEM z ls) ⇒
(IS_SOME ((k =+ SOME v) f z) ⇔ MEM z (k::ls))``,
rw[combinTheory.APPLY_UPDATE_THM])
in
fun updates_equal_some_cases z cs =
INST_TYPE [beta|->optionSyntax.dest_option(type_of(rand cs))] (ISPEC z base_case) handle HOL_ERR _ =>
let
val ((k,sv),f) = combinSyntax.dest_update_comb cs
val v = optionSyntax.dest_some sv
val th = updates_equal_some_cases z f
val ls = th |> concl |> rhs |> listSyntax.dest_mem |> snd
in
MP (ISPECL [f,z,k,v,ls] step_case) th
end
end
val IS_SOME_cs_thm = prove(
``(∀vs tyvs tmvs. (cs vs = SOME (tyvs,tmvs)) ⇒ P vs tyvs tmvs) ⇔
(∀vs. IS_SOME (cs vs) ⇒ P vs (FST (THE (cs vs))) (SND (THE (cs vs))))``,
rw[IS_SOME_EXISTS,PULL_EXISTS,pairTheory.FORALL_PROD])
val inhabited_tm = ``inhabited``
val inhabited_eta = prove(``inhabited x ⇔ (λs. inhabited s) x``,rw[])
fun EVERY_range_inhabited vti tys =
join_EVERY inhabited_tm (map (
CONV_RULE(REWR_CONV(inhabited_eta))
o MATCH_MP inhabited_range o (wf_to_inner_mk_to_inner vti)) tys)
(* val inner_upd = update_to_inner upd *)
fun prove_lengths_match_thm hyps cs cs_cases cs_rws inner_upd =
let