src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 39657 5e57675b7e40
parent 39541 6605c1e87c7f
child 39658 b3644e40f661
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 23 14:50:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 23 17:22:44 2010 +0200
     1.3 @@ -142,8 +142,11 @@
     1.4    val default_options : options
     1.5    val bool_options : string list
     1.6    val print_step : options -> string -> unit
     1.7 +  (* conversions *)
     1.8 +  val imp_prems_conv : conv -> conv
     1.9    (* simple transformations *)
    1.10    val expand_tuples : theory -> thm -> thm
    1.11 +  val expand_tuples_elim : Proof.context -> thm -> thm
    1.12    val eta_contract_ho_arguments : theory -> thm -> thm
    1.13    val remove_equalities : theory -> thm -> thm
    1.14    val remove_pointless_clauses : thm -> thm list
    1.15 @@ -789,35 +792,38 @@
    1.16  
    1.17  (** tuple processing **)
    1.18  
    1.19 +fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
    1.20 +  | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
    1.21 +    (case HOLogic.strip_tupleT (fastype_of arg) of
    1.22 +      (Ts as _ :: _ :: _) =>
    1.23 +      let
    1.24 +        fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
    1.25 +          (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
    1.26 +          | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
    1.27 +            let
    1.28 +              val thy = ProofContext.theory_of ctxt
    1.29 +              val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
    1.30 +              val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
    1.31 +              val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
    1.32 +              val args' = map (Pattern.rewrite_term thy [pat] []) args
    1.33 +            in
    1.34 +              rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
    1.35 +            end
    1.36 +          | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
    1.37 +        val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
    1.38 +          (args, (pats, intro_t, ctxt))
    1.39 +      in
    1.40 +        rewrite_args args' (pats, intro_t', ctxt')
    1.41 +      end
    1.42 +  | _ => rewrite_args args (pats, intro_t, ctxt))
    1.43 +
    1.44 +fun rewrite_prem atom =
    1.45 +  let
    1.46 +    val (_, args) = strip_comb atom
    1.47 +  in rewrite_args args end
    1.48 +
    1.49  fun expand_tuples thy intro =
    1.50    let
    1.51 -    fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
    1.52 -      | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
    1.53 -      (case HOLogic.strip_tupleT (fastype_of arg) of
    1.54 -        (Ts as _ :: _ :: _) =>
    1.55 -        let
    1.56 -          fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
    1.57 -            (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
    1.58 -            | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
    1.59 -              let
    1.60 -                val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
    1.61 -                val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
    1.62 -                val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
    1.63 -                val args' = map (Pattern.rewrite_term thy [pat] []) args
    1.64 -              in
    1.65 -                rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
    1.66 -              end
    1.67 -            | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
    1.68 -          val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
    1.69 -            (args, (pats, intro_t, ctxt))
    1.70 -        in
    1.71 -          rewrite_args args' (pats, intro_t', ctxt')
    1.72 -        end
    1.73 -      | _ => rewrite_args args (pats, intro_t, ctxt))
    1.74 -    fun rewrite_prem atom =
    1.75 -      let
    1.76 -        val (_, args) = strip_comb atom
    1.77 -      in rewrite_args args end
    1.78      val ctxt = ProofContext.init_global thy
    1.79      val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
    1.80      val intro_t = prop_of intro'
    1.81 @@ -842,6 +848,68 @@
    1.82      intro'''''
    1.83    end
    1.84  
    1.85 +(*** conversions ***)
    1.86 +
    1.87 +fun imp_prems_conv cv ct =
    1.88 +  case Thm.term_of ct of
    1.89 +    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
    1.90 +  | _ => Conv.all_conv ct
    1.91 +
    1.92 +fun all_params_conv cv ctxt ct =
    1.93 +  if Logic.is_all (Thm.term_of ct)
    1.94 +  then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct
    1.95 +  else cv ctxt ct;
    1.96 +  
    1.97 +fun expand_tuples_elim ctxt elimrule =
    1.98 +  let
    1.99 +    val thy = ProofContext.theory_of ctxt
   1.100 +    val ((_, [elimrule]), ctxt1) = Variable.import false [elimrule] ctxt
   1.101 +    val prems = Thm.prems_of elimrule
   1.102 +    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
   1.103 +    fun preprocess_case t =
   1.104 +      let
   1.105 +        val (param_names, param_Ts)  = split_list (Logic.strip_params t)
   1.106 +        val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t)
   1.107 +        val (free_names, ctxt2) = Variable.variant_fixes param_names ctxt1
   1.108 +        val frees = map Free (free_names ~~ param_Ts)
   1.109 +        val prop' = subst_bounds (rev frees, prop)
   1.110 +        val (eqs, prems) = chop nargs (Logic.strip_imp_prems prop')
   1.111 +        val rhss = map (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs
   1.112 +        val (pats, prop'', ctxt2) = fold 
   1.113 +          rewrite_prem (map HOLogic.dest_Trueprop prems)
   1.114 +            (rewrite_args rhss ([], prop', ctxt2)) 
   1.115 +        val new_frees = fold Term.add_frees (frees @ map snd pats) [] (* FIXME: frees are not minimal and not ordered *)
   1.116 +      in
   1.117 +        fold Logic.all (map Free new_frees) prop''
   1.118 +      end
   1.119 +    val cases' = map preprocess_case (tl prems)
   1.120 +    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
   1.121 +    val tac = (fn _ => Skip_Proof.cheat_tac thy)
   1.122 +    val eq = Goal.prove ctxt1 [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
   1.123 +    val exported_elimrule' = Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt1 ctxt)
   1.124 +    val elimrule'' = Conv.fconv_rule (imp_prems_conv (all_params_conv (fn ctxt => Conv.concl_conv nargs 
   1.125 +      (Simplifier.full_rewrite
   1.126 +        (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]))) ctxt1)) 
   1.127 +      exported_elimrule'
   1.128 +    (* splitting conjunctions introduced by Pair_eq*)
   1.129 +    fun split_conj prem =
   1.130 +      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
   1.131 +    fun map_cases f t =
   1.132 +      let
   1.133 +        val (prems, concl) = Logic.strip_horn t
   1.134 +        val ([pred], prems') = chop 1 prems
   1.135 +        fun map_params f t =
   1.136 +          let
   1.137 +            val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t)
   1.138 +          in Term.list_all (Logic.strip_params t, f prop) end 
   1.139 +        val prems'' = map (map_params f) prems'
   1.140 +      in
   1.141 +        Logic.list_implies (pred :: prems'', concl)
   1.142 +      end
   1.143 +    val elimrule''' = map_term thy (map_cases (maps_premises split_conj)) elimrule''
   1.144 +   in
   1.145 +     elimrule'''
   1.146 +  end
   1.147  (** eta contract higher-order arguments **)
   1.148  
   1.149  fun eta_contract_ho_arguments thy intro =