# HG changeset patch # User wenzelm # Date 1326451828 -3600 # Node ID afdc69f5156edce7230f13cf3a6afaf436cae2b3 # Parent 4a892432e8f16b1957ef2b89379868e7750d63c4 eliminated dead code; diff -r 4a892432e8f1 -r afdc69f5156e src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Thu Jan 12 23:29:03 2012 +0100 +++ b/src/HOL/Import/proof_kernel.ML Fri Jan 13 11:50:28 2012 +0100 @@ -906,7 +906,6 @@ end val reflexivity_thm = @{thm refl} -val substitution_thm = @{thm subst} val mp_thm = @{thm mp} val imp_antisym_thm = @{thm light_imp_as} val disch_thm = @{thm impI} @@ -937,7 +936,6 @@ val abs_thm = @{thm ext} val trans_thm = @{thm trans} val symmetry_thm = @{thm sym} -val transitivity_thm = @{thm trans} val eqmp_thm = @{thm iffD1} val eqimp_thm = @{thm HOL4Setup.eq_imp} val comb_thm = @{thm cong} @@ -1003,41 +1001,16 @@ th |> forall_intr_list dom |> forall_elim_list rng -val collect_vars = - let - fun F vars (Bound _) = vars - | F vars (tm as Free _) = - if member (op =) vars tm - then vars - else (tm::vars) - | F vars (Const _) = vars - | F vars (tm1 $ tm2) = F (F vars tm1) tm2 - | F vars (Abs(_,_,body)) = F vars body - | F vars (Var _) = raise ERR "collect_vars" "Schematic variable found" - in - F [] - end - (* Code for disambiguating variablenames (wrt. types) *) val disamb_info_empty = {vars=[],rens=[]} fun rens_of {vars,rens} = rens -fun name_of_var (Free(vname,_)) = vname - | name_of_var _ = raise ERR "name_of_var" "Not a variable" - fun disamb_term_from info tm = (info, tm) -fun swap (x,y) = (y,x) - fun has_ren (HOLThm _) = false -fun prinfo {vars,rens} = (writeln "Vars:"; - app prin vars; - writeln "Renaming:"; - app (fn(x,y)=>(prin x; writeln " -->"; prin y)) rens) - fun disamb_thm_from info (HOLThm (_,thm)) = (info, thm) fun disamb_terms_from info tms = (info, tms) @@ -1045,11 +1018,10 @@ fun disamb_thms_from info hthms = (info, map hthm2thm hthms) fun disamb_term tm = disamb_term_from disamb_info_empty tm -fun disamb_terms tms = disamb_terms_from disamb_info_empty tms fun disamb_thm thm = disamb_thm_from disamb_info_empty thm fun disamb_thms thms = disamb_thms_from disamb_info_empty thms -fun norm_hthm sg (hth as HOLThm _) = hth +fun norm_hthm thy (hth as HOLThm _) = hth (* End of disambiguating code *) @@ -1073,7 +1045,7 @@ end val new_name = new_name' "a" fun replace_name n' (Free (n, t)) = Free (n', t) - | replace_name n' _ = ERR "replace_name" + | replace_name _ _ = ERR "replace_name" (* map: old or fresh name -> old free, invmap: old free which has fresh name assigned to it -> fresh name *) fun dis v (mapping as (map,invmap)) = @@ -1110,8 +1082,6 @@ fun if_debug f x = if !debug then f x else () val message = if_debug writeln -val conjE_helper = Thm.permute_prems 0 1 conjE - fun get_hol4_thm thyname thmname thy = case get_hol4_theorem thyname thmname thy of SOME hth => SOME (HOLThm hth) @@ -1131,25 +1101,6 @@ then I else insert (op =) c | _ => I) t []; -fun match_consts t (* th *) = - let - fun add_consts (Const (c, _), cs) = - (case c of - @{const_name HOL.eq} => insert (op =) "==" cs - | @{const_name HOL.implies} => insert (op =) "==>" cs - | @{const_name All} => cs - | "all" => cs - | @{const_name HOL.conj} => cs - | @{const_name Trueprop} => cs - | _ => insert (op =) c cs) - | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) - | add_consts (Abs (_, _, t), cs) = add_consts (t, cs) - | add_consts (_, cs) = cs - val t_consts = add_consts(t,[]) - in - fn th => eq_set (op =) (t_consts, add_consts (prop_of th, [])) - end - fun split_name str = let val sub = Substring.full str @@ -1755,7 +1706,7 @@ | inst_type ty1 ty2 (ty as TFree _) = if ty1 = ty then ty2 else ty - | inst_type ty1 ty2 (ty as Type(name,tys)) = + | inst_type ty1 ty2 (Type(name,tys)) = Type(name,map (inst_type ty1 ty2) tys) in fold_rev (fn v => fn th => @@ -1819,7 +1770,6 @@ val _ = if_debug pth hth val (info,th) = disamb_thm hth val (info',tm') = disamb_term_from info tm - val prems = prems_of th val th1 = beta_eta_thm th val th2 = implies_elim_all th1 val th3 = Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2 @@ -2004,7 +1954,6 @@ val tfrees = Misc_Legacy.term_tfrees c val tnames = map fst tfrees val tsyn = mk_syn thy tycname - val typ = (tycname,tnames,tsyn) val ((_, typedef_info), thy') = Typedef.add_typedef_global false (SOME (Binding.name thmname)) (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy @@ -2077,15 +2026,12 @@ val tfrees = Misc_Legacy.term_tfrees c val tnames = sort_strings (map fst tfrees) val tsyn = mk_syn thy tycname - val typ = (tycname,tnames,tsyn) val ((_, typedef_info), thy') = Typedef.add_typedef_global false NONE (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy val fulltyname = Sign.intern_type thy' tycname val aty = Type (fulltyname, map mk_vartype tnames) - val abs_ty = tT --> aty - val rep_ty = aty --> tT val typedef_hol2hollight' = Drule.instantiate' [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] diff -r 4a892432e8f1 -r afdc69f5156e src/HOL/Import/replay.ML --- a/src/HOL/Import/replay.ML Thu Jan 12 23:29:03 2012 +0100 +++ b/src/HOL/Import/replay.ML Fri Jan 13 11:50:28 2012 +0100 @@ -229,7 +229,7 @@ then let val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...") - val (f_opt,prf) = import_proof thyname' thmname thy' + val (_, prf) = import_proof thyname' thmname thy' val prf = prf thy' val (thy',th) = replay_proof int_thms thyname' thmname prf thy' val _ = writeln ("Successfully finished replaying "^thmname^" !") diff -r 4a892432e8f1 -r afdc69f5156e src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Thu Jan 12 23:29:03 2012 +0100 +++ b/src/HOL/Import/shuffler.ML Fri Jan 13 11:50:28 2012 +0100 @@ -37,20 +37,6 @@ val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context; -fun mk_meta_eq th = - (case concl_of th of - Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th RS eq_reflection - | Const("==",_) $ _ $ _ => th - | _ => raise THM("Not an equality",0,[th])) - handle _ => raise THM("Couldn't make meta equality",0,[th]) (* FIXME avoid handle _ *) - -fun mk_obj_eq th = - (case concl_of th of - Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th - | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq - | _ => raise THM("Not an equality",0,[th])) - handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *) - structure ShuffleData = Theory_Data ( type T = thm list @@ -102,33 +88,6 @@ Thm.equal_intr th1 th2 |> Drule.export_without_context end -val def_norm = - let - val cert = cterm_of Pure.thy - val aT = TFree("'a",[]) - val bT = TFree("'b",[]) - val v = Free("v",aT) - val P = Free("P",aT-->bT) - val Q = Free("Q",aT-->bT) - val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0))) - val cPQ = cert (Logic.mk_equals(P,Q)) - val cv = cert v - val rew = Thm.assume cvPQ - |> Thm.forall_elim cv - |> Thm.abstract_rule "v" cv - val (lhs,rhs) = Logic.dest_equals(concl_of rew) - val th1 = Thm.transitive (Thm.transitive - (Thm.eta_conversion (cert lhs) |> Thm.symmetric) - rew) - (Thm.eta_conversion (cert rhs)) - |> Thm.implies_intr cvPQ - val th2 = Thm.combination (Thm.assume cPQ) (Thm.reflexive cv) - |> Thm.forall_intr cv - |> Thm.implies_intr cPQ - in - Thm.equal_intr th1 th2 |> Drule.export_without_context - end - val all_comm = let val cert = cterm_of Pure.thy @@ -201,7 +160,7 @@ all_comm RS init end -fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) = +fun quant_rewrite thy _ (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) = let val res = (find_bound 0 body;2) handle RESULT i => i in @@ -270,7 +229,7 @@ end | eta_redex _ = false -fun eta_contract thy assumes origt = +fun eta_contract thy _ origt = let val (typet,Tinst) = freeze_thaw_term origt val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet)) @@ -293,7 +252,7 @@ end in case t of - Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) => + Const("all",_) $ (Abs(x,xT,Const("==",_) $ P $ Q)) => (if eta_redex P andalso eta_redex Q then let @@ -314,7 +273,6 @@ |> Thm.implies_intr cu val rew_th = Thm.equal_intr (th' |> Thm.implies_intr ct) uth' val res = final rew_th - val lhs = (#1 (Logic.dest_equals (prop_of res))) in SOME res end @@ -322,17 +280,7 @@ | _ => NONE end -fun beta_fun thy assume t = - SOME (Thm.beta_conversion true (cterm_of thy t)) - -val meta_sym_rew = @{thm refl} - -fun equals_fun thy assume t = - case t of - Const("op ==",_) $ u $ v => if Term_Ord.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE - | _ => NONE - -fun eta_expand thy assumes origt = +fun eta_expand thy _ origt = let val (typet,Tinst) = freeze_thaw_term origt val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet)) @@ -400,17 +348,6 @@ val S = mk_free "S" xT val S' = mk_free "S'" xT in -fun beta_simproc thy = Simplifier.simproc_global_i - thy - "Beta-contraction" - [Abs("x",xT,Q) $ S] - beta_fun - -fun equals_simproc thy = Simplifier.simproc_global_i - thy - "Ordered rewriting of meta equalities" - [Const("op ==",xT) $ S $ S'] - equals_fun fun quant_simproc thy = Simplifier.simproc_global_i thy @@ -564,7 +501,6 @@ val rew_th = norm_term thy closed_t val rhs = Thm.rhs_of rew_th - val shuffles = ShuffleData.get thy fun process [] = NONE | process ((name,th)::thms) = let