# HG changeset patch # User haftmann # Date 1330105561 -3600 # Node ID 4e258158be3882f145bb3c1f6b8ca71679c3d970 # Parent d2ac78ba805e7a5c2e7e9b4bcbd2117bef8fb7f4 dropped dead code diff -r d2ac78ba805e -r 4e258158be38 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Feb 24 22:58:13 2012 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Feb 24 18:46:01 2012 +0100 @@ -186,7 +186,7 @@ | map2_optional f [] [] = [] fun find_indices f xs = - map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs) + map_filter (fn (i, true) => SOME i | (_, false) => NONE) (map_index (apsnd f) xs) (* mode *) @@ -253,7 +253,7 @@ raise Fail "Invocation of all_modes_of_typ with a non-predicate type" end | all_modes_of_typ @{typ bool} = [Bool] - | all_modes_of_typ T = + | all_modes_of_typ _ = raise Fail "Invocation of all_modes_of_typ with a non-predicate type" fun all_smodes_of_typ (T as Type ("fun", _)) = @@ -394,7 +394,7 @@ fun split_modeT mode Ts = let - fun split_arg_mode (Fun _) T = ([], []) + fun split_arg_mode (Fun _) _ = ([], []) | split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = let val (i1, o1) = split_arg_mode m1 T1 @@ -481,8 +481,6 @@ fun is_intro constname t = is_intro_term constname (prop_of t) -fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT); - fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool}) | is_predT _ = false @@ -504,12 +502,6 @@ | _ => false) in check end; -fun is_funtype (Type ("fun", [_, _])) = true - | is_funtype _ = false; - -fun is_Type (Type _) = true - | is_Type _ = false - (* returns true if t is an application of an datatype constructor *) (* which then consequently would be splitted *) (* else false *) @@ -565,7 +557,7 @@ fun fold_atoms f intro s = let - val (literals, head) = Logic.strip_horn intro + val (literals, _) = Logic.strip_horn intro fun appl t s = (case t of (@{term Not} $ t') => f t' s | _ => f t s) @@ -582,13 +574,6 @@ (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') end; -fun map_premises f intro = - let - val (premises, head) = Logic.strip_horn intro - in - Logic.list_implies (map f premises, head) - end - fun map_filter_premises f intro = let val (premises, head) = Logic.strip_horn intro @@ -623,7 +608,7 @@ |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]}, @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}] -fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype.info_of_case thy name) +fun find_split_thm thy (Const (name, _)) = Option.map #split (Datatype.info_of_case thy name) | find_split_thm thy _ = NONE (* lifting term operations to theorems *) @@ -826,7 +811,7 @@ fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) | rewrite_args (arg::args) (pats, intro_t, ctxt) = (case HOLogic.strip_tupleT (fastype_of arg) of - (Ts as _ :: _ :: _) => + (_ :: _ :: _) => let fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2])) (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) @@ -868,7 +853,7 @@ fun dest_conjunct_prem th = case HOLogic.dest_Trueprop (prop_of th) of - (Const (@{const_name HOL.conj}, _) $ t $ t') => + (Const (@{const_name HOL.conj}, _) $ _ $ _) => dest_conjunct_prem (th RS @{thm conjunct1}) @ dest_conjunct_prem (th RS @{thm conjunct2}) | _ => [th] @@ -879,10 +864,9 @@ val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt val intro_t = prop_of intro' val concl = Logic.strip_imp_concl intro_t - val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) + val (_, args) = strip_comb (HOLogic.dest_Trueprop concl) val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) - val (pats', intro_t', ctxt3) = - fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) + val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) fun rewrite_pat (ct1, ct2) = (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2))) val t_insts' = map rewrite_pat t_insts @@ -947,7 +931,6 @@ val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))) val Type ("fun", [uninst_T, uninst_T']) = fastype_of f val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt - val T = TFree (tname, HOLogic.typeS) val T' = TFree (tname', HOLogic.typeS) val U = TFree (uname, HOLogic.typeS) val y = Free (yname, U) @@ -980,11 +963,6 @@ Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct | _ => Conv.all_conv ct -fun all_params_conv cv ctxt ct = - if Logic.is_all (Thm.term_of ct) - then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct - else cv ctxt ct; - (** eta contract higher-order arguments **) fun eta_contract_ho_arguments thy intro = @@ -1062,7 +1040,7 @@ val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt val T = fastype_of outp_pred val paramTs = ho_argsT_of_typ (binder_types T) - val (param_names, ctxt'') = Variable.variant_fixes + val (param_names, _) = Variable.variant_fixes (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt' val params = map2 (curry Free) param_names paramTs in @@ -1197,8 +1175,8 @@ fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B | strip_imp_prems _ = []; -fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B - | strip_imp_concl A = A : term; +fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ _ $ B) = strip_imp_concl B + | strip_imp_concl A = A; fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);