src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 40101 f7fc517e21c6
parent 40054 cd7b1fa20bce
child 40139 6a53d57fa902
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Oct 22 18:38:59 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Oct 22 18:38:59 2010 +0200
     1.3 @@ -53,6 +53,7 @@
     1.4    val is_constr : Proof.context -> string -> bool
     1.5    val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context
     1.6    val strip_all : term -> (string * typ) list * term
     1.7 +  val strip_intro_concl : thm -> term * term list
     1.8    (* introduction rule combinators *)
     1.9    val map_atoms : (term -> term) -> term -> term
    1.10    val fold_atoms : (term -> 'a -> 'a) -> term -> 'a -> 'a
    1.11 @@ -157,6 +158,11 @@
    1.12    val remove_equalities : theory -> thm -> thm
    1.13    val remove_pointless_clauses : thm -> thm list
    1.14    val peephole_optimisation : theory -> thm -> thm option
    1.15 +  (* auxillary *)
    1.16 +  val unify_consts : theory -> term list -> term list -> (term list * term list)
    1.17 +  val mk_casesrule : Proof.context -> term -> thm list -> term
    1.18 +  val preprocess_intro : theory -> thm -> thm
    1.19 +  
    1.20    val define_quickcheck_predicate :
    1.21      term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory
    1.22  end;
    1.23 @@ -546,6 +552,8 @@
    1.24      val t'' = Term.subst_bounds (rev vs, t');
    1.25    in ((ps', t''), nctxt') end;
    1.26  
    1.27 +val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
    1.28 +  
    1.29  (* introduction rule combinators *)
    1.30  
    1.31  fun map_atoms f intro = 
    1.32 @@ -1048,6 +1056,144 @@
    1.33        (process_False (process_True (prop_of (process intro))))
    1.34    end
    1.35  
    1.36 +
    1.37 +(* importing introduction rules *)
    1.38 +
    1.39 +fun import_intros inp_pred [] ctxt =
    1.40 +  let
    1.41 +    val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
    1.42 +    val T = fastype_of outp_pred
    1.43 +    val paramTs = ho_argsT_of_typ (binder_types T)
    1.44 +    val (param_names, ctxt'') = Variable.variant_fixes
    1.45 +      (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
    1.46 +    val params = map2 (curry Free) param_names paramTs
    1.47 +  in
    1.48 +    (((outp_pred, params), []), ctxt')
    1.49 +  end
    1.50 +  | import_intros inp_pred (th :: ths) ctxt =
    1.51 +    let
    1.52 +      val ((_, [th']), ctxt') = Variable.import true [th] ctxt
    1.53 +      val thy = ProofContext.theory_of ctxt'
    1.54 +      val (pred, args) = strip_intro_concl th'
    1.55 +      val T = fastype_of pred
    1.56 +      val ho_args = ho_args_of_typ T args
    1.57 +      fun subst_of (pred', pred) =
    1.58 +        let
    1.59 +          val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
    1.60 +            handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
    1.61 +            ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
    1.62 +            ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
    1.63 +            ^ " in " ^ Display.string_of_thm ctxt th)
    1.64 +        in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
    1.65 +      fun instantiate_typ th =
    1.66 +        let
    1.67 +          val (pred', _) = strip_intro_concl th
    1.68 +          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
    1.69 +            raise Fail "Trying to instantiate another predicate" else ()
    1.70 +        in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
    1.71 +      fun instantiate_ho_args th =
    1.72 +        let
    1.73 +          val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
    1.74 +          val ho_args' = map dest_Var (ho_args_of_typ T args')
    1.75 +        in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
    1.76 +      val outp_pred =
    1.77 +        Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
    1.78 +      val ((_, ths'), ctxt1) =
    1.79 +        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
    1.80 +    in
    1.81 +      (((outp_pred, ho_args), th' :: ths'), ctxt1)
    1.82 +    end
    1.83 +  
    1.84 +(* generation of case rules from user-given introduction rules *)
    1.85 +
    1.86 +fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
    1.87 +    let
    1.88 +      val (t1, st') = mk_args2 T1 st
    1.89 +      val (t2, st'') = mk_args2 T2 st'
    1.90 +    in
    1.91 +      (HOLogic.mk_prod (t1, t2), st'')
    1.92 +    end
    1.93 +  (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) = 
    1.94 +    let
    1.95 +      val (S, U) = strip_type T
    1.96 +    in
    1.97 +      if U = HOLogic.boolT then
    1.98 +        (hd params, (tl params, ctxt))
    1.99 +      else
   1.100 +        let
   1.101 +          val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
   1.102 +        in
   1.103 +          (Free (x, T), (params, ctxt'))
   1.104 +        end
   1.105 +    end*)
   1.106 +  | mk_args2 T (params, ctxt) =
   1.107 +    let
   1.108 +      val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
   1.109 +    in
   1.110 +      (Free (x, T), (params, ctxt'))
   1.111 +    end
   1.112 +
   1.113 +fun mk_casesrule ctxt pred introrules =
   1.114 +  let
   1.115 +    (* TODO: can be simplified if parameters are not treated specially ? *)
   1.116 +    val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
   1.117 +    (* TODO: distinct required ? -- test case with more than one parameter! *)
   1.118 +    val params = distinct (op aconv) params
   1.119 +    val intros = map prop_of intros_th
   1.120 +    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
   1.121 +    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
   1.122 +    val argsT = binder_types (fastype_of pred)
   1.123 +    (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *)
   1.124 +    val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)
   1.125 +    fun mk_case intro =
   1.126 +      let
   1.127 +        val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro
   1.128 +        val prems = Logic.strip_imp_prems intro
   1.129 +        val eqprems =
   1.130 +          map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
   1.131 +        val frees = map Free (fold Term.add_frees (args @ prems) [])
   1.132 +      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
   1.133 +    val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
   1.134 +    val cases = map mk_case intros
   1.135 +  in Logic.list_implies (assm :: cases, prop) end;
   1.136 +  
   1.137 +
   1.138 +(* unifying constants to have the same type variables *)
   1.139 +
   1.140 +fun unify_consts thy cs intr_ts =
   1.141 +  (let
   1.142 +     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
   1.143 +     fun varify (t, (i, ts)) =
   1.144 +       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
   1.145 +       in (maxidx_of_term t', t'::ts) end;
   1.146 +     val (i, cs') = List.foldr varify (~1, []) cs;
   1.147 +     val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
   1.148 +     val rec_consts = fold add_term_consts_2 cs' [];
   1.149 +     val intr_consts = fold add_term_consts_2 intr_ts' [];
   1.150 +     fun unify (cname, cT) =
   1.151 +       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
   1.152 +       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
   1.153 +     val (env, _) = fold unify rec_consts (Vartab.empty, i');
   1.154 +     val subst = map_types (Envir.norm_type env)
   1.155 +   in (map subst cs', map subst intr_ts')
   1.156 +   end) handle Type.TUNIFY =>
   1.157 +     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
   1.158 +
   1.159 +(* preprocessing rules *)
   1.160 +
   1.161 +fun Trueprop_conv cv ct =
   1.162 +  case Thm.term_of ct of
   1.163 +    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
   1.164 +  | _ => raise Fail "Trueprop_conv"
   1.165 +
   1.166 +fun preprocess_equality thy rule =
   1.167 +  Conv.fconv_rule
   1.168 +    (imp_prems_conv
   1.169 +      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
   1.170 +    (Thm.transfer thy rule)
   1.171 +
   1.172 +fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
   1.173 +
   1.174  (* defining a quickcheck predicate *)
   1.175  
   1.176  fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B