moving general functions from core_data to predicate_compile_aux
authorbulwahn
Fri Oct 22 18:38:59 2010 +0200 (2010-10-22)
changeset 40101f7fc517e21c6
parent 40100 98d74bbe8cd8
child 40102 a9e4e94b3022
moving general functions from core_data to predicate_compile_aux
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Oct 22 18:38:59 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Oct 22 18:38:59 2010 +0200
     1.3 @@ -26,11 +26,6 @@
     1.4      needs_random : mode list
     1.5    };
     1.6  
     1.7 -  (* general operations *)
     1.8 -  val unify_consts : theory -> term list -> term list -> (term list * term list)
     1.9 -  val mk_casesrule : Proof.context -> term -> thm list -> term
    1.10 -  val preprocess_intro : theory -> thm -> thm
    1.11 -
    1.12    structure PredData : THEORY_DATA
    1.13    
    1.14    (* queries *)
    1.15 @@ -90,10 +85,6 @@
    1.16  
    1.17  open Predicate_Compile_Aux;
    1.18  
    1.19 -(* FIXME: should be moved to Predicate_Compile_Aux *)
    1.20 -val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
    1.21 -
    1.22 -
    1.23  (* book-keeping *)
    1.24  
    1.25  datatype predfun_data = PredfunData of {
    1.26 @@ -214,140 +205,6 @@
    1.27  val intros_graph_of =
    1.28    Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
    1.29  
    1.30 -(** preprocessing rules **)
    1.31 -
    1.32 -fun Trueprop_conv cv ct =
    1.33 -  case Thm.term_of ct of
    1.34 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
    1.35 -  | _ => raise Fail "Trueprop_conv"
    1.36 -
    1.37 -fun preprocess_equality thy rule =
    1.38 -  Conv.fconv_rule
    1.39 -    (imp_prems_conv
    1.40 -      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
    1.41 -    (Thm.transfer thy rule)
    1.42 -
    1.43 -fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
    1.44 -
    1.45 -(* importing introduction rules *)
    1.46 -
    1.47 -fun unify_consts thy cs intr_ts =
    1.48 -  (let
    1.49 -     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
    1.50 -     fun varify (t, (i, ts)) =
    1.51 -       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
    1.52 -       in (maxidx_of_term t', t'::ts) end;
    1.53 -     val (i, cs') = List.foldr varify (~1, []) cs;
    1.54 -     val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
    1.55 -     val rec_consts = fold add_term_consts_2 cs' [];
    1.56 -     val intr_consts = fold add_term_consts_2 intr_ts' [];
    1.57 -     fun unify (cname, cT) =
    1.58 -       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
    1.59 -       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
    1.60 -     val (env, _) = fold unify rec_consts (Vartab.empty, i');
    1.61 -     val subst = map_types (Envir.norm_type env)
    1.62 -   in (map subst cs', map subst intr_ts')
    1.63 -   end) handle Type.TUNIFY =>
    1.64 -     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
    1.65 -
    1.66 -fun import_intros inp_pred [] ctxt =
    1.67 -  let
    1.68 -    val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
    1.69 -    val T = fastype_of outp_pred
    1.70 -    val paramTs = ho_argsT_of_typ (binder_types T)
    1.71 -    val (param_names, ctxt'') = Variable.variant_fixes
    1.72 -      (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
    1.73 -    val params = map2 (curry Free) param_names paramTs
    1.74 -  in
    1.75 -    (((outp_pred, params), []), ctxt')
    1.76 -  end
    1.77 -  | import_intros inp_pred (th :: ths) ctxt =
    1.78 -    let
    1.79 -      val ((_, [th']), ctxt') = Variable.import true [th] ctxt
    1.80 -      val thy = ProofContext.theory_of ctxt'
    1.81 -      val (pred, args) = strip_intro_concl th'
    1.82 -      val T = fastype_of pred
    1.83 -      val ho_args = ho_args_of_typ T args
    1.84 -      fun subst_of (pred', pred) =
    1.85 -        let
    1.86 -          val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
    1.87 -            handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
    1.88 -            ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
    1.89 -            ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
    1.90 -            ^ " in " ^ Display.string_of_thm ctxt th)
    1.91 -        in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
    1.92 -      fun instantiate_typ th =
    1.93 -        let
    1.94 -          val (pred', _) = strip_intro_concl th
    1.95 -          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
    1.96 -            raise Fail "Trying to instantiate another predicate" else ()
    1.97 -        in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
    1.98 -      fun instantiate_ho_args th =
    1.99 -        let
   1.100 -          val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
   1.101 -          val ho_args' = map dest_Var (ho_args_of_typ T args')
   1.102 -        in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
   1.103 -      val outp_pred =
   1.104 -        Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
   1.105 -      val ((_, ths'), ctxt1) =
   1.106 -        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
   1.107 -    in
   1.108 -      (((outp_pred, ho_args), th' :: ths'), ctxt1)
   1.109 -    end
   1.110 -
   1.111 -(* generation of case rules from user-given introduction rules *)
   1.112 -
   1.113 -fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
   1.114 -    let
   1.115 -      val (t1, st') = mk_args2 T1 st
   1.116 -      val (t2, st'') = mk_args2 T2 st'
   1.117 -    in
   1.118 -      (HOLogic.mk_prod (t1, t2), st'')
   1.119 -    end
   1.120 -  (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) = 
   1.121 -    let
   1.122 -      val (S, U) = strip_type T
   1.123 -    in
   1.124 -      if U = HOLogic.boolT then
   1.125 -        (hd params, (tl params, ctxt))
   1.126 -      else
   1.127 -        let
   1.128 -          val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
   1.129 -        in
   1.130 -          (Free (x, T), (params, ctxt'))
   1.131 -        end
   1.132 -    end*)
   1.133 -  | mk_args2 T (params, ctxt) =
   1.134 -    let
   1.135 -      val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
   1.136 -    in
   1.137 -      (Free (x, T), (params, ctxt'))
   1.138 -    end
   1.139 -
   1.140 -fun mk_casesrule ctxt pred introrules =
   1.141 -  let
   1.142 -    (* TODO: can be simplified if parameters are not treated specially ? *)
   1.143 -    val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
   1.144 -    (* TODO: distinct required ? -- test case with more than one parameter! *)
   1.145 -    val params = distinct (op aconv) params
   1.146 -    val intros = map prop_of intros_th
   1.147 -    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
   1.148 -    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
   1.149 -    val argsT = binder_types (fastype_of pred)
   1.150 -    (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *)
   1.151 -    val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)
   1.152 -    fun mk_case intro =
   1.153 -      let
   1.154 -        val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro
   1.155 -        val prems = Logic.strip_imp_prems intro
   1.156 -        val eqprems =
   1.157 -          map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
   1.158 -        val frees = map Free (fold Term.add_frees (args @ prems) [])
   1.159 -      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
   1.160 -    val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
   1.161 -    val cases = map mk_case intros
   1.162 -  in Logic.list_implies (assm :: cases, prop) end;
   1.163 -
   1.164  fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =
   1.165    let
   1.166      val thy = ProofContext.theory_of ctxt
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Oct 22 18:38:59 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Oct 22 18:38:59 2010 +0200
     2.3 @@ -53,6 +53,7 @@
     2.4    val is_constr : Proof.context -> string -> bool
     2.5    val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context
     2.6    val strip_all : term -> (string * typ) list * term
     2.7 +  val strip_intro_concl : thm -> term * term list
     2.8    (* introduction rule combinators *)
     2.9    val map_atoms : (term -> term) -> term -> term
    2.10    val fold_atoms : (term -> 'a -> 'a) -> term -> 'a -> 'a
    2.11 @@ -157,6 +158,11 @@
    2.12    val remove_equalities : theory -> thm -> thm
    2.13    val remove_pointless_clauses : thm -> thm list
    2.14    val peephole_optimisation : theory -> thm -> thm option
    2.15 +  (* auxillary *)
    2.16 +  val unify_consts : theory -> term list -> term list -> (term list * term list)
    2.17 +  val mk_casesrule : Proof.context -> term -> thm list -> term
    2.18 +  val preprocess_intro : theory -> thm -> thm
    2.19 +  
    2.20    val define_quickcheck_predicate :
    2.21      term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory
    2.22  end;
    2.23 @@ -546,6 +552,8 @@
    2.24      val t'' = Term.subst_bounds (rev vs, t');
    2.25    in ((ps', t''), nctxt') end;
    2.26  
    2.27 +val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
    2.28 +  
    2.29  (* introduction rule combinators *)
    2.30  
    2.31  fun map_atoms f intro = 
    2.32 @@ -1048,6 +1056,144 @@
    2.33        (process_False (process_True (prop_of (process intro))))
    2.34    end
    2.35  
    2.36 +
    2.37 +(* importing introduction rules *)
    2.38 +
    2.39 +fun import_intros inp_pred [] ctxt =
    2.40 +  let
    2.41 +    val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
    2.42 +    val T = fastype_of outp_pred
    2.43 +    val paramTs = ho_argsT_of_typ (binder_types T)
    2.44 +    val (param_names, ctxt'') = Variable.variant_fixes
    2.45 +      (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
    2.46 +    val params = map2 (curry Free) param_names paramTs
    2.47 +  in
    2.48 +    (((outp_pred, params), []), ctxt')
    2.49 +  end
    2.50 +  | import_intros inp_pred (th :: ths) ctxt =
    2.51 +    let
    2.52 +      val ((_, [th']), ctxt') = Variable.import true [th] ctxt
    2.53 +      val thy = ProofContext.theory_of ctxt'
    2.54 +      val (pred, args) = strip_intro_concl th'
    2.55 +      val T = fastype_of pred
    2.56 +      val ho_args = ho_args_of_typ T args
    2.57 +      fun subst_of (pred', pred) =
    2.58 +        let
    2.59 +          val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
    2.60 +            handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
    2.61 +            ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
    2.62 +            ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
    2.63 +            ^ " in " ^ Display.string_of_thm ctxt th)
    2.64 +        in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
    2.65 +      fun instantiate_typ th =
    2.66 +        let
    2.67 +          val (pred', _) = strip_intro_concl th
    2.68 +          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
    2.69 +            raise Fail "Trying to instantiate another predicate" else ()
    2.70 +        in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
    2.71 +      fun instantiate_ho_args th =
    2.72 +        let
    2.73 +          val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
    2.74 +          val ho_args' = map dest_Var (ho_args_of_typ T args')
    2.75 +        in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
    2.76 +      val outp_pred =
    2.77 +        Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
    2.78 +      val ((_, ths'), ctxt1) =
    2.79 +        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
    2.80 +    in
    2.81 +      (((outp_pred, ho_args), th' :: ths'), ctxt1)
    2.82 +    end
    2.83 +  
    2.84 +(* generation of case rules from user-given introduction rules *)
    2.85 +
    2.86 +fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
    2.87 +    let
    2.88 +      val (t1, st') = mk_args2 T1 st
    2.89 +      val (t2, st'') = mk_args2 T2 st'
    2.90 +    in
    2.91 +      (HOLogic.mk_prod (t1, t2), st'')
    2.92 +    end
    2.93 +  (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) = 
    2.94 +    let
    2.95 +      val (S, U) = strip_type T
    2.96 +    in
    2.97 +      if U = HOLogic.boolT then
    2.98 +        (hd params, (tl params, ctxt))
    2.99 +      else
   2.100 +        let
   2.101 +          val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
   2.102 +        in
   2.103 +          (Free (x, T), (params, ctxt'))
   2.104 +        end
   2.105 +    end*)
   2.106 +  | mk_args2 T (params, ctxt) =
   2.107 +    let
   2.108 +      val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
   2.109 +    in
   2.110 +      (Free (x, T), (params, ctxt'))
   2.111 +    end
   2.112 +
   2.113 +fun mk_casesrule ctxt pred introrules =
   2.114 +  let
   2.115 +    (* TODO: can be simplified if parameters are not treated specially ? *)
   2.116 +    val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
   2.117 +    (* TODO: distinct required ? -- test case with more than one parameter! *)
   2.118 +    val params = distinct (op aconv) params
   2.119 +    val intros = map prop_of intros_th
   2.120 +    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
   2.121 +    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
   2.122 +    val argsT = binder_types (fastype_of pred)
   2.123 +    (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *)
   2.124 +    val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)
   2.125 +    fun mk_case intro =
   2.126 +      let
   2.127 +        val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro
   2.128 +        val prems = Logic.strip_imp_prems intro
   2.129 +        val eqprems =
   2.130 +          map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
   2.131 +        val frees = map Free (fold Term.add_frees (args @ prems) [])
   2.132 +      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
   2.133 +    val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
   2.134 +    val cases = map mk_case intros
   2.135 +  in Logic.list_implies (assm :: cases, prop) end;
   2.136 +  
   2.137 +
   2.138 +(* unifying constants to have the same type variables *)
   2.139 +
   2.140 +fun unify_consts thy cs intr_ts =
   2.141 +  (let
   2.142 +     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
   2.143 +     fun varify (t, (i, ts)) =
   2.144 +       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
   2.145 +       in (maxidx_of_term t', t'::ts) end;
   2.146 +     val (i, cs') = List.foldr varify (~1, []) cs;
   2.147 +     val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
   2.148 +     val rec_consts = fold add_term_consts_2 cs' [];
   2.149 +     val intr_consts = fold add_term_consts_2 intr_ts' [];
   2.150 +     fun unify (cname, cT) =
   2.151 +       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
   2.152 +       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
   2.153 +     val (env, _) = fold unify rec_consts (Vartab.empty, i');
   2.154 +     val subst = map_types (Envir.norm_type env)
   2.155 +   in (map subst cs', map subst intr_ts')
   2.156 +   end) handle Type.TUNIFY =>
   2.157 +     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
   2.158 +
   2.159 +(* preprocessing rules *)
   2.160 +
   2.161 +fun Trueprop_conv cv ct =
   2.162 +  case Thm.term_of ct of
   2.163 +    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
   2.164 +  | _ => raise Fail "Trueprop_conv"
   2.165 +
   2.166 +fun preprocess_equality thy rule =
   2.167 +  Conv.fconv_rule
   2.168 +    (imp_prems_conv
   2.169 +      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
   2.170 +    (Thm.transfer thy rule)
   2.171 +
   2.172 +fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
   2.173 +
   2.174  (* defining a quickcheck predicate *)
   2.175  
   2.176  fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B