# HG changeset patch # User wenzelm # Date 1256422225 -7200 # Node ID b8f4c2107a6214886b099a9920ab624a37cadee1 # Parent 9d7d0bef2a777ddffbfe7c1e55387cee88fd81a2# Parent 75eddea4abefe3e5d77dd90c510fe108a8ec731b merged diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/Predicate.thy Sun Oct 25 00:10:25 2009 +0200 @@ -471,49 +471,49 @@ "is_empty (A \ B) \ is_empty A \ is_empty B" by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2) -definition singleton :: "'a pred \ 'a" where - "singleton A = (if \!x. eval A x then THE x. eval A x else undefined)" +definition singleton :: "(unit => 'a) \ 'a pred \ 'a" where + "singleton dfault A = (if \!x. eval A x then THE x. eval A x else dfault ())" lemma singleton_eqI: - "\!x. eval A x \ eval A x \ singleton A = x" + "\!x. eval A x \ eval A x \ singleton dfault A = x" by (auto simp add: singleton_def) lemma eval_singletonI: - "\!x. eval A x \ eval A (singleton A)" + "\!x. eval A x \ eval A (singleton dfault A)" proof - assume assm: "\!x. eval A x" then obtain x where "eval A x" .. - moreover with assm have "singleton A = x" by (rule singleton_eqI) + moreover with assm have "singleton dfault A = x" by (rule singleton_eqI) ultimately show ?thesis by simp qed lemma single_singleton: - "\!x. eval A x \ single (singleton A) = A" + "\!x. eval A x \ single (singleton dfault A) = A" proof - assume assm: "\!x. eval A x" - then have "eval A (singleton A)" + then have "eval A (singleton dfault A)" by (rule eval_singletonI) - moreover from assm have "\x. eval A x \ singleton A = x" + moreover from assm have "\x. eval A x \ singleton dfault A = x" by (rule singleton_eqI) - ultimately have "eval (single (singleton A)) = eval A" + ultimately have "eval (single (singleton dfault A)) = eval A" by (simp (no_asm_use) add: single_def expand_fun_eq) blast then show ?thesis by (simp add: eval_inject) qed lemma singleton_undefinedI: - "\ (\!x. eval A x) \ singleton A = undefined" + "\ (\!x. eval A x) \ singleton dfault A = dfault ()" by (simp add: singleton_def) lemma singleton_bot: - "singleton \ = undefined" + "singleton dfault \ = dfault ()" by (auto simp add: bot_pred_def intro: singleton_undefinedI) lemma singleton_single: - "singleton (single x) = x" + "singleton dfault (single x) = x" by (auto simp add: intro: singleton_eqI singleI elim: singleE) lemma singleton_sup_single_single: - "singleton (single x \ single y) = (if x = y then x else undefined)" + "singleton dfault (single x \ single y) = (if x = y then x else dfault ())" proof (cases "x = y") case True then show ?thesis by (simp add: singleton_single) next @@ -523,25 +523,25 @@ by (auto intro: supI1 supI2 singleI) with False have "\ (\!z. eval (single x \ single y) z)" by blast - then have "singleton (single x \ single y) = undefined" + then have "singleton dfault (single x \ single y) = dfault ()" by (rule singleton_undefinedI) with False show ?thesis by simp qed lemma singleton_sup_aux: - "singleton (A \ B) = (if A = \ then singleton B - else if B = \ then singleton A - else singleton - (single (singleton A) \ single (singleton B)))" + "singleton dfault (A \ B) = (if A = \ then singleton dfault B + else if B = \ then singleton dfault A + else singleton dfault + (single (singleton dfault A) \ single (singleton dfault B)))" proof (cases "(\!x. eval A x) \ (\!y. eval B y)") case True then show ?thesis by (simp add: single_singleton) next case False from False have A_or_B: - "singleton A = undefined \ singleton B = undefined" + "singleton dfault A = dfault () \ singleton dfault B = dfault ()" by (auto intro!: singleton_undefinedI) - then have rhs: "singleton - (single (singleton A) \ single (singleton B)) = undefined" + then have rhs: "singleton dfault + (single (singleton dfault A) \ single (singleton dfault B)) = dfault ()" by (auto simp add: singleton_sup_single_single singleton_single) from False have not_unique: "\ (\!x. eval A x) \ \ (\!y. eval B y)" by simp @@ -551,7 +551,7 @@ by (blast elim: not_bot) with True not_unique have "\ (\!x. eval (A \ B) x)" by (auto simp add: sup_pred_def bot_pred_def) - then have "singleton (A \ B) = undefined" by (rule singleton_undefinedI) + then have "singleton dfault (A \ B) = dfault ()" by (rule singleton_undefinedI) with True rhs show ?thesis by simp next case False then show ?thesis by auto @@ -559,10 +559,10 @@ qed lemma singleton_sup: - "singleton (A \ B) = (if A = \ then singleton B - else if B = \ then singleton A - else if singleton A = singleton B then singleton A else undefined)" -using singleton_sup_aux [of A B] by (simp only: singleton_sup_single_single) + "singleton dfault (A \ B) = (if A = \ then singleton dfault B + else if B = \ then singleton dfault A + else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())" +using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single) subsubsection {* Derived operations *} @@ -743,36 +743,43 @@ "is_empty (Seq f) \ null (f ())" by (simp add: null_is_empty Seq_def) -primrec the_only :: "'a seq \ 'a" where - [code del]: "the_only Empty = undefined" - | "the_only (Insert x P) = (if is_empty P then x else let y = singleton P in if x = y then x else undefined)" - | "the_only (Join P xq) = (if is_empty P then the_only xq else if null xq then singleton P - else let x = singleton P; y = the_only xq in - if x = y then x else undefined)" +primrec the_only :: "(unit \ 'a) \ 'a seq \ 'a" where + [code del]: "the_only dfault Empty = dfault ()" + | "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())" + | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P + else let x = singleton dfault P; y = the_only dfault xq in + if x = y then x else dfault ())" lemma the_only_singleton: - "the_only xq = singleton (pred_of_seq xq)" + "the_only dfault xq = singleton dfault (pred_of_seq xq)" by (induct xq) (auto simp add: singleton_bot singleton_single is_empty_def null_is_empty Let_def singleton_sup) lemma singleton_code [code]: - "singleton (Seq f) = (case f () - of Empty \ undefined + "singleton dfault (Seq f) = (case f () + of Empty \ dfault () | Insert x P \ if is_empty P then x - else let y = singleton P in - if x = y then x else undefined - | Join P xq \ if is_empty P then the_only xq - else if null xq then singleton P - else let x = singleton P; y = the_only xq in - if x = y then x else undefined)" + else let y = singleton dfault P in + if x = y then x else dfault () + | Join P xq \ if is_empty P then the_only dfault xq + else if null xq then singleton dfault P + else let x = singleton dfault P; y = the_only dfault xq in + if x = y then x else dfault ())" by (cases "f ()") (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 +definition not_unique :: "'a pred => 'a" +where + [code del]: "not_unique A = (THE x. eval A x)" + +definition the :: "'a pred => 'a" +where + [code del]: "the A = (THE x. eval A x)" + +lemma the_eq[code]: "the A = singleton (\x. not_unique A) A" +by (auto simp add: the_def singleton_def not_unique_def) ML {* signature PREDICATE = @@ -819,6 +826,8 @@ code_const Seq and Empty and Insert and Join (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)") +code_abort not_unique + text {* dummy setup for @{text code_pred} and @{text values} keywords *} ML {* @@ -852,6 +861,6 @@ hide (open) type pred seq hide (open) const Pred eval single bind is_empty singleton if_pred not_pred - Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map + Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the end diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sun Oct 25 00:10:25 2009 +0200 @@ -6,8 +6,16 @@ structure Predicate_Compile_Aux = struct +(* general syntactic functions *) + +(*Like dest_conj, but flattens conjunctions however nested*) +fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs) + | conjuncts_aux t conjs = t::conjs; + +fun conjuncts t = conjuncts_aux t []; + (* syntactic functions *) - + fun is_equationlike_term (Const ("==", _) $ _ $ _) = true | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true | is_equationlike_term _ = false @@ -69,26 +77,52 @@ in ((ps', t''), nctxt') end; +(* introduction rule combinators *) +(* combinators to apply a function to all literals of an introduction rules *) -(* fun map_atoms f intro = -fun fold_atoms f intro = -*) + let + val (literals, head) = Logic.strip_horn intro + fun appl t = (case t of + (@{term "Not"} $ t') => HOLogic.mk_not (f t') + | _ => f t) + in + Logic.list_implies + (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head) + end + +fun fold_atoms f intro s = + let + val (literals, head) = Logic.strip_horn intro + fun appl t s = (case t of + (@{term "Not"} $ t') => f t' s + | _ => f t s) + in fold appl (map HOLogic.dest_Trueprop literals) s end + 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 + (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s) | _ => 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 maps_premises f intro = + let + val (premises, head) = Logic.strip_horn intro + in + Logic.list_implies (maps f premises, head) + end +(* lifting term operations to theorems *) + +fun map_term thy f th = + Skip_Proof.make_thm thy (f (prop_of th)) + (* fun equals_conv lhs_cv rhs_cv ct = case Thm.term_of ct of @@ -96,5 +130,107 @@ | _ => error "equals_conv" *) +(* Different options for compiler *) + +datatype options = Options of { + expected_modes : (string * int list list) option, + show_steps : bool, + show_mode_inference : bool, + show_proof_trace : bool, + show_intermediate_results : bool, + show_compilation : bool, + skip_proof : bool, + + inductify : bool, + rpred : bool, + depth_limited : bool +}; + +fun expected_modes (Options opt) = #expected_modes opt +fun show_steps (Options opt) = #show_steps opt +fun show_mode_inference (Options opt) = #show_mode_inference opt +fun show_intermediate_results (Options opt) = #show_intermediate_results opt +fun show_proof_trace (Options opt) = #show_proof_trace opt +fun show_compilation (Options opt) = #show_compilation opt +fun skip_proof (Options opt) = #skip_proof opt + +fun is_inductify (Options opt) = #inductify opt +fun is_rpred (Options opt) = #rpred opt +fun is_depth_limited (Options opt) = #depth_limited opt + +val default_options = Options { + expected_modes = NONE, + show_steps = false, + show_intermediate_results = false, + show_proof_trace = false, + show_mode_inference = false, + show_compilation = false, + skip_proof = false, + + inductify = false, + rpred = false, + depth_limited = false +} + + +fun print_step options s = + if show_steps options then tracing s else () + +(* tuple processing *) + +fun expand_tuples thy intro = + let + fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) + | rewrite_args (arg::args) (pats, intro_t, ctxt) = + (case HOLogic.strip_tupleT (fastype_of arg) of + (Ts as _ :: _ :: _) => + let + fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2])) + (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) + | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) = + let + val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt + val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) + val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t + val args' = map (Pattern.rewrite_term thy [pat] []) args + in + rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt')) + end + | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt)) + val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg) + (args, (pats, intro_t, ctxt)) + in + rewrite_args args' (pats, intro_t', ctxt') + end + | _ => rewrite_args args (pats, intro_t, ctxt)) + fun rewrite_prem atom = + let + val (_, args) = strip_comb atom + in rewrite_args args end + val ctxt = ProofContext.init thy + val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt + val intro_t = prop_of intro' + val concl = Logic.strip_imp_concl intro_t + val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) + val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) + val (pats', intro_t', ctxt3) = + fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) + fun rewrite_pat (ct1, ct2) = + (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2))) + val t_insts' = map rewrite_pat t_insts + val intro'' = Thm.instantiate (T_insts, t_insts') intro + val [intro'''] = Variable.export ctxt3 ctxt [intro''] + val intro'''' = Simplifier.full_simplify + (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) + intro''' + (* splitting conjunctions introduced by Pair_eq*) + fun split_conj prem = + map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem)) + val intro''''' = map_term thy (maps_premises split_conj) intro'''' + in + intro''''' + end + + end; diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sun Oct 25 00:10:25 2009 +0200 @@ -3,16 +3,16 @@ Book-keeping datastructure for the predicate compiler *) -signature PRED_COMPILE_DATA = +signature PREDICATE_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 obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T val normalize_equation : theory -> thm -> thm end; -structure Pred_Compile_Data : PRED_COMPILE_DATA = +structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA = struct open Predicate_Compile_Aux; @@ -81,11 +81,13 @@ Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection} | _ => th +val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp} + 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; + in funpow i (fn th => th RS meta_fun_cong) th end; fun declare_names s xs ctxt = let @@ -117,7 +119,7 @@ fun normalize_equation thy th = mk_meta_equation th - |> Pred_Compile_Set.unfold_set_notation + |> Predicate_Compile_Set.unfold_set_notation |> full_fun_cong_expand |> split_all_pairs thy |> tap check_equation_format @@ -127,19 +129,18 @@ fun store_thm_in_table ignore_consts thy th= let - val th = AxClass.unoverload thy th + val th = th |> inline_equations thy + |> Predicate_Compile_Set.unfold_set_notation + |> AxClass.unoverload 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 if (is_introlike th) then (defining_const_of_introrule th, th) else error "store_thm: unexpected definition format" in if not (member (op =) ignore_consts const) then @@ -147,18 +148,6 @@ 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_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))) @@ -166,35 +155,27 @@ |> store [] Predicate_Compile_Alternative_Defs.get val ignore_consts = Symtab.keys table in - table + table |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get |> store ignore_consts Nitpick_Simps.get |> store ignore_consts Nitpick_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 + SOME thms => thms | 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 &"}] + [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"}, + @{const_name "op &"}] -val special_cases = member (op =) [@{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat}, +val special_cases = member (op =) [ + @{const_name "False"}, + @{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 "Option.option.option_case"}, @{const_name Nat.ord_nat_inst.less_eq_nat}, @{const_name number_nat_inst.number_of_nat}, @{const_name Int.Bit0}, @@ -203,13 +184,19 @@ @{const_name "Int.zero_int_inst.zero_int"}, @{const_name "List.filter"}] -fun obtain_specification_graph table constname = +fun case_consts thy s = is_some (Datatype.info_of_case thy s) + +fun obtain_specification_graph thy table constname = let fun is_nondefining_constname c = member (op =) logic_operator_names c val is_defining_constname = member (op =) (Symtab.keys table) + fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c) fun defiants_of specs = fold (Term.add_const_names o prop_of) specs [] |> filter is_defining_constname + |> filter_out is_nondefining_constname + |> filter_out has_code_pred_intros + |> filter_out (case_consts thy) |> filter_out special_cases fun extend constname = let diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sun Oct 25 00:10:25 2009 +0200 @@ -5,9 +5,10 @@ signature PREDICATE_COMPILE_FUN = sig - val define_predicates : (string * thm list) list -> theory -> theory +val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory val rewrite_intro : theory -> thm -> thm list val setup_oracle : theory -> theory + val pred_of_function : theory -> string -> string option end; structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN = @@ -63,6 +64,8 @@ fun merge _ = Symtab.merge (op =); ) +fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name + fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) @@ -99,23 +102,29 @@ (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 = +fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t + | mk_param thy 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; - - + val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t)) + in if Predicate_Compile_Aux.is_predT (fastype_of t) then + t + else + 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 = case try lookup_pred f of SOME P => P | NONE => error "mk_param" + val pred_body = list_comb (P, args @ [resvar]) + *) + val pred_body = HOLogic.mk_eq (body', resvar) + val param = fold_rev lambda (vs' @ [resvar]) pred_body + in param end + end (* creates the list of premises for every intro rule *) (* theory -> term -> (string list, term list list) *) @@ -210,10 +219,14 @@ let fun mk_prems' (t as Const (name, T)) (names, prems) = if is_constr thy name orelse (is_none (try lookup_pred t)) then - [(t ,(names, prems))] + [(t, (names, prems))] else [(lookup_pred t, (names, prems))] | mk_prems' (t as Free (f, T)) (names, prems) = [(lookup_pred t, (names, prems))] + | mk_prems' (t as Abs _) (names, prems) = + if Predicate_Compile_Aux.is_predT (fastype_of t) then + [(t, (names, prems))] else error "mk_prems': Abs " + (* mk_param *) | mk_prems' t (names, prems) = if Predicate_Compile_Aux.is_constrt thy t then [(t, (names, prems))] @@ -243,8 +256,10 @@ maps mk_prems_of_assm assms end else - let + let val (f, args) = strip_comb t + (* TODO: special procedure for higher-order functions: split arguments in + simple types and function types *) val resname = Name.variant names "res" val resvar = Free (resname, body_type (fastype_of t)) val names' = resname :: names @@ -261,8 +276,7 @@ val pred = lookup_pred t val nparams = get_nparams pred val (params, args) = chop nparams args - val _ = tracing ("mk_prems'': " ^ (Syntax.string_of_term_global thy t) ^ " has " ^ string_of_int nparams ^ " parameters.") - val params' = map (mk_param lookup_pred) params + val params' = map (mk_param thy lookup_pred) params in folds_map mk_prems' args (names', prems) |> map (fn (argvs, (names'', prems')) => @@ -281,7 +295,8 @@ 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) + | mk_prems'' t = + error ("Invalid term: " ^ Syntax.string_of_term_global thy t) in map (pair resvar) (mk_prems'' f) end @@ -292,7 +307,7 @@ (* 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 + ([], thy) else let val consts = map fst specs @@ -307,16 +322,14 @@ 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)) = + fun 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)) = + | lookup_pred (Free (name, T)) = if member op = (map fst pnames) name then Free (name, transform_ho_typ T) else @@ -347,12 +360,10 @@ Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) end fun mk_rewr_thm (func, pred) = @{thm refl} - in + in case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of - NONE => thy - | SOME intr_ts => let - val _ = map (tracing o (Syntax.string_of_term_global thy)) intr_ts - in + NONE => ([], thy) + | SOME intr_ts => if is_some (try (map (cterm_of thy)) intr_ts) then let val (ind_result, thy') = @@ -367,10 +378,15 @@ 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 *) - in Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy' end + val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) (#intrs ind_result))) prednames + val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy' + in + (specs, thy'') + end else - thy - end + let + val _ = tracing "Introduction rules of function_predicate are not welltyped" + in ([], thy) end end (* preprocessing intro rules - uses oracle *) @@ -391,7 +407,6 @@ | 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 rewrite prem names = @@ -415,8 +430,6 @@ rewrite concl frees' |> map (fn (concl'::conclprems, _) => Logic.list_implies ((flat prems') @ conclprems, concl'))) - val _ = 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; diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sun Oct 25 00:10:25 2009 +0200 @@ -123,16 +123,67 @@ else error ("unexpected specification for constant " ^ quote constname ^ ":\n" ^ commas (map (quote o Display.string_of_thm_global thy) specs)) - val _ = tracing ("Introduction rules of definitions before flattening: " - ^ commas (map (Display.string_of_thm ctxt) intros)) - val _ = tracing "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'') + ((constname, intros') :: flat intross,thy'') end; fun preprocess_term t thy = error "preprocess_pred_term: to implement" - - + +fun is_Abs (Abs _) = true + | is_Abs _ = false + +fun flat_higher_order_arguments (intross, thy) = + let + fun process constname atom (new_defs, thy) = + let + val (pred, args) = strip_comb atom + val abs_args = filter is_Abs args + fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) = + let + val _ = tracing ("Introduce new constant for " ^ + Syntax.string_of_term_global thy abs_arg) + val vars = map Var (Term.add_vars abs_arg []) + val abs_arg' = Logic.unvarify abs_arg + val frees = map Free (Term.add_frees abs_arg' []) + val constname = Name.variant (map (Long_Name.base_name o fst) new_defs) + ((Long_Name.base_name constname) ^ "_hoaux") + val full_constname = Sign.full_bname thy constname + val constT = map fastype_of frees ---> (fastype_of abs_arg') + val const = Const (full_constname, constT) + val lhs = list_comb (const, frees) + val def = Logic.mk_equals (lhs, abs_arg') + val _ = tracing (Syntax.string_of_term_global thy def) + val ([definition], thy') = thy + |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] + |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])] + in + (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy')) + end + | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy)) + val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy) + in + (list_comb (pred, args'), (new_defs', thy')) + end + fun flat_intro intro (new_defs, thy) = + let + val constname = fst (dest_Const (fst (strip_comb + (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro)))))) + val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy) + val th = Skip_Proof.make_thm thy intro_ts + in + (th, (new_defs, thy)) + end + fun fold_map_spec f [] s = ([], s) + | fold_map_spec f ((c, ths) :: specs) s = + let + val (ths', s') = f ths s + val (specs', s'') = fold_map_spec f specs s' + in ((c, ths') :: specs', s'') end + val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy) + in + (intross', (new_defs, thy')) + end + end; diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sun Oct 25 00:10:25 2009 +0200 @@ -3,18 +3,19 @@ A quickcheck generator based on the predicate compiler *) -signature PRED_COMPILE_QUICKCHECK = +signature PREDICATE_COMPILE_QUICKCHECK = sig val quickcheck : Proof.context -> term -> int -> term list option val test_ref : ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref end; -structure Pred_Compile_Quickcheck : PRED_COMPILE_QUICKCHECK = +structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = struct val test_ref = Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) + val target = "Quickcheck" fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs @@ -63,21 +64,21 @@ val _ = tracing (Display.string_of_thm ctxt' intro) val thy'' = thy' |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro) - |> Predicate_Compile.preprocess full_constname - |> Predicate_Compile_Core.add_equations [full_constname] - |> Predicate_Compile_Core.add_sizelim_equations [full_constname] - |> Predicate_Compile_Core.add_quickcheck_equations [full_constname] - val sizelim_modes = Predicate_Compile_Core.sizelim_modes_of thy'' full_constname + |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname + (* |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]*) + (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) + (* |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] *) + val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname val prog = if member (op =) modes ([], []) then let val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], []) - val T = @{typ code_numeral} --> (mk_rpredT (HOLogic.mk_tupleT (map snd vs'))) - in Const (name, T) $ Bound 0 end - else if member (op =) sizelim_modes ([], []) then + val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs'))) + in Const (name, T) $ @{term True} $ Bound 0 end + else if member (op =) depth_limited_modes ([], []) then let - val name = Predicate_Compile_Core.sizelim_function_name_of thy'' full_constname ([], []) + val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs'))) in lift_pred (Const (name, T) $ Bound 0) end else error "Predicate Compile Quickcheck failed" @@ -85,7 +86,7 @@ mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))) val _ = tracing (Syntax.string_of_term ctxt' qc_term) - val compile = Code_ML.eval (SOME target) ("Pred_Compile_Quickcheck.test_ref", test_ref) + val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc) thy'' qc_term [] in diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/Tools/Predicate_Compile/pred_compile_set.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Sun Oct 25 00:10:25 2009 +0200 @@ -3,7 +3,7 @@ Preprocessing sets to predicates *) -signature PRED_COMPILE_SET = +signature PREDICATE_COMPILE_SET = sig (* val preprocess_intro : thm -> theory -> thm * theory @@ -12,10 +12,11 @@ val unfold_set_notation : thm -> thm; end; -structure Pred_Compile_Set : PRED_COMPILE_SET = +structure Predicate_Compile_Set : PREDICATE_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_lemmas = [@{thm Collect_def}, @{thm mem_def}, +@{thm Ball_def}, @{thm Bex_def}] val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Oct 25 00:10:25 2009 +0200 @@ -4,87 +4,170 @@ signature PREDICATE_COMPILE = sig val setup : theory -> theory - val preprocess : string -> theory -> theory + val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory end; structure Predicate_Compile : PREDICATE_COMPILE = struct +(* options *) +val fail_safe_mode = true + 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 = +fun tracing s = () + +fun print_intross options thy msg intross = + if show_intermediate_results options then + Output.tracing (msg ^ + (space_implode "\n" (map + (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^ + commas (map (Display.string_of_thm_global thy) intros)) intross))) + else () + +fun print_specs thy specs = + map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" + ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs + +fun map_specs f specs = + map (fn (s, ths) => (s, f ths)) specs + +fun process_specification options specs thy' = + let + val _ = print_step options "Compiling predicates to flat introrules..." + val specs = map (apsnd (map + (fn th => if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th))) specs + val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy') + val _ = print_intross options thy'' "Flattened introduction rules: " intross1 + val _ = print_step options "Replacing functions in introrules..." + val intross2 = + if fail_safe_mode then + case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of + SOME intross => intross + | NONE => let val _ = warning "Function replacement failed!" in intross1 end + else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 + val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2 + val _ = print_step options "Introducing new constants for abstractions at higher-order argument positions..." + val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'') + val (new_intross, thy'''') = + if not (null new_defs) then + let + val _ = print_step options "Recursively obtaining introduction rules for new definitions..." + in process_specification options new_defs thy''' end + else ([], thy''') + in + (intross3 @ new_intross, thy'''') + end + + +fun preprocess_strong_conn_constnames options gr constnames thy = let val get_specs = map (fn k => (k, Graph.get_node gr k)) - val _ = priority ("Preprocessing scc of " ^ commas constnames) + val _ = print_step options ("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 _ = 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 ("Flattened introduction rules: " ^ - commas (map (Display.string_of_thm_global thy'') (flat intross))) - val _ = priority "Replacing functions in introrules..." - (* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *) - val intross' = - case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross of - SOME intross' => intross' - | NONE => let val _ = warning "Function replacement failed!" in intross end - val _ = tracing ("Introduction rules with replaced functions: " ^ - commas (map (Display.string_of_thm_global thy'') (flat intross'))) - val intross'' = burrow (maps remove_pointless_clauses) intross' - val intross'' = burrow (map (AxClass.overload thy'')) intross'' - val _ = priority "Registering intro rules..." - val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy'' + val _ = print_step options + ("Compiling functions (" ^ commas funnames ^ ") to predicates...") + val (fun_pred_specs, thy') = + if not (null funnames) then Predicate_Compile_Fun.define_predicates + (get_specs funnames) thy else ([], thy) + val _ = print_specs thy' fun_pred_specs + val specs = (get_specs prednames) @ fun_pred_specs + val (intross3, thy''') = process_specification options specs thy' + val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 + val intross4 = map_specs (maps remove_pointless_clauses) intross3 + val _ = print_intross options thy''' "After removing pointless clauses: " intross4 + (*val intross5 = map (fn s, ths) => ( s, map (AxClass.overload thy''') ths)) intross4*) + val intross6 = map_specs (map (expand_tuples thy''')) intross4 + val _ = print_intross options thy''' "introduction rules before registering: " intross6 + val _ = print_step options "Registering introduction rules..." + val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' in - thy''' + thy'''' end; -fun preprocess const thy = +fun preprocess options const thy = let - val _ = tracing ("Fetching definitions from theory...") - val table = Pred_Compile_Data.make_const_spec_table thy - val gr = Pred_Compile_Data.obtain_specification_graph table const - val _ = tracing (commas (Graph.all_succs gr [const])) + val _ = print_step options "Fetching definitions from theory..." + val table = Predicate_Compile_Data.make_const_spec_table thy + val gr = Predicate_Compile_Data.obtain_specification_graph thy table const val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr - in fold_rev (preprocess_strong_conn_constnames gr) + in fold_rev (preprocess_strong_conn_constnames options gr) (Graph.strong_conn gr) 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 lthy' = LocalTheory.theory (preprocess const) lthy - |> LocalTheory.checkpoint - val _ = tracing "Starting Predicate Compile Core..." - in Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy' end - else - Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy +fun extract_options ((modes, raw_options), const) = + let + fun chk s = member (op =) raw_options s + in + Options { + expected_modes = Option.map (pair const) modes, + show_steps = chk "show_steps", + show_intermediate_results = chk "show_intermediate_results", + show_proof_trace = chk "show_proof_trace", + show_mode_inference = chk "show_mode_inference", + show_compilation = chk "show_compilation", + skip_proof = chk "skip_proof", + inductify = chk "inductify", + rpred = chk "rpred", + depth_limited = chk "depth_limited" + } + end + +fun code_pred_cmd ((modes, raw_options), raw_const) lthy = + let + val thy = ProofContext.theory_of lthy + val const = Code.read_const thy raw_const + val options = extract_options ((modes, raw_options), const) + in + if (is_inductify options) then + let + val lthy' = LocalTheory.theory (preprocess options const) lthy + |> LocalTheory.checkpoint + val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of + SOME c => c + | NONE => const + val _ = print_step options "Starting Predicate Compile Core..." + in + Predicate_Compile_Core.code_pred options const lthy' + end + else + Predicate_Compile_Core.code_pred_cmd options raw_const lthy + end val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup -val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred"] +val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", + "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"] local structure P = OuterParse in +val opt_modes = + Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |-- + P.enum1 "," (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]") + --| P.$$$ ")" >> SOME) NONE + +val scan_params = + let + val scan_bool_param = foldl1 (op ||) (map Args.$$$ bool_options) + in + Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") [] + end + 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) + OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> + code_pred_cmd) end diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Oct 25 00:10:25 2009 +0200 @@ -7,26 +7,25 @@ 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 + val code_pred: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state + val code_pred_cmd: Predicate_Compile_Aux.options -> 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 register_predicate : (string * thm list * thm * int) -> theory -> theory + val register_intros : string * 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 val predfun_elim_of: theory -> string -> mode -> thm - val strip_intro_concl: int -> term -> term * (term list * term list) val predfun_name_of: theory -> string -> mode -> string val all_preds_of : theory -> string list val modes_of: theory -> string -> mode list - val sizelim_modes_of: theory -> string -> mode list - val sizelim_function_name_of : theory -> string -> mode -> string + val depth_limited_modes_of: theory -> string -> mode list + val depth_limited_function_name_of : theory -> string -> mode -> string val generator_modes_of: theory -> string -> mode list val generator_name_of : theory -> string -> mode -> string + val all_modes_of : theory -> (string * mode list) list + val all_generator_modes_of : theory -> (string * mode list) list val string_of_mode : mode -> string val intros_of: theory -> string -> thm list val nparams_of: theory -> string -> int @@ -35,24 +34,12 @@ val set_nparams : string -> int -> theory -> theory val print_stored_rules: theory -> unit val print_all_modes: theory -> unit - val do_proofs: bool Unsynchronized.ref - val mk_casesrule : Proof.context -> int -> thm list -> term - val analyze_compr: theory -> term -> term - val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref - val add_equations : string list -> theory -> theory + val mk_casesrule : Proof.context -> term -> int -> thm list -> term + val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref + val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) option Unsynchronized.ref val code_pred_intros_attrib : attribute (* used by Quickcheck_Generator *) - (*val funT_of : mode -> typ -> typ - val mk_if_pred : term -> term - val mk_Eval : term * term -> term*) - val mk_tupleT : typ list -> typ -(* val mk_predT : typ -> typ *) (* temporary for testing of the compilation *) - datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term | - GeneratorPrem of term list * term | Generator of (string * typ); - (* val prepare_intrs: theory -> string list -> - (string * typ) list * int * string list * string list * (string * mode list) list * - (string * (term list * indprem list) list) list * (string * (int option list * int)) list*) datatype compilation_funs = CompilationFuns of { mk_predT : typ -> typ, dest_predT : typ -> typ, @@ -64,66 +51,39 @@ mk_not : term -> term, mk_map : typ -> typ -> term -> term -> term, lift_pred : term -> term - }; - type moded_clause = term list * (indprem * tmode) list - type 'a pred_mode_table = (string * (mode * 'a) list) list - val infer_modes : theory -> (string * mode list) list - -> (string * mode list) list - -> string list - -> (string * (term list * indprem list) list) list - -> (moded_clause list) pred_mode_table - val infer_modes_with_generator : theory -> (string * mode list) list - -> (string * mode list) list - -> string list - -> (string * (term list * indprem list) list) list - -> (moded_clause list) pred_mode_table - (*val compile_preds : theory -> compilation_funs -> string list -> string list - -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table - val rpred_create_definitions :(string * typ) list -> string * mode list - -> theory -> theory - val split_smode : int list -> term list -> (term list * term list) *) - val print_moded_clauses : - theory -> (moded_clause list) pred_mode_table -> unit - val print_compiled_terms : theory -> term pred_mode_table -> unit - (*val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table*) + }; val pred_compfuns : compilation_funs val rpred_compfuns : compilation_funs - val dest_funT : typ -> typ * typ - (* val depending_preds_of : theory -> thm list -> string list *) - val add_quickcheck_equations : string list -> theory -> theory - val add_sizelim_equations : string list -> theory -> theory - val is_inductive_predicate : theory -> string -> bool - val terms_vs : term list -> string list - val subsets : int -> int -> int list list - val check_mode_clause : bool -> theory -> string list -> - (string * mode list) list -> (string * mode list) list -> mode -> (term list * indprem list) - -> (term list * (indprem * tmode) list) option - val string_of_moded_prem : theory -> (indprem * tmode) -> string - val all_modes_of : theory -> (string * mode list) list - val all_generator_modes_of : theory -> (string * mode list) list - val compile_clause : compilation_funs -> term option -> (term list -> term) -> - theory -> string list -> string list -> mode -> term -> moded_clause -> term - val preprocess_intro : theory -> thm -> thm - val is_constrt : theory -> term -> bool - val is_predT : typ -> bool - val guess_nparams : typ -> int - val cprods_subset : 'a list list -> 'a list list + (* val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory + val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory + val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory + *) end; structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE = struct open Predicate_Compile_Aux; + (** auxiliary **) (* debug stuff *) -fun tracing s = (if ! Toplevel.debug then tracing s else ()); +fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); + +fun print_tac s = Seq.single; + +fun print_tac' options s = + if show_proof_trace options then Tactical.print_tac s else Seq.single; -fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *) -fun debug_tac msg = Seq.single; (* (fn st => (tracing msg; Seq.single st)); *) +fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *) -val do_proofs = Unsynchronized.ref true; +datatype assertion = Max_number_of_subgoals of int +fun assert_tac (Max_number_of_subgoals i) st = + if (nprems_of st <= i) then Seq.single st + else error ("assert_tac: Numbers of subgoals mismatch at goal state :" + ^ "\n" ^ Pretty.string_of (Pretty.chunks + (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st))); (* reference to preprocessing of InductiveSet package *) @@ -139,20 +99,6 @@ HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs in mk_eqs x xs end; -fun mk_tupleT [] = HOLogic.unitT - | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts; - -fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = [] - | dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2) - | dest_tupleT t = [t] - -fun mk_tuple [] = HOLogic.unit - | mk_tuple ts = foldr1 HOLogic.mk_prod ts; - -fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = [] - | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2) - | dest_tuple t = [t] - fun mk_scomp (t, u) = let val T = fastype_of t @@ -189,6 +135,13 @@ (** data structures **) +(* new datatype for modes: *) +(* +datatype instantiation = Input | Output +type arg_mode = Tuple of instantiation list | Atom of instantiation | HigherOrderMode of mode +type mode = arg_mode list +type tmode = Mode of mode * +*) type smode = (int * int list option) list type mode = smode option list * smode; datatype tmode = Mode of mode * smode * tmode option list; @@ -241,35 +194,8 @@ (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_th), ctxt1) = Variable.import false introrules ctxt - val intros = map prop_of intros_th - val (pred, (params, args)) = strip_intro_concl nparams (hd intros) - val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 - val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) - val (argnames, ctxt3) = Variable.variant_fixes - (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt2 - 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); +datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term + | Generator of (string * typ); type moded_clause = term list * (indprem * tmode) list type 'a pred_mode_table = (string * (mode * 'a) list) list @@ -300,25 +226,25 @@ nparams : int, functions : (mode * predfun_data) list, generators : (mode * function_data) list, - sizelim_functions : (mode * function_data) list + depth_limited_functions : (mode * function_data) list }; fun rep_pred_data (PredData data) = data; -fun mk_pred_data ((intros, elim, nparams), (functions, generators, sizelim_functions)) = +fun mk_pred_data ((intros, elim, nparams), (functions, generators, depth_limited_functions)) = PredData {intros = intros, elim = elim, nparams = nparams, - functions = functions, generators = generators, sizelim_functions = sizelim_functions} -fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, sizelim_functions}) = - mk_pred_data (f ((intros, elim, nparams), (functions, generators, sizelim_functions))) - + functions = functions, generators = generators, depth_limited_functions = depth_limited_functions} +fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, depth_limited_functions}) = + mk_pred_data (f ((intros, elim, nparams), (functions, generators, depth_limited_functions))) + fun eq_option eq (NONE, NONE) = true | eq_option eq (SOME x, SOME y) = eq (x, y) | eq_option eq _ = false - + fun eq_pred_data (PredData d1, PredData d2) = eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso #nparams d1 = #nparams d2 - + structure PredData = TheoryDataFun ( type T = pred_data Graph.T; @@ -353,7 +279,7 @@ val modes_of = (map fst) o #functions oo the_pred_data -val sizelim_modes_of = (map fst) o #sizelim_functions oo the_pred_data +val depth_limited_modes_of = (map fst) o #depth_limited_functions oo the_pred_data val rpred_modes_of = (map fst) o #generators oo the_pred_data @@ -380,7 +306,7 @@ fun lookup_generator_data thy name mode = Option.map rep_function_data (AList.lookup (op =) (#generators (the_pred_data thy name)) mode) - + fun the_generator_data thy name mode = case lookup_generator_data thy name mode of NONE => error ("No generator defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name) | SOME data => data @@ -392,24 +318,25 @@ fun all_generator_modes_of thy = map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy) -fun lookup_sizelim_function_data thy name mode = +fun lookup_depth_limited_function_data thy name mode = Option.map rep_function_data (AList.lookup (op =) - (#sizelim_functions (the_pred_data thy name)) mode) + (#depth_limited_functions (the_pred_data thy name)) mode) -fun the_sizelim_function_data thy name mode = case lookup_sizelim_function_data thy name mode - of NONE => error ("No size-limited function defined for mode " ^ string_of_mode mode +fun the_depth_limited_function_data thy name mode = case lookup_depth_limited_function_data thy name mode + of NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name) | SOME data => data -val sizelim_function_name_of = #name ooo the_sizelim_function_data +val depth_limited_function_name_of = #name ooo the_depth_limited_function_data (*val generator_modes_of = (map fst) o #generators oo the_pred_data*) - + (* diagnostic display functions *) -fun print_modes modes = tracing ("Inferred modes:\n" ^ - cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map - string_of_mode ms)) modes)); +fun print_modes modes = + Output.tracing ("Inferred modes:\n" ^ + cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map + string_of_mode ms)) modes)); fun print_pred_mode_table string_of_entry thy pred_mode_table = let @@ -417,15 +344,20 @@ ^ (string_of_entry pred mode entry) fun print_pred (pred, modes) = "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes) - val _ = tracing (cat_lines (map print_pred pred_mode_table)) + val _ = Output.tracing (cat_lines (map print_pred pred_mode_table)) in () end; +fun string_of_prem thy (Prem (ts, p)) = + (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ "(premise)" + | string_of_prem thy (Negprem (ts, p)) = + (Syntax.string_of_term_global thy (HOLogic.mk_not (list_comb (p, ts)))) ^ "(negative premise)" + | string_of_prem thy (Sidecond t) = + (Syntax.string_of_term_global thy t) ^ "(sidecondition)" + | string_of_prem thy _ = error "string_of_prem: unexpected input" + fun string_of_moded_prem thy (Prem (ts, p), tmode) = (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ "(" ^ (string_of_tmode tmode) ^ ")" - | string_of_moded_prem thy (GeneratorPrem (ts, p), Mode (predmode, is, _)) = - (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ - "(generator_mode: " ^ (string_of_mode predmode) ^ ")" | string_of_moded_prem thy (Generator (v, T), _) = "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T) | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) = @@ -435,18 +367,25 @@ (Syntax.string_of_term_global thy t) ^ "(sidecond mode: " ^ string_of_smode is ^ ")" | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented" - + fun print_moded_clauses thy = - let + let fun string_of_clause pred mode clauses = cat_lines (map (fn (ts, prems) => (space_implode " --> " (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " " ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses) in print_pred_mode_table string_of_clause thy end; -fun print_compiled_terms thy = - print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy - +fun string_of_clause thy pred (ts, prems) = + (space_implode " --> " + (map (string_of_prem thy) prems)) ^ " --> " ^ pred ^ " " + ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts)) + +fun print_compiled_terms options thy = + if show_compilation options then + print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy + else K () + fun print_stored_rules thy = let val preds = (Graph.keys o PredData.get) thy @@ -477,7 +416,105 @@ in fold print (all_modes_of thy) () end - + +(* validity checks *) + +fun check_expected_modes (options : Predicate_Compile_Aux.options) modes = + case expected_modes options of + SOME (s, ms) => (case AList.lookup (op =) modes s of + SOME modes => + if not (eq_set (op =) (map (map (rpair NONE)) ms, map snd modes)) then + error ("expected modes were not inferred:\n" + ^ "inferred modes for " ^ s ^ ": " + ^ commas (map ((enclose "[" "]") o string_of_smode o snd) modes)) + else () + | NONE => ()) + | NONE => () + +(* importing introduction rules *) + +fun unify_consts thy cs intr_ts = + (let + val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I); + fun varify (t, (i, ts)) = + let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t)) + in (maxidx_of_term t', t'::ts) end; + val (i, cs') = List.foldr varify (~1, []) cs; + val (i', intr_ts') = List.foldr varify (i, []) intr_ts; + val rec_consts = fold add_term_consts_2 cs' []; + val intr_consts = fold add_term_consts_2 intr_ts' []; + fun unify (cname, cT) = + let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts) + in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end; + val (env, _) = fold unify rec_consts (Vartab.empty, i'); + val subst = map_types (Envir.norm_type env) + in (map subst cs', map subst intr_ts') + end) handle Type.TUNIFY => + (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts)); + +fun import_intros inp_pred nparams [] ctxt = + let + val ([outp_pred], ctxt') = Variable.import_terms false [inp_pred] ctxt + val (paramTs, _) = chop nparams (binder_types (fastype_of outp_pred)) + val (param_names, ctxt'') = Variable.variant_fixes (map (fn i => "p" ^ (string_of_int i)) + (1 upto nparams)) ctxt' + val params = map Free (param_names ~~ paramTs) + in (((outp_pred, params), []), ctxt') end + | import_intros inp_pred nparams (th :: ths) ctxt = + let + val ((_, [th']), ctxt') = Variable.import false [th] ctxt + val thy = ProofContext.theory_of ctxt' + val (pred, (params, args)) = strip_intro_concl nparams (prop_of th') + val ho_args = filter (is_predT o fastype_of) args + fun subst_of (pred', pred) = + let + val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty + in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end + fun instantiate_typ th = + let + val (pred', _) = strip_intro_concl 0 (prop_of th) + val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then + error "Trying to instantiate another predicate" else () + in Thm.certify_instantiate (subst_of (pred', pred), []) th end; + fun instantiate_ho_args th = + let + val (_, (params', args')) = strip_intro_concl nparams (prop_of th) + val ho_args' = map dest_Var (filter (is_predT o fastype_of) args') + in Thm.certify_instantiate ([], map dest_Var params' ~~ params) th end + val outp_pred = + Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred + val ((_, ths'), ctxt1) = + Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt' + in + (((outp_pred, params), th' :: ths'), ctxt1) + end + +(* generation of case rules from user-given introduction rules *) + +fun mk_casesrule ctxt pred nparams introrules = + let + val (((pred, params), intros_th), ctxt1) = import_intros pred nparams introrules ctxt + val intros = map prop_of intros_th + val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 + val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) + val (_, argsT) = chop nparams (binder_types (fastype_of pred)) + val (argnames, ctxt3) = Variable.variant_fixes + (map (fn i => "a" ^ string_of_int i) (1 upto length argsT)) ctxt2 + val argvs = map2 (curry Free) argnames argsT + 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; + (** preprocessing rules **) fun imp_prems_conv cv ct = @@ -498,39 +535,30 @@ fun preprocess_elim thy nparams elimrule = let - val _ = tracing ("Preprocessing elimination rule " - ^ (Display.string_of_thm_global thy elimrule)) fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) = HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs) | replace_eqs t = t + val ctxt = ProofContext.init thy + val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt val prems = Thm.prems_of elimrule val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) - nparams fun preprocess_case t = - let + let val params = Logic.strip_params t val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t) val assums_hyp' = assums1 @ (map replace_eqs assums2) - in + in list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t)) - end + end val cases' = map preprocess_case (tl prems) val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule) - (*val _ = tracing ("elimrule': "^ (Syntax.string_of_term_global thy elimrule'))*) val bigeq = (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}]) (cterm_of thy elimrule'))) - (* - val _ = tracing ("bigeq:" ^ (Display.string_of_thm_global thy bigeq)) - val res = - Thm.equal_elim bigeq elimrule - *) - (* - val t = (fn {...} => mycheat_tac thy 1) - val eq = Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) t - *) - val _ = tracing "Preprocessed elimination rule" + val tac = (fn _ => Skip_Proof.cheat_tac thy) + val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac in - Thm.equal_elim bigeq elimrule + Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt) end; (* special case: predicate with no introduction rule *) @@ -552,6 +580,8 @@ ([intro], elim) end +fun expand_tuples_elim th = th + fun fetch_pred_data thy name = case try (Inductive.the_inductive (ProofContext.init thy)) name of SOME (info as (_, result)) => @@ -560,17 +590,23 @@ let val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) in (fst (dest_Const const) = name) end; - val intros = ind_set_codegen_preproc thy ((map (preprocess_intro thy)) - (filter is_intro_of (#intrs result))) - val pre_elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info))) + val intros = ind_set_codegen_preproc thy + (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result))) + val index = find_index (fn s => s = name) (#names (fst info)) + val pre_elim = nth (#elims result) index + val pred = nth (#preds result) index val nparams = length (Inductive.params_of (#raw_induct result)) - val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim) - val (intros, elim) = if null intros then noclause thy name elim else (intros, elim) + (*val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams + (expand_tuples_elim pre_elim))*) + val elim = + (Drule.standard o Skip_Proof.make_thm thy) + (mk_casesrule (ProofContext.init thy) pred nparams intros) + val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim) in mk_pred_data ((intros, SOME elim, nparams), ([], [], [])) end | NONE => error ("No such predicate: " ^ quote name) - + (* updaters *) fun apfst3 f (x, y, z) = (f x, y, z) @@ -605,6 +641,7 @@ (data, keys) end; *) + (* guessing number of parameters *) fun find_indexes pred xs = let @@ -624,7 +661,7 @@ fun cons_intro gr = case try (Graph.get_node gr) name of SOME pred_data => Graph.map_node name (map_pred_data - (apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr + (apfst (fn (intros, elim, nparams) => (thm::intros, elim, nparams)))) gr | NONE => let val nparams = the_default (guess_nparams T) (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name) @@ -640,30 +677,34 @@ fun set_nparams name nparams = let 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 = + +fun register_predicate (constname, 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 - if not (member (op =) (Graph.keys (PredData.get thy)) name) then + if not (member (op =) (Graph.keys (PredData.get thy)) constname) then PredData.map - (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy + (Graph.new_node (constname, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy else thy end -fun register_intros pre_intros thy = +fun register_intros (constname, pre_intros) thy = let - val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros)))) - val _ = tracing ("Registering introduction rules of " ^ c) - val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros)) + val T = Sign.the_const_type thy constname + fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl 0 (prop_of intr)))) + val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then + error ("register_intros: Introduction rules of different constants are used\n" ^ + "expected rules for " ^ constname ^ ", but received rules for " ^ + commas (map constname_of_intro pre_intros)) + else () + val pred = Const (constname, T) val nparams = guess_nparams T val pre_elim = (Drule.standard o Skip_Proof.make_thm thy) - (mk_casesrule (ProofContext.init thy) nparams pre_intros) - in register_predicate (pre_intros, pre_elim, nparams) thy end + (mk_casesrule (ProofContext.init thy) pred nparams pre_intros) + in register_predicate (constname, pre_intros, pre_elim, nparams) thy end fun set_generator_name pred mode name = let @@ -672,7 +713,7 @@ PredData.map (Graph.map_node pred (map_pred_data set)) end -fun set_sizelim_function_name pred mode name = +fun set_depth_limited_function_name pred mode name = let val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE)) in @@ -694,8 +735,6 @@ mk_sup : term * term -> term, mk_if : term -> term, mk_not : term -> term, -(* funT_of : mode -> typ -> typ, *) -(* mk_fun_of : theory -> (string * typ) -> mode -> term, *) mk_map : typ -> typ -> term -> term -> term, lift_pred : term -> term }; @@ -708,8 +747,6 @@ fun mk_sup (CompilationFuns funs) = #mk_sup funs fun mk_if (CompilationFuns funs) = #mk_if funs fun mk_not (CompilationFuns funs) = #mk_not funs -(*fun funT_of (CompilationFuns funs) = #funT_of funs*) -(*fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs*) fun mk_map (CompilationFuns funs) = #mk_map funs fun lift_pred (CompilationFuns funs) = #lift_pred funs @@ -719,7 +756,7 @@ val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs in - (paramTs' @ inargTs) ---> (mk_predT compfuns (mk_tupleT outargTs)) + (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) end; fun mk_fun_of compfuns thy (name, T) mode = @@ -809,9 +846,11 @@ fun mk_if cond = Const (@{const_name RPred.if_rpred}, HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond; -fun mk_not t = error "Negation is not defined for RPred" +fun mk_not t = let val T = mk_rpredT HOLogic.unitT + in Const (@{const_name RPred.not_rpred}, T --> T) $ t end -fun mk_map t = error "FIXME" (*FIXME*) +fun mk_map T1 T2 tf tp = Const (@{const_name RPred.map}, + (T1 --> T2) --> mk_rpredT T1 --> mk_rpredT T2) $ tf $ tp fun lift_pred t = let @@ -839,20 +878,21 @@ RPredCompFuns.mk_rpredT T) $ random end; -fun sizelim_funT_of compfuns (iss, is) T = +fun depth_limited_funT_of compfuns (iss, is) T = let val Ts = binder_types T val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn SOME is => sizelim_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs + val paramTs' = map2 (fn SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs in - (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs)) + (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}]) + ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) end; -fun mk_sizelim_fun_of compfuns thy (name, T) mode = - Const (sizelim_function_name_of thy name mode, sizelim_funT_of compfuns mode T) +fun mk_depth_limited_fun_of compfuns thy (name, T) mode = + Const (depth_limited_function_name_of thy name mode, depth_limited_funT_of compfuns mode T) fun mk_generator_of compfuns thy (name, T) mode = - Const (generator_name_of thy name mode, sizelim_funT_of compfuns mode T) + Const (generator_name_of thy name mode, depth_limited_funT_of compfuns mode T) (* Mode analysis *) @@ -882,16 +922,16 @@ fun term_vTs tm = fold_aterms (fn Free xT => cons xT | _ => I) tm []; -(*FIXME this function should not be named merge... make it local instead*) -fun merge xs [] = xs - | merge [] ys = ys - | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys) - else y::merge (x::xs) ys; - -fun subsets i j = if i <= j then - let val is = subsets (i+1) j - in merge (map (fn ks => i::ks) is) is end - else [[]]; +fun subsets i j = + if i <= j then + let + fun merge xs [] = xs + | merge [] ys = ys + | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys) + else y::merge (x::xs) ys; + val is = subsets (i+1) j + in merge (map (fn ks => i::ks) is) is end + else [[]]; (* FIXME: should be in library - cprod = map_prod I *) fun cprod ([], ys) = [] @@ -905,46 +945,9 @@ val yss = (cprods_subset xss) in maps (fn ys => map (fn x => cons x ys) xs) yss @ yss end -(*TODO: cleanup function and put together with modes_of_term *) -(* -fun modes_of_param default modes t = let - val (vs, t') = strip_abs t - val b = length vs - fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) => - let - val (args1, args2) = - if length args < length iss then - error ("Too few arguments for inductive predicate " ^ name) - else chop (length iss) args; - val k = length args2; - val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1) - (1 upto b) - val partial_mode = (1 upto k) \\ perm - in - if not (partial_mode subset is) then [] else - let - val is' = - (fold_index (fn (i, j) => if j mem is then cons (i + 1) else I) perm []) - |> fold (fn i => if i > k then cons (i - k + b) else I) is - - val res = map (fn x => Mode (m, is', x)) (cprods (map - (fn (NONE, _) => [NONE] - | (SOME js, arg) => map SOME (filter - (fn Mode (_, js', _) => js=js') (modes_of_term modes arg))) - (iss ~~ args1))) - in res end - end)) (AList.lookup op = modes name) - in case strip_comb t' of - (Const (name, _), args) => the_default default (mk_modes name args) - | (Var ((name, _), _), args) => the (mk_modes name args) - | (Free (name, _), args) => the (mk_modes name args) - | _ => default end - -and -*) fun modes_of_term modes t = let - val ks = map_index (fn (i, T) => (i, NONE)) (binder_types (fastype_of t)); + val ks = map_index (fn (i, T) => (i + 1, NONE)) (binder_types (fastype_of t)); val default = [Mode (([], ks), ks, [])]; fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) => let @@ -956,7 +959,7 @@ val prfx = map (rpair NONE) (1 upto k) in if not (is_prefix op = prfx is) then [] else - let val is' = List.drop (is, k) + let val is' = map (fn (i, t) => (i - k, t)) (List.drop (is, k)) in map (fn x => Mode (m, is', x)) (cprods (map (fn (NONE, _) => [NONE] | (SOME js, arg) => map SOME (filter @@ -992,7 +995,7 @@ (modes_of_term modes t handle Option => error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) | Negprem (us, t) => find_first (fn Mode (_, is, _) => - length us = length is andalso + is = map (rpair NONE) (1 upto length us) andalso subset (op =) (terms_vs us, vs) andalso subset (op =) (term_vs t, vs)) (modes_of_term modes t handle Option => @@ -1015,24 +1018,8 @@ (Generator (v, T), Mode (([], []), [], [])) end; -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, _))) = - if member (op =) param_vs v then - GeneratorPrem (us, t) - else p - | param_gen_prem param_vs p = p - fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) = let - (* - val _ = tracing ("param_vs:" ^ commas param_vs) - val _ = tracing ("iss:" ^ - commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss)) - *) val modes' = modes @ map_filter (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)])) (param_vs ~~ iss); @@ -1046,7 +1033,7 @@ NONE => (if with_generator then (case select_mode_prem thy gen_modes' vs ps of - SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) + SOME (p as Prem _, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs) (filter_out (equal p) ps) | _ => @@ -1057,14 +1044,11 @@ (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps) (union (op =) vs generator_vs) ps - | NONE => let - val _ = tracing ("ps:" ^ (commas - (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps))) - in (*error "mode analysis failed"*)NONE end + | NONE => NONE end) else NONE) - | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) + | SOME (p, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs) (filter_out (equal p) ps)) val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts)); @@ -1083,33 +1067,41 @@ else NONE end; -fun check_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) = - let val SOME rs = AList.lookup (op =) clauses p +fun print_failed_mode options thy modes p m rs i = + if show_mode_inference options then + let + val _ = Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ + p ^ " violates mode " ^ string_of_mode m) + val _ = Output.tracing (string_of_clause thy p (nth rs i)) + in () end + else () + +fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) = + let + val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => [] in (p, List.filter (fn m => case find_index (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of ~1 => true - | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ - p ^ " violates mode " ^ string_of_mode m); - tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms) + | i => (print_failed_mode options thy modes p m rs i; false)) ms) end; fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) = let - val SOME rs = AList.lookup (op =) clauses p + val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => [] in (p, map (fn m => (m, map (the o check_mode_clause with_generator thy param_vs modes gen_modes m) rs)) ms) end; - + fun fixp f (x : (string * mode list) list) = let val y = f x in if x = y then x else fixp f y end; -fun infer_modes thy extra_modes all_modes param_vs clauses = +fun infer_modes options thy extra_modes all_modes param_vs clauses = let val modes = fixp (fn modes => - map (check_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes) + map (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes) all_modes in map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes @@ -1122,19 +1114,24 @@ | SOME vs' => (k, subtract (op =) vs' vs)) :: remove_from rem xs -fun infer_modes_with_generator thy extra_modes all_modes param_vs clauses = +fun infer_modes_with_generator options thy extra_modes all_modes param_vs clauses = let val prednames = map fst clauses - val extra_modes = all_modes_of thy + val extra_modes' = all_modes_of thy val gen_modes = all_generator_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name) - val starting_modes = remove_from extra_modes all_modes + val starting_modes = remove_from extra_modes' all_modes + fun eq_mode (m1, m2) = (m1 = m2) val modes = fixp (fn modes => - map (check_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes) - starting_modes + map (check_modes_pred options true thy param_vs clauses extra_modes' (gen_modes @ modes)) modes) + starting_modes in - map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes + AList.join (op =) + (fn _ => fn ((mps1, mps2)) => + merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2)) + (infer_modes options thy extra_modes all_modes param_vs clauses, + map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes) end; (* term construction *) @@ -1157,136 +1154,10 @@ in (t' $ u', nvs'') end | distinct_v x nvs = (x, nvs); -fun compile_match thy compfuns eqs eqs' out_ts success_t = - let - val eqs'' = maps mk_eq eqs @ eqs' - val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) []; - val name = Name.variant names "x"; - val name' = Name.variant (name :: names) "y"; - val T = mk_tupleT (map fastype_of out_ts); - val U = fastype_of success_t; - val U' = dest_predT compfuns U; - val v = Free (name, T); - val v' = Free (name', T); - in - lambda v (fst (Datatype.make_case - (ProofContext.init thy) DatatypeCase.Quiet [] v - [(mk_tuple out_ts, - if null eqs'' then success_t - else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $ - foldr1 HOLogic.mk_conj eqs'' $ success_t $ - mk_bot compfuns U'), - (v', mk_bot compfuns U')])) - end; - -(*FIXME function can be removed*) -fun mk_funcomp f t = - let - val names = Term.add_free_names t []; - val Ts = binder_types (fastype_of t); - val vs = map Free - (Name.variant_list names (replicate (length Ts) "x") ~~ Ts) - in - fold_rev lambda vs (f (list_comb (t, vs))) - end; -(* -fun compile_param_ext thy compfuns modes (NONE, t) = t - | compile_param_ext thy compfuns modes (m as SOME (Mode ((iss, is'), is, ms)), t) = - let - val (vs, u) = strip_abs t - val (ivs, ovs) = split_mode is vs - val (f, args) = strip_comb u - val (params, args') = chop (length ms) args - val (inargs, outargs) = split_mode is' args' - val b = length vs - val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b) - val outp_perm = - snd (split_mode is perm) - |> map (fn i => i - length (filter (fn x => x < i) is')) - val names = [] -- TODO - val out_names = Name.variant_list names (replicate (length outargs) "x") - val f' = case f of - Const (name, T) => - if AList.defined op = modes name then - mk_predfun_of thy compfuns (name, T) (iss, is') - else error "compile param: Not an inductive predicate with correct mode" - | Free (name, T) => Free (name, param_funT_of compfuns T (SOME is')) - val outTs = dest_tupleT (dest_predT compfuns (body_type (fastype_of f'))) - val out_vs = map Free (out_names ~~ outTs) - val params' = map (compile_param thy modes) (ms ~~ params) - val f_app = list_comb (f', params' @ inargs) - val single_t = (mk_single compfuns (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm))) - val match_t = compile_match thy compfuns [] [] out_vs single_t - in list_abs (ivs, - mk_bind compfuns (f_app, match_t)) - end - | compile_param_ext _ _ _ _ = error "compile params" -*) - -fun compile_param neg_in_sizelim size thy compfuns (NONE, t) = t - | compile_param neg_in_sizelim size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) = - let - val (f, args) = strip_comb (Envir.eta_contract t) - val (params, args') = chop (length ms) args - val params' = map (compile_param neg_in_sizelim size thy compfuns) (ms ~~ params) - val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of - val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of - val f' = - case f of - Const (name, T) => - mk_fun_of compfuns thy (name, T) (iss, is') - | Free (name, T) => - case neg_in_sizelim of - SOME _ => Free (name, sizelim_funT_of compfuns (iss, is') T) - | NONE => Free (name, funT_of compfuns (iss, is') T) - - | _ => error ("PredicateCompiler: illegal parameter term") - in - (case neg_in_sizelim of SOME size_t => - (fn t => - let - val Ts = fst (split_last (binder_types (fastype_of t))) - val names = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) - in - list_abs (names ~~ Ts, list_comb (t, (map Bound ((length Ts) - 1 downto 0)) @ [size_t])) - end) - | NONE => I) - (list_comb (f', params' @ args')) - end - -fun compile_expr neg_in_sizelim size thy ((Mode (mode, is, ms)), t) = - case strip_comb t of - (Const (name, T), params) => - let - val params' = map (compile_param neg_in_sizelim size thy PredicateCompFuns.compfuns) (ms ~~ params) - val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of - in - list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params') - end - | (Free (name, T), args) => - let - val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of - in - list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), args) - end; - -fun compile_gen_expr size thy compfuns ((Mode (mode, is, ms)), t) inargs = - case strip_comb t of - (Const (name, T), params) => - let - val params' = map (compile_param NONE size thy PredicateCompFuns.compfuns) (ms ~~ params) - in - list_comb (mk_generator_of compfuns thy (name, T) mode, params' @ inargs) - end - | (Free (name, T), params) => - lift_pred compfuns - (list_comb (Free (name, sizelim_funT_of PredicateCompFuns.compfuns ([], is) T), params @ inargs)) - - (** specific rpred functions -- move them to the correct place in this file *) -fun mk_Eval_of size ((x, T), NONE) names = (x, names) - | mk_Eval_of size ((x, T), SOME mode) names = +fun mk_Eval_of additional_arguments ((x, T), NONE) names = (x, names) + | mk_Eval_of additional_arguments ((x, T), SOME mode) names = let val Ts = binder_types T (*val argnames = Name.variant_list names @@ -1331,32 +1202,99 @@ end val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts)) val (inargs, outargs) = pairself flat (split_list inoutargs) - val size_t = case size of NONE => [] | SOME size_t => [size_t] - val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs @ size_t), mk_tuple outargs) + val r = PredicateCompFuns.mk_Eval + (list_comb (x, inargs @ additional_arguments), HOLogic.mk_tuple outargs) val t = fold_rev mk_split_lambda args r in (t, names) end; -fun compile_arg size thy param_vs iss arg = +fun compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss arg = let - val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of fun map_params (t as Free (f, T)) = if member (op =) param_vs f then case (the (AList.lookup (op =) (param_vs ~~ iss) f)) of - SOME is => let val T' = funT_of PredicateCompFuns.compfuns ([], is) T - in fst (mk_Eval_of size ((Free (f, T'), T), SOME is) []) end + SOME is => + let + val T' = #funT_of compilation_modifiers compfuns ([], is) T + in fst (mk_Eval_of additional_arguments ((Free (f, T'), T), SOME is) []) end | NONE => t else t | map_params t = t in map_aterms map_params arg end - -fun compile_clause compfuns size final_term thy all_vs param_vs (iss, is) inp (ts, moded_ps) = + +fun compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy eqs eqs' out_ts success_t = + let + val eqs'' = maps mk_eq eqs @ eqs' + val eqs'' = + map (compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss) eqs'' + val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) []; + val name = Name.variant names "x"; + val name' = Name.variant (name :: names) "y"; + val T = HOLogic.mk_tupleT (map fastype_of out_ts); + val U = fastype_of success_t; + val U' = dest_predT compfuns U; + val v = Free (name, T); + val v' = Free (name', T); + in + lambda v (fst (Datatype.make_case + (ProofContext.init thy) DatatypeCase.Quiet [] v + [(HOLogic.mk_tuple out_ts, + if null eqs'' then success_t + else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $ + foldr1 HOLogic.mk_conj eqs'' $ success_t $ + mk_bot compfuns U'), + (v', mk_bot compfuns U')])) + end; + +(*FIXME function can be removed*) +fun mk_funcomp f t = let + val names = Term.add_free_names t []; + val Ts = binder_types (fastype_of t); + val vs = map Free + (Name.variant_list names (replicate (length Ts) "x") ~~ Ts) + in + fold_rev lambda vs (f (list_comb (t, vs))) + end; + +fun compile_param compilation_modifiers compfuns thy (NONE, t) = t + | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms)), t) = + let + val (f, args) = strip_comb (Envir.eta_contract t) + val (params, args') = chop (length ms) args + val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) + val f' = + case f of + Const (name, T) => Const (#const_name_of compilation_modifiers thy name mode, + #funT_of compilation_modifiers compfuns mode T) + | Free (name, T) => Free (name, #funT_of compilation_modifiers compfuns mode T) + | _ => error ("PredicateCompiler: illegal parameter term") + in + list_comb (f', params' @ args') + end + +fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t) inargs additional_arguments = + case strip_comb t of + (Const (name, T), params) => + let + val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) + (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*) + val name' = #const_name_of compilation_modifiers thy name mode + val T' = #funT_of compilation_modifiers compfuns mode T + in + (list_comb (Const (name', T'), params' @ inargs @ additional_arguments)) + end + | (Free (name, T), params) => + list_comb (Free (name, #funT_of compilation_modifiers compfuns mode T), params @ inargs @ additional_arguments) + +fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments (iss, is) inp (ts, moded_ps) = + let + val compile_match = compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy fun check_constrt t (names, eqs) = if is_constrt thy t then (t, (names, eqs)) else let - val s = Name.variant names "x"; + val s = Name.variant names "x" val v = Free (s, fastype_of t) in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end; @@ -1371,12 +1309,8 @@ val (out_ts''', (names'', constr_vs)) = fold_map distinct_v out_ts'' (names', map (rpair []) vs); in - (* termify code: - compile_match thy compfuns constr_vs (eqs @ eqs') out_ts''' - (mk_single compfuns (mk_tuple (map mk_valtermify_term out_ts))) - *) - compile_match thy compfuns constr_vs (eqs @ eqs') out_ts''' - (final_term out_ts) + compile_match constr_vs (eqs @ eqs') out_ts''' + (mk_single compfuns (HOLogic.mk_tuple out_ts)) end | compile_prems out_ts vs names ((p, mode as Mode ((_, is), _, _)) :: ps) = let @@ -1385,16 +1319,16 @@ fold_map check_constrt out_ts (names, []) val (out_ts'', (names'', constr_vs')) = fold_map distinct_v out_ts' ((names', map (rpair []) vs)) + val additional_arguments' = + #transform_additional_arguments compilation_modifiers p additional_arguments val (compiled_clause, rest) = case p of Prem (us, t) => let val (in_ts, out_ts''') = split_smode is us; - val in_ts = map (compile_arg size thy param_vs iss) in_ts - val args = case size of - NONE => in_ts - | SOME size_t => in_ts @ [size_t] - val u = lift_pred compfuns - (list_comb (compile_expr NONE size thy (mode, t), args)) + val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments + thy param_vs iss) in_ts + val u = + compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments' val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) @@ -1402,38 +1336,32 @@ | Negprem (us, t) => let val (in_ts, out_ts''') = split_smode is us - val u = lift_pred compfuns - (mk_not PredicateCompFuns.compfuns (list_comb (compile_expr size NONE thy (mode, t), in_ts))) + val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments + thy param_vs iss) in_ts + val u = mk_not compfuns + (compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments') val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) end | Sidecond t => let + val t = compile_arg compilation_modifiers compfuns additional_arguments + thy param_vs iss t val rest = compile_prems [] vs' names'' ps; in (mk_if compfuns t, rest) end - | GeneratorPrem (us, t) => - let - val (in_ts, out_ts''') = split_smode is us; - val args = case size of - NONE => in_ts - | SOME size_t => in_ts @ [size_t] - val u = compile_gen_expr size thy compfuns (mode, t) args - val rest = compile_prems out_ts''' vs' names'' ps - in - (u, rest) - end | Generator (v, T) => let - val u = lift_random (HOLogic.mk_random T (the size)) + val [size] = additional_arguments + val u = lift_random (HOLogic.mk_random T size) val rest = compile_prems [Free (v, T)] vs' names'' ps; in (u, rest) end in - compile_match thy compfuns constr_vs' eqs out_ts'' + compile_match constr_vs' eqs out_ts'' (mk_bind compfuns (compiled_clause, rest)) end val prem_t = compile_prems in_ts' param_vs all_vs' moded_ps; @@ -1441,14 +1369,13 @@ mk_bind compfuns (mk_single compfuns inp, prem_t) end -fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls = +fun compile_pred compilation_modifiers compfuns thy all_vs param_vs s T mode moded_cls = let val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T) val (Us1, Us2) = split_smodeT (snd mode) Ts2 - val funT_of = if use_size then sizelim_funT_of else funT_of - val Ts1' = map2 (fn NONE => I | SOME is => funT_of PredicateCompFuns.compfuns ([], is)) (fst mode) Ts1 - val size_name = Name.variant (all_vs @ param_vs) "size" - fun mk_input_term (i, NONE) = + val Ts1' = + map2 (fn NONE => I | SOME is => #funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1 + fun mk_input_term (i, NONE) = [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of [] => error "strange unit input" @@ -1461,30 +1388,22 @@ else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end val in_ts = maps mk_input_term (snd mode) val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1' - val size = Free (size_name, @{typ "code_numeral"}) - val decr_size = - if use_size then - SOME (Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"}) - $ size $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"})) - else - NONE + val additional_arguments = #additional_arguments compilation_modifiers (all_vs @ param_vs) val cl_ts = - map (compile_clause compfuns decr_size (fn out_ts => mk_single compfuns (mk_tuple out_ts)) - thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls; - val t = foldr1 (mk_sup compfuns) cl_ts - val T' = mk_predT compfuns (mk_tupleT Us2) - val size_t = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T') - $ HOLogic.mk_eq (size, @{term "0 :: code_numeral"}) - $ mk_bot compfuns (dest_predT compfuns T') $ t - val fun_const = mk_fun_of compfuns thy (s, T) mode - val eq = if use_size then - (list_comb (fun_const, params @ in_ts @ [size]), size_t) - else - (list_comb (fun_const, params @ in_ts), t) + map (compile_clause compilation_modifiers compfuns + thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts)) moded_cls; + val compilation = #wrap_compilation compilation_modifiers compfuns s T mode additional_arguments + (if null cl_ts then + mk_bot compfuns (HOLogic.mk_tupleT Us2) + else foldr1 (mk_sup compfuns) cl_ts) + val fun_const = + Const (#const_name_of compilation_modifiers thy s mode, + #funT_of compilation_modifiers compfuns mode T) in - HOLogic.mk_Trueprop (HOLogic.mk_eq eq) + HOLogic.mk_Trueprop + (HOLogic.mk_eq (list_comb (fun_const, params @ in_ts @ additional_arguments), compilation)) end; - + (* special setup for simpset *) val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}]) setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac)) @@ -1531,15 +1450,15 @@ val param_names' = Name.variant_list (param_names @ argnames) (map (fn i => "p" ^ string_of_int i) (1 upto (length iss))) val param_vs = map Free (param_names' ~~ Ts1) - val (params', names) = fold_map (mk_Eval_of NONE) ((params ~~ Ts1) ~~ iss) [] + val (params', names) = fold_map (mk_Eval_of []) ((params ~~ Ts1) ~~ iss) [] val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ args)) val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ args)) val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params') val funargs = params @ inargs val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs), - if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs)) + if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs)) val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs), - mk_tuple outargs)) + HOLogic.mk_tuple outargs)) val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI) val simprules = [defthm, @{thm eval_pred}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}] @@ -1601,7 +1520,7 @@ val (Ts1, Ts2) = chop (length iss) Ts val (Us1, Us2) = split_smodeT is Ts2 val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1 - val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (mk_tupleT Us2)) + val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2)) val names = Name.variant_list [] (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); (* old *) @@ -1634,7 +1553,7 @@ val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names val (xinout, xargs) = split_list xinoutargs val (xins, xouts) = pairself flat (split_list xinout) - val (xparams', names') = fold_map (mk_Eval_of NONE) ((xparams ~~ Ts1) ~~ iss) names + val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t | mk_split_lambda [x] t = lambda x t | mk_split_lambda xs t = @@ -1663,16 +1582,16 @@ fold create_definition modes thy end; -fun sizelim_create_definitions preds (name, modes) thy = +fun create_definitions_of_depth_limited_functions preds (name, modes) thy = let val T = AList.lookup (op =) preds name |> the fun create_definition mode thy = let - val mode_cname = create_constname_of_mode thy "sizelim_" name mode - val funT = sizelim_funT_of PredicateCompFuns.compfuns mode T + val mode_cname = create_constname_of_mode thy "depth_limited_" name mode + val funT = depth_limited_funT_of PredicateCompFuns.compfuns mode T in thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> set_sizelim_function_name name mode mode_cname + |> set_depth_limited_function_name name mode mode_cname end; in fold create_definition modes thy @@ -1682,9 +1601,10 @@ let val Ts = binder_types T val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn SOME is => sizelim_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs + val paramTs' = map2 (fn SOME is => generator_funT_of ([], is) | NONE => I) iss paramTs in - (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT RPredCompFuns.compfuns (mk_tupleT outargTs)) + (paramTs' @ inargTs @ [@{typ code_numeral}]) ---> + (mk_predT RPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs)) end fun rpred_create_definitions preds (name, modes) thy = @@ -1696,7 +1616,7 @@ val funT = generator_funT_of mode T in thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> set_generator_name name mode mode_cname + |> set_generator_name name mode mode_cname end; in fold create_definition modes thy @@ -1818,7 +1738,7 @@ (* need better control here! *) end -fun prove_clause thy nargs modes (iss, is) (_, clauses) (ts, moded_ps) = +fun prove_clause options thy nargs modes (iss, is) (_, clauses) (ts, moded_ps) = let val (in_ts, clause_out_ts) = split_smode is ts; fun prove_prems out_ts [] = @@ -1874,7 +1794,8 @@ end; val prems_tac = prove_prems in_ts moded_ps in - rtac @{thm bindI} 1 + print_tac' options "Proving clause..." + THEN rtac @{thm bindI} 1 THEN rtac @{thm singleI} 1 THEN prems_tac end; @@ -1883,20 +1804,20 @@ | select_sup _ 1 = [rtac @{thm supI1}] | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1)); -fun prove_one_direction thy clauses preds modes pred mode moded_clauses = +fun prove_one_direction options thy clauses preds modes pred mode moded_clauses = let val T = the (AList.lookup (op =) preds pred) val nargs = length (binder_types T) - nparams_of thy pred val pred_case_rule = the_elim_of thy pred in REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})) - THEN print_tac "before applying elim rule" + THEN print_tac' options "before applying elim rule" THEN etac (predfun_elim_of thy pred mode) 1 THEN etac pred_case_rule 1 THEN (EVERY (map (fn i => EVERY' (select_sup (length moded_clauses) i) i) (1 upto (length moded_clauses)))) - THEN (EVERY (map2 (prove_clause thy nargs modes mode) clauses moded_clauses)) + THEN (EVERY (map2 (prove_clause options thy nargs modes mode) clauses moded_clauses)) THEN print_tac "proved one direction" end; @@ -1914,15 +1835,20 @@ | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm") val (_, ts) = strip_comb t in - (Splitter.split_asm_tac split_rules 1) -(* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1) - THEN (DETERM (TRY (etac @{thm Pair_inject} 1))) *) - THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)) + (print_tac ("Term " ^ (Syntax.string_of_term_global thy t) ^ + "splitting with rules \n" ^ + commas (map (Display.string_of_thm_global thy) split_rules))) + THEN TRY ((Splitter.split_asm_tac split_rules 1) + THEN (print_tac "after splitting with split_asm rules") + (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1) + THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*) + THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))) + THEN (assert_tac (Max_number_of_subgoals 2)) THEN (EVERY (map split_term_tac ts)) end else all_tac in - split_term_tac (mk_tuple out_ts) + split_term_tac (HOLogic.mk_tuple out_ts) THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2)))) end @@ -2053,7 +1979,7 @@ THEN prems_tac end; -fun prove_other_direction thy modes pred mode moded_clauses = +fun prove_other_direction options thy modes pred mode moded_clauses = let fun prove_clause clause i = (if i < length moded_clauses then etac @{thm supE} 1 else all_tac) @@ -2063,26 +1989,28 @@ THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all}))) THEN (rtac (predfun_intro_of thy pred mode) 1) THEN (REPEAT_DETERM (rtac @{thm refl} 2)) - THEN (EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses)))) + THEN (if null moded_clauses then + etac @{thm botE} 1 + else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses)))) end; (** proof procedure **) -fun prove_pred thy clauses preds modes pred mode (moded_clauses, compiled_term) = +fun prove_pred options thy clauses preds modes pred mode (moded_clauses, compiled_term) = let val ctxt = ProofContext.init thy - val clauses = the (AList.lookup (op =) clauses pred) + val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => [] in Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term - (if !do_proofs then + (if not (skip_proof options) then (fn _ => rtac @{thm pred_iffI} 1 - THEN print_tac "after pred_iffI" - THEN prove_one_direction thy clauses preds modes pred mode moded_clauses - THEN print_tac "proved one direction" - THEN prove_other_direction thy modes pred mode moded_clauses - THEN print_tac "proved other direction") - else fn _ => Skip_Proof.cheat_tac thy) + THEN print_tac' options "after pred_iffI" + THEN prove_one_direction options thy clauses preds modes pred mode moded_clauses + THEN print_tac' options "proved one direction" + THEN prove_other_direction options thy modes pred mode moded_clauses + THEN print_tac' options "proved other direction") + else (fn _ => Skip_Proof.cheat_tac thy)) end; (* composition of mode inference, definition, compilation and proof *) @@ -2101,48 +2029,57 @@ map (fn (pred, modes) => (pred, map (fn (mode, value) => value) modes)) preds_modes_table -fun compile_preds compfuns mk_fun_of use_size thy all_vs param_vs preds moded_clauses = - map_preds_modes (fn pred => compile_pred compfuns mk_fun_of use_size thy all_vs param_vs pred - (the (AList.lookup (op =) preds pred))) moded_clauses - -fun prove thy clauses preds modes moded_clauses compiled_terms = - map_preds_modes (prove_pred thy clauses preds modes) +fun compile_preds comp_modifiers compfuns thy all_vs param_vs preds moded_clauses = + map_preds_modes (fn pred => compile_pred comp_modifiers compfuns thy all_vs param_vs pred + (the (AList.lookup (op =) preds pred))) moded_clauses + +fun prove options thy clauses preds modes moded_clauses compiled_terms = + map_preds_modes (prove_pred options thy clauses preds modes) (join_preds_modes moded_clauses compiled_terms) -fun prove_by_skip thy _ _ _ _ compiled_terms = +fun prove_by_skip options thy _ _ _ _ compiled_terms = map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t)) compiled_terms + +fun dest_prem thy params t = + (case strip_comb t of + (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t + | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of + Prem (ts, t) => Negprem (ts, t) + | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) + | Sidecond t => Sidecond (c $ t)) + | (c as Const (s, _), ts) => + if is_registered thy s then + let val (ts1, ts2) = chop (nparams_of thy s) ts + in Prem (ts2, list_comb (c, ts1)) end + else Sidecond t + | _ => Sidecond t) -fun prepare_intrs thy prednames = +fun prepare_intrs thy prednames intros = let - val intrs = maps (intros_of thy) prednames - |> map (Logic.unvarify o prop_of) + val intrs = map prop_of intros val nparams = nparams_of thy (hd prednames) + val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames + val (preds, intrs) = unify_consts thy preds intrs + val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] (ProofContext.init thy) + val preds = map dest_Const preds val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name) - val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs) - val _ $ u = Logic.strip_imp_concl (hd intrs); - val params = List.take (snd (strip_comb u), nparams); + val params = case intrs of + [] => + let + val (paramTs, _) = chop nparams (binder_types (snd (hd preds))) + val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i) (1 upto length paramTs)) + in map Free (param_names ~~ paramTs) end + | intr :: _ => fst (chop nparams + (snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))))) val param_vs = maps term_vs params val all_vs = terms_vs intrs - fun dest_prem t = - (case strip_comb t of - (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t - | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem t of - Prem (ts, t) => Negprem (ts, t) - | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) - | Sidecond t => Sidecond (c $ t)) - | (c as Const (s, _), ts) => - if is_registered thy s then - let val (ts1, ts2) = chop (nparams_of thy s) ts - in Prem (ts2, list_comb (c, ts1)) end - else Sidecond t - | _ => Sidecond t) fun add_clause intr (clauses, arities) = let val _ $ t = Logic.strip_imp_concl intr; val (Const (name, T), ts) = strip_comb t; val (ts1, ts2) = chop nparams ts; - val prems = map (dest_prem o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr); + val prems = map (dest_prem thy params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr); val (Ts, Us) = chop nparams (binder_types T) in (AList.update op = (name, these (AList.lookup op = clauses name) @ @@ -2177,31 +2114,74 @@ val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end; +fun check_format_of_intro_rule thy intro = + let + val concl = Logic.strip_imp_concl (prop_of intro) + val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) + val params = List.take (args, nparams_of thy (fst (dest_Const p))) + fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of + (Ts as _ :: _ :: _) => + if (length (HOLogic.strip_tuple arg) = length Ts) then true + else + error ("Format of introduction rule is invalid: tuples must be expanded:" + ^ (Syntax.string_of_term_global thy arg) ^ " in " ^ + (Display.string_of_thm_global thy intro)) + | _ => true + val prems = Logic.strip_imp_prems (prop_of intro) + fun check_prem (Prem (args, _)) = forall check_arg args + | check_prem (Negprem (args, _)) = forall check_arg args + | check_prem _ = true + in + forall check_arg args andalso + forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems + end + +(* +fun check_intros_elim_match thy prednames = + let + fun check predname = + let + val intros = intros_of thy predname + val elim = the_elim_of thy predname + val nparams = nparams_of thy predname + val elim' = + (Drule.standard o (Skip_Proof.make_thm thy)) + (mk_casesrule (ProofContext.init thy) nparams intros) + in + if not (Thm.equiv_thm (elim, elim')) then + error "Introduction and elimination rules do not match!" + else true + end + in forall check prednames end +*) + (** main function of predicate compiler **) -fun add_equations_of steps prednames thy = +fun add_equations_of steps options prednames thy = let - val _ = tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") + val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames))) + (*val _ = check_intros_elim_match thy prednames*) + (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) = - prepare_intrs thy prednames - val _ = tracing "Infering modes..." - val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses + prepare_intrs thy prednames (maps (intros_of thy) prednames) + val _ = print_step options "Infering modes..." + val moded_clauses = #infer_modes steps options thy extra_modes all_modes param_vs clauses val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses + val _ = check_expected_modes options modes val _ = print_modes modes - val _ = print_moded_clauses thy moded_clauses - val _ = tracing "Defining executable functions..." + (*val _ = print_moded_clauses thy moded_clauses*) + val _ = print_step options "Defining executable functions..." val thy' = fold (#create_definitions steps preds) modes thy |> Theory.checkpoint - val _ = tracing "Compiling equations..." + val _ = print_step options "Compiling equations..." val compiled_terms = (#compile_preds steps) thy' all_vs param_vs preds moded_clauses - val _ = print_compiled_terms thy' compiled_terms - val _ = tracing "Proving equations..." - val result_thms = #prove steps thy' clauses preds (extra_modes @ modes) + val _ = print_compiled_terms options thy' compiled_terms + val _ = print_step options "Proving equations..." + val result_thms = #prove steps options thy' clauses preds (extra_modes @ modes) moded_clauses compiled_terms val qname = #qname steps - (* val attrib = gn thy => Attrib.attribute_i thy Code.add_eqn_attrib *) val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)))) val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss @@ -2226,7 +2206,7 @@ fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) -fun gen_add_equations steps names thy = +fun gen_add_equations steps options names thy = let val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy |> Theory.checkpoint; @@ -2235,33 +2215,83 @@ val scc = strong_conn_of (PredData.get thy') names val thy'' = fold_rev (fn preds => fn thy => - if #are_not_defined steps thy preds then add_equations_of steps preds thy else thy) + if #are_not_defined steps thy preds then + add_equations_of steps options preds thy else thy) scc thy' |> Theory.checkpoint in thy'' end (* different instantiantions of the predicate compiler *) +val predicate_comp_modifiers = + {const_name_of = predfun_name_of, + funT_of = funT_of, + additional_arguments = K [], + wrap_compilation = K (K (K (K (K I)))), + transform_additional_arguments = K I + } + +val depth_limited_comp_modifiers = + {const_name_of = depth_limited_function_name_of, + funT_of = depth_limited_funT_of, + additional_arguments = fn names => + let + val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"] + in [Free (polarity_name, @{typ "bool"}), Free (depth_name, @{typ "code_numeral"})] end, + wrap_compilation = + fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation => + let + val [polarity, depth] = additional_arguments + val (_, Ts2) = chop (length (fst mode)) (binder_types T) + val (_, Us2) = split_smodeT (snd mode) Ts2 + val T' = mk_predT compfuns (HOLogic.mk_tupleT Us2) + val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T') + val full_mode = null Us2 + in + if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) + $ (if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T') + $ (if full_mode then mk_single compfuns HOLogic.unit else Const (@{const_name undefined}, T'))) + $ compilation + end, + transform_additional_arguments = + fn prem => fn additional_arguments => + let + val [polarity, depth] = additional_arguments + val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity + val depth' = + Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"}) + $ depth $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"}) + in [polarity', depth'] end + } + +val rpred_comp_modifiers = + {const_name_of = generator_name_of, + funT_of = K generator_funT_of, + additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})], + wrap_compilation = K (K (K (K (K I)))), + transform_additional_arguments = K I + } + + val add_equations = gen_add_equations {infer_modes = infer_modes, create_definitions = create_definitions, - compile_preds = compile_preds PredicateCompFuns.compfuns mk_fun_of false, + compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns, prove = prove, are_not_defined = fn thy => forall (null o modes_of thy), qname = "equation"} -val add_sizelim_equations = gen_add_equations +val add_depth_limited_equations = gen_add_equations {infer_modes = infer_modes, - create_definitions = sizelim_create_definitions, - compile_preds = compile_preds PredicateCompFuns.compfuns mk_sizelim_fun_of true, + create_definitions = create_definitions_of_depth_limited_functions, + compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns, prove = prove_by_skip, - are_not_defined = fn thy => forall (null o sizelim_modes_of thy), - qname = "sizelim_equation" - } + are_not_defined = fn thy => forall (null o depth_limited_modes_of thy), + qname = "depth_limited_equation"} val add_quickcheck_equations = gen_add_equations {infer_modes = infer_modes_with_generator, create_definitions = rpred_create_definitions, - compile_preds = compile_preds RPredCompFuns.compfuns mk_generator_of true, + compile_preds = compile_preds rpred_comp_modifiers RPredCompFuns.compfuns, prove = prove_by_skip, are_not_defined = fn thy => forall (null o rpred_modes_of thy), qname = "rpred_equation"} @@ -2283,15 +2313,11 @@ 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 rpred raw_const lthy = +fun generic_code_pred prep_const options raw_const lthy = let val thy = ProofContext.theory_of lthy val const = prep_const thy raw_const @@ -2302,9 +2328,11 @@ val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy') fun mk_cases const = let + val T = Sign.the_const_type thy const + val pred = Const (const, T) val nparams = nparams_of thy' const val intros = intros_of thy' const - in mk_casesrule lthy' nparams intros end + in mk_casesrule lthy' pred nparams intros end val cases_rules = map mk_cases preds val cases = map (fn case_rule => RuleCases.Case {fixes = [], @@ -2320,11 +2348,14 @@ (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms) in goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> - (if rpred then - (add_equations [const] #> - add_sizelim_equations [const] #> add_quickcheck_equations [const]) - else add_equations [const])) - end + (if is_rpred options then + (add_equations options [const] #> + add_quickcheck_equations options [const]) + else if is_depth_limited options then + add_depth_limited_equations options [const] + else + add_equations options [const])) + end in Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy'' end; @@ -2335,9 +2366,11 @@ (* transformation for code generation *) val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option); +val random_eval_ref = Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option); (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) -fun analyze_compr thy t_compr = +(* TODO: *) +fun analyze_compr thy compfuns (depth_limit, random) t_compr = let val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr); @@ -2348,6 +2381,8 @@ (fn (i, t) => case t of Bound j => if j < length Ts then NONE else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*) val user_mode' = map (rpair NONE) user_mode + val all_modes_of = if random then all_generator_modes_of else all_modes_of + (*val compile_expr = if random then compile_gen_expr else compile_expr*) val modes = filter (fn Mode (_, is, _) => is = user_mode') (modes_of_term (all_modes_of thy) (list_comb (pred, params))); val m = case modes @@ -2357,7 +2392,17 @@ | m :: _ :: _ => (warning ("Multiple modes possible for comprehension " ^ 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 NONE thy (m, list_comb (pred, params)), inargs); + val additional_arguments = + case depth_limit of + NONE => (if random then [@{term "5 :: code_numeral"}] else []) + | SOME d => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d] + val comp_modifiers = + case depth_limit of NONE => + (if random then rpred_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers + val mk_fun_of = if random then mk_generator_of else + if (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of + val t_pred = compile_expr comp_modifiers compfuns thy + (m, list_comb (pred, params)) inargs additional_arguments; val t_eval = if null outargs then t_pred else let val outargs_bounds = map (fn Bound i => i) outargs; @@ -2370,22 +2415,30 @@ val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split (Term.list_abs (map (pair "") outargsTs, HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds))) - in mk_map PredicateCompFuns.compfuns T_pred T_compr arrange t_pred end + in mk_map compfuns T_pred T_compr arrange t_pred end in t_eval end; -fun eval thy t_compr = +fun eval thy (options as (depth_limit, random)) t_compr = let - 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_Core.eval_ref", eval_ref) Predicate.map thy t' []) end; + val compfuns = if random then RPredCompFuns.compfuns else PredicateCompFuns.compfuns + val t = analyze_compr thy compfuns options t_compr; + val T = dest_predT compfuns (fastype_of t); + val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t; + val eval = + if random then + Code_ML.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref) + (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' [] + |> Random_Engine.run + else + Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' [] + in (T, eval) end; -fun values ctxt k t_compr = +fun values ctxt options k t_compr = let val thy = ProofContext.theory_of ctxt; - val (T, t) = eval thy t_compr; + val (T, ts) = eval thy options t_compr; + val (ts, _) = Predicate.yieldn k ts; val setT = HOLogic.mk_setT T; - val (ts, _) = Predicate.yieldn k t; val elemsT = HOLogic.mk_set T ts; in if k = ~1 orelse length ts < k then elemsT else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr @@ -2398,11 +2451,11 @@ in end; *) -fun values_cmd modes k raw_t state = +fun values_cmd modes options k raw_t state = let val ctxt = Toplevel.context_of state; val t = Syntax.read_term ctxt raw_t; - val t' = values ctxt k t; + val t' = values ctxt options k t; val ty' = Term.type_of t'; val ctxt' = Variable.auto_fixes t' ctxt; val p = PrintMode.with_modes modes (fn () => @@ -2410,15 +2463,24 @@ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); in Pretty.writeln p end; - local structure P = OuterParse in val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; +val _ = List.app OuterKeyword.keyword ["depth_limit", "random"] + +val options = + let + val depth_limit = Scan.optional (P.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE + val random = Scan.optional (P.$$$ "random" >> K true) false + in + Scan.optional (P.$$$ "[" |-- depth_limit -- random --| P.$$$ "]") (NONE, false) + end + val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag - (opt_modes -- Scan.optional P.nat ~1 -- P.term - >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep - (values_cmd modes k t))); + (opt_modes -- options -- Scan.optional P.nat ~1 -- P.term + >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep + (values_cmd modes options k t))); end; diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/ex/Predicate_Compile.thy --- a/src/HOL/ex/Predicate_Compile.thy Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile.thy Sun Oct 25 00:10:25 2009 +0200 @@ -12,6 +12,6 @@ begin setup {* Predicate_Compile.setup *} -setup {* Quickcheck.add_generator ("pred_compile", Pred_Compile_Quickcheck.quickcheck) *} +setup {* Quickcheck.add_generator ("pred_compile", Predicate_Compile_Quickcheck.quickcheck) *} end \ No newline at end of file diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Sun Oct 25 00:10:25 2009 +0200 @@ -0,0 +1,76 @@ +theory Predicate_Compile_Alternative_Defs +imports Predicate_Compile +begin + +section {* Set operations *} +(* +definition Empty where "Empty == {}" +declare empty_def[symmetric, code_pred_inline] +*) +declare eq_reflection[OF empty_def, code_pred_inline] +(* +definition Union where "Union A B == A Un B" + +lemma [code_pred_intros]: "A x ==> Union A B x" +and [code_pred_intros] : "B x ==> Union A B x" +unfolding Union_def Un_def Collect_def mem_def by auto + +code_pred Union +unfolding Union_def Un_def Collect_def mem_def by auto + +declare Union_def[symmetric, code_pred_inline] +*) +declare eq_reflection[OF Un_def, code_pred_inline] + +section {* Alternative list definitions *} + +subsection {* Alternative rules for set *} + +lemma set_ConsI1 [code_pred_intros]: + "set (x # xs) x" +unfolding mem_def[symmetric, of _ x] +by auto + +lemma set_ConsI2 [code_pred_intros]: + "set xs x ==> set (x' # xs) x" +unfolding mem_def[symmetric, of _ x] +by auto + +code_pred set +proof - + case set + from this show thesis + apply (case_tac a1) + apply auto + unfolding mem_def[symmetric, of _ a2] + apply auto + unfolding mem_def + apply auto + done +qed + + +subsection {* Alternative rules for list_all2 *} + +lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []" +by auto + +lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)" +by auto + +code_pred list_all2 +proof - + case list_all2 + from this show thesis + apply - + apply (case_tac a1) + apply (case_tac a2) + apply auto + apply (case_tac a2) + apply auto + done +qed + + + +end \ No newline at end of file diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Sun Oct 25 00:10:25 2009 +0200 @@ -1,5 +1,5 @@ theory Predicate_Compile_ex -imports Main Predicate_Compile +imports Main Predicate_Compile_Alternative_Defs begin inductive even :: "nat \ bool" and odd :: "nat \ bool" where @@ -7,66 +7,216 @@ | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" -code_pred even . +code_pred (mode: [], [1]) even . +code_pred [depth_limited] even . +code_pred [rpred] even . thm odd.equation thm even.equation +thm odd.depth_limited_equation +thm even.depth_limited_equation +thm even.rpred_equation +thm odd.rpred_equation values "{x. even 2}" values "{x. odd 2}" values 10 "{n. even n}" values 10 "{n. odd n}" +values [depth_limit = 2] "{x. even 6}" +values [depth_limit = 7] "{x. even 6}" +values [depth_limit = 2] "{x. odd 7}" +values [depth_limit = 8] "{x. odd 7}" + +values [depth_limit = 7] 10 "{n. even n}" + +definition odd' where "odd' x == \ even x" + +code_pred [inductify] odd' . +code_pred [inductify, depth_limited] odd' . +code_pred [inductify, rpred] odd' . + +thm odd'.depth_limited_equation +values [depth_limit = 2] "{x. odd' 7}" +values [depth_limit = 9] "{x. odd' 7}" inductive append :: "'a list \ 'a list \ 'a list \ bool" where "append [] xs xs" | "append xs ys zs \ append (x # xs) ys (x # zs)" -code_pred append . -code_pred (inductify_all) (rpred) append . +code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append . +code_pred [depth_limited] append . +code_pred [rpred] append . thm append.equation +thm append.depth_limited_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}" -values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}" +values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}" +values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" +values [random] 15 "{(ys, zs). append [1::nat, 2] ys zs}" + +value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" +value [code] "Predicate.the (append_3 ([]::int list))" + +subsection {* Tricky case with alternative rules *} + +inductive append2 +where + "append2 [] xs xs" +| "append2 xs ys zs \ append2 (x # xs) ys (x # zs)" + +lemma append2_Nil: "append2 [] (xs::'b list) xs" + by (simp add: append2.intros(1)) + +lemmas [code_pred_intros] = append2_Nil append2.intros(2) + +code_pred append2 +proof - + case append2 + from append2.cases[OF append2(1)] append2(2-3) show thesis by blast +qed + +subsection {* Tricky cases with tuples *} + +inductive zerozero :: "nat * nat => bool" +where + "zerozero (0, 0)" + +code_pred zerozero . +code_pred [rpred] zerozero . + +inductive tupled_append :: "'a list \ 'a list \ 'a list \ bool" +where + "tupled_append ([], xs, xs)" +| "tupled_append (xs, ys, zs) \ tupled_append (x # xs, ys, x # zs)" + +code_pred tupled_append . +code_pred [rpred] tupled_append . +thm tupled_append.equation +(* +TODO: values with tupled modes +values "{xs. tupled_append ([1,2,3], [4,5], xs)}" +*) + +inductive tupled_append' +where +"tupled_append' ([], xs, xs)" +| "[| ys = fst (xa, y); x # zs = snd (xa, y); + tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)" + +code_pred tupled_append' . +thm tupled_append'.equation + +inductive tupled_append'' :: "'a list \ 'a list \ 'a list \ bool" +where + "tupled_append'' ([], xs, xs)" +| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \ tupled_append'' (x # xs, yszs)" + +thm tupled_append''.cases + +code_pred [inductify] tupled_append'' . +thm tupled_append''.equation + +inductive tupled_append''' :: "'a list \ 'a list \ 'a list \ bool" +where + "tupled_append''' ([], xs, xs)" +| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \ tupled_append''' (x # xs, ys, x # zs)" + +code_pred [inductify] tupled_append''' . +thm tupled_append'''.equation + +inductive map_ofP :: "('a \ 'b) list \ 'a \ 'b \ bool" +where + "map_ofP ((a, b)#xs) a b" +| "map_ofP xs a b \ map_ofP (x#xs) a b" + +code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP . +thm map_ofP.equation + +inductive filter1 +for P +where + "filter1 P [] []" +| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)" +| "\ P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys" + +code_pred (mode: [1], [1, 2]) filter1 . +code_pred [depth_limited] filter1 . +code_pred [rpred] filter1 . + +thm filter1.equation + +inductive filter2 +where + "filter2 P [] []" +| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)" +| "\ P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys" + +code_pred (mode: [1, 2, 3], [1, 2]) filter2 . +code_pred [depth_limited] filter2 . +code_pred [rpred] filter2 . +thm filter2.equation +thm filter2.rpred_equation + +inductive filter3 +for P +where + "List.filter P xs = ys ==> filter3 P xs ys" + +code_pred filter3 . +code_pred [depth_limited] filter3 . +thm filter3.depth_limited_equation +(*code_pred [rpred] filter3 .*) +inductive filter4 +where + "List.filter P xs = ys ==> filter4 P xs ys" + +code_pred filter4 . +code_pred [depth_limited] filter4 . +code_pred [rpred] filter4 . + +section {* reverse *} inductive rev where "rev [] []" | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" -code_pred rev . +code_pred (mode: [1], [2], [1, 2]) rev . thm rev.equation values "{xs. rev [0, 1, 2, 3::nat] xs}" +inductive tupled_rev where + "tupled_rev ([], [])" +| "tupled_rev (xs, xs') \ tupled_append (xs', [x], ys) \ tupled_rev (x#xs, ys)" + +code_pred tupled_rev . +thm tupled_rev.equation + inductive partition :: "('a \ bool) \ 'a list \ 'a list \ 'a list \ bool" for f where "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)" -code_pred partition . +code_pred (mode: [1], [2, 3], [1, 2], [1, 3], [1, 2, 3]) partition . +code_pred [depth_limited] partition . +code_pred [rpred] partition . -thm partition.equation +inductive tupled_partition :: "('a \ bool) \ ('a list \ 'a list \ 'a list) \ bool" + for f where + "tupled_partition f ([], [], [])" + | "f x \ tupled_partition f (xs, ys, zs) \ tupled_partition f (x # xs, x # ys, zs)" + | "\ f x \ tupled_partition f (xs, ys, zs) \ tupled_partition f (x # xs, ys, x # zs)" + +code_pred tupled_partition . + +thm tupled_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" @@ -88,18 +238,20 @@ case tranclp from this converse_tranclpE[OF this(1)] show thesis by metis qed -(* -code_pred (inductify_all) (rpred) tranclp . + +code_pred [depth_limited] tranclp . +code_pred [rpred] tranclp . thm tranclp.equation thm tranclp.rpred_equation -*) + inductive succ :: "nat \ nat \ bool" where "succ 0 1" | "succ m n \ succ (Suc m) (Suc n)" code_pred succ . - +code_pred [rpred] succ . thm succ.equation +thm succ.rpred_equation values 10 "{(m, n). succ n m}" values "{m. succ 0 m}" @@ -141,6 +293,16 @@ (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1)))) [3,5] t}" +inductive tupled_exec :: "(com \ state \ state) \ bool" where +"tupled_exec (Skip, s, s)" | +"tupled_exec (Ass x e, s, s[x := e(s)])" | +"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" | +"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" | +"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" | +"~b s ==> tupled_exec (While b c, s, s)" | +"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)" + +code_pred tupled_exec . subsection{* CCS *} @@ -171,6 +333,17 @@ values 3 "{(a,q). step (par nil nil) a q}" *) +inductive tupled_step :: "(proc \ nat \ proc) \ bool" +where +"tupled_step (pre n p, n, p)" | +"tupled_step (p1, a, q) \ tupled_step (or p1 p2, a, q)" | +"tupled_step (p2, a, q) \ tupled_step (or p1 p2, a, q)" | +"tupled_step (p1, a, q) \ tupled_step (par p1 p2, a, par q p2)" | +"tupled_step (p2, a, q) \ tupled_step (par p1 p2, a, par p1 q)" + +code_pred tupled_step . +thm tupled_step.equation + subsection {* divmod *} inductive divmod_rel :: "nat \ nat \ nat \ nat \ bool" where @@ -179,52 +352,75 @@ code_pred divmod_rel .. -value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)" +value [code] "Predicate.the (divmod_rel_1_2 1705 42)" section {* 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] Min . subsection {* Examples with lists *} -inductive filterP for Pa where -"(filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) [] []" -| "[| (res::'a list) = (y::'a) # (resa::'a list); (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) resa; Pa y |] -==> filterP Pa (y # xt) res" -| "[| (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) (res::'a list); ~ Pa (y::'a) |] ==> filterP Pa (y # xt) res" +subsubsection {* Lexicographic order *} + +thm lexord_def +code_pred [inductify] lexord . +code_pred [inductify, rpred] lexord . +thm lexord.equation +thm lexord.rpred_equation + +inductive less_than_nat :: "nat * nat => bool" +where + "less_than_nat (0, x)" +| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)" + +code_pred less_than_nat . + +code_pred [depth_limited] less_than_nat . +code_pred [rpred] less_than_nat . +inductive test_lexord :: "nat list * nat list => bool" +where + "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)" + +code_pred [rpred] test_lexord . +code_pred [depth_limited] test_lexord . +thm test_lexord.depth_limited_equation +thm test_lexord.rpred_equation + +values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" +values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" +(*values [random] "{xys. test_lexord xys}"*) +(*values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}"*) (* -code_pred (inductify_all) (rpred) filterP . -thm filterP.rpred_equation +lemma "(u, v) : lexord less_than_nat ==> (x @ u, y @ v) : lexord less_than_nat" +quickcheck[generator=pred_compile] +oops *) - -code_pred (inductify_all) lexord . - -thm lexord.equation - -lemma "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r" -(*quickcheck[generator=pred_compile]*) -oops - lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv -code_pred (inductify_all) lexn . +code_pred [inductify] lexn . thm lexn.equation -code_pred (inductify_all) lenlex . +code_pred [rpred] lexn . + +thm lexn.rpred_equation + +code_pred [inductify, show_steps] lenlex . thm lenlex.equation -(* -code_pred (inductify_all) (rpred) lenlex . + +code_pred [inductify, rpred] lenlex . thm lenlex.rpred_equation -*) + thm lists.intros -code_pred (inductify_all) lists . +code_pred [inductify] lists . thm lists.equation +section {* AVL Tree Example *} + datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat fun height :: "'a tree => nat" where "height ET = 0" @@ -236,40 +432,107 @@ "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 . +code_pred [inductify] avl . thm avl.equation -lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\(y::'a::type). False)" -unfolding bot_fun_inst.bot_fun[symmetric] bot_bool_eq[symmetric] bot_fun_eq by simp +code_pred [rpred] avl . +thm avl.rpred_equation +(*values [random] 10 "{t. avl (t::int tree)}"*) 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 +fun is_ord :: "nat tree => bool" 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] - -code_pred (inductify_all) set_of . +code_pred (mode: [1], [1, 2]) [inductify] set_of . thm set_of.equation -(* FIXME *) -(* -code_pred (inductify_all) is_ord . + +code_pred [inductify] is_ord . thm is_ord.equation -*) +code_pred [rpred] is_ord . +thm is_ord.rpred_equation + section {* Definitions about Relations *} -code_pred (inductify_all) converse . +code_pred [inductify] converse . thm converse.equation +code_pred [inductify] rel_comp . +thm rel_comp.equation +code_pred [inductify] Image . +thm Image.equation +(*TODO: *) +ML {* Toplevel.debug := true *} +declare Id_on_def[unfolded UNION_def, code_pred_def] + +code_pred [inductify] Id_on . +thm Id_on.equation +code_pred [inductify] Domain . +thm Domain.equation +code_pred [inductify] Range . +thm sym_def +code_pred [inductify] Field . +declare Sigma_def[unfolded UNION_def, code_pred_def] +declare refl_on_def[unfolded UNION_def, code_pred_def] +code_pred [inductify] refl_on . +thm refl_on.equation +code_pred [inductify] total_on . +thm total_on.equation +(* +code_pred [inductify] sym . +thm sym.equation +*) +code_pred [inductify] antisym . +thm antisym.equation +code_pred [inductify] trans . +thm trans.equation +code_pred [inductify] single_valued . +thm single_valued.equation +code_pred [inductify] inv_image . +thm inv_image.equation -code_pred (inductify_all) Domain . -thm Domain.equation +section {* List functions *} + +code_pred [inductify] length . +thm size_listP.equation +code_pred [inductify, rpred] length . +thm size_listP.rpred_equation +values [random] 20 "{xs. size_listP (xs::nat list) (5::nat)}" +code_pred [inductify] concat . +code_pred [inductify] hd . +code_pred [inductify] tl . +code_pred [inductify] last . +code_pred [inductify] butlast . +(*code_pred [inductify] listsum .*) +code_pred [inductify] take . +code_pred [inductify] drop . +code_pred [inductify] zip . +code_pred [inductify] upt . +code_pred [inductify] remdups . +code_pred [inductify] remove1 . +code_pred [inductify] removeAll . +code_pred [inductify] distinct . +code_pred [inductify] replicate . +code_pred [inductify] splice . +code_pred [inductify] List.rev . +code_pred [inductify] map . +code_pred [inductify] foldr . +code_pred [inductify] foldl . +code_pred [inductify] filter . +code_pred [inductify, rpred] filter . +thm filterP.rpred_equation + +definition test where "test xs = filter (\x. x = (1::nat)) xs" +code_pred [inductify] test . +thm testP.equation +code_pred [inductify, rpred] test . +thm testP.rpred_equation section {* Context Free Grammar *} @@ -283,15 +546,86 @@ | "w \ S\<^isub>1 \ b # w \ S\<^isub>1" | "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" -code_pred (inductify_all) S\<^isub>1p . +code_pred [inductify] S\<^isub>1p . +code_pred [inductify, rpred] S\<^isub>1p . +thm S\<^isub>1p.equation +thm S\<^isub>1p.rpred_equation -thm S\<^isub>1p.equation +values [random] 5 "{x. S\<^isub>1p x}" + +inductive is_a where + "is_a a" + +inductive is_b where + "is_b b" -theorem S\<^isub>1_sound: -"w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=pred_compile] +code_pred is_a . +code_pred [depth_limited] is_a . +code_pred [rpred] is_a . + +values [random] "{x. is_a x}" +code_pred [depth_limited] is_b . +code_pred [rpred] is_b . + +code_pred [inductify, depth_limited] filter . + +values [depth_limit=5] "{x. filterP is_a [a, b] x}" +values [depth_limit=3] "{x. filterP is_b [a, b] x}" + +lemma "w \ S\<^isub>1 \ length (filter (\x. x = a) w) = 1" +(*quickcheck[generator=pred_compile, size=10]*) oops +inductive test_lemma where + "S\<^isub>1p w ==> filterP is_a w r1 ==> size_listP r1 r2 ==> filterP is_b w r3 ==> size_listP r3 r4 ==> r2 \ r4 ==> test_lemma w" +(* +code_pred [rpred] test_lemma . +*) +(* +definition test_lemma' where + "test_lemma' w == (w \ S\<^isub>1 \ (\ length [x <- w. x = a] = length [x <- w. x = b]))" + +code_pred [inductify, rpred] test_lemma' . +thm test_lemma'.rpred_equation +*) +(*thm test_lemma'.rpred_equation*) +(* +values [depth_limit=3 random] "{x. S\<^isub>1 x}" +*) +code_pred [depth_limited] is_b . +(* +code_pred [inductify, depth_limited] filter . +*) +thm filterP.intros +thm filterP.equation +(* +values [depth_limit=3] "{x. filterP is_b [a, b] x}" +find_theorems "test_lemma'_hoaux" +code_pred [depth_limited] test_lemma'_hoaux . +thm test_lemma'_hoaux.depth_limited_equation +values [depth_limit=2] "{x. test_lemma'_hoaux b}" +inductive test1 where + "\ test_lemma'_hoaux x ==> test1 x" +code_pred test1 . +code_pred [depth_limited] test1 . +thm test1.depth_limited_equation +thm test_lemma'_hoaux.depth_limited_equation +thm test1.intros + +values [depth_limit=2] "{x. test1 b}" + +thm filterP.intros +thm filterP.depth_limited_equation +values [depth_limit=3] "{x. filterP test_lemma'_hoaux [a, b] x}" +values [depth_limit=4 random] "{w. test_lemma w}" +values [depth_limit=4 random] "{w. test_lemma' w}" +*) +(* +theorem S\<^isub>1_sound: +"w \ S\<^isub>1p \ length [x \ w. x = a] = length [x \ w. x = b]" +quickcheck[generator=pred_compile, size=15] +oops +*) inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where "[] \ S\<^isub>2" | "w \ A\<^isub>2 \ b # w \ S\<^isub>2" @@ -299,14 +633,18 @@ | "w \ S\<^isub>2 \ a # w \ A\<^isub>2" | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" -(* -code_pred (inductify_all) (rpred) S\<^isub>2 . -ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name "B\<^isub>2"} *} -*) + +code_pred [inductify, rpred] S\<^isub>2 . +thm S\<^isub>2.rpred_equation +thm A\<^isub>2.rpred_equation +thm B\<^isub>2.rpred_equation + +values [random] 10 "{x. S\<^isub>2 x}" + theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" (*quickcheck[generator=SML]*) -quickcheck[generator=pred_compile, size=15, iterations=100] +(*quickcheck[generator=pred_compile, size=15, iterations=1]*) oops inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where @@ -317,23 +655,35 @@ | "w \ S\<^isub>3 \ b # w \ B\<^isub>3" | "\v \ B\<^isub>3; w \ B\<^isub>3\ \ a # v @ w \ B\<^isub>3" +code_pred [inductify] S\<^isub>3 . +thm S\<^isub>3.equation + +values 10 "{x. S\<^isub>3 x}" (* -code_pred (inductify_all) S\<^isub>3 . -*) theorem S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" quickcheck[generator=pred_compile, size=10, iterations=1] oops - +*) lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])" -quickcheck[size=10, generator = pred_compile] +(*quickcheck[size=10, generator = pred_compile]*) oops +(* +inductive test +where + "length [x \ w. a = x] = length [x \ w. x = b] ==> test w" +ML {* @{term "[x \ w. x = a]"} *} +code_pred (inductify_all) test . +thm test.equation +*) +(* theorem S\<^isub>3_complete: -"length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>3" +"length [x \ w. x = a] = length [x \ w. b = x] \ w \ S\<^isub>3" (*quickcheck[generator=SML]*) quickcheck[generator=pred_compile, size=10, iterations=100] oops +*) inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where "[] \ S\<^isub>4" @@ -343,15 +693,15 @@ | "\v \ A\<^isub>4; w \ A\<^isub>4\ \ b # v @ w \ A\<^isub>4" | "w \ S\<^isub>4 \ b # w \ B\<^isub>4" | "\v \ B\<^isub>4; w \ B\<^isub>4\ \ a # v @ w \ B\<^isub>4" - +(* theorem S\<^isub>4_sound: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" quickcheck[generator = pred_compile, size=2, iterations=1] oops - +*) theorem S\<^isub>4_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" -quickcheck[generator = pred_compile, size=5, iterations=1] +(*quickcheck[generator = pred_compile, size=5, iterations=1]*) oops theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete: @@ -361,8 +711,8 @@ (*quickcheck[generator = pred_compile, size=5, iterations=1]*) oops +section {* Lambda *} -section {* Lambda *} datatype type = Atom nat | Fun type type (infixr "\" 200) @@ -378,15 +728,15 @@ "[]\i\ = None" | "(x # xs)\i\ = (case i of 0 \ Some x | Suc j \ xs \j\)" -(* + inductive nth_el' :: "'a list \ nat \ 'a \ bool" where "nth_el' (x # xs) 0 x" | "nth_el' xs i y \ nth_el' (x # xs) (Suc i) y" -*) + inductive typing :: "type list \ dB \ type \ bool" ("_ \ _ : _" [50, 50, 50] 50) where - Var [intro!]: "nth_el env x = Some T \ env \ Var x : T" + Var [intro!]: "nth_el' env x T \ env \ Var x : T" | Abs [intro!]: "T # env \ t : U \ env \ Abs T t : (T \ U)" (* | App [intro!]: "env \ s : T \ U \ env \ t : T \ env \ (s \ t) : U" *) | App [intro!]: "env \ s : U \ T \ env \ t : T \ env \ (s \ t) : U" @@ -414,22 +764,8 @@ | abs [simp, intro!]: "s \\<^sub>\ t ==> Abs T s \\<^sub>\ Abs T t" lemma "Gamma \ t : T \ t \\<^sub>\ t' \ Gamma \ t' : T" -quickcheck[generator = pred_compile, size = 10, iterations = 1000] +(*quickcheck[generator = pred_compile, size = 10, iterations = 1]*) oops -(* FIXME *) -(* -inductive test for P where -"[| filter P vs = res |] -==> test P vs res" - -code_pred test . -*) -(* -export_code test_for_1_yields_1_2 in SML file - -code_pred (inductify_all) (rpred) test . - -thm test.equation -*) lemma filter_eq_ConsD: "filter P ys = x#xs \ diff -r 9d7d0bef2a77 -r b8f4c2107a62 src/HOL/ex/RPred.thy --- a/src/HOL/ex/RPred.thy Sun Oct 25 00:05:57 2009 +0200 +++ b/src/HOL/ex/RPred.thy Sun Oct 25 00:10:25 2009 +0200 @@ -2,7 +2,7 @@ imports Quickcheck Random Predicate begin -types 'a rpred = "Random.seed \ ('a Predicate.pred \ Random.seed)" +types 'a "rpred" = "Random.seed \ ('a Predicate.pred \ Random.seed)" section {* The RandomPred Monad *} @@ -33,9 +33,9 @@ (* Missing a good definition for negation: not_rpred *) -definition not_rpred :: "unit Predicate.pred \ unit rpred" +definition not_rpred :: "unit rpred \ unit rpred" where - "not_rpred = Pair o Predicate.not_pred" + "not_rpred P = (\s. let (P', s') = P s in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))" definition lift_pred :: "'a Predicate.pred \ 'a rpred" where @@ -44,9 +44,9 @@ definition lift_random :: "(Random.seed \ ('a \ (unit \ term)) \ Random.seed) \ 'a rpred" where "lift_random g = scomp g (Pair o (Predicate.single o fst))" -definition map_rpred :: "('a \ 'b) \ ('a rpred \ 'b rpred)" -where "map_rpred f P = bind P (return o f)" +definition map :: "('a \ 'b) \ ('a rpred \ 'b rpred)" + where "map f P = bind P (return o f)" -hide (open) const return bind supp +hide (open) const return bind supp map end \ No newline at end of file