(* * Copyright 2003 Georg Weissenbacher * Institute for Software Technology/Graz University of Technology * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation; either version 2 of the License, or * (at your option) any later version. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with this program; if not, write to the Free Software * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *)open HolKernel Parse basicHol90Lib intLib numLib realLib;val _ = new_theory "boop";val _ = bossLib.Hol_datatype `loc =     IntLoc of int  | RealLoc of real  | NumLoc of num`;val BOOP_UNREPINT_THM = bossLib.Define `    unrepInt (IntLoc i) = i`;val BOOP_UNREPREAL_THM = bossLib.Define `    unrepReal (RealLoc r) = r`;val BOOP_UNREPNUM_THM = bossLib.Define `    unrepNum (NumLoc i) = i`;val BOOP_SHIFTLEFT_THM = bossLib.Define `   (BOOP_SHIFTLEFT (v:int) 0n = v ) /\   (BOOP_SHIFTLEFT (v:int) (SUC n) = (BOOP_SHIFTLEFT (v+v) n))`;val BOOP_SHIFTRIGHT_THM = bossLib.Define `   (BOOP_SHIFTRIGHT (v:int) 0n = v ) /\   (BOOP_SHIFTRIGHT (v:int) (SUC n) = (BOOP_SHIFTRIGHT (v / 2) n))`;val BOOP_SHIFTMULDIV_THM = store_thm (    "BOOP_SHIFTMULDIV_THM",    ``!a n. BOOP_SHIFTLEFT (2 * a) n / 2 = BOOP_SHIFTLEFT a n``,    Tactical.THENL (bossLib.Induct_on `n`,        [          Tactical.THEN (REWRITE_TAC [BOOP_SHIFTLEFT_THM],            Tactical.THEN (ONCE_REWRITE_TAC [integerTheory.INT_MUL_SYM],                           simpLib.FULL_SIMP_TAC intSimps.int_ss                              [integerTheory.INT_MUL_DIV,                               integerTheory.INT_MUL_RID]                          )), 	  Tactical.THEN (REWRITE_TAC [BOOP_SHIFTLEFT_THM,                                       integerTheory.INT_DOUBLE],	                 ASM_REWRITE_TAC [])]));val BOOP_SHIFTLR_THM = store_thm (    "BOOP_SHIFTLR_THM",    ``!a n. BOOP_SHIFTRIGHT (BOOP_SHIFTLEFT a n) n = a``,    Tactical.THENL (bossLib.Induct_on `n`,        [          REWRITE_TAC [BOOP_SHIFTLEFT_THM, BOOP_SHIFTRIGHT_THM],          Tactical.THEN (REWRITE_TAC [BOOP_SHIFTLEFT_THM,                                      BOOP_SHIFTRIGHT_THM],	    Tactical.THEN (REWRITE_TAC [integerTheory.INT_DOUBLE],              Tactical.THEN (REWRITE_TAC [BOOP_SHIFTMULDIV_THM],                             ASM_REWRITE_TAC [])))]));val _ = save_thm ("BOOP_UNREPINT_THM",  BOOP_UNREPINT_THM);val _ = save_thm ("BOOP_UNREPREAL_THM",  BOOP_UNREPREAL_THM);val _ = save_thm ("BOOP_UNREPNUM_THM",  BOOP_UNREPNUM_THM);val _ = save_thm ("BOOP_SHIFTLEFT_THM",  BOOP_SHIFTLEFT_THM);val _ = save_thm ("BOOP_SHIFTRIGHT_THM",  BOOP_SHIFTRIGHT_THM);val _ = export_theory ();