moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule
authorbulwahn
Thu Sep 23 17:22:44 2010 +0200 (2010-09-23)
changeset 396575e57675b7e40
parent 39656 f398f66969ce
child 39658 b3644e40f661
moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 23 14:50:18 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 23 17:22:44 2010 +0200
     1.3 @@ -1327,10 +1327,10 @@
     1.4  text {* The global introduction rules must be redeclared as introduction rules and then 
     1.5    one could invoke code_pred. *}
     1.6  
     1.7 -declare A.hd_predicate_in_locale.intros [unfolded Predicate.eq_is_eq[symmetric], code_pred_intro]
     1.8 +declare A.hd_predicate_in_locale.intros [code_pred_intro]
     1.9  
    1.10  code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
    1.11 -unfolding eq_is_eq by (auto elim: A.hd_predicate_in_locale.cases)
    1.12 +by (auto elim: A.hd_predicate_in_locale.cases)
    1.13      
    1.14  interpretation A partial_hd .
    1.15  thm hd_predicate_in_locale.intros
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 23 14:50:18 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 23 17:22:44 2010 +0200
     2.3 @@ -142,8 +142,11 @@
     2.4    val default_options : options
     2.5    val bool_options : string list
     2.6    val print_step : options -> string -> unit
     2.7 +  (* conversions *)
     2.8 +  val imp_prems_conv : conv -> conv
     2.9    (* simple transformations *)
    2.10    val expand_tuples : theory -> thm -> thm
    2.11 +  val expand_tuples_elim : Proof.context -> thm -> thm
    2.12    val eta_contract_ho_arguments : theory -> thm -> thm
    2.13    val remove_equalities : theory -> thm -> thm
    2.14    val remove_pointless_clauses : thm -> thm list
    2.15 @@ -789,35 +792,38 @@
    2.16  
    2.17  (** tuple processing **)
    2.18  
    2.19 +fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
    2.20 +  | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
    2.21 +    (case HOLogic.strip_tupleT (fastype_of arg) of
    2.22 +      (Ts as _ :: _ :: _) =>
    2.23 +      let
    2.24 +        fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
    2.25 +          (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
    2.26 +          | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
    2.27 +            let
    2.28 +              val thy = ProofContext.theory_of ctxt
    2.29 +              val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
    2.30 +              val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
    2.31 +              val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
    2.32 +              val args' = map (Pattern.rewrite_term thy [pat] []) args
    2.33 +            in
    2.34 +              rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
    2.35 +            end
    2.36 +          | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
    2.37 +        val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
    2.38 +          (args, (pats, intro_t, ctxt))
    2.39 +      in
    2.40 +        rewrite_args args' (pats, intro_t', ctxt')
    2.41 +      end
    2.42 +  | _ => rewrite_args args (pats, intro_t, ctxt))
    2.43 +
    2.44 +fun rewrite_prem atom =
    2.45 +  let
    2.46 +    val (_, args) = strip_comb atom
    2.47 +  in rewrite_args args end
    2.48 +
    2.49  fun expand_tuples thy intro =
    2.50    let
    2.51 -    fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
    2.52 -      | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
    2.53 -      (case HOLogic.strip_tupleT (fastype_of arg) of
    2.54 -        (Ts as _ :: _ :: _) =>
    2.55 -        let
    2.56 -          fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
    2.57 -            (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
    2.58 -            | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
    2.59 -              let
    2.60 -                val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
    2.61 -                val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
    2.62 -                val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
    2.63 -                val args' = map (Pattern.rewrite_term thy [pat] []) args
    2.64 -              in
    2.65 -                rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
    2.66 -              end
    2.67 -            | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
    2.68 -          val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
    2.69 -            (args, (pats, intro_t, ctxt))
    2.70 -        in
    2.71 -          rewrite_args args' (pats, intro_t', ctxt')
    2.72 -        end
    2.73 -      | _ => rewrite_args args (pats, intro_t, ctxt))
    2.74 -    fun rewrite_prem atom =
    2.75 -      let
    2.76 -        val (_, args) = strip_comb atom
    2.77 -      in rewrite_args args end
    2.78      val ctxt = ProofContext.init_global thy
    2.79      val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
    2.80      val intro_t = prop_of intro'
    2.81 @@ -842,6 +848,68 @@
    2.82      intro'''''
    2.83    end
    2.84  
    2.85 +(*** conversions ***)
    2.86 +
    2.87 +fun imp_prems_conv cv ct =
    2.88 +  case Thm.term_of ct of
    2.89 +    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
    2.90 +  | _ => Conv.all_conv ct
    2.91 +
    2.92 +fun all_params_conv cv ctxt ct =
    2.93 +  if Logic.is_all (Thm.term_of ct)
    2.94 +  then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct
    2.95 +  else cv ctxt ct;
    2.96 +  
    2.97 +fun expand_tuples_elim ctxt elimrule =
    2.98 +  let
    2.99 +    val thy = ProofContext.theory_of ctxt
   2.100 +    val ((_, [elimrule]), ctxt1) = Variable.import false [elimrule] ctxt
   2.101 +    val prems = Thm.prems_of elimrule
   2.102 +    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
   2.103 +    fun preprocess_case t =
   2.104 +      let
   2.105 +        val (param_names, param_Ts)  = split_list (Logic.strip_params t)
   2.106 +        val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t)
   2.107 +        val (free_names, ctxt2) = Variable.variant_fixes param_names ctxt1
   2.108 +        val frees = map Free (free_names ~~ param_Ts)
   2.109 +        val prop' = subst_bounds (rev frees, prop)
   2.110 +        val (eqs, prems) = chop nargs (Logic.strip_imp_prems prop')
   2.111 +        val rhss = map (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs
   2.112 +        val (pats, prop'', ctxt2) = fold 
   2.113 +          rewrite_prem (map HOLogic.dest_Trueprop prems)
   2.114 +            (rewrite_args rhss ([], prop', ctxt2)) 
   2.115 +        val new_frees = fold Term.add_frees (frees @ map snd pats) [] (* FIXME: frees are not minimal and not ordered *)
   2.116 +      in
   2.117 +        fold Logic.all (map Free new_frees) prop''
   2.118 +      end
   2.119 +    val cases' = map preprocess_case (tl prems)
   2.120 +    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
   2.121 +    val tac = (fn _ => Skip_Proof.cheat_tac thy)
   2.122 +    val eq = Goal.prove ctxt1 [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
   2.123 +    val exported_elimrule' = Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt1 ctxt)
   2.124 +    val elimrule'' = Conv.fconv_rule (imp_prems_conv (all_params_conv (fn ctxt => Conv.concl_conv nargs 
   2.125 +      (Simplifier.full_rewrite
   2.126 +        (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]))) ctxt1)) 
   2.127 +      exported_elimrule'
   2.128 +    (* splitting conjunctions introduced by Pair_eq*)
   2.129 +    fun split_conj prem =
   2.130 +      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
   2.131 +    fun map_cases f t =
   2.132 +      let
   2.133 +        val (prems, concl) = Logic.strip_horn t
   2.134 +        val ([pred], prems') = chop 1 prems
   2.135 +        fun map_params f t =
   2.136 +          let
   2.137 +            val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t)
   2.138 +          in Term.list_all (Logic.strip_params t, f prop) end 
   2.139 +        val prems'' = map (map_params f) prems'
   2.140 +      in
   2.141 +        Logic.list_implies (pred :: prems'', concl)
   2.142 +      end
   2.143 +    val elimrule''' = map_term thy (map_cases (maps_premises split_conj)) elimrule''
   2.144 +   in
   2.145 +     elimrule'''
   2.146 +  end
   2.147  (** eta contract higher-order arguments **)
   2.148  
   2.149  fun eta_contract_ho_arguments thy intro =
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 14:50:18 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 17:22:44 2010 +0200
     3.3 @@ -218,6 +218,7 @@
     3.4  datatype pred_data = PredData of {
     3.5    intros : (string option * thm) list,
     3.6    elim : thm option,
     3.7 +  preprocessed : bool,
     3.8    function_names : (compilation * (mode * string) list) list,
     3.9    predfun_data : (mode * predfun_data) list,
    3.10    needs_random : mode list
    3.11 @@ -225,12 +226,12 @@
    3.12  
    3.13  fun rep_pred_data (PredData data) = data;
    3.14  
    3.15 -fun mk_pred_data ((intros, elim), (function_names, (predfun_data, needs_random))) =
    3.16 -  PredData {intros = intros, elim = elim,
    3.17 +fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
    3.18 +  PredData {intros = intros, elim = elim, preprocessed = preprocessed,
    3.19      function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
    3.20  
    3.21 -fun map_pred_data f (PredData {intros, elim, function_names, predfun_data, needs_random}) =
    3.22 -  mk_pred_data (f ((intros, elim), (function_names, (predfun_data, needs_random))))
    3.23 +fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
    3.24 +  mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
    3.25  
    3.26  fun eq_option eq (NONE, NONE) = true
    3.27    | eq_option eq (SOME x, SOME y) = eq (x, y)
    3.28 @@ -613,23 +614,20 @@
    3.29  
    3.30  (** preprocessing rules **)
    3.31  
    3.32 -fun imp_prems_conv cv ct =
    3.33 -  case Thm.term_of ct of
    3.34 -    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
    3.35 -  | _ => Conv.all_conv ct
    3.36 -
    3.37  fun Trueprop_conv cv ct =
    3.38    case Thm.term_of ct of
    3.39      Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
    3.40    | _ => raise Fail "Trueprop_conv"
    3.41  
    3.42 -fun preprocess_intro thy rule =
    3.43 +fun preprocess_equality thy rule =
    3.44    Conv.fconv_rule
    3.45      (imp_prems_conv
    3.46        (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
    3.47      (Thm.transfer thy rule)
    3.48  
    3.49 -fun preprocess_elim ctxt elimrule =
    3.50 +fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
    3.51 +
    3.52 +fun preprocess_equality_elim ctxt elimrule =
    3.53    let
    3.54      fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, T) $ lhs $ rhs)) =
    3.55         HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
    3.56 @@ -640,11 +638,11 @@
    3.57      val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
    3.58      fun preprocess_case t =
    3.59        let
    3.60 -       val params = Logic.strip_params t
    3.61 -       val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
    3.62 -       val assums_hyp' = assums1 @ (map replace_eqs assums2)
    3.63 +        val params = Logic.strip_params t
    3.64 +        val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
    3.65 +        val assums_hyp' = assums1 @ (map replace_eqs assums2)
    3.66        in
    3.67 -       list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))
    3.68 +        list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))
    3.69        end
    3.70      val cases' = map preprocess_case (tl prems)
    3.71      val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
    3.72 @@ -657,6 +655,8 @@
    3.73      Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
    3.74    end;
    3.75  
    3.76 +fun preprocess_elim ctxt = expand_tuples_elim ctxt #> preprocess_equality_elim ctxt
    3.77 +  
    3.78  val no_compilation = ([], ([], []))
    3.79  
    3.80  fun fetch_pred_data ctxt name =
    3.81 @@ -668,17 +668,15 @@
    3.82              val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
    3.83            in (fst (dest_Const const) = name) end;
    3.84          val thy = ProofContext.theory_of ctxt
    3.85 -        val intros =
    3.86 -          (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result)))
    3.87 +        val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
    3.88          val index = find_index (fn s => s = name) (#names (fst info))
    3.89          val pre_elim = nth (#elims result) index
    3.90          val pred = nth (#preds result) index
    3.91 +        val elim_t = mk_casesrule ctxt pred intros
    3.92          val nparams = length (Inductive.params_of (#raw_induct result))
    3.93 -        val elim_t = mk_casesrule ctxt pred intros
    3.94 -        val elim =
    3.95 -          prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
    3.96 +        val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
    3.97        in
    3.98 -        mk_pred_data ((map (pair NONE) intros, SOME elim), no_compilation)
    3.99 +        mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
   3.100        end
   3.101    | NONE => error ("No such predicate: " ^ quote name)
   3.102  
   3.103 @@ -695,6 +693,10 @@
   3.104      val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value)
   3.105    in
   3.106      fold Term.add_const_names intros []
   3.107 +      |> (fn cs =>
   3.108 +        if member (op =) cs @{const_name "HOL.eq"} then
   3.109 +          insert (op =) @{const_name Predicate.eq} cs
   3.110 +        else cs)
   3.111        |> filter (fn c => (not (c = key)) andalso
   3.112          (is_inductive_predicate ctxt c orelse is_registered ctxt c))
   3.113    end;
   3.114 @@ -705,26 +707,24 @@
   3.115      fun cons_intro gr =
   3.116       case try (Graph.get_node gr) name of
   3.117         SOME pred_data => Graph.map_node name (map_pred_data
   3.118 -         (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))) gr
   3.119 -     | NONE => Graph.new_node (name, mk_pred_data (([(opt_case_name, thm)], NONE), no_compilation)) gr
   3.120 +         (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
   3.121 +     | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
   3.122    in PredData.map cons_intro thy end
   3.123  
   3.124  fun set_elim thm =
   3.125    let
   3.126      val (name, _) = dest_Const (fst 
   3.127        (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
   3.128 -    fun set (intros, _) = (intros, SOME thm)
   3.129 -  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
   3.130 +  in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
   3.131  
   3.132 -fun register_predicate (constname, pre_intros, pre_elim) thy =
   3.133 +fun register_predicate (constname, intros, elim) thy =
   3.134    let
   3.135 -    val intros = map (pair NONE o preprocess_intro thy) pre_intros
   3.136 -    val elim = preprocess_elim (ProofContext.init_global thy) pre_elim
   3.137 +    val named_intros = map (pair NONE) intros
   3.138    in
   3.139      if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
   3.140        PredData.map
   3.141          (Graph.new_node (constname,
   3.142 -          mk_pred_data ((intros, SOME elim), no_compilation))) thy
   3.143 +          mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy
   3.144      else thy
   3.145    end
   3.146  
   3.147 @@ -795,7 +795,7 @@
   3.148      val alt_compilations = map (apsnd fst) compilations
   3.149    in
   3.150      PredData.map (Graph.new_node
   3.151 -      (pred_name, mk_pred_data (([], SOME @{thm refl}), (dummy_function_names, ([], needs_random)))))
   3.152 +      (pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
   3.153      #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
   3.154    end
   3.155  
   3.156 @@ -2911,8 +2911,26 @@
   3.157      fun strong_conn_of gr keys =
   3.158        Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
   3.159      val scc = strong_conn_of (PredData.get thy') names
   3.160 -    
   3.161 -    val thy'' = fold_rev
   3.162 +    fun preprocess name thy =
   3.163 +      PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) =>
   3.164 +        if preprocessed then (rules, preprocessed)
   3.165 +        else
   3.166 +          let
   3.167 +            val (named_intros, SOME elim) = rules
   3.168 +            val named_intros' = map (apsnd (preprocess_intro thy)) named_intros
   3.169 +            val pred = Const (name, Sign.the_const_type thy name)
   3.170 +            val ctxt = ProofContext.init_global thy
   3.171 +            val elim_t = mk_casesrule ctxt pred (map snd named_intros')
   3.172 +            val nparams = (case try (Inductive.the_inductive ctxt) name of
   3.173 +                SOME (_, result) => length (Inductive.params_of (#raw_induct result))
   3.174 +              | NONE => 0)
   3.175 +            val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
   3.176 +          in
   3.177 +            ((named_intros', SOME elim'), true)
   3.178 +          end))))
   3.179 +        thy
   3.180 +    val thy'' = fold preprocess (flat scc) thy'
   3.181 +    val thy''' = fold_rev
   3.182        (fn preds => fn thy =>
   3.183          if not (forall (defined (ProofContext.init_global thy)) preds) then
   3.184            let
   3.185 @@ -2924,8 +2942,8 @@
   3.186              add_equations_of steps mode_analysis_options options preds thy
   3.187            end
   3.188          else thy)
   3.189 -      scc thy' |> Theory.checkpoint
   3.190 -  in thy'' end
   3.191 +      scc thy'' |> Theory.checkpoint
   3.192 +  in thy''' end
   3.193  
   3.194  val add_equations = gen_add_equations
   3.195    (Steps {