--- 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)]
--- 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^" !")
--- 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