1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Feb 24 22:58:13 2012 +0100
1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Feb 24 18:46:01 2012 +0100
1.3 @@ -186,7 +186,7 @@
1.4 | map2_optional f [] [] = []
1.5
1.6 fun find_indices f xs =
1.7 - map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
1.8 + map_filter (fn (i, true) => SOME i | (_, false) => NONE) (map_index (apsnd f) xs)
1.9
1.10 (* mode *)
1.11
1.12 @@ -253,7 +253,7 @@
1.13 raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
1.14 end
1.15 | all_modes_of_typ @{typ bool} = [Bool]
1.16 - | all_modes_of_typ T =
1.17 + | all_modes_of_typ _ =
1.18 raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
1.19
1.20 fun all_smodes_of_typ (T as Type ("fun", _)) =
1.21 @@ -394,7 +394,7 @@
1.22
1.23 fun split_modeT mode Ts =
1.24 let
1.25 - fun split_arg_mode (Fun _) T = ([], [])
1.26 + fun split_arg_mode (Fun _) _ = ([], [])
1.27 | split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
1.28 let
1.29 val (i1, o1) = split_arg_mode m1 T1
1.30 @@ -481,8 +481,6 @@
1.31
1.32 fun is_intro constname t = is_intro_term constname (prop_of t)
1.33
1.34 -fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
1.35 -
1.36 fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
1.37 | is_predT _ = false
1.38
1.39 @@ -504,12 +502,6 @@
1.40 | _ => false)
1.41 in check end;
1.42
1.43 -fun is_funtype (Type ("fun", [_, _])) = true
1.44 - | is_funtype _ = false;
1.45 -
1.46 -fun is_Type (Type _) = true
1.47 - | is_Type _ = false
1.48 -
1.49 (* returns true if t is an application of an datatype constructor *)
1.50 (* which then consequently would be splitted *)
1.51 (* else false *)
1.52 @@ -565,7 +557,7 @@
1.53
1.54 fun fold_atoms f intro s =
1.55 let
1.56 - val (literals, head) = Logic.strip_horn intro
1.57 + val (literals, _) = Logic.strip_horn intro
1.58 fun appl t s = (case t of
1.59 (@{term Not} $ t') => f t' s
1.60 | _ => f t s)
1.61 @@ -582,13 +574,6 @@
1.62 (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
1.63 end;
1.64
1.65 -fun map_premises f intro =
1.66 - let
1.67 - val (premises, head) = Logic.strip_horn intro
1.68 - in
1.69 - Logic.list_implies (map f premises, head)
1.70 - end
1.71 -
1.72 fun map_filter_premises f intro =
1.73 let
1.74 val (premises, head) = Logic.strip_horn intro
1.75 @@ -623,7 +608,7 @@
1.76 |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
1.77 @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
1.78
1.79 -fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype.info_of_case thy name)
1.80 +fun find_split_thm thy (Const (name, _)) = Option.map #split (Datatype.info_of_case thy name)
1.81 | find_split_thm thy _ = NONE
1.82
1.83 (* lifting term operations to theorems *)
1.84 @@ -826,7 +811,7 @@
1.85 fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
1.86 | rewrite_args (arg::args) (pats, intro_t, ctxt) =
1.87 (case HOLogic.strip_tupleT (fastype_of arg) of
1.88 - (Ts as _ :: _ :: _) =>
1.89 + (_ :: _ :: _) =>
1.90 let
1.91 fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
1.92 (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
1.93 @@ -868,7 +853,7 @@
1.94
1.95 fun dest_conjunct_prem th =
1.96 case HOLogic.dest_Trueprop (prop_of th) of
1.97 - (Const (@{const_name HOL.conj}, _) $ t $ t') =>
1.98 + (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
1.99 dest_conjunct_prem (th RS @{thm conjunct1})
1.100 @ dest_conjunct_prem (th RS @{thm conjunct2})
1.101 | _ => [th]
1.102 @@ -879,10 +864,9 @@
1.103 val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
1.104 val intro_t = prop_of intro'
1.105 val concl = Logic.strip_imp_concl intro_t
1.106 - val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
1.107 + val (_, args) = strip_comb (HOLogic.dest_Trueprop concl)
1.108 val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
1.109 - val (pats', intro_t', ctxt3) =
1.110 - fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
1.111 + val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
1.112 fun rewrite_pat (ct1, ct2) =
1.113 (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
1.114 val t_insts' = map rewrite_pat t_insts
1.115 @@ -947,7 +931,6 @@
1.116 val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
1.117 val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
1.118 val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
1.119 - val T = TFree (tname, HOLogic.typeS)
1.120 val T' = TFree (tname', HOLogic.typeS)
1.121 val U = TFree (uname, HOLogic.typeS)
1.122 val y = Free (yname, U)
1.123 @@ -980,11 +963,6 @@
1.124 Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
1.125 | _ => Conv.all_conv ct
1.126
1.127 -fun all_params_conv cv ctxt ct =
1.128 - if Logic.is_all (Thm.term_of ct)
1.129 - then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct
1.130 - else cv ctxt ct;
1.131 -
1.132 (** eta contract higher-order arguments **)
1.133
1.134 fun eta_contract_ho_arguments thy intro =
1.135 @@ -1062,7 +1040,7 @@
1.136 val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
1.137 val T = fastype_of outp_pred
1.138 val paramTs = ho_argsT_of_typ (binder_types T)
1.139 - val (param_names, ctxt'') = Variable.variant_fixes
1.140 + val (param_names, _) = Variable.variant_fixes
1.141 (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
1.142 val params = map2 (curry Free) param_names paramTs
1.143 in
1.144 @@ -1197,8 +1175,8 @@
1.145 fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
1.146 | strip_imp_prems _ = [];
1.147
1.148 -fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
1.149 - | strip_imp_concl A = A : term;
1.150 +fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ _ $ B) = strip_imp_concl B
1.151 + | strip_imp_concl A = A;
1.152
1.153 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
1.154