# HG changeset patch # User bulwahn # Date 1253715612 -7200 # Node ID b2de450075379800c8cfc5b6c2a69b651f95ac63 # Parent 09546e6542224fbf29a80686d0c1d88a3f1b1b96 added first prototype of the extended predicate compiler diff -r 09546e654222 -r b2de45007537 src/HOL/HOL.thy --- 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 *} diff -r 09546e654222 -r b2de45007537 src/HOL/Predicate.thy --- 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 diff -r 09546e654222 -r b2de45007537 src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML --- /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; diff -r 09546e654222 -r b2de45007537 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- /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; diff -r 09546e654222 -r b2de45007537 src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML --- /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; diff -r 09546e654222 -r b2de45007537 src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML --- /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; diff -r 09546e654222 -r b2de45007537 src/HOL/Tools/Predicate_Compile/pred_compile_set.ML --- /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; diff -r 09546e654222 -r b2de45007537 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- /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 diff -r 09546e654222 -r b2de45007537 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 09546e654222 -r b2de45007537 src/HOL/ex/Predicate_Compile.thy --- 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 *} diff -r 09546e654222 -r b2de45007537 src/HOL/ex/Predicate_Compile_ex.thy --- 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 \ 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 \ partition f xs ys zs \ partition f (x # xs) (x # ys) zs" | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" -ML {* set Toplevel.debug *} + code_pred partition . thm partition.equation + +inductive member +for xs +where "x \ 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 \ bool" where "n mod 2 = 0 \ 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 \ nat \ 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 \ nat \ nat \ nat \ bool" where "k < l \ 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 \ s x \ (\y. r x y \ 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 \ height l = 1 + height r \ height r = 1+height l) \ + h = max (height l) (height r) + 1 \ avl l \ 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 \ set_of r)" + +fun is_ord +where +"is_ord ET = True" +| "is_ord (MKT n l r h) = + ((\n' \ set_of l. n' < n) \ (\n' \ set_of r. n < n') \ is_ord l \ is_ord r)" + +declare Un_def[code_pred_def] + +lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\(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