--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Thu Oct 21 19:13:09 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Thu Oct 21 19:13:10 2010 +0200
@@ -1,9 +1,99 @@
+(* Title: HOL/Tools/Predicate_Compile/core_data.ML
+ Author: Lukas Bulwahn, TU Muenchen
-structure Core_Data =
+Data of the predicate compiler core
+
+*)
+signature CORE_DATA =
+sig
+ type mode = Predicate_Compile_Aux.mode
+ type compilation = Predicate_Compile_Aux.compilation
+ type compilation_funs = Predicate_Compile_Aux.compilation_funs
+
+ datatype predfun_data = PredfunData of {
+ definition : thm,
+ intro : thm,
+ elim : thm,
+ neg_intro : thm option
+ };
+
+ datatype pred_data = PredData of {
+ intros : (string option * thm) list,
+ elim : thm option,
+ preprocessed : bool,
+ function_names : (compilation * (mode * string) list) list,
+ predfun_data : (mode * predfun_data) list,
+ needs_random : mode list
+ };
+
+ (* general operations *)
+ val unify_consts : theory -> term list -> term list -> (term list * term list)
+ val mk_casesrule : Proof.context -> term -> thm list -> term
+ val preprocess_intro : theory -> thm -> thm
+
+ structure PredData : THEORY_DATA
+
+ (* queries *)
+ val defined_functions : compilation -> Proof.context -> string -> bool
+ val is_registered : Proof.context -> string -> bool
+ val function_name_of : compilation -> Proof.context -> string -> mode -> string
+ val the_elim_of : Proof.context -> string -> thm
+ val has_elim : Proof.context -> string -> bool
+
+ val needs_random : Proof.context -> string -> mode -> bool
+
+ val predfun_intro_of : Proof.context -> string -> mode -> thm
+ val predfun_neg_intro_of : Proof.context -> string -> mode -> thm option
+ val predfun_elim_of : Proof.context -> string -> mode -> thm
+ val predfun_definition_of : Proof.context -> string -> mode -> thm
+
+ val all_preds_of : Proof.context -> string list
+ val modes_of: compilation -> Proof.context -> string -> mode list
+ val all_modes_of : compilation -> Proof.context -> (string * mode list) list
+ val all_random_modes_of : Proof.context -> (string * mode list) list
+ val intros_of : Proof.context -> string -> thm list
+ val names_of : Proof.context -> string -> string option list
+
+ val intros_graph_of : Proof.context -> thm list Graph.T
+
+ (* updaters *)
+
+ val register_predicate : (string * thm list * thm) -> theory -> theory
+ val register_intros : string * thm list -> theory -> theory
+
+ (* FIXME: naming of function is strange *)
+ val defined_function_of : compilation -> string -> theory -> theory
+ val add_intro : string option * thm -> theory -> theory
+ val set_elim : thm -> theory -> theory
+ val set_function_name : compilation -> string -> mode -> string -> theory -> theory
+ val add_predfun_data : string -> mode -> thm * ((thm * thm) * thm option) -> theory -> theory
+ val set_needs_random : string -> mode list -> theory -> theory
+ (* sophisticated updaters *)
+ val extend_intro_graph : string list -> theory -> theory
+ val preprocess_intros : string -> theory -> theory
+
+ (* alternative function definitions *)
+ val register_alternative_function : string -> mode -> string -> theory -> theory
+ val alternative_compilation_of_global : theory -> string -> mode ->
+ (compilation_funs -> typ -> term) option
+ val alternative_compilation_of : Proof.context -> string -> mode ->
+ (compilation_funs -> typ -> term) option
+ val functional_compilation : string -> mode -> compilation_funs -> typ -> term
+ val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory
+ val force_modes_and_compilations : string ->
+ (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
+
+end;
+
+structure Core_Data : CORE_DATA =
struct
open Predicate_Compile_Aux;
+(* FIXME: should be moved to Predicate_Compile_Aux *)
+val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
+
+
(* book-keeping *)
datatype predfun_data = PredfunData of {
@@ -124,6 +214,330 @@
val intros_graph_of =
Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
+(** preprocessing rules **)
+
+fun Trueprop_conv cv ct =
+ case Thm.term_of ct of
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
+ | _ => raise Fail "Trueprop_conv"
+
+fun preprocess_equality thy rule =
+ Conv.fconv_rule
+ (imp_prems_conv
+ (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
+ (Thm.transfer thy rule)
+
+fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
+
+(* importing introduction rules *)
+
+fun unify_consts thy cs intr_ts =
+ (let
+ val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
+ fun varify (t, (i, ts)) =
+ let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
+ in (maxidx_of_term t', t'::ts) end;
+ val (i, cs') = List.foldr varify (~1, []) cs;
+ val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
+ val rec_consts = fold add_term_consts_2 cs' [];
+ val intr_consts = fold add_term_consts_2 intr_ts' [];
+ fun unify (cname, cT) =
+ let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
+ in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
+ val (env, _) = fold unify rec_consts (Vartab.empty, i');
+ val subst = map_types (Envir.norm_type env)
+ in (map subst cs', map subst intr_ts')
+ end) handle Type.TUNIFY =>
+ (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
+
+fun import_intros inp_pred [] ctxt =
+ let
+ val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
+ val T = fastype_of outp_pred
+ val paramTs = ho_argsT_of_typ (binder_types T)
+ val (param_names, ctxt'') = Variable.variant_fixes
+ (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
+ val params = map2 (curry Free) param_names paramTs
+ in
+ (((outp_pred, params), []), ctxt')
+ end
+ | import_intros inp_pred (th :: ths) ctxt =
+ let
+ val ((_, [th']), ctxt') = Variable.import true [th] ctxt
+ val thy = ProofContext.theory_of ctxt'
+ val (pred, args) = strip_intro_concl th'
+ val T = fastype_of pred
+ val ho_args = ho_args_of_typ T args
+ fun subst_of (pred', pred) =
+ let
+ val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
+ handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
+ ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
+ ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
+ ^ " in " ^ Display.string_of_thm ctxt th)
+ in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
+ fun instantiate_typ th =
+ let
+ val (pred', _) = strip_intro_concl th
+ val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
+ raise Fail "Trying to instantiate another predicate" else ()
+ in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
+ fun instantiate_ho_args th =
+ let
+ val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
+ val ho_args' = map dest_Var (ho_args_of_typ T args')
+ in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
+ val outp_pred =
+ Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
+ val ((_, ths'), ctxt1) =
+ Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
+ in
+ (((outp_pred, ho_args), th' :: ths'), ctxt1)
+ end
+
+(* generation of case rules from user-given introduction rules *)
+
+fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
+ let
+ val (t1, st') = mk_args2 T1 st
+ val (t2, st'') = mk_args2 T2 st'
+ in
+ (HOLogic.mk_prod (t1, t2), st'')
+ end
+ (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) =
+ let
+ val (S, U) = strip_type T
+ in
+ if U = HOLogic.boolT then
+ (hd params, (tl params, ctxt))
+ else
+ let
+ val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
+ in
+ (Free (x, T), (params, ctxt'))
+ end
+ end*)
+ | mk_args2 T (params, ctxt) =
+ let
+ val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
+ in
+ (Free (x, T), (params, ctxt'))
+ end
+
+fun mk_casesrule ctxt pred introrules =
+ let
+ (* TODO: can be simplified if parameters are not treated specially ? *)
+ val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
+ (* TODO: distinct required ? -- test case with more than one parameter! *)
+ val params = distinct (op aconv) params
+ val intros = map prop_of intros_th
+ val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
+ val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
+ val argsT = binder_types (fastype_of pred)
+ (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *)
+ val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)
+ fun mk_case intro =
+ let
+ val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro
+ val prems = Logic.strip_imp_prems intro
+ val eqprems =
+ map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
+ val frees = map Free (fold Term.add_frees (args @ prems) [])
+ in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
+ val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
+ val cases = map mk_case intros
+ in Logic.list_implies (assm :: cases, prop) end;
+
+fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val nargs = length (binder_types (fastype_of pred))
+ fun PEEK f dependent_tactic st = dependent_tactic (f st) st
+ fun meta_eq_of th = th RS @{thm eq_reflection}
+ val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
+ fun instantiate i n {context = ctxt, params = p, prems = prems,
+ asms = a, concl = cl, schematics = s} =
+ let
+ fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
+ fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
+ |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
+ val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
+ val case_th = MetaSimplifier.simplify true
+ (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
+ val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
+ val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
+ val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
+ OF (replicate nargs @{thm refl})
+ val thesis =
+ Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th'
+ OF prems'
+ in
+ (rtac thesis 1)
+ end
+ val tac =
+ etac pre_cases_rule 1
+ THEN
+ (PEEK nprems_of
+ (fn n =>
+ ALLGOALS (fn i =>
+ MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i
+ THEN (SUBPROOF (instantiate i n) ctxt i))))
+ in
+ Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
+ end
+
+(* updaters *)
+
+(* fetching introduction rules or registering introduction rules *)
+
+val no_compilation = ([], ([], []))
+
+fun fetch_pred_data ctxt name =
+ case try (Inductive.the_inductive ctxt) name of
+ SOME (info as (_, result)) =>
+ let
+ fun is_intro_of intro =
+ let
+ val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
+ in (fst (dest_Const const) = name) end;
+ val thy = ProofContext.theory_of ctxt
+ val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
+ val index = find_index (fn s => s = name) (#names (fst info))
+ val pre_elim = nth (#elims result) index
+ val pred = nth (#preds result) index
+ val elim_t = mk_casesrule ctxt pred intros
+ val nparams = length (Inductive.params_of (#raw_induct result))
+ val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
+ in
+ mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
+ end
+ | NONE => error ("No such predicate: " ^ quote name)
+
+fun add_predfun_data name mode data =
+ let
+ val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
+ in PredData.map (Graph.map_node name (map_pred_data add)) end
+
+fun is_inductive_predicate ctxt name =
+ is_some (try (Inductive.the_inductive ctxt) name)
+
+fun depending_preds_of ctxt (key, value) =
+ let
+ val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value)
+ in
+ fold Term.add_const_names intros []
+ |> (fn cs =>
+ if member (op =) cs @{const_name "HOL.eq"} then
+ insert (op =) @{const_name Predicate.eq} cs
+ else cs)
+ |> filter (fn c => (not (c = key)) andalso
+ (is_inductive_predicate ctxt c orelse is_registered ctxt c))
+ end;
+
+fun add_intro (opt_case_name, thm) thy =
+ let
+ val (name, T) = dest_Const (fst (strip_intro_concl thm))
+ fun cons_intro gr =
+ case try (Graph.get_node gr) name of
+ SOME pred_data => Graph.map_node name (map_pred_data
+ (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
+ | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
+ in PredData.map cons_intro thy end
+
+fun set_elim thm =
+ let
+ val (name, _) = dest_Const (fst
+ (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
+ in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
+
+fun register_predicate (constname, intros, elim) thy =
+ let
+ val named_intros = map (pair NONE) intros
+ in
+ if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
+ PredData.map
+ (Graph.new_node (constname,
+ mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy
+ else thy
+ end
+
+fun register_intros (constname, pre_intros) thy =
+ let
+ val T = Sign.the_const_type thy constname
+ fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr)))
+ val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then
+ error ("register_intros: Introduction rules of different constants are used\n" ^
+ "expected rules for " ^ constname ^ ", but received rules for " ^
+ commas (map constname_of_intro pre_intros))
+ else ()
+ val pred = Const (constname, T)
+ val pre_elim =
+ (Drule.export_without_context o Skip_Proof.make_thm thy)
+ (mk_casesrule (ProofContext.init_global thy) pred pre_intros)
+ in register_predicate (constname, pre_intros, pre_elim) thy end
+
+fun defined_function_of compilation pred =
+ let
+ val set = (apsnd o apfst) (cons (compilation, []))
+ in
+ PredData.map (Graph.map_node pred (map_pred_data set))
+ end
+
+fun set_function_name compilation pred mode name =
+ let
+ val set = (apsnd o apfst)
+ (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
+ in
+ PredData.map (Graph.map_node pred (map_pred_data set))
+ end
+
+fun set_needs_random name modes =
+ let
+ val set = (apsnd o apsnd o apsnd) (K modes)
+ in
+ PredData.map (Graph.map_node name (map_pred_data set))
+ end
+
+fun extend' value_of edges_of key (G, visited) =
+ let
+ val (G', v) = case try (Graph.get_node G) key of
+ SOME v => (G, v)
+ | NONE => (Graph.new_node (key, value_of key) G, value_of key)
+ val (G'', visited') = fold (extend' value_of edges_of)
+ (subtract (op =) visited (edges_of (key, v)))
+ (G', key :: visited)
+ in
+ (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
+ end;
+
+fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, []))
+
+fun extend_intro_graph names thy =
+ let
+ val ctxt = ProofContext.init_global thy
+ in
+ PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names) thy
+ end
+
+fun preprocess_intros name thy =
+ PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) =>
+ if preprocessed then (rules, preprocessed)
+ else
+ let
+ val (named_intros, SOME elim) = rules
+ val named_intros' = map (apsnd (preprocess_intro thy)) named_intros
+ val pred = Const (name, Sign.the_const_type thy name)
+ val ctxt = ProofContext.init_global thy
+ val elim_t = mk_casesrule ctxt pred (map snd named_intros')
+ val nparams = (case try (Inductive.the_inductive ctxt) name of
+ SOME (_, result) => length (Inductive.params_of (#raw_induct result))
+ | NONE => 0)
+ val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
+ in
+ ((named_intros', SOME elim'), true)
+ end))))
+ thy
+
(* registration of alternative function names *)
structure Alt_Compilations_Data = Theory_Data
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Oct 21 19:13:09 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Oct 21 19:13:10 2010 +0200
@@ -75,7 +75,7 @@
fun preprocess_strong_conn_constnames options gr ts thy =
if forall (fn (Const (c, _)) =>
- Predicate_Compile_Core.is_registered (ProofContext.init_global thy) c) ts then
+ Core_Data.is_registered (ProofContext.init_global thy) c) ts then
thy
else
let
@@ -121,7 +121,7 @@
val intross10 = map_specs (map_filter (peephole_optimisation thy3)) intross9
val _ = print_intross options thy3 "introduction rules before registering: " intross10
val _ = print_step options "Registering introduction rules..."
- val thy4 = fold Predicate_Compile_Core.register_intros intross10 thy3
+ val thy4 = fold Core_Data.register_intros intross10 thy3
in
thy4
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 21 19:13:09 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 21 19:13:10 2010 +0200
@@ -16,33 +16,9 @@
val code_pred_cmd : options -> string -> Proof.context -> Proof.state
val values_cmd : string list -> mode option list option
-> ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
- val register_predicate : (string * thm list * thm) -> theory -> theory
- val register_intros : string * thm list -> theory -> theory
- val is_registered : Proof.context -> string -> bool
- val function_name_of : compilation -> Proof.context -> string -> mode -> string
- val predfun_intro_of: Proof.context -> string -> mode -> thm
- val predfun_elim_of: Proof.context -> string -> mode -> thm
- val all_preds_of : Proof.context -> string list
- val modes_of: compilation -> Proof.context -> string -> mode list
- val all_modes_of : compilation -> Proof.context -> (string * mode list) list
- val all_random_modes_of : Proof.context -> (string * mode list) list
- val intros_of : Proof.context -> string -> thm list
- val intros_graph_of : Proof.context -> thm list Graph.T
- val add_intro : string option * thm -> theory -> theory
- val set_elim : thm -> theory -> theory
- val register_alternative_function : string -> mode -> string -> theory -> theory
- val alternative_compilation_of_global : theory -> string -> mode ->
- (compilation_funs -> typ -> term) option
- val alternative_compilation_of : Proof.context -> string -> mode ->
- (compilation_funs -> typ -> term) option
- val functional_compilation : string -> mode -> compilation_funs -> typ -> term
- val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory
- val force_modes_and_compilations : string ->
- (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
- val preprocess_intro : theory -> thm -> thm
+
val print_stored_rules : Proof.context -> unit
val print_all_modes : compilation -> Proof.context -> unit
- val mk_casesrule : Proof.context -> term -> thm list -> term
val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
val put_pred_random_result : (unit -> int * int -> term Predicate.pred * (int * int)) ->
@@ -128,8 +104,6 @@
Const(@{const_name Code_Evaluation.tracing},
@{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
-val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
-
(* representation of inferred clauses with modes *)
type moded_clause = term list * (indprem * mode_derivation) list
@@ -264,289 +238,6 @@
ms
end
-
-(* importing introduction rules *)
-
-fun unify_consts thy cs intr_ts =
- (let
- val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
- fun varify (t, (i, ts)) =
- let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
- in (maxidx_of_term t', t'::ts) end;
- val (i, cs') = List.foldr varify (~1, []) cs;
- val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
- val rec_consts = fold add_term_consts_2 cs' [];
- val intr_consts = fold add_term_consts_2 intr_ts' [];
- fun unify (cname, cT) =
- let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
- in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
- val (env, _) = fold unify rec_consts (Vartab.empty, i');
- val subst = map_types (Envir.norm_type env)
- in (map subst cs', map subst intr_ts')
- end) handle Type.TUNIFY =>
- (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
-
-fun import_intros inp_pred [] ctxt =
- let
- val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
- val T = fastype_of outp_pred
- val paramTs = ho_argsT_of_typ (binder_types T)
- val (param_names, ctxt'') = Variable.variant_fixes
- (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
- val params = map2 (curry Free) param_names paramTs
- in
- (((outp_pred, params), []), ctxt')
- end
- | import_intros inp_pred (th :: ths) ctxt =
- let
- val ((_, [th']), ctxt') = Variable.import true [th] ctxt
- val thy = ProofContext.theory_of ctxt'
- val (pred, args) = strip_intro_concl th'
- val T = fastype_of pred
- val ho_args = ho_args_of_typ T args
- fun subst_of (pred', pred) =
- let
- val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
- handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
- ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
- ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
- ^ " in " ^ Display.string_of_thm ctxt th)
- in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
- fun instantiate_typ th =
- let
- val (pred', _) = strip_intro_concl th
- val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
- raise Fail "Trying to instantiate another predicate" else ()
- in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
- fun instantiate_ho_args th =
- let
- val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
- val ho_args' = map dest_Var (ho_args_of_typ T args')
- in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
- val outp_pred =
- Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
- val ((_, ths'), ctxt1) =
- Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
- in
- (((outp_pred, ho_args), th' :: ths'), ctxt1)
- end
-
-(* generation of case rules from user-given introduction rules *)
-
-fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
- let
- val (t1, st') = mk_args2 T1 st
- val (t2, st'') = mk_args2 T2 st'
- in
- (HOLogic.mk_prod (t1, t2), st'')
- end
- (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) =
- let
- val (S, U) = strip_type T
- in
- if U = HOLogic.boolT then
- (hd params, (tl params, ctxt))
- else
- let
- val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
- in
- (Free (x, T), (params, ctxt'))
- end
- end*)
- | mk_args2 T (params, ctxt) =
- let
- val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
- in
- (Free (x, T), (params, ctxt'))
- end
-
-fun mk_casesrule ctxt pred introrules =
- let
- (* TODO: can be simplified if parameters are not treated specially ? *)
- val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
- (* TODO: distinct required ? -- test case with more than one parameter! *)
- val params = distinct (op aconv) params
- val intros = map prop_of intros_th
- val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
- val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
- val argsT = binder_types (fastype_of pred)
- (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *)
- val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)
- fun mk_case intro =
- let
- val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro
- val prems = Logic.strip_imp_prems intro
- val eqprems =
- map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
- val frees = map Free (fold Term.add_frees (args @ prems) [])
- in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
- val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
- val cases = map mk_case intros
- in Logic.list_implies (assm :: cases, prop) end;
-
-fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =
- let
- val thy = ProofContext.theory_of ctxt
- val nargs = length (binder_types (fastype_of pred))
- fun PEEK f dependent_tactic st = dependent_tactic (f st) st
- fun meta_eq_of th = th RS @{thm eq_reflection}
- val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
- fun instantiate i n {context = ctxt, params = p, prems = prems,
- asms = a, concl = cl, schematics = s} =
- let
- fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
- fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
- |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
- val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
- val case_th = MetaSimplifier.simplify true
- (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
- val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
- val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
- val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
- OF (replicate nargs @{thm refl})
- val thesis =
- Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th'
- OF prems'
- in
- (rtac thesis 1)
- end
- val tac =
- etac pre_cases_rule 1
- THEN
- (PEEK nprems_of
- (fn n =>
- ALLGOALS (fn i =>
- MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i
- THEN (SUBPROOF (instantiate i n) ctxt i))))
- in
- Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
- end
-
-(** preprocessing rules **)
-
-fun Trueprop_conv cv ct =
- case Thm.term_of ct of
- Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
- | _ => raise Fail "Trueprop_conv"
-
-fun preprocess_equality thy rule =
- Conv.fconv_rule
- (imp_prems_conv
- (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
- (Thm.transfer thy rule)
-
-fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
-
-(* fetching introduction rules or registering introduction rules *)
-
-val no_compilation = ([], ([], []))
-
-fun fetch_pred_data ctxt name =
- case try (Inductive.the_inductive ctxt) name of
- SOME (info as (_, result)) =>
- let
- fun is_intro_of intro =
- let
- val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
- in (fst (dest_Const const) = name) end;
- val thy = ProofContext.theory_of ctxt
- val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
- val index = find_index (fn s => s = name) (#names (fst info))
- val pre_elim = nth (#elims result) index
- val pred = nth (#preds result) index
- val elim_t = mk_casesrule ctxt pred intros
- val nparams = length (Inductive.params_of (#raw_induct result))
- val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
- in
- mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
- end
- | NONE => error ("No such predicate: " ^ quote name)
-
-fun add_predfun_data name mode data =
- let
- val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
- in PredData.map (Graph.map_node name (map_pred_data add)) end
-
-fun is_inductive_predicate ctxt name =
- is_some (try (Inductive.the_inductive ctxt) name)
-
-fun depending_preds_of ctxt (key, value) =
- let
- val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value)
- in
- fold Term.add_const_names intros []
- |> (fn cs =>
- if member (op =) cs @{const_name "HOL.eq"} then
- insert (op =) @{const_name Predicate.eq} cs
- else cs)
- |> filter (fn c => (not (c = key)) andalso
- (is_inductive_predicate ctxt c orelse is_registered ctxt c))
- end;
-
-fun add_intro (opt_case_name, thm) thy =
- let
- val (name, T) = dest_Const (fst (strip_intro_concl thm))
- fun cons_intro gr =
- case try (Graph.get_node gr) name of
- SOME pred_data => Graph.map_node name (map_pred_data
- (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
- | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
- in PredData.map cons_intro thy end
-
-fun set_elim thm =
- let
- val (name, _) = dest_Const (fst
- (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
- in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
-
-fun register_predicate (constname, intros, elim) thy =
- let
- val named_intros = map (pair NONE) intros
- in
- if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
- PredData.map
- (Graph.new_node (constname,
- mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy
- else thy
- end
-
-fun register_intros (constname, pre_intros) thy =
- let
- val T = Sign.the_const_type thy constname
- fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr)))
- val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then
- error ("register_intros: Introduction rules of different constants are used\n" ^
- "expected rules for " ^ constname ^ ", but received rules for " ^
- commas (map constname_of_intro pre_intros))
- else ()
- val pred = Const (constname, T)
- val pre_elim =
- (Drule.export_without_context o Skip_Proof.make_thm thy)
- (mk_casesrule (ProofContext.init_global thy) pred pre_intros)
- in register_predicate (constname, pre_intros, pre_elim) thy end
-
-fun defined_function_of compilation pred =
- let
- val set = (apsnd o apfst) (cons (compilation, []))
- in
- PredData.map (Graph.map_node pred (map_pred_data set))
- end
-
-fun set_function_name compilation pred mode name =
- let
- val set = (apsnd o apfst)
- (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
- in
- PredData.map (Graph.map_node pred (map_pred_data set))
- end
-
-fun set_needs_random name modes =
- let
- val set = (apsnd o apsnd o apsnd) (K modes)
- in
- PredData.map (Graph.map_node name (map_pred_data set))
- end
-
(* compilation modifiers *)
structure Comp_Mod =
@@ -1719,51 +1410,16 @@
in
thy'''
end
-
-fun extend' value_of edges_of key (G, visited) =
- let
- val (G', v) = case try (Graph.get_node G) key of
- SOME v => (G, v)
- | NONE => (Graph.new_node (key, value_of key) G, value_of key)
- val (G'', visited') = fold (extend' value_of edges_of)
- (subtract (op =) visited (edges_of (key, v)))
- (G', key :: visited)
- in
- (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
- end;
-
-fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, []))
fun gen_add_equations steps options names thy =
let
fun dest_steps (Steps s) = s
val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
- val ctxt = ProofContext.init_global thy
- val thy' = thy
- |> PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names)
- |> Theory.checkpoint;
+ val thy' = extend_intro_graph names thy |> Theory.checkpoint;
fun strong_conn_of gr keys =
Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
val scc = strong_conn_of (PredData.get thy') names
- fun preprocess name thy =
- PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) =>
- if preprocessed then (rules, preprocessed)
- else
- let
- val (named_intros, SOME elim) = rules
- val named_intros' = map (apsnd (preprocess_intro thy)) named_intros
- val pred = Const (name, Sign.the_const_type thy name)
- val ctxt = ProofContext.init_global thy
- val elim_t = mk_casesrule ctxt pred (map snd named_intros')
- val nparams = (case try (Inductive.the_inductive ctxt) name of
- SOME (_, result) => length (Inductive.params_of (#raw_induct result))
- | NONE => 0)
- val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
- in
- ((named_intros', SOME elim'), true)
- end))))
- thy
- val thy'' = fold preprocess (flat scc) thy'
+ val thy'' = fold preprocess_intros (flat scc) thy'
val thy''' = fold_rev
(fn preds => fn thy =>
if not (forall (defined (ProofContext.init_global thy)) preds) then
@@ -1930,9 +1586,7 @@
let
val thy = ProofContext.theory_of lthy
val const = prep_const thy raw_const
- val ctxt = ProofContext.init_global thy
- val lthy' = Local_Theory.background_theory (PredData.map
- (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy
+ val lthy' = Local_Theory.background_theory (extend_intro_graph [const]) lthy
val thy' = ProofContext.theory_of lthy'
val ctxt' = ProofContext.init_global thy'
val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt')
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Oct 21 19:13:09 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Oct 21 19:13:10 2010 +0200
@@ -255,7 +255,7 @@
let
val ctxt = ProofContext.init_global thy
fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
- fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of ctxt) c
+ fun has_code_pred_intros (c, T) = can (Core_Data.intros_of ctxt) c
fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
fun defiants_of specs =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Oct 21 19:13:09 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Oct 21 19:13:10 2010 +0200
@@ -312,7 +312,7 @@
fun functional_mode_of T =
list_fun_mode (replicate (length (binder_types T)) Input @ [Output])
val thy''' = fold
- (fn (predname, Const (name, T)) => Predicate_Compile_Core.register_alternative_function
+ (fn (predname, Const (name, T)) => Core_Data.register_alternative_function
predname (functional_mode_of T) name)
(dst_prednames ~~ dst_funs) thy''
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Oct 21 19:13:09 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Oct 21 19:13:10 2010 +0200
@@ -109,7 +109,7 @@
val optimised_intros =
map_filter (Predicate_Compile_Aux.peephole_optimisation thy'') exported_intros
val ([spec], thy''') = find_specialisations black_list [(constname, optimised_intros)] thy''
- val thy'''' = Predicate_Compile_Core.register_intros spec thy'''
+ val thy'''' = Core_Data.register_intros spec thy'''
in
thy''''
end
@@ -180,7 +180,7 @@
if member (op =) ((map fst specs) @ black_list) pred_name then
thy
else
- (case try (Predicate_Compile_Core.intros_of (ProofContext.init_global thy)) pred_name of
+ (case try (Core_Data.intros_of (ProofContext.init_global thy)) pred_name of
NONE => thy
| SOME [] => thy
| SOME intros =>