--- a/src/HOL/HOL.thy Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/HOL.thy Wed Sep 23 16:20:12 2009 +0200
@@ -2023,7 +2023,27 @@
subsection {* Preprocessing for the predicate compiler *}
-setup {* Predicate_Compile_Preproc_Const_Defs.setup *}
+ML {*
+structure Predicate_Compile_Alternative_Defs = Named_Thms
+(
+ val name = "code_pred_def"
+ val description = "alternative definitions of constants for the Predicate Compiler"
+)
+*}
+
+ML {*
+structure Predicate_Compile_Inline_Defs = Named_Thms
+(
+ val name = "code_pred_inline"
+ val description = "inlining definitions for the Predicate Compiler"
+)
+*}
+
+setup {*
+ Predicate_Compile_Alternative_Defs.setup
+ #> Predicate_Compile_Inline_Defs.setup
+ #> Predicate_Compile_Preproc_Const_Defs.setup
+*}
subsection {* Nitpick setup *}
--- a/src/HOL/Predicate.thy Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Predicate.thy Wed Sep 23 16:20:12 2009 +0200
@@ -797,6 +797,10 @@
(auto simp add: Seq_def the_only_singleton is_empty_def
null_is_empty singleton_bot singleton_single singleton_sup Let_def)
+lemma meta_fun_cong:
+"f == g ==> f x == g x"
+by simp
+
ML {*
signature PREDICATE =
sig
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Wed Sep 23 16:20:12 2009 +0200
@@ -0,0 +1,100 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Auxilary functions for predicate compiler
+*)
+
+structure Predicate_Compile_Aux =
+struct
+
+(* syntactic functions *)
+
+fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
+ | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
+ | is_equationlike_term _ = false
+
+val is_equationlike = is_equationlike_term o prop_of
+
+fun is_pred_equation_term (Const ("==", _) $ u $ v) =
+ (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
+ | is_pred_equation_term _ = false
+
+val is_pred_equation = is_pred_equation_term o prop_of
+
+fun is_intro_term constname t =
+ case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
+ Const (c, _) => c = constname
+ | _ => false
+
+fun is_intro constname t = is_intro_term constname (prop_of t)
+
+fun is_pred thy constname =
+ let
+ val T = (Sign.the_const_type thy constname)
+ in body_type T = @{typ "bool"} end;
+
+
+fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
+ | is_predT _ = false
+
+
+(*** check if a term contains only constructor functions ***)
+fun is_constrt thy =
+ let
+ val cnstrs = flat (maps
+ (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
+ (Symtab.dest (Datatype.get_all thy)));
+ fun check t = (case strip_comb t of
+ (Free _, []) => true
+ | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
+ (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
+ | _ => false)
+ | _ => false)
+ in check end;
+
+fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
+ let
+ val (xTs, t') = strip_ex t
+ in
+ ((x, T) :: xTs, t')
+ end
+ | strip_ex t = ([], t)
+
+fun focus_ex t nctxt =
+ let
+ val ((xs, Ts), t') = apfst split_list (strip_ex t)
+ val (xs', nctxt') = Name.variants xs nctxt;
+ val ps' = xs' ~~ Ts;
+ val vs = map Free ps';
+ val t'' = Term.subst_bounds (rev vs, t');
+ in ((ps', t''), nctxt') end;
+
+
+
+
+(*
+fun map_atoms f intro =
+fun fold_atoms f intro =
+*)
+fun fold_map_atoms f intro s =
+ let
+ val (literals, head) = Logic.strip_horn intro
+ fun appl t s = (case t of
+ (@{term "Not"} $ t') =>
+ let
+ val (t'', s') = f t' s
+ in (@{term "Not"} $ t'', s') end
+ | _ => f t s)
+ val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
+ in
+ (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
+ end;
+
+(*
+fun equals_conv lhs_cv rhs_cv ct =
+ case Thm.term_of ct of
+ Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
+ | _ => error "equals_conv"
+*)
+
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Wed Sep 23 16:20:12 2009 +0200
@@ -0,0 +1,215 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Book-keeping datastructure for the predicate compiler
+
+*)
+signature PRED_COMPILE_DATA =
+sig
+ type specification_table;
+ val make_const_spec_table : theory -> specification_table
+ val get_specification : specification_table -> string -> thm list
+ val obtain_specification_graph : specification_table -> string -> thm list Graph.T
+ val normalize_equation : theory -> thm -> thm
+end;
+
+structure Pred_Compile_Data : PRED_COMPILE_DATA =
+struct
+
+open Predicate_Compile_Aux;
+
+structure Data = TheoryDataFun
+(
+ type T =
+ {const_spec_table : thm list Symtab.table};
+ val empty =
+ {const_spec_table = Symtab.empty};
+ val copy = I;
+ val extend = I;
+ fun merge _
+ ({const_spec_table = const_spec_table1},
+ {const_spec_table = const_spec_table2}) =
+ {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
+);
+
+fun mk_data c = {const_spec_table = c}
+fun map_data f {const_spec_table = c} = mk_data (f c)
+
+type specification_table = thm list Symtab.table
+
+fun defining_const_of_introrule_term t =
+ let
+ val _ $ u = Logic.strip_imp_concl t
+ val (pred, all_args) = strip_comb u
+ in case pred of
+ Const (c, T) => c
+ | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
+ end
+
+val defining_const_of_introrule = defining_const_of_introrule_term o prop_of
+
+(*TODO*)
+fun is_introlike_term t = true
+
+val is_introlike = is_introlike_term o prop_of
+
+fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
+ (case strip_comb u of
+ (Const (c, T), args) =>
+ if (length (binder_types T) = length args) then
+ true
+ else
+ raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
+ | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
+ | check_equation_format_term t =
+ raise TERM ("check_equation_format_term failed: Not an equation", [t])
+
+val check_equation_format = check_equation_format_term o prop_of
+
+fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) =
+ (case fst (strip_comb u) of
+ Const (c, _) => c
+ | _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t]))
+ | defining_const_of_equation_term t =
+ raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
+
+val defining_const_of_equation = defining_const_of_equation_term o prop_of
+
+(* Normalizing equations *)
+
+fun mk_meta_equation th =
+ case prop_of th of
+ Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
+ | _ => th
+
+fun full_fun_cong_expand th =
+ let
+ val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
+ val i = length (binder_types (fastype_of f)) - length args
+ in funpow i (fn th => th RS @{thm meta_fun_cong}) th end;
+
+fun declare_names s xs ctxt =
+ let
+ val res = Name.names ctxt s xs
+ in (res, fold Name.declare (map fst res) ctxt) end
+
+fun split_all_pairs thy th =
+ let
+ val ctxt = ProofContext.init thy
+ val ((_, [th']), ctxt') = Variable.import true [th] ctxt
+ val t = prop_of th'
+ val frees = Term.add_frees t []
+ val freenames = Term.add_free_names t []
+ val nctxt = Name.make_context freenames
+ fun mk_tuple_rewrites (x, T) nctxt =
+ let
+ val Ts = HOLogic.flatten_tupleT T
+ val (xTs, nctxt') = declare_names x Ts nctxt
+ val paths = HOLogic.flat_tupleT_paths T
+ in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
+ val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
+ val t' = Pattern.rewrite_term thy rewr [] t
+ val tac = SkipProof.cheat_tac thy
+ val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
+ val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
+ in
+ th'''
+ end;
+
+fun normalize_equation thy th =
+ mk_meta_equation th
+ |> Pred_Compile_Set.unfold_set_notation
+ |> full_fun_cong_expand
+ |> split_all_pairs thy
+ |> tap check_equation_format
+
+fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite
+((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
+
+fun store_thm_in_table ignore_consts thy th=
+ let
+ val th = AxClass.unoverload thy th
+ |> inline_equations thy
+ val (const, th) =
+ if is_equationlike th then
+ let
+ val _ = priority "Normalizing definition..."
+ val eq = normalize_equation thy th
+ in
+ (defining_const_of_equation eq, eq)
+ end
+ else if (is_introlike th) then
+ let val th = Pred_Compile_Set.unfold_set_notation th
+ in (defining_const_of_introrule th, th) end
+ else error "store_thm: unexpected definition format"
+ in
+ if not (member (op =) ignore_consts const) then
+ Symtab.cons_list (const, th)
+ else I
+ end
+
+(*
+fun make_const_spec_table_warning thy =
+ fold
+ (fn th => fn thy => case try (store_thm th) thy of
+ SOME thy => thy
+ | NONE => (warning ("store_thm fails for " ^ Display.string_of_thm_global thy th) ; thy))
+ (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
+
+fun make_const_spec_table thy =
+ fold store_thm (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
+ |> (fn thy => fold store_thm (Nitpick_Const_Simps.get (ProofContext.init thy)) thy)
+*)
+fun make_const_spec_table thy =
+ let
+ fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
+ val table = Symtab.empty
+ |> store [] Predicate_Compile_Alternative_Defs.get
+ val ignore_consts = Symtab.keys table
+ in
+ table
+ |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
+ |> store ignore_consts Nitpick_Const_Simps.get
+ |> store ignore_consts Nitpick_Ind_Intros.get
+ end
+ (*
+fun get_specification thy constname =
+ case Symtab.lookup (#const_spec_table (Data.get thy)) constname of
+ SOME thms => thms
+ | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
+ *)
+fun get_specification table constname =
+ case Symtab.lookup table constname of
+ SOME thms =>
+ let
+ val _ = tracing ("Looking up specification of " ^ constname ^ ": "
+ ^ (commas (map Display.string_of_thm_without_context thms)))
+ in thms end
+ | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
+
+val logic_operator_names =
+ [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "op &"}]
+
+val special_cases = member (op =) [@{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
+ @{const_name Nat.one_nat_inst.one_nat},
+@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
+@{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus},
+@{const_name "Nat.nat.nat_case"}, @{const_name "List.list.list_case"}, @{const_name Nat.ord_nat_inst.less_eq_nat}]
+
+fun obtain_specification_graph table constname =
+ let
+ fun is_nondefining_constname c = member (op =) logic_operator_names c
+ val is_defining_constname = member (op =) (Symtab.keys table)
+ fun defiants_of specs =
+ fold (Term.add_const_names o prop_of) specs []
+ |> filter is_defining_constname
+ |> filter_out special_cases
+ fun extend constname =
+ let
+ val specs = get_specification table constname
+ in (specs, defiants_of specs) end;
+ in
+ Graph.extend extend constname Graph.empty
+ end;
+
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Wed Sep 23 16:20:12 2009 +0200
@@ -0,0 +1,414 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Preprocessing functions to predicates
+*)
+
+signature PREDICATE_COMPILE_FUN =
+sig
+ val define_predicates : (string * thm list) list -> theory -> theory
+ val rewrite_intro : theory -> thm -> thm list
+ val setup_oracle : theory -> theory
+end;
+
+structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
+struct
+
+
+(* Oracle for preprocessing *)
+
+val (oracle : (string * (cterm -> thm)) option ref) = ref NONE;
+
+fun the_oracle () =
+ case !oracle of
+ NONE => error "Oracle is not setup"
+ | SOME (_, oracle) => oracle
+
+val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #->
+ (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end)
+
+
+fun is_funtype (Type ("fun", [_, _])) = true
+ | is_funtype _ = false;
+
+fun is_Type (Type _) = true
+ | is_Type _ = false
+
+(* returns true if t is an application of an datatype constructor *)
+(* which then consequently would be splitted *)
+(* else false *)
+(*
+fun is_constructor thy t =
+ if (is_Type (fastype_of t)) then
+ (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
+ NONE => false
+ | SOME info => (let
+ val constr_consts = flat (map (fn (_, (_, _, constrs)) => map fst constrs) (#descr info))
+ val (c, _) = strip_comb t
+ in (case c of
+ Const (name, _) => name mem_string constr_consts
+ | _ => false) end))
+ else false
+*)
+
+(* must be exported in code.ML *)
+fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
+
+(* Table from constant name (string) to term of inductive predicate *)
+structure Pred_Compile_Preproc = TheoryDataFun
+(
+ type T = string Symtab.table;
+ val empty = Symtab.empty;
+ val copy = I;
+ val extend = I;
+ fun merge _ = Symtab.merge (op =);
+)
+
+fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy)
+
+
+fun transform_ho_typ (T as Type ("fun", _)) =
+ let
+ val (Ts, T') = strip_type T
+ in (Ts @ [T']) ---> HOLogic.boolT end
+| transform_ho_typ t = t
+
+fun transform_ho_arg arg =
+ case (fastype_of arg) of
+ (T as Type ("fun", _)) => (* if T = bool might be a relation already *)
+ (case arg of
+ Free (name, _) => Free (name, transform_ho_typ T)
+ | _ => error "I am surprised")
+| _ => arg
+
+fun pred_type T =
+ let
+ val (Ts, T') = strip_type T
+ val Ts' = map transform_ho_typ Ts
+ in
+ (Ts' @ [T']) ---> HOLogic.boolT
+ end;
+
+(* FIXME: create new predicate name -- does not avoid nameclashing *)
+fun pred_of f =
+ let
+ val (name, T) = dest_Const f
+ in
+ if (body_type T = @{typ bool}) then
+ (Free (Long_Name.base_name name ^ "P", T))
+ else
+ (Free (Long_Name.base_name name ^ "P", pred_type T))
+ end
+
+fun mk_param lookup_pred (t as Free (v, _)) = lookup_pred t
+ | mk_param lookup_pred t =
+ let
+ val (vs, body) = strip_abs t
+ val names = Term.add_free_names body []
+ val vs_names = Name.variant_list names (map fst vs)
+ val vs' = map2 (curry Free) vs_names (map snd vs)
+ val body' = subst_bounds (rev vs', body)
+ val (f, args) = strip_comb body'
+ val resname = Name.variant (vs_names @ names) "res"
+ val resvar = Free (resname, body_type (fastype_of body'))
+ val P = lookup_pred f
+ val pred_body = list_comb (P, args @ [resvar])
+ val param = fold_rev lambda (vs' @ [resvar]) pred_body
+ in param end;
+
+
+(* creates the list of premises for every intro rule *)
+(* theory -> term -> (string list, term list list) *)
+
+fun dest_code_eqn eqn = let
+ val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn))
+ val (func, args) = strip_comb lhs
+in ((func, args), rhs) end;
+
+fun string_of_typ T = Syntax.string_of_typ_global @{theory} T
+
+fun string_of_term t =
+ case t of
+ Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")"
+ | Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")"
+ | Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")"
+ | Bound i => "Bound " ^ string_of_int i
+ | Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")"
+ | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
+
+fun ind_package_get_nparams thy name =
+ case try (Inductive.the_inductive (ProofContext.init thy)) name of
+ SOME (_, result) => length (Inductive.params_of (#raw_induct result))
+ | NONE => error ("No such predicate: " ^ quote name)
+
+(* TODO: does not work with higher order functions yet *)
+fun mk_rewr_eq (func, pred) =
+ let
+ val (argTs, resT) = (strip_type (fastype_of func))
+ val nctxt =
+ Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
+ val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
+ val ([resname], nctxt'') = Name.variants ["r"] nctxt'
+ val args = map Free (argnames ~~ argTs)
+ val res = Free (resname, resT)
+ in Logic.mk_equals
+ (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
+ end;
+
+fun has_split_rule_cname @{const_name "nat_case"} = true
+ | has_split_rule_cname @{const_name "list_case"} = true
+ | has_split_rule_cname _ = false
+
+fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true
+ | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true
+ | has_split_rule_term thy _ = false
+
+fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
+ | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
+ | has_split_rule_term' thy c = has_split_rule_term thy c
+
+fun prepare_split_thm ctxt split_thm =
+ (split_thm RS @{thm iffD2})
+ |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
+ @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
+
+fun find_split_thm thy (Const (name, typ)) =
+ let
+ fun split_name str =
+ case first_field "." str
+ of (SOME (field, rest)) => field :: split_name rest
+ | NONE => [str]
+ val splitted_name = split_name name
+ in
+ if length splitted_name > 0 andalso
+ String.isSuffix "_case" (List.last splitted_name)
+ then
+ (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
+ |> String.concatWith "."
+ |> PureThy.get_thm thy
+ |> SOME
+ handle ERROR msg => NONE
+ else NONE
+ end
+ | find_split_thm _ _ = NONE
+
+fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
+ | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
+ | find_split_thm' thy c = find_split_thm thy c
+
+fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
+
+fun folds_map f xs y =
+ let
+ fun folds_map' acc [] y = [(rev acc, y)]
+ | folds_map' acc (x :: xs) y =
+ maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y)
+ in
+ folds_map' [] xs y
+ end;
+
+fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) =
+ let
+ fun mk_prems' (t as Const (name, T)) (names, prems) =
+ [(lookup_pred t, (names, prems))]
+ | mk_prems' (t as Free (f, T)) (names, prems) =
+ [(lookup_pred t, (names, prems))]
+ | mk_prems' t (names, prems) =
+ if Predicate_Compile_Aux.is_constrt thy t then
+ [(t, (names, prems))]
+ else
+ if has_split_rule_term' thy (fst (strip_comb t)) then
+ let
+ val (f, args) = strip_comb t
+ val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
+ (* TODO: contextify things - this line is to unvarify the split_thm *)
+ (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
+ val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
+ val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
+ val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
+ val (_, split_args) = strip_comb split_t
+ val match = split_args ~~ args
+ fun mk_prems_of_assm assm =
+ let
+ val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
+ val var_names = Name.variant_list names (map fst vTs)
+ val vars = map Free (var_names ~~ (map snd vTs))
+ val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
+ val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
+ in
+ mk_prems' inner_t (var_names @ names, prems' @ prems)
+ end
+ in
+ maps mk_prems_of_assm assms
+ end
+ else
+ let
+ val (f, args) = strip_comb t
+ val resname = Name.variant names "res"
+ val resvar = Free (resname, body_type (fastype_of t))
+ val names' = resname :: names
+ fun mk_prems'' (t as Const (c, _)) =
+ if is_constr thy c then
+ folds_map mk_prems' args (names', prems) |>
+ map
+ (fn (argvs, (names'', prems')) =>
+ let
+ val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
+ in (names'', prem :: prems') end)
+ else
+ let
+ val pred = lookup_pred t
+ val nparams = get_nparams pred
+ val (params, args) = chop nparams args
+ val params' = map (mk_param lookup_pred) params
+ in
+ folds_map mk_prems' args (names', prems)
+ |> map (fn (argvs, (names'', prems')) =>
+ let
+ val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar]))
+ in (names'', prem :: prems') end)
+ end
+ | mk_prems'' (t as Free (_, _)) =
+ let
+ (* higher order argument call *)
+ val pred = lookup_pred t
+ in
+ folds_map mk_prems' args (resname :: names, prems)
+ |> map (fn (argvs, (names', prems')) =>
+ let
+ val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar]))
+ in (names', prem :: prems') end)
+ end
+ | mk_prems'' t = error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
+ in
+ map (pair resvar) (mk_prems'' f)
+ end
+ in
+ mk_prems' t (names, prems)
+ end;
+
+(* assumption: mutual recursive predicates all have the same parameters. *)
+fun define_predicates specs thy =
+ if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then
+ thy
+ else
+ let
+ val consts = map fst specs
+ val eqns = maps snd specs
+ (*val eqns = maps (Predicate_Compile_Preproc_Data.get_specification thy) consts*)
+ (* create prednames *)
+ val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
+ val argss' = map (map transform_ho_arg) argss
+ val pnames = map (dest_Free) (distinct (op =) (flat argss' \\ flat argss))
+ val preds = map pred_of funs
+ val prednames = map (fst o dest_Free) preds
+ val funnames = map (fst o dest_Const) funs
+ val fun_pred_names = (funnames ~~ prednames)
+ (* mapping from term (Free or Const) to term *)
+ fun lookup_pred (Const (@{const_name Cons}, T)) =
+ Const ("Preprocessing.ConsP", pred_type T) (* FIXME: temporary - Cons lookup *)
+ | lookup_pred (Const (name, T)) =
+ (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
+ SOME c => Const (c, pred_type T)
+ | NONE =>
+ (case AList.lookup op = fun_pred_names name of
+ SOME f => Free (f, pred_type T)
+ | NONE => Const (name, T)))
+ | lookup_pred (Free (name, T)) =
+ if member op = (map fst pnames) name then
+ Free (name, transform_ho_typ T)
+ else
+ Free (name, T)
+ | lookup_pred t =
+ error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t)
+
+ (* mapping from term (predicate term, not function term!) to int *)
+ fun get_nparams (Const (name, _)) =
+ the_default 0 (try (ind_package_get_nparams thy) name)
+ | get_nparams (Free (name, _)) =
+ (if member op = prednames name then
+ length pnames
+ else 0)
+ | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
+
+ (* create intro rules *)
+
+ fun mk_intros ((func, pred), (args, rhs)) =
+ if (body_type (fastype_of func) = @{typ bool}) then
+ (*TODO: preprocess predicate definition of rhs *)
+ [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
+ else
+ let
+ val names = Term.add_free_names rhs []
+ in mk_prems thy (lookup_pred, get_nparams) rhs (names, [])
+ |> map (fn (resultt, (names', prems)) =>
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
+ end
+ fun mk_rewr_thm (func, pred) = @{thm refl}
+
+ val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
+ val _ = map (tracing o (Syntax.string_of_term_global thy)) intr_ts
+ (* define new inductive predicates *)
+ val (ind_result, thy') =
+ Inductive.add_inductive_global (serial_string ())
+ {quiet_mode = false, verbose = false, kind = Thm.internalK,
+ alt_name = Binding.empty, coind = false, no_elim = false,
+ no_ind = false, skip_mono = false, fork_mono = false}
+ (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
+ pnames
+ (map (fn x => (Attrib.empty_binding, x)) intr_ts)
+ [] thy
+ val prednames = map (fst o dest_Const) (#preds ind_result)
+ (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
+ (* add constants to my table *)
+ val thy'' = thy'
+ |> Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames))
+ in
+ thy''
+ end
+
+(* preprocessing intro rules - uses oracle *)
+
+(* theory -> thm -> thm *)
+fun rewrite_intro thy intro =
+ let
+ fun lookup_pred (Const (name, T)) =
+ (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
+ SOME c => Const (c, pred_type T)
+ | NONE => Const (name, T))
+ | lookup_pred (Free (name, T)) = Free (name, T)
+ | lookup_pred _ = error "lookup function is not defined!"
+
+ fun get_nparams (Const (name, _)) =
+ the_default 0 (try (ind_package_get_nparams thy) name)
+ | get_nparams (Free _) = 0
+ | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
+
+ val intro_t = (Logic.unvarify o prop_of) intro
+ val _ = tracing (Syntax.string_of_term_global thy intro_t)
+ val (prems, concl) = Logic.strip_horn intro_t
+ val frees = map fst (Term.add_frees intro_t [])
+ fun opt_dest_Not t = the_default t (try HOLogic.dest_not t)
+ fun rewrite prem names =
+ let
+ val (P, args) = (strip_comb o opt_dest_Not o HOLogic.dest_Trueprop) prem
+ in
+ folds_map (
+ fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)])
+ else mk_prems thy (lookup_pred, get_nparams) t) args (names, [])
+ |> map (fn (resargs, (names', prems')) =>
+ let
+ val prem' = HOLogic.mk_Trueprop (list_comb (P, resargs))
+ in (prem'::prems', names') end)
+ end
+ val intro_ts' = folds_map rewrite prems frees
+ |> maps (fn (prems', frees') =>
+ rewrite concl frees'
+ |> map (fn (concl'::conclprems, _) =>
+ Logic.list_implies ((flat prems') @ conclprems, concl')))
+ val _ = Output.tracing ("intro_ts': " ^
+ commas (map (Syntax.string_of_term_global thy) intro_ts'))
+ in
+ map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
+ end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Wed Sep 23 16:20:12 2009 +0200
@@ -0,0 +1,131 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Preprocessing definitions of predicates to introduction rules
+*)
+
+signature PREDICATE_COMPILE_PRED =
+sig
+ (* preprocesses an equation to a set of intro rules; defines new constants *)
+ (*
+ val preprocess_pred_equation : thm -> theory -> thm list * theory
+ *)
+ val preprocess : string -> theory -> (thm list list * theory)
+ (* output is the term list of clauses of an unknown predicate *)
+ val preprocess_term : term -> theory -> (term list * theory)
+
+ (*val rewrite : thm -> thm*)
+
+end;
+(* : PREDICATE_COMPILE_PREPROC_PRED *)
+structure Predicate_Compile_Pred =
+struct
+
+open Predicate_Compile_Aux
+
+fun is_compound ((Const ("Not", _)) $ t) =
+ error "is_compound: Negation should not occur; preprocessing is defect"
+ | is_compound ((Const ("Ex", _)) $ _) = true
+ | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
+ | is_compound ((Const ("op &", _)) $ _ $ _) =
+ error "is_compound: Conjunction should not occur; preprocessing is defect"
+ | is_compound _ = false
+
+fun flatten constname atom (defs, thy) =
+ if is_compound atom then
+ let
+ val constname = Name.variant (map (Long_Name.base_name o fst) defs)
+ ((Long_Name.base_name constname) ^ "_aux")
+ val full_constname = Sign.full_bname thy constname
+ val (params, args) = List.partition (is_predT o fastype_of)
+ (map Free (Term.add_frees atom []))
+ val constT = map fastype_of (params @ args) ---> HOLogic.boolT
+ val lhs = list_comb (Const (full_constname, constT), params @ args)
+ val def = Logic.mk_equals (lhs, atom)
+ val ([definition], thy') = thy
+ |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+ |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+ in
+ (lhs, ((full_constname, [definition]) :: defs, thy'))
+ end
+ else
+ (atom, (defs, thy))
+
+fun flatten_intros constname intros thy =
+ let
+ val ctxt = ProofContext.init thy
+ val ((_, intros), ctxt') = Variable.import true intros ctxt
+ val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
+ (flatten constname) (map prop_of intros) ([], thy)
+ val tac = fn {...} => SkipProof.cheat_tac thy'
+ val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
+ |> Variable.export ctxt' ctxt
+ in
+ (intros'', (local_defs, thy'))
+ end
+
+(* TODO: same function occurs in inductive package *)
+fun select_disj 1 1 = []
+ | select_disj _ 1 = [rtac @{thm disjI1}]
+ | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1));
+
+fun introrulify thy th =
+ let
+ val ctxt = (ProofContext.init thy)
+ val ((_, [th']), ctxt') = Variable.import true [th] ctxt
+ val (lhs, rhs) = Logic.dest_equals (prop_of th')
+ val frees = Term.add_free_names rhs []
+ val disjuncts = HOLogic.dest_disj rhs
+ val nctxt = Name.make_context frees
+ fun mk_introrule t =
+ let
+ val ((ps, t'), nctxt') = focus_ex t nctxt
+ val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
+ in
+ (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
+ end
+ val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
+ Logic.dest_implies o prop_of) @{thm exI}
+ fun prove_introrule (index, (ps, introrule)) =
+ let
+ val tac = Simplifier.simp_tac (HOL_basic_ss addsimps [th]) 1
+ THEN EVERY1 (select_disj (length disjuncts) (index + 1))
+ THEN (EVERY (map (fn y =>
+ rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
+ THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
+ THEN TRY (atac 1)
+ in
+ Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac)
+ |> singleton (Variable.export ctxt' ctxt)
+ end
+ in
+ map_index prove_introrule (map mk_introrule disjuncts)
+ end;
+
+val rewrite =
+ Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}])
+ #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
+ #> Conv.fconv_rule nnf_conv
+ #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
+
+fun preprocess (constname, specs) thy =
+ let
+ val ctxt = ProofContext.init thy
+ val intros =
+ if forall is_pred_equation specs then
+ maps (introrulify thy o rewrite) specs
+ else if forall (is_intro constname) specs then
+ specs
+ else
+ error ("unexpected specification for constant " ^ quote constname ^ ":\n"
+ ^ commas (map (quote o Display.string_of_thm_global thy) specs))
+ val _ = priority "Defining local predicates and their intro rules..."
+ val (intros', (local_defs, thy')) = flatten_intros constname intros thy
+ val (intross, thy'') = fold_map preprocess local_defs thy'
+ in
+ (intros' :: flat intross,thy'')
+ end;
+
+fun preprocess_term t thy = error "preprocess_pred_term: to implement"
+
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Wed Sep 23 16:20:12 2009 +0200
@@ -0,0 +1,51 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Preprocessing sets to predicates
+*)
+
+signature PRED_COMPILE_SET =
+sig
+(*
+ val preprocess_intro : thm -> theory -> thm * theory
+ val preprocess_clause : term -> theory -> term * theory
+*)
+ val unfold_set_notation : thm -> thm;
+end;
+
+structure Pred_Compile_Set : PRED_COMPILE_SET =
+struct
+(*FIXME: unfolding Ball in pretty adhoc here *)
+val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, @{thm Ball_def}]
+
+val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
+
+(*
+fun find_set_theorems ctxt cname =
+ let
+ val _ = cname
+*)
+
+(*
+fun preprocess_term t ctxt =
+ case t of
+ Const ("op :", _) $ x $ A =>
+ case strip_comb A of
+ (Const (cname, T), params) =>
+ let
+ val _ = find_set_theorems
+ in
+ (t, ctxt)
+ end
+ | _ => (t, ctxt)
+ | _ => (t, ctxt)
+*)
+(*
+fun preprocess_intro th thy =
+ let
+ val cnames = find_heads_of_prems
+ val set_cname = filter (has_set_definition
+ val _ = define_preds
+ val _ = prep_pred_def
+ in
+*)
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Sep 23 16:20:12 2009 +0200
@@ -0,0 +1,75 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+*)
+signature PREDICATE_COMPILE =
+sig
+ val setup : theory -> theory
+end;
+
+structure Predicate_Compile : PREDICATE_COMPILE =
+struct
+
+open Predicate_Compile_Aux;
+
+val priority = tracing;
+
+(* Some last processing *)
+fun remove_pointless_clauses intro =
+ if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
+ []
+ else [intro]
+
+fun preprocess_strong_conn_constnames gr constnames thy =
+ let
+ val get_specs = map (fn k => (k, Graph.get_node gr k))
+ val _ = priority ("Preprocessing scc of " ^ commas constnames)
+ val (prednames, funnames) = List.partition (is_pred thy) constnames
+ (* untangle recursion by defining predicates for all functions *)
+ val _ = priority "Compiling functions to predicates..."
+ val _ = Output.tracing ("funnames: " ^ commas funnames)
+ val thy' =
+ thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates
+ (get_specs funnames)
+ val _ = priority "Compiling predicates to flat introrules..."
+ val (intross, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess
+ (get_specs prednames) thy')
+ val _ = tracing ("intross: " ^ commas (map (Display.string_of_thm_global thy'') (flat intross)))
+ val _ = priority "Replacing functions in introrules..."
+ val intross' = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross
+ val intross'' = burrow (maps remove_pointless_clauses) intross
+ val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy''
+ in
+ thy'''
+ end;
+
+fun code_pred_cmd ((inductify_all, rpred), raw_const) lthy =
+ if inductify_all then
+ let
+ val thy = ProofContext.theory_of lthy
+ val const = Code.read_const thy raw_const
+ val _ = Output.tracing ("fetching definition from theory")
+ val table = Pred_Compile_Data.make_const_spec_table thy
+ val gr = Pred_Compile_Data.obtain_specification_graph table const
+ val _ = Output.tracing (commas (Graph.all_succs gr [const]))
+ val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr
+ val lthy' = LocalTheory.theory (fold_rev (preprocess_strong_conn_constnames gr)
+ (Graph.strong_conn gr)) lthy
+ |> LocalTheory.checkpoint
+ in Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy' end
+ else
+ Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy
+
+val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
+
+val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred"]
+
+local structure P = OuterParse
+in
+
+val _ = OuterSyntax.local_theory_to_proof "code_pred"
+ "prove equations for predicate specified by intro/elim rules"
+ OuterKeyword.thy_goal (P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd)
+
+end
+
+end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 23 16:20:12 2009 +0200
@@ -6,11 +6,15 @@
signature PREDICATE_COMPILE_CORE =
sig
+ val setup: theory -> theory
+ val code_pred: bool -> string -> Proof.context -> Proof.state
+ val code_pred_cmd: bool -> string -> Proof.context -> Proof.state
type smode = (int * int list option) list
type mode = smode option list * smode
datatype tmode = Mode of mode * smode * tmode option list;
(*val add_equations_of: bool -> string list -> theory -> theory *)
val register_predicate : (thm list * thm * int) -> theory -> theory
+ val register_intros : thm list -> theory -> theory
val is_registered : theory -> string -> bool
(* val fetch_pred_data : theory -> string -> (thm list * thm * int) *)
val predfun_intro_of: theory -> string -> mode -> thm
@@ -24,9 +28,7 @@
val nparams_of: theory -> string -> int
val add_intro: thm -> theory -> theory
val set_elim: thm -> theory -> theory
- val setup: theory -> theory
- val code_pred: string -> Proof.context -> Proof.state
- val code_pred_cmd: string -> Proof.context -> Proof.state
+ val set_nparams : string -> int -> theory -> theory
val print_stored_rules: theory -> unit
val print_all_modes: theory -> unit
val do_proofs: bool ref
@@ -106,6 +108,7 @@
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
struct
+open Predicate_Compile_Aux;
(** auxiliary **)
(* debug stuff *)
@@ -187,7 +190,7 @@
(** data structures **)
-type smode = (int * int list option) list;
+type smode = (int * int list option) list
type mode = smode option list * smode;
datatype tmode = Mode of mode * smode * tmode option list;
@@ -238,7 +241,33 @@
"predmode: " ^ (string_of_mode predmode) ^
(if null param_modes then "" else
"; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))
+
+(* generation of case rules from user-given introduction rules *)
+
+fun mk_casesrule ctxt nparams introrules =
+ let
+ val intros = map (Logic.unvarify o prop_of) introrules
+ val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
+ val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
+ val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
+ val (argnames, ctxt2) = Variable.variant_fixes
+ (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
+ val argvs = map2 (curry Free) argnames (map fastype_of args)
+ fun mk_case intro =
+ let
+ val (_, (_, args)) = strip_intro_concl nparams intro
+ val prems = Logic.strip_imp_prems intro
+ val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
+ val frees = (fold o fold_aterms)
+ (fn t as Free _ =>
+ if member (op aconv) params t then I else insert (op aconv) t
+ | _ => I) (args @ prems) []
+ in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
+ val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
+ val cases = map mk_case intros
+ in Logic.list_implies (assm :: cases, prop) end;
+
datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
GeneratorPrem of term list * term | Generator of (string * typ);
@@ -579,9 +608,6 @@
| find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs;
in rev (find [] 0 xs) end;
-fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
- | is_predT _ = false
-
fun guess_nparams T =
let
val argTs = binder_types T
@@ -611,16 +637,28 @@
fun set (intros, elim, _ ) = (intros, elim, nparams)
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
-fun register_predicate (pre_intros, pre_elim, nparams) thy = let
+fun register_predicate (pre_intros, pre_elim, nparams) thy =
+ let
val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd pre_intros))))
(* preprocessing *)
val intros = ind_set_codegen_preproc thy (map (preprocess_intro thy) pre_intros)
val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim)
in
- PredData.map
+ if not (member (op =) (Graph.keys (PredData.get thy)) name) then
+ PredData.map
(Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy
+ else thy
end
+fun register_intros pre_intros thy =
+ let
+ val (_, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))
+ val nparams = guess_nparams T
+ val pre_elim =
+ (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
+ (mk_casesrule (ProofContext.init thy) nparams pre_intros)
+ in register_predicate (pre_intros, pre_elim, nparams) thy end
+
fun set_generator_name pred mode name =
let
val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE))
@@ -864,7 +902,7 @@
in merge (map (fn ks => i::ks) is) is end
else [[]];
-(* FIXME: should be in library - map_prod *)
+(* FIXME: should be in library - cprod = map_prod I *)
fun cprod ([], ys) = []
| cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
@@ -986,7 +1024,9 @@
(Generator (v, T), Mode (([], []), [], []))
end;
-fun gen_prem (Prem (us, t)) = GeneratorPrem (us, t)
+fun gen_prem (Prem (us, t)) = GeneratorPrem (us, t)
+ | gen_prem (Negprem (us, t)) = error "it is a negated prem"
+ | gen_prem (Sidecond t) = error "it is a sidecond"
| gen_prem _ = error "gen_prem : invalid input for gen_prem"
fun param_gen_prem param_vs (p as Prem (us, t as Free (v, _))) =
@@ -997,6 +1037,11 @@
fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
let
+ (*
+ val _ = Output.tracing ("param_vs:" ^ commas param_vs)
+ val _ = Output.tracing ("iss:" ^
+ commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss))
+ *)
val modes' = modes @ List.mapPartial
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
(param_vs ~~ iss);
@@ -1010,7 +1055,7 @@
NONE =>
(if with_generator then
(case select_mode_prem thy gen_modes' vs ps of
- SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps)
+ SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps)
(case p of Prem (us, _) => vs union terms_vs us | _ => vs)
(filter_out (equal p) ps)
| NONE =>
@@ -1021,7 +1066,10 @@
(select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
(vs union generator_vs) ps
- | NONE => NONE
+ | NONE => let
+ val _ = Output.tracing ("ps:" ^ (commas
+ (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
+ in error "mode analysis failed" end
end)
else
NONE)
@@ -1493,9 +1541,6 @@
val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
- val _ = Output.tracing (Display.string_of_thm_global thy elimthm)
- val _ = Output.tracing (Display.string_of_thm_global thy introthm)
-
in
(introthm, elimthm)
end;
@@ -1609,13 +1654,11 @@
(list_comb (Const (name, T), xparams' @ xargs)))
val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
val def = Logic.mk_equals (lhs, predterm)
- val _ = Output.tracing ("def:" ^ (Syntax.string_of_term_global thy def))
val ([definition], thy') = thy |>
Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
val (intro, elim) =
create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
- val _ = Output.tracing (Display.string_of_thm_global thy' definition)
in thy'
|> add_predfun name mode (mode_cname, definition, intro, elim)
|> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
@@ -2120,7 +2163,8 @@
case HOLogic.strip_tupleT U of
[] => [(i + 1, NONE)]
| [U] => [(i + 1, NONE)]
- | Us => map (pair (i + 1) o SOME) ((subsets 1 (length Us)) \\ [[], 1 upto (length Us)]))
+ | Us => (i + 1, NONE) ::
+ (map (pair (i + 1) o SOME) ((subsets 1 (length Us)) \\ [[], 1 upto (length Us)])))
Ts)
in
cprod (cprods (map (fn T => case strip_type T of
@@ -2220,41 +2264,30 @@
(** user interface **)
-(* generation of case rules from user-given introduction rules *)
-
-fun mk_casesrule ctxt nparams introrules =
- let
- val intros = map (Logic.unvarify o prop_of) introrules
- val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
- val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
- val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
- val (argnames, ctxt2) = Variable.variant_fixes
- (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
- val argvs = map2 (curry Free) argnames (map fastype_of args)
- fun mk_case intro =
- let
- val (_, (_, args)) = strip_intro_concl nparams intro
- val prems = Logic.strip_imp_prems intro
- val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
- val frees = (fold o fold_aterms)
- (fn t as Free _ =>
- if member (op aconv) params t then I else insert (op aconv) t
- | _ => I) (args @ prems) []
- in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
- val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
- val cases = map mk_case intros
- in Logic.list_implies (assm :: cases, prop) end;
-
(* code_pred_intro attribute *)
fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
val code_pred_intros_attrib = attrib add_intro;
-local
+
+(*FIXME
+- Naming of auxiliary rules necessary?
+- add default code equations P x y z = P_i_i_i x y z
+*)
+
+val setup = PredData.put (Graph.empty) #>
+ Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
+ "adding alternative introduction rules for code generation of inductive predicates"
+(* Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
+ "adding alternative elimination rules for code generation of inductive predicates";
+ *)
+ (*FIXME name discrepancy in attribs and ML code*)
+ (*FIXME intros should be better named intro*)
+ (*FIXME why distinguished attribute for cases?*)
(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
-fun generic_code_pred prep_const raw_const lthy =
+fun generic_code_pred prep_const rpred raw_const lthy =
let
val thy = ProofContext.theory_of lthy
val const = prep_const thy raw_const
@@ -2282,40 +2315,18 @@
val global_thms = ProofContext.export goal_ctxt
(ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
in
- goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> add_equations [const])
+ goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
+ (if rpred then
+ (add_sizelim_equations [const] #> add_quickcheck_equations [const])
+ else add_equations [const]))
end
in
Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
end;
-structure P = OuterParse
-
-in
-
val code_pred = generic_code_pred (K I);
val code_pred_cmd = generic_code_pred Code.read_const
-val setup = PredData.put (Graph.empty) #>
- Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
- "adding alternative introduction rules for code generation of inductive predicates"
-(* Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
- "adding alternative elimination rules for code generation of inductive predicates";
- *)
- (*FIXME name discrepancy in attribs and ML code*)
- (*FIXME intros should be better named intro*)
- (*FIXME why distinguished attribute for cases?*)
-
-val _ = OuterSyntax.local_theory_to_proof "code_pred"
- "prove equations for predicate specified by intro/elim rules"
- OuterKeyword.thy_goal (P.term_group >> code_pred_cmd)
-
-end
-
-(*FIXME
-- Naming of auxiliary rules necessary?
-- add default code equations P x y z = P_i_i_i x y z
-*)
-
(* transformation for code generation *)
val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
@@ -2342,7 +2353,8 @@
^ Syntax.string_of_term_global thy t_compr); m);
val (inargs, outargs) = split_smode user_mode' args;
val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs);
- val t_eval = if null outargs then t_pred else let
+ val t_eval = if null outargs then t_pred else
+ let
val outargs_bounds = map (fn Bound i => i) outargs;
val outargsTs = map (nth Ts) outargs_bounds;
val T_pred = HOLogic.mk_tupleT outargsTs;
@@ -2361,7 +2373,7 @@
val t = analyze_compr thy t_compr;
val T = dest_predT PredicateCompFuns.compfuns (fastype_of t);
val t' = mk_map PredicateCompFuns.compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
- in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
+ in (T, Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []) end;
fun values ctxt k t_compr =
let
--- a/src/HOL/ex/Predicate_Compile.thy Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy Wed Sep 23 16:20:12 2009 +0200
@@ -1,6 +1,13 @@
theory Predicate_Compile
imports Complex_Main RPred
-uses "../Tools/Predicate_Compile/predicate_compile_core.ML"
+uses
+ "../Tools/Predicate_Compile/pred_compile_aux.ML"
+ "../Tools/Predicate_Compile/predicate_compile_core.ML"
+ "../Tools/Predicate_Compile/pred_compile_set.ML"
+ "../Tools/Predicate_Compile/pred_compile_data.ML"
+ "../Tools/Predicate_Compile/pred_compile_fun.ML"
+ "../Tools/Predicate_Compile/pred_compile_pred.ML"
+ "../Tools/Predicate_Compile/predicate_compile.ML"
begin
setup {* Predicate_Compile.setup *}
--- a/src/HOL/ex/Predicate_Compile_ex.thy Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed Sep 23 16:20:12 2009 +0200
@@ -22,8 +22,10 @@
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
code_pred append .
+code_pred (inductify_all) (rpred) append .
thm append.equation
+thm append.rpred_equation
values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
@@ -44,11 +46,27 @@
"partition f [] [] []"
| "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
-ML {* set Toplevel.debug *}
+
code_pred partition .
thm partition.equation
+
+inductive member
+for xs
+where "x \<in> set xs ==> member xs x"
+
+lemma [code_pred_intros]:
+ "member (x#xs') x"
+by (auto intro: member.intros)
+
+lemma [code_pred_intros]:
+"member xs x ==> member (x'#xs) x"
+by (auto intro: member.intros elim!: member.cases)
+(* strange bug must be repaired! *)
+(*
+code_pred member sorry
+*)
inductive is_even :: "nat \<Rightarrow> bool"
where
"n mod 2 = 0 \<Longrightarrow> is_even n"
@@ -71,13 +89,9 @@
from this converse_tranclpE[OF this(1)] show thesis by metis
qed
+code_pred (inductify_all) (rpred) tranclp .
thm tranclp.equation
-(*
-setup {* Predicate_Compile.add_sizelim_equations [@{const_name tranclp}] *}
-setup {* fn thy => exception_trace (fn () => Predicate_Compile.add_quickcheck_equations [@{const_name tranclp}] thy) *}
-
thm tranclp.rpred_equation
-*)
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
@@ -157,6 +171,7 @@
values 3 "{(a,q). step (par nil nil) a q}"
*)
+subsection {* divmod *}
inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"k < l \<Longrightarrow> divmod_rel k l 0 k"
@@ -166,4 +181,75 @@
value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
+subsection {* Executing definitions *}
+
+definition Min
+where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
+
+code_pred (inductify_all) Min .
+
+code_pred (inductify_all) lexord .
+
+thm lexord.equation
+
+
+lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
+
+code_pred (inductify_all) lexn .
+thm lexn.equation
+
+code_pred (inductify_all) lenlex .
+thm lenlex.equation
+(*
+code_pred (inductify_all) (rpred) lenlex .
+thm lenlex.rpred_equation
+*)
+
+datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
+fun height :: "'a tree => nat" where
+"height ET = 0"
+| "height (MKT x l r h) = max (height l) (height r) + 1"
+
+consts avl :: "'a tree => bool"
+primrec
+ "avl ET = True"
+ "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
+ h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
+
+code_pred (inductify_all) avl .
+thm avl.equation
+
+fun set_of
+where
+"set_of ET = {}"
+| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
+
+fun is_ord
+where
+"is_ord ET = True"
+| "is_ord (MKT n l r h) =
+ ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
+
+declare Un_def[code_pred_def]
+
+lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\<lambda>(y::'a::type). False)"
+unfolding bot_fun_inst.bot_fun[symmetric]
+unfolding bot_bool_eq[symmetric]
+unfolding bot_fun_eq by simp
+
+code_pred (inductify_all) set_of .
+thm set_of.equation
+
+code_pred (inductify_all) is_ord .
+thm is_ord.equation
+
+section {* Definitions about Relations *}
+
+code_pred (inductify_all) converse .
+thm converse.equation
+
+code_pred (inductify_all) Domain .
+thm Domain.equation
+
+
end
\ No newline at end of file