1(* file inttoScript.sml, split off from totoScript 12/13/13 to be the *) 2(* only theory that loads intLib. *) 3 4(* app load ["totoTheory", "intLib"]; *) 5 6open HolKernel boolLib Parse; 7 8val _ = set_trace "Unicode" 0; 9open pred_setLib pred_setTheory relationTheory pairTheory; 10open bossLib PairRules arithmeticTheory numeralTheory Defn; 11open totoTheory intLib; 12 13val _ = new_theory "intto"; 14val _ = ParseExtras.temp_loose_equality() 15 16(* My habitual abbreviations: *) 17 18val AR = ASM_REWRITE_TAC []; 19fun ulist x = [x]; 20 21val _ = intLib.deprecate_int (); 22 23val _ = Defn.def_suffix := ""; (* replacing default "_def" *) 24 25(* ***************************************************************** *) 26(* Following switch, BigSig, allows "maybe_thm" to act either as *) 27(* store_thm or as prove, thus maximizing or minimizing the output *) 28(* from print_theory and the stuff known to DB.match, DB.find *) 29(* ***************************************************************** *) 30 31val BigSig = false; 32 33fun maybe_thm (s, tm, tac) = if BigSig then store_thm (s, tm, tac) 34 else prove (tm, tac); 35 36(* **************************************************************** *) 37(* Theorems to support intto_CONV, for comparing at type int. *) 38(* **************************************************************** *) 39 40(* integer parsing remains deprecated; note use of suffix i below. *) 41 42(* An integer ground term is, as well as I can see, either a application of 43 ``$&`` to a num ground term (which is either ``0`` or an application 44 of NUMERAL to a pile of ZERO, BIT0, and BIT1) or an application of 45 numeric_negate:int -> int to such a &-application. ``-0`` is possible. *) 46 47val intOrd = Define`intOrd = TO_of_LinearOrder ($< :int reln)`; 48 49val StrongLinearOrder_int_lt = maybe_thm ("StrongLinearOrder_int_lt", 50``StrongLinearOrder ($< :int reln)``, 51SRW_TAC [][StrongLinearOrder, 52 StrongOrder_ALT, trichotomous, Order, irreflexive_def, transitive_def] THENL 53[IMP_RES_TAC integerTheory.INT_LT_TRANS 54,STRIP_ASSUME_TAC (SPECL [``a:int``, ``b:int``] integerTheory.INT_LT_TOTAL) 55 THEN AR]); 56 57val TO_intOrd = maybe_thm ("TO_intOrd", ``TotOrd intOrd``, 58REWRITE_TAC [intOrd] THEN MATCH_MP_TAC TotOrd_TO_of_Strong THEN 59ACCEPT_TAC StrongLinearOrder_int_lt); 60 61val intto = Define`intto = TO intOrd`; 62 63val apintto_thm = store_thm ("apintto_thm", ``apto intto = intOrd``, 64REWRITE_TAC [intto, GSYM TO_apto_TO_ID, TO_intOrd]); 65 66val pos_pos_thm = store_thm ("pos_pos_thm", 67``!m:num n:num. intOrd (&m) (&n) = numOrd m n``, 68 SRW_TAC [] [TO_of_LinearOrder, intOrd, numOrd]); 69 70val neg_neg_thm = store_thm ("neg_neg_thm", 71``!m:num n:num. intOrd (numeric_negate (&m)) (numeric_negate (&n)) = 72 numOrd n m``, 73 SRW_TAC [] [TO_of_LinearOrder, intOrd, numOrd]); 74 75val BIT1_nz = store_thm ("BIT1_nz", 76``!n. BIT1 n <> 0``, 77SRW_TAC [] [arithmeticTheory.NOT_ZERO_LT_ZERO, numeralTheory.numeral_lt, 78 GSYM arithmeticTheory.ALT_ZERO]); 79 80val BIT2_nz = store_thm ("BIT2_nz", 81``!n. BIT2 n <> 0``, 82SRW_TAC [] [arithmeticTheory.NOT_ZERO_LT_ZERO, numeralTheory.numeral_lt, 83 GSYM arithmeticTheory.ALT_ZERO]); 84 85val neg_lt_BIT1_thm = store_thm ("neg_lt_BIT1_thm", 86``!m:num n:num. intOrd (numeric_negate (&m)) (& (BIT1 n)) = LESS``, 87SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]); 88 89val neg_lt_BIT2_thm = store_thm ("neg_lt_BIT2_thm", 90``!m:num n:num. intOrd (numeric_negate (&m)) (& (BIT2 n)) = LESS``, 91SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]); 92 93val neg_BIT1_lt_thm = store_thm ("neg_BIT1_lt_thm", 94``!m:num n:num. intOrd (numeric_negate (& (BIT1 m))) (& n) = LESS``, 95SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]); 96 97val neg_BIT2_lt_thm = store_thm ("neg_BIT2_lt_thm", 98``!m:num n:num. intOrd (numeric_negate (& (BIT2 m))) (& n) = LESS``, 99SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]); 100 101val neg_ZERO_eq_ZERO_thm = store_thm ("neg_ZERO_eq_ZERO_thm", 102``intOrd (numeric_negate (& ZERO)) (& ZERO) = EQUAL``, 103SRW_TAC [] [TO_of_LinearOrder, intOrd, GSYM arithmeticTheory.ALT_ZERO]); 104 105val BIT1_gt_neg_thm = store_thm ("BIT1_gt_neg_thm", 106``!m:num n:num. intOrd (& (BIT1 m)) (numeric_negate (&n)) = GREATER``, 107SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]); 108 109val BIT2_gt_neg_thm = store_thm ("BIT2_gt_neg_thm", 110``!m:num n:num. intOrd (& (BIT2 m)) (numeric_negate (&n)) = GREATER``, 111SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]); 112 113val gt_neg_BIT1_thm = store_thm ("gt_neg_BIT1_thm", 114``!m:num n:num. intOrd (& m) (numeric_negate (& (BIT1 n))) = GREATER``, 115SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]); 116 117val gt_neg_BIT2_thm = store_thm ("gt_neg_BIT2_thm", 118``!m:num n:num. intOrd (& m) (numeric_negate (& (BIT2 n))) = GREATER``, 119SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]); 120 121val ZERO_eq_neg_ZERO_thm = store_thm ("ZERO_eq_neg_ZERO_thm", 122``intOrd (& ZERO) (numeric_negate (& ZERO)) = EQUAL``, 123SRW_TAC [] [TO_of_LinearOrder, intOrd, GSYM arithmeticTheory.ALT_ZERO]); 124 125val _ = export_theory (); 126