1(* non-interactive mode
2*)
3structure listContext :> listContext =
4struct
5open HolKernel Parse boolLib;
6
7(* interactive mode
8if !show_assums then () else
9 (loadPath := ".."::"../../prob"::(!loadPath);
10  load "bossLib";
11  load "pred_setTheory";
12  load "millerTools";
13  load "miller_extraTheory";
14  show_assums := true);
15*)
16
17open bossLib pairTheory pred_setTheory
18     res_quanTheory extra_listTheory listTheory
19     HurdUseful ho_basicTools ho_proverTools res_quanTools
20     subtypeTools numContext;
21
22infixr 0 ++ || ORELSEC ## THENC THEN_TCL ORELSE_TCL;
23infix 1 >>;
24nonfix THEN THENL ORELSE;
25
26val op!! = op REPEAT;
27val op++ = op THEN;
28val op|| = op ORELSE;
29val op>> = op THEN1;
30
31(* --------------------------------------------------------------------- *)
32(* Subtype checking.                                                     *)
33(* --------------------------------------------------------------------- *)
34
35val list_sc =
36  map SC_SIMPLIFICATION
37  [LIST_UNIV] @
38  map SC_JUDGEMENT
39  [GTLIST0_SUBTYPE_JUDGEMENT, GTLIST1_SUBTYPE_JUDGEMENT,
40   GTLIST1_SUBSET_GTLIST0, LIST_SUBSET] @
41  map SC_SUBTYPE
42  [NIL_SUBTYPE, CONS_SUBTYPE, MAP_SUBTYPE, HD_SUBTYPE, TL_SUBTYPE,
43   LENGTH_SUBTYPE];
44
45(* --------------------------------------------------------------------- *)
46(* Contextual rewriting.                                                 *)
47(* --------------------------------------------------------------------- *)
48
49(* Rules *)
50
51(* Congruences *)
52
53(* Rewrites *)
54
55(* The module *)
56
57val list_pc = precontext_add
58  ("list",
59   map C_SUBTYPE list_sc @
60   map C_THM
61   [GTLIST0_SUBTYPE_REWRITE,
62    GTLIST1_SUBTYPE_REWRITE,
63    NOT_CONS_NIL,
64    NOT_NIL_CONS,
65    CONS_11,
66    MEM_KILL_DUPS,
67    HD,
68    TL])
69  num_pc;
70
71val list_c = precontext_compile list_pc;
72
73(* non-interactive mode
74*)
75end;
76
77
78
79