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 92val Abbrev_CONG = store_thm( 93 "Abbrev_CONG", 94 ���r1 = r2 ==> Abbrev(v = r1) = Abbrev (v = r2)���, 95 STRIP_TAC THEN ASM_REWRITE_TAC[]); 96 97 98(* ---------------------------------------------------------------------- 99 For telling the simplifier to case-split on if-then-else terms in 100 the goal. Not used as yet. 101 ---------------------------------------------------------------------- *) 102 103val IfCases_def = new_definition("IfCases_def", ``IfCases = T``) 104 105 106(*---------------------------------------------------------------------------*) 107(* Support for the simplifier *) 108(*---------------------------------------------------------------------------*) 109 110val AC_DEF = new_definition("AC_DEF", ``AC b1 b2 <=> b1 /\ b2``); 111val Req0_def = new_definition("Req0_def", ���Req0 = T���); 112val ReqD_def = new_definition("ReqD_def", ���ReqD = T���); 113val Cong_def = new_definition("Cong_def", ``Cong (x:bool) = x``); 114val Exclude_def = new_definition("Exclude_def", ���Exclude (x:'a) = T���); 115val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="AC"},name=(["Data","Bool"],"/\\")} 116val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="bool",Name="/\\"},name=(["Data","Bool"],"/\\")} 117val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="Cong"},name=(["Unwanted"],"id")} 118 119 120(*---------------------------------------------------------------------------*) 121(* Support for random user-supplied labels. *) 122(*---------------------------------------------------------------------------*) 123 124val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 2)), 125 fixity = Infix(NONASSOC, 80), 126 paren_style = OnlyIfNecessary, 127 pp_elements = [HardSpace 1, TOK ":-", BreakSpace(1,0)], 128 term_name = ":-"}; 129 130Type label[local] = ���:ind��� 131 132val label_def = new_definition( 133 "label_def", 134 ``((lab:label) :- (argument:bool)) = argument``); 135 136(* ---------------------------------------------------------------------- 137 The 'using' label 138 ---------------------------------------------------------------------- *) 139 140val using_def = new_definition("using_def", ���using (x:label) = T���); 141val usingThm_def = new_definition("usingThm_def", ���usingThm (b:bool) = b���); 142 143val _ = remove_ovl_mapping "using" {Name = "using", Thy = "marker"} 144val _ = remove_ovl_mapping "usingThm" {Name = "usingThm", Thy = "marker"} 145 146(*---------------------------------------------------------------------------*) 147(* Case *) 148(* *) 149(* For marking the current case in case divisions and inductive proofs *) 150(*---------------------------------------------------------------------------*) 151 152val Case_def = new_definition( 153 "Case_def", 154 ``Case X = T``); 155 156val add_Case = store_thm ( 157 "add_Case", 158 ``!X. P <=> (Case X ==> P)``, 159 REWRITE_TAC [Case_def]); 160 161val elim_Case = store_thm ( 162 "elim_Case", 163 ``(Case X /\ Y) = Y /\ 164 (Y /\ Case X) = Y /\ 165 (Case X ==> Y) = Y``, 166 REWRITE_TAC [Case_def] 167 ); 168 169val _ = export_theory(); 170