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