1open HolKernel Parse boolLib 2 3val _ = new_theory "marker"; 4 5(* ---------------------------------------------------------------------- 6 stmarker 7 8 stmarker stands for "short term marker"; use this constant to mark 9 sub-terms for a short period (within a conversion, say) and be sure 10 to remove the marker soon after use. 11 ---------------------------------------------------------------------- *) 12 13val stmarker_def = new_definition("stmarker_def", ``stmarker (x:'a) = x``); 14val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="stmarker"},name=(["Unwanted"],"id")} 15 16(* the following move_<dir>_<op> theorems will loop if more than one term 17 is marked at the same level *) 18val move_left_conj = store_thm( 19 "move_left_conj", 20 ``!p q m. (p /\ stmarker m = stmarker m /\ p) /\ 21 ((stmarker m /\ p) /\ q = stmarker m /\ (p /\ q)) /\ 22 (p /\ (stmarker m /\ q) = stmarker m /\ (p /\ q))``, 23 REWRITE_TAC [stmarker_def, CONJ_ASSOC] THEN 24 REPEAT STRIP_TAC THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN 25 MATCH_ACCEPT_TAC CONJ_COMM); 26 27val move_right_conj = store_thm( 28 "move_right_conj", 29 ``!p q m. (stmarker m /\ p = p /\ stmarker m) /\ 30 (p /\ (q /\ stmarker m) = (p /\ q) /\ stmarker m) /\ 31 ((p /\ stmarker m) /\ q = (p /\ q) /\ stmarker m)``, 32 REWRITE_TAC [stmarker_def, GSYM CONJ_ASSOC] THEN 33 REPEAT STRIP_TAC THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN 34 MATCH_ACCEPT_TAC CONJ_COMM); 35 36val move_left_disj = store_thm( 37 "move_left_disj", 38 ``!p q m. (p \/ stmarker m = stmarker m \/ p) /\ 39 ((stmarker m \/ p) \/ q = stmarker m \/ (p \/ q)) /\ 40 (p \/ (stmarker m \/ q) = stmarker m \/ (p \/ q))``, 41 REWRITE_TAC [stmarker_def, DISJ_ASSOC] THEN 42 REPEAT STRIP_TAC THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN 43 MATCH_ACCEPT_TAC DISJ_COMM); 44 45val move_right_disj = store_thm( 46 "move_right_disj", 47 ``!p q m. (stmarker m \/ p = p \/ stmarker m) /\ 48 (p \/ (q \/ stmarker m) = (p \/ q) \/ stmarker m) /\ 49 ((p \/ stmarker m) \/ q = (p \/ q) \/ stmarker m)``, 50 REWRITE_TAC [stmarker_def, GSYM DISJ_ASSOC] THEN 51 REPEAT STRIP_TAC THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN 52 MATCH_ACCEPT_TAC DISJ_COMM); 53 54(* Note, if you want to move a pair of things to the edge of a term, 55 you can move one of them, and then the second in two successive 56 passes. Something like 57 find_and_move_left THENC RAND_CONV find_and_move_left 58 will result in a term 59 t1 /\ (t2 /\ ...) 60 rewriting with CONJ_ASSOC will even give you 61 (t1 /\ t2) /\ ... 62*) 63 64(* ---------------------------------------------------------------------- 65 unint 66 67 unint stands for "uninterpreted", and can be used to mark and/or 68 breakup terms that represent "bad" situations. One can be sure 69 that unint terms will never be written away, so that they will 70 persist and act as a signal to the user that something has gone wrong. 71 72 Just make sure that unint never appears on the LHS of a rewrite rule. 73 (Idea and name taken from Joe Hurd's development of the positive reals 74 with an infinity.) 75 ---------------------------------------------------------------------- *) 76 77val unint_def = new_definition( 78 "unint_def", 79 ``unint (x:'a) = x``); 80 81(* ---------------------------------------------------------------------- 82 Abbrev 83 84 For wrapping up abbreviations in the assumption list. This tag 85 protects equalities so that they can appear in assumptions and not 86 be eliminated or unduly messed with by other tactics 87 ---------------------------------------------------------------------- *) 88 89val Abbrev_def = new_definition("Abbrev_def", ``Abbrev (x:bool) = x``) 90val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="Abbrev"},name=(["Unwanted"],"id")} 91 92 93(* ---------------------------------------------------------------------- 94 For telling the simplifier to case-split on if-then-else terms in 95 the goal. Not used as yet. 96 ---------------------------------------------------------------------- *) 97 98val IfCases_def = new_definition("IfCases_def", ``IfCases = T``) 99 100 101(*---------------------------------------------------------------------------*) 102(* Support for the simplifier *) 103(*---------------------------------------------------------------------------*) 104 105val AC_DEF = new_definition("AC_DEF", ``AC b1 b2 = b1 /\ b2``); 106val Cong_def = new_definition("Cong_def", ``Cong (x:bool) = x``); 107val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="AC"},name=(["Data","Bool"],"/\\")} 108val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="bool",Name="/\\"},name=(["Data","Bool"],"/\\")} 109val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="Cong"},name=(["Unwanted"],"id")} 110 111 112(*---------------------------------------------------------------------------*) 113(* Support for random user-supplied labels. *) 114(*---------------------------------------------------------------------------*) 115 116val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 2)), 117 fixity = Infix(NONASSOC, 80), 118 paren_style = OnlyIfNecessary, 119 pp_elements = [HardSpace 1, TOK ":-", BreakSpace(1,0)], 120 term_name = ":-"}; 121 122val _ = Parse.temp_type_abbrev ("label", ``:ind``); 123 124val label_def = new_definition( 125 "label_def", 126 ``((lab:label) :- (argument:bool)) = argument``); 127 128val _ = export_theory(); 129