1structure ramanaLib = 2struct 3 4open HolKernel boolLib bossLib Parse lcsymtacs pairLib 5 6val ERR = mk_HOL_ERR "ramanaLib" 7 8fun store_term_thm (s,t) = 9 store_thm(s,mk_comb(inst[``:'a``|->type_of t]``K:bool-> 'a -> bool T``,t),SIMP_TAC std_ss []) 10 11fun store_type_thm (s,t) = 12 store_thm(s,inst[``:'a``|->t]``K T (x:'a)``,SIMP_TAC std_ss []) 13 14fun SIMP_TERM ss thms t = (* use ASSUME to get a theorem to simplify instead? *) 15 t |> SIMP_CONV ss thms |> concl |> rhs 16 handle UNCHANGED => t 17val simp_term = SIMP_TERM 18 19fun TermWithCase q = let 20 val a = Absyn q 21 open Preterm errormonad 22 val M = absyn_to_preterm a >- (fn ptm0 => 23 typecheck_phase1 NONE ptm0 >> 24 overloading_resolution ptm0 >- (fn (ptm, b) => 25 report_ovl_ambiguity b >> 26 to_term ptm)) 27in 28 smash M Pretype.Env.empty 29end 30 31fun RWstore_thm (s,q,t) = Q.store_thm(s,q,t) before export_rewrites [s] 32fun RWsave_thm (s,t) = save_thm(s,t) before export_rewrites [s] 33fun RWDefine q = 34 case q |> Absyn |> Defn.parse_absyn of 35 (_,[name]) => Define q before export_rewrites[name^"_def"] 36 | _ => raise ERR "RWDefine" "Multiple definitions" 37fun RWnew_specification (s,l,t) = new_specification (s,l,t) before export_rewrites [s] 38fun RWtDefine s q t = tDefine s q t before export_rewrites [s^"_def"] 39 40val CONJ1_TAC = conj_asm1_tac 41val conj1_tac = CONJ1_TAC 42val CONJ2_TAC = conj_asm2_tac 43val conj2_tac = CONJ2_TAC 44 45fun SPEC_ALL_TAC except (g as (asl,t)) = let 46val fvs = free_vars t in 47(MAP_EVERY ID_SPEC_TAC 48 (filter 49 (not o (C mem (map (parse_in_context fvs) except))) 50 fvs)) 51end g 52val spec_all_tac = SPEC_ALL_TAC 53 54local open pred_setTheory in 55fun SetCases_on q (asl,w) = 56let val t = parse_in_context(free_varsl(w::asl)) q in 57if is_var t then 58 FULL_STRUCT_CASES_TAC (ISPEC t SET_CASES) 59 else 60 STRIP_ASSUME_TAC (ISPEC t SET_CASES) 61 end (asl,w) 62end 63 64fun Define_sbag rs emptyq replaceq = let 65 fun [QUOTE s1] + [QUOTE s2] = [QUOTE (s1^s2)] 66 val rq = [QUOTE rs] 67 val rdef = Define (rq+` = <|empty := `+emptyq+`; replace := `+replaceq+`|>`) 68in 69 RWstore_thm(rs^"_empty",rq+`.empty = `+emptyq, SRW_TAC [][rdef]); 70 RWstore_thm(rs^"_replace",rq+`.replace = `+replaceq, SRW_TAC [][rdef]); 71 rdef 72end 73 74end 75