# HG changeset patch # User panny # Date 1385407522 -3600 # Node ID c822230fd22b6ce3e0475c211c9900049c9bd838 # Parent 19cd731eb745e81a864edb0f0149c256e25ec3a8 prevent exception when equations for a function are missing; pave the way for "exhaustive" diff -r 19cd731eb745 -r c822230fd22b src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Nov 25 18:18:58 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Nov 25 20:25:22 2013 +0100 @@ -2921,19 +2921,23 @@ Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes" (parse_co_datatype_cmd Greatest_FP construct_gfp); -val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true); +val option_parser = Parse.group (fn () => "option") + ((Parse.reserved "sequential" >> K Option_Sequential) + || (Parse.reserved "exhaustive" >> K Option_Exhaustive)) val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|" (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const))); val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"} "define primitive corecursive functions" - ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) -- + ((Scan.optional (@{keyword "("} |-- + Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) -- (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd); val _ = Outer_Syntax.local_theory @{command_spec "primcorec"} "define primitive corecursive functions" - ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) -- + ((Scan.optional (@{keyword "("} |-- + Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) -- (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd); end; diff -r 19cd731eb745 -r c822230fd22b src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Mon Nov 25 18:18:58 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Mon Nov 25 20:25:22 2013 +0100 @@ -8,10 +8,13 @@ signature BNF_GFP_REC_SUGAR = sig - val add_primcorecursive_cmd: bool -> + datatype primcorec_option = + Option_Sequential | + Option_Exhaustive + val add_primcorecursive_cmd: primcorec_option list -> (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list -> Proof.context -> Proof.state - val add_primcorec_cmd: bool -> + val add_primcorec_cmd: primcorec_option list -> (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list -> local_theory -> local_theory end; @@ -43,6 +46,10 @@ fun primcorec_error_eqn str eqn = raise Primcorec_Error (str, [eqn]); fun primcorec_error_eqns str eqns = raise Primcorec_Error (str, eqns); +datatype primcorec_option = + Option_Sequential | + Option_Exhaustive + datatype corec_call = Dummy_No_Corec of int | No_Corec of int | @@ -824,7 +831,7 @@ |> K |> nth_map sel_no |> AList.map_entry (op =) ctr end; -fun add_primcorec_ursive maybe_tac seq fixes specs maybe_of_specs lthy = +fun add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy = let val thy = Proof_Context.theory_of lthy; @@ -835,6 +842,9 @@ [] => () | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort")); + val seq = member (op =) opts Option_Sequential; + val exhaustive = member (op =) opts Option_Exhaustive; + val fun_names = map Binding.name_of bs; val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts; val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); @@ -898,6 +908,8 @@ |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd)) |> split_list o map split_list; + val exhaustive_props = map (mk_disjs o map (mk_conjs o #prems)) disc_eqnss; + fun prove thmss' def_thms' lthy = let val def_thms = map (snd o snd) def_thms'; @@ -1002,77 +1014,82 @@ fun prove_code disc_eqns sel_eqns ctr_alist ctr_specs = let - val (fun_name, fun_T, fun_args, maybe_rhs) = + val fun_data = (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns, find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns) |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x)) ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE)) - |> the o merge_options; - - val bound_Ts = List.rev (map fastype_of fun_args); + |> merge_options; + in + (case fun_data of + NONE => [] + | SOME (fun_name, fun_T, fun_args, maybe_rhs) => + let + val bound_Ts = List.rev (map fastype_of fun_args); - val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); - val maybe_rhs_info = - (case maybe_rhs of - SOME rhs => - let - val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs; - val cond_ctrs = - fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs []; - val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs; - in SOME (rhs, raw_rhs, ctr_thms) end - | NONE => - let - fun prove_code_ctr {ctr, sels, ...} = - if not (exists (equal ctr o fst) ctr_alist) then NONE else - let - val prems = find_first (equal ctr o #ctr) disc_eqns - |> Option.map #prems |> the_default []; - val t = - filter (equal ctr o #ctr) sel_eqns - |> fst o finds ((op =) o apsnd #sel) sels - |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) - #-> abstract) - |> curry list_comb ctr; - in - SOME (prems, t) - end; - val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; - in - if exists is_none maybe_ctr_conds_argss then NONE else + val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); + val maybe_rhs_info = + (case maybe_rhs of + SOME rhs => + let + val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs; + val cond_ctrs = + fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs []; + val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs; + in SOME (rhs, raw_rhs, ctr_thms) end + | NONE => let - val rhs = fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t) - maybe_ctr_conds_argss - (Const (@{const_name Code.abort}, @{typ String.literal} --> - (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ - HOLogic.mk_literal fun_name $ - absdummy @{typ unit} (incr_boundvars 1 lhs)); - in SOME (rhs, rhs, map snd ctr_alist) end - end); - in - (case maybe_rhs_info of - NONE => [] - | SOME (rhs, raw_rhs, ctr_thms) => - let - val ms = map (Logic.count_prems o prop_of) ctr_thms; - val (raw_t, t) = (raw_rhs, rhs) - |> pairself - (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T), - map Bound (length fun_args - 1 downto 0))) - #> HOLogic.mk_Trueprop - #> curry Logic.list_all (map dest_Free fun_args)); - val (distincts, discIs, sel_splits, sel_split_asms) = - case_thms_of_term lthy bound_Ts raw_rhs; + fun prove_code_ctr {ctr, sels, ...} = + if not (exists (equal ctr o fst) ctr_alist) then NONE else + let + val prems = find_first (equal ctr o #ctr) disc_eqns + |> Option.map #prems |> the_default []; + val t = + filter (equal ctr o #ctr) sel_eqns + |> fst o finds ((op =) o apsnd #sel) sels + |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) + #-> abstract) + |> curry list_comb ctr; + in + SOME (prems, t) + end; + val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; + in + if exists is_none maybe_ctr_conds_argss then NONE else + let + val rhs = fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t) + maybe_ctr_conds_argss + (Const (@{const_name Code.abort}, @{typ String.literal} --> + (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ + HOLogic.mk_literal fun_name $ + absdummy @{typ unit} (incr_boundvars 1 lhs)); + in SOME (rhs, rhs, map snd ctr_alist) end + end); + in + (case maybe_rhs_info of + NONE => [] + | SOME (rhs, raw_rhs, ctr_thms) => + let + val ms = map (Logic.count_prems o prop_of) ctr_thms; + val (raw_t, t) = (raw_rhs, rhs) + |> pairself + (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T), + map Bound (length fun_args - 1 downto 0))) + #> HOLogic.mk_Trueprop + #> curry Logic.list_all (map dest_Free fun_args)); + val (distincts, discIs, sel_splits, sel_split_asms) = + case_thms_of_term lthy bound_Ts raw_rhs; - val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits - sel_split_asms ms ctr_thms - |> K |> Goal.prove lthy [] [] raw_t - |> Thm.close_derivation; - in - mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm - |> K |> Goal.prove lthy [] [] t - |> Thm.close_derivation - |> single + val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits + sel_split_asms ms ctr_thms + |> K |> Goal.prove lthy [] [] raw_t + |> Thm.close_derivation; + in + mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm + |> K |> Goal.prove lthy [] [] t + |> Thm.close_derivation + |> single + end) end) end; @@ -1120,13 +1137,13 @@ (goalss, after_qed, lthy') end; -fun add_primcorec_ursive_cmd maybe_tac seq (raw_fixes, raw_specs') lthy = +fun add_primcorec_ursive_cmd maybe_tac opts (raw_fixes, raw_specs') lthy = let val (raw_specs, maybe_of_specs) = split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy)); val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy; in - add_primcorec_ursive maybe_tac seq fixes specs maybe_of_specs lthy + add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy handle ERROR str => primcorec_error str end handle Primcorec_Error (str, eqns) =>