# HG changeset patch # User panny # Date 1379543553 -7200 # Node ID e176d6d3345f69afb7b6292b8beb5b0abd845c35 # Parent ccaceea6c768ce7a39677932500962ceedf94c61 generate more theorems (e.g. for types with only one constructor) diff -r ccaceea6c768 -r e176d6d3345f src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 18 18:11:32 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 19 00:32:33 2013 +0200 @@ -1624,13 +1624,15 @@ appears directly to the right of the equal sign: *} - primcorec_notyet literate :: "('a \ 'a) \ 'a \ 'a llist" where + primcorec literate :: "('a \ 'a) \ 'a \ 'a llist" where "literate f x = LCons x (literate f (f x))" + . text {* \blankline *} - primcorec_notyet siterate :: "('a \ 'a) \ 'a \ 'a stream" where + primcorec siterate :: "('a \ 'a) \ 'a \ 'a stream" where "siterate f x = SCons x (siterate f (f x))" + . text {* \noindent @@ -1648,7 +1650,6 @@ (*<*) locale dummy_dest_view begin -end (*>*) primcorec literate :: "('a \ 'a) \ 'a \ 'a llist" where "\ lnull (literate _ x)" | @@ -1663,7 +1664,7 @@ "stl (siterate f x) = siterate f (f x)" . (*<*) -(* end*) + end (*>*) text {* @@ -1680,8 +1681,9 @@ element in a stream: *} - primcorec_notyet every_snd :: "'a stream \ 'a stream" where + primcorec every_snd :: "'a stream \ 'a stream" where "every_snd s = SCons (shd s) (stl (stl s))" + . text {* \noindent @@ -1735,8 +1737,9 @@ Corecursion is useful to specify not only functions but also infinite objects: *} - primcorec_notyet infty :: enat where + primcorec infty :: enat where "infty = ESuc infty" + . text {* \noindent @@ -1818,12 +1821,13 @@ datatypes is anything but surprising. Following the constructor view: *} - primcorec_notyet + primcorec even_infty :: even_enat and odd_infty :: odd_enat where "even_infty = Even_ESuc odd_infty" | "odd_infty = Odd_ESuc even_infty" + . text {* And following the destructor view: @@ -1856,13 +1860,15 @@ tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}): *} - primcorec_notyet iterate\<^sub>i\<^sub>i :: "('a \ 'a llist) \ 'a \ 'a tree\<^sub>i\<^sub>i" where + primcorec iterate\<^sub>i\<^sub>i :: "('a \ 'a llist) \ 'a \ 'a tree\<^sub>i\<^sub>i" where "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))" + . text {* \blankline *} - primcorec_notyet iterate\<^sub>i\<^sub>s :: "('a \ 'a fset) \ 'a \ 'a tree\<^sub>i\<^sub>s" where + primcorec iterate\<^sub>i\<^sub>s :: "('a \ 'a fset) \ 'a \ 'a tree\<^sub>i\<^sub>s" where "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))" + . text {* Again, let us not forget our destructor-oriented passengers. Here is the first @@ -1889,8 +1895,9 @@ function translates a DFA into a @{type state_machine}: *} - primcorec_notyet of_dfa :: "('q \ 'a \ 'q) \ 'q set \ 'q \ 'a state_machine" where + primcorec of_dfa :: "('q \ 'a \ 'q) \ 'q set \ 'q \ 'a state_machine" where "of_dfa \ F q = State_Machine (q \ F) (of_dfa \ F o \ q)" + . subsubsection {* Nested-as-Mutual Corecursion diff -r ccaceea6c768 -r e176d6d3345f src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 18 18:11:32 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 19 00:32:33 2013 +0200 @@ -661,15 +661,17 @@ |> rpair exclss' end; -fun mk_real_disc_eqns fun_binding arg_Ts {ctr_specs, ...} disc_eqns = +fun mk_real_disc_eqns fun_binding arg_Ts {ctr_specs, ...} sel_eqns disc_eqns = if length disc_eqns <> length ctr_specs - 1 then disc_eqns else let val n = 0 upto length ctr_specs |> the o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)); + val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns) + |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options; val extra_disc_eqn = { fun_name = Binding.name_of fun_binding, fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))), - fun_args = the_default (map (curry Free Name.uu) arg_Ts) (try (#fun_args o hd) disc_eqns), + fun_args = fun_args, ctr = #ctr (nth ctr_specs n), ctr_no = n, disc = #disc (nth ctr_specs n), @@ -718,7 +720,7 @@ val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); val arg_Tss = map (binder_types o snd o fst) fixes; - val disc_eqnss = map4 mk_real_disc_eqns bs arg_Tss corec_specs disc_eqnss'; + val disc_eqnss = map5 mk_real_disc_eqns bs arg_Tss corec_specs sel_eqnss disc_eqnss'; val (defs, exclss') = co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss; @@ -744,13 +746,12 @@ fun prove_disc {ctr_specs, ...} exclsss {fun_name, fun_T, fun_args, ctr_no, prems, user_eqn, ...} = - if user_eqn = undef_const then [] else + if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\x. x = x"}) then [] else let - val disc_corec = nth ctr_specs ctr_no |> #disc_corec; + val {disc_corec, ...} = nth ctr_specs ctr_no; val k = 1 + ctr_no; val m = length prems; val t = - (* FIXME use applied_fun from dissect_\ instead? *) list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)) |> curry betapply (#disc (nth ctr_specs ctr_no)) (*###*) |> HOLogic.mk_Trueprop @@ -790,22 +791,24 @@ fun prove_ctr (_, disc_thms) (_, sel_thms') disc_eqns sel_eqns {ctr, disc, sels, collapse, ...} = +let val _ = tracing ("disc = " ^ @{make_string} disc); in if not (exists (equal ctr o #ctr) disc_eqns) -andalso (warning ("no disc_eqn for ctr " ^ Syntax.string_of_term lthy ctr); true) - orelse (* don't try to prove theorems where some sel_eqns are missing *) + andalso not (exists (equal ctr o #ctr) sel_eqns) +andalso (warning ("no eqns for ctr " ^ Syntax.string_of_term lthy ctr); true) + orelse (* don't try to prove theorems when some sel_eqns are missing *) filter (equal ctr o #ctr) sel_eqns |> fst o finds ((op =) o apsnd #sel) sels |> exists (null o snd) andalso (warning ("sel_eqn(s) missing for ctr " ^ Syntax.string_of_term lthy ctr); true) - orelse - #user_eqn (the (find_first (equal ctr o #ctr) disc_eqns)) = undef_const -andalso (warning ("auto-generated disc_eqn for ctr " ^ Syntax.string_of_term lthy ctr); true) then [] else let val _ = tracing ("ctr = " ^ Syntax.string_of_term lthy ctr); -val _ = tracing ("disc = " ^ Syntax.string_of_term lthy (#disc (the (find_first (equal ctr o #ctr) disc_eqns)))); - val {fun_name, fun_T, fun_args, prems, ...} = - the (find_first (equal ctr o #ctr) disc_eqns); +val _ = tracing (the_default "NO disc_eqn" (Option.map (curry (op ^) "disc = " o Syntax.string_of_term lthy o #disc) (find_first (equal ctr o #ctr) disc_eqns))); + val (fun_name, fun_T, fun_args, prems) = + (find_first (equal ctr o #ctr) disc_eqns, find_first (equal ctr o #ctr) sel_eqns) + |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x)) + ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [])) + |> the o merge_options; val m = length prems; val t = sel_eqns |> fst o finds ((op =) o apsnd #sel) sels @@ -816,17 +819,19 @@ |> HOLogic.mk_Trueprop |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) |> curry Logic.list_all (map dest_Free fun_args); - val disc_thm = the_default TrueI (AList.lookup (op =) disc_thms disc); + val maybe_disc_thm = AList.lookup (op =) disc_thms disc; val sel_thms = map snd (filter (member (op =) sels o fst) sel_thms'); val _ = tracing ("t = " ^ Syntax.string_of_term lthy t); val _ = tracing ("m = " ^ @{make_string} m); val _ = tracing ("collapse = " ^ @{make_string} collapse); -val _ = tracing ("disc_thm = " ^ @{make_string} disc_thm); +val _ = tracing ("maybe_disc_thm = " ^ @{make_string} maybe_disc_thm); val _ = tracing ("sel_thms = " ^ @{make_string} sel_thms); in - mk_primcorec_ctr_of_dtr_tac lthy m collapse disc_thm sel_thms + mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms |> K |> Goal.prove lthy [] [] t |> single +(*handle ERROR x => (warning x; []))*) +end end; val (disc_notes, disc_thmss) = diff -r ccaceea6c768 -r e176d6d3345f src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 18 18:11:32 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Thu Sep 19 00:32:33 2013 +0200 @@ -10,7 +10,7 @@ val mk_primcorec_assumption_tac: Proof.context -> tactic val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic - val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic + val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> thm list -> thm list -> thm list -> tactic val mk_primcorec_disc_of_ctr_tac: thm -> thm -> tactic; @@ -63,9 +63,9 @@ if_cancel[of _ False] o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl); -fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_f sel_fs = +fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs = HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN' - rtac disc_f THEN' REPEAT_DETERM_N m o atac) THEN + (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl); fun mk_primcorec_disc_of_ctr_tac discI f_ctr =