# HG changeset patch # User panny # Date 1380028619 -7200 # Node ID 6304b12c7627ff1717d7383f6d2910bb9fcde2c5 # Parent 9bae89bb032ce816b0a417e51fa0f1f79e227f18 add "primcorec" command (cf. ae7f50e70c09) diff -r 9bae89bb032c -r 6304b12c7627 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Sep 24 14:07:23 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Sep 24 15:16:59 2013 +0200 @@ -10,19 +10,14 @@ theory Datatypes imports Setup keywords - "primcorec" :: thy_goal and "primcorecursive_notyet" :: thy_decl begin (*<*) -(* FIXME: Temporary setup until "primcorec" and "primcorecursive" are fully - implemented. *) +(* FIXME: Temporary setup until "primcorec" and "primcorecursive" are fully implemented. *) ML_command {* fun add_dummy_cmd _ _ lthy = lthy; -val _ = Outer_Syntax.local_theory @{command_spec "primcorec"} "" - (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd); - val _ = Outer_Syntax.local_theory @{command_spec "primcorecursive_notyet"} "" (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd); *} diff -r 9bae89bb032c -r 6304b12c7627 src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Tue Sep 24 14:07:23 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Tue Sep 24 15:16:59 2013 +0200 @@ -11,7 +11,8 @@ imports BNF_FP_Base Equiv_Relations_More "~~/src/HOL/Library/Sublist" keywords "codatatype" :: thy_decl and - "primcorecursive" :: thy_goal + "primcorecursive" :: thy_goal and + "primcorec" :: thy_decl begin lemma sum_case_expand_Inr: "f o Inl = g \ f x = sum_case g (f o Inr) x" diff -r 9bae89bb032c -r 6304b12c7627 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Tue Sep 24 14:07:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Tue Sep 24 15:16:59 2013 +0200 @@ -12,6 +12,9 @@ val add_primcorecursive_cmd: bool -> (binding * string option * mixfix) list * (Attrib.binding * string) list -> Proof.context -> Proof.state + val add_primcorec_cmd: bool -> + (binding * string option * mixfix) list * (Attrib.binding * string) list -> local_theory -> + local_theory end; structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR = @@ -387,7 +390,7 @@ if null eqns then error ("primrec_new error:\n " ^ str) else error ("primrec_new error:\n " ^ str ^ "\nin\n " ^ - space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)) + space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)); @@ -401,6 +404,7 @@ ctr_no: int, (*###*) disc: term, prems: term list, + auto_gen: bool, user_eqn: term }; type co_eqn_data_sel = { @@ -469,6 +473,7 @@ ctr_no = ctr_no, disc = #disc (nth ctr_specs ctr_no), prems = real_prems, + auto_gen = catch_all, user_eqn = user_eqn }, matchedsss') end; @@ -649,10 +654,11 @@ val exclss' = disc_eqnss - |> map (map (fn {fun_args, ctr_no, prems, ...} => (fun_args, ctr_no, prems)) + |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x)) #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs []) #> maps (uncurry (map o pair) - #> map (fn ((fun_args, c, x), (_, c', y)) => ((c, c'), (x, s_not (mk_conjs y))) + #> map (fn ((fun_args, c, x, a), (_, c', y, a')) => + ((c, c', a orelse a'), (x, s_not (mk_conjs y))) ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop ||> Logic.list_implies ||> curry Logic.list_all (map dest_Free fun_args)))) @@ -680,12 +686,13 @@ ctr_no = n, disc = #disc (nth ctr_specs n), prems = maps (invert_prems o #prems) disc_eqns, + auto_gen = true, user_eqn = undef_const}; in chop n disc_eqns ||> cons extra_disc_eqn |> (op @) end; -fun add_primcorec sequential fixes specs lthy = +fun add_primcorec simple sequential fixes specs lthy = let val (bs, mxs) = map_split (apfst fst) fixes; val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list; @@ -723,10 +730,16 @@ val (defs, exclss') = co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss; - (* try to prove (automatically generated) tautologies by ourselves *) - val exclss'' = exclss' - |> map (map (apsnd - (`(try (fn t => Goal.prove lthy [] [] t (mk_primcorec_assumption_tac lthy |> K)))))); + fun prove_excl_tac (c, c', a) = + if a orelse c = c' orelse sequential then SOME (K (mk_primcorec_assumption_tac lthy)) + else if simple then SOME (K (auto_tac lthy)) + else NONE; + +val _ = tracing ("exclusiveness properties:\n \ " ^ + space_implode "\n \ " (maps (map (Syntax.string_of_term lthy o snd)) exclss')); + + val exclss'' = exclss' |> map (map (fn (idx, t) => + (idx, (Option.map (Goal.prove lthy [] [] t) (prove_excl_tac idx), t)))); val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss''; val (obligation_idxss, obligationss) = exclss'' |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd)) @@ -739,7 +752,7 @@ val exclss' = map (op ~~) (obligation_idxss ~~ thmss'); fun mk_exclsss excls n = (excls, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1)) - |-> fold (fn ((c, c'), thm) => nth_map c (nth_map c' (K [thm]))); + |-> fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm]))); val exclssss = (exclss' ~~ taut_thmss |> map (op @), fun_names ~~ corec_specs) |-> map2 (fn excls => fn (_, {ctr_specs, ...}) => mk_exclsss excls (length ctr_specs)); @@ -799,8 +812,6 @@ andalso (warning ("sel_eqn(s) missing for ctr " ^ Syntax.string_of_term lthy ctr); true) then [] else let -val _ = tracing ("ctr = " ^ Syntax.string_of_term lthy ctr); -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)) @@ -818,11 +829,6 @@ |> curry Logic.list_all (map dest_Free fun_args); val maybe_disc_thm = AList.lookup (op =) disc_alist disc; val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist); -val _ = tracing ("t = " ^ Syntax.string_of_term lthy t); -val _ = tracing ("m = " ^ @{make_string} m); -val _ = tracing ("collapse = " ^ @{make_string} collapse); -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 maybe_disc_thm sel_thms |> K |> Goal.prove lthy [] [] t @@ -838,9 +844,7 @@ (map #ctr_specs corec_specs); val safess = map (map (K false)) ctr_thmss; (* FIXME: "true" for non-corecursive theorems *) - val safe_ctr_thmss = - map2 (map_filter (fn (safe, thm) => if safe then SOME thm else NONE) oo curry (op ~~)) - safess ctr_thmss; + val safe_ctr_thmss = map (map snd o filter fst o (op ~~)) (safess ~~ ctr_thmss); fun mk_simp_thms disc_thms sel_thms ctr_thms = disc_thms @ sel_thms @ ctr_thms; @@ -875,24 +879,38 @@ in lthy |> Local_Theory.notes (anonymous_notes @ notes @ common_notes) |> snd end; + + fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss'; + + val _ = if not simple orelse forall null obligationss then () else + primrec_error "need exclusiveness proofs - use primcorecursive instead of primcorec"; in - lthy' - |> Proof.theorem NONE (curry (op #->) (fold_map Local_Theory.define defs) o prove) obligationss - |> Proof.refine (Method.primitive_text I) - |> Seq.hd - end + if simple then + lthy' + |> after_qed (map (fn [] => []) obligationss) + |> pair NONE o SOME + else + lthy' + |> Proof.theorem NONE after_qed obligationss + |> Proof.refine (Method.primitive_text I) + |> Seq.hd + |> rpair NONE o SOME + end; -fun add_primcorecursive_cmd seq (raw_fixes, raw_specs) lthy = +fun add_primcorec_ursive_cmd simple seq (raw_fixes, raw_specs) lthy = let val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy); in - add_primcorec seq fixes specs lthy + add_primcorec simple seq fixes specs lthy handle ERROR str => primrec_error str end handle Primrec_Error (str, eqns) => if null eqns then error ("primcorec error:\n " ^ str) else error ("primcorec error:\n " ^ str ^ "\nin\n " ^ - space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)) + space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)); + +val add_primcorecursive_cmd = (the o fst) ooo add_primcorec_ursive_cmd false; +val add_primcorec_cmd = (the o snd) ooo add_primcorec_ursive_cmd true; end; diff -r 9bae89bb032c -r 6304b12c7627 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue Sep 24 14:07:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue Sep 24 15:16:59 2013 +0200 @@ -2926,4 +2926,9 @@ ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) -- (Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorecursive_cmd); +val _ = Outer_Syntax.local_theory @{command_spec "primcorec"} + "define primitive corecursive functions" + ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) -- + (Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorec_cmd); + end;