src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 46662 4e258158be38
parent 46638 fc315796794e
child 48221 e0ed7fab0d09
     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