1.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Nov 25 18:18:58 2013 +0100
1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Nov 25 20:25:22 2013 +0100
1.3 @@ -2921,19 +2921,23 @@
1.4 Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
1.5 (parse_co_datatype_cmd Greatest_FP construct_gfp);
1.6
1.7 -val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true);
1.8 +val option_parser = Parse.group (fn () => "option")
1.9 + ((Parse.reserved "sequential" >> K Option_Sequential)
1.10 + || (Parse.reserved "exhaustive" >> K Option_Exhaustive))
1.11
1.12 val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
1.13 (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const)));
1.14
1.15 val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
1.16 "define primitive corecursive functions"
1.17 - ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
1.18 + ((Scan.optional (@{keyword "("} |--
1.19 + Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) --
1.20 (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd);
1.21
1.22 val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
1.23 "define primitive corecursive functions"
1.24 - ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
1.25 + ((Scan.optional (@{keyword "("} |--
1.26 + Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) --
1.27 (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd);
1.28
1.29 end;
2.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Mon Nov 25 18:18:58 2013 +0100
2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Mon Nov 25 20:25:22 2013 +0100
2.3 @@ -8,10 +8,13 @@
2.4
2.5 signature BNF_GFP_REC_SUGAR =
2.6 sig
2.7 - val add_primcorecursive_cmd: bool ->
2.8 + datatype primcorec_option =
2.9 + Option_Sequential |
2.10 + Option_Exhaustive
2.11 + val add_primcorecursive_cmd: primcorec_option list ->
2.12 (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
2.13 Proof.context -> Proof.state
2.14 - val add_primcorec_cmd: bool ->
2.15 + val add_primcorec_cmd: primcorec_option list ->
2.16 (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
2.17 local_theory -> local_theory
2.18 end;
2.19 @@ -43,6 +46,10 @@
2.20 fun primcorec_error_eqn str eqn = raise Primcorec_Error (str, [eqn]);
2.21 fun primcorec_error_eqns str eqns = raise Primcorec_Error (str, eqns);
2.22
2.23 +datatype primcorec_option =
2.24 + Option_Sequential |
2.25 + Option_Exhaustive
2.26 +
2.27 datatype corec_call =
2.28 Dummy_No_Corec of int |
2.29 No_Corec of int |
2.30 @@ -824,7 +831,7 @@
2.31 |> K |> nth_map sel_no |> AList.map_entry (op =) ctr
2.32 end;
2.33
2.34 -fun add_primcorec_ursive maybe_tac seq fixes specs maybe_of_specs lthy =
2.35 +fun add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy =
2.36 let
2.37 val thy = Proof_Context.theory_of lthy;
2.38
2.39 @@ -835,6 +842,9 @@
2.40 [] => ()
2.41 | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
2.42
2.43 + val seq = member (op =) opts Option_Sequential;
2.44 + val exhaustive = member (op =) opts Option_Exhaustive;
2.45 +
2.46 val fun_names = map Binding.name_of bs;
2.47 val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
2.48 val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
2.49 @@ -898,6 +908,8 @@
2.50 |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
2.51 |> split_list o map split_list;
2.52
2.53 + val exhaustive_props = map (mk_disjs o map (mk_conjs o #prems)) disc_eqnss;
2.54 +
2.55 fun prove thmss' def_thms' lthy =
2.56 let
2.57 val def_thms = map (snd o snd) def_thms';
2.58 @@ -1002,77 +1014,82 @@
2.59
2.60 fun prove_code disc_eqns sel_eqns ctr_alist ctr_specs =
2.61 let
2.62 - val (fun_name, fun_T, fun_args, maybe_rhs) =
2.63 + val fun_data =
2.64 (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
2.65 find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
2.66 |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x))
2.67 ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE))
2.68 - |> the o merge_options;
2.69 + |> merge_options;
2.70 + in
2.71 + (case fun_data of
2.72 + NONE => []
2.73 + | SOME (fun_name, fun_T, fun_args, maybe_rhs) =>
2.74 + let
2.75 + val bound_Ts = List.rev (map fastype_of fun_args);
2.76
2.77 - val bound_Ts = List.rev (map fastype_of fun_args);
2.78 + val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
2.79 + val maybe_rhs_info =
2.80 + (case maybe_rhs of
2.81 + SOME rhs =>
2.82 + let
2.83 + val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
2.84 + val cond_ctrs =
2.85 + fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
2.86 + val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
2.87 + in SOME (rhs, raw_rhs, ctr_thms) end
2.88 + | NONE =>
2.89 + let
2.90 + fun prove_code_ctr {ctr, sels, ...} =
2.91 + if not (exists (equal ctr o fst) ctr_alist) then NONE else
2.92 + let
2.93 + val prems = find_first (equal ctr o #ctr) disc_eqns
2.94 + |> Option.map #prems |> the_default [];
2.95 + val t =
2.96 + filter (equal ctr o #ctr) sel_eqns
2.97 + |> fst o finds ((op =) o apsnd #sel) sels
2.98 + |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x))
2.99 + #-> abstract)
2.100 + |> curry list_comb ctr;
2.101 + in
2.102 + SOME (prems, t)
2.103 + end;
2.104 + val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs;
2.105 + in
2.106 + if exists is_none maybe_ctr_conds_argss then NONE else
2.107 + let
2.108 + val rhs = fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t)
2.109 + maybe_ctr_conds_argss
2.110 + (Const (@{const_name Code.abort}, @{typ String.literal} -->
2.111 + (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
2.112 + HOLogic.mk_literal fun_name $
2.113 + absdummy @{typ unit} (incr_boundvars 1 lhs));
2.114 + in SOME (rhs, rhs, map snd ctr_alist) end
2.115 + end);
2.116 + in
2.117 + (case maybe_rhs_info of
2.118 + NONE => []
2.119 + | SOME (rhs, raw_rhs, ctr_thms) =>
2.120 + let
2.121 + val ms = map (Logic.count_prems o prop_of) ctr_thms;
2.122 + val (raw_t, t) = (raw_rhs, rhs)
2.123 + |> pairself
2.124 + (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
2.125 + map Bound (length fun_args - 1 downto 0)))
2.126 + #> HOLogic.mk_Trueprop
2.127 + #> curry Logic.list_all (map dest_Free fun_args));
2.128 + val (distincts, discIs, sel_splits, sel_split_asms) =
2.129 + case_thms_of_term lthy bound_Ts raw_rhs;
2.130
2.131 - val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
2.132 - val maybe_rhs_info =
2.133 - (case maybe_rhs of
2.134 - SOME rhs =>
2.135 - let
2.136 - val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
2.137 - val cond_ctrs =
2.138 - fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
2.139 - val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
2.140 - in SOME (rhs, raw_rhs, ctr_thms) end
2.141 - | NONE =>
2.142 - let
2.143 - fun prove_code_ctr {ctr, sels, ...} =
2.144 - if not (exists (equal ctr o fst) ctr_alist) then NONE else
2.145 - let
2.146 - val prems = find_first (equal ctr o #ctr) disc_eqns
2.147 - |> Option.map #prems |> the_default [];
2.148 - val t =
2.149 - filter (equal ctr o #ctr) sel_eqns
2.150 - |> fst o finds ((op =) o apsnd #sel) sels
2.151 - |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x))
2.152 - #-> abstract)
2.153 - |> curry list_comb ctr;
2.154 - in
2.155 - SOME (prems, t)
2.156 - end;
2.157 - val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs;
2.158 - in
2.159 - if exists is_none maybe_ctr_conds_argss then NONE else
2.160 - let
2.161 - val rhs = fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t)
2.162 - maybe_ctr_conds_argss
2.163 - (Const (@{const_name Code.abort}, @{typ String.literal} -->
2.164 - (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
2.165 - HOLogic.mk_literal fun_name $
2.166 - absdummy @{typ unit} (incr_boundvars 1 lhs));
2.167 - in SOME (rhs, rhs, map snd ctr_alist) end
2.168 - end);
2.169 - in
2.170 - (case maybe_rhs_info of
2.171 - NONE => []
2.172 - | SOME (rhs, raw_rhs, ctr_thms) =>
2.173 - let
2.174 - val ms = map (Logic.count_prems o prop_of) ctr_thms;
2.175 - val (raw_t, t) = (raw_rhs, rhs)
2.176 - |> pairself
2.177 - (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
2.178 - map Bound (length fun_args - 1 downto 0)))
2.179 - #> HOLogic.mk_Trueprop
2.180 - #> curry Logic.list_all (map dest_Free fun_args));
2.181 - val (distincts, discIs, sel_splits, sel_split_asms) =
2.182 - case_thms_of_term lthy bound_Ts raw_rhs;
2.183 -
2.184 - val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
2.185 - sel_split_asms ms ctr_thms
2.186 - |> K |> Goal.prove lthy [] [] raw_t
2.187 - |> Thm.close_derivation;
2.188 - in
2.189 - mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
2.190 - |> K |> Goal.prove lthy [] [] t
2.191 - |> Thm.close_derivation
2.192 - |> single
2.193 + val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
2.194 + sel_split_asms ms ctr_thms
2.195 + |> K |> Goal.prove lthy [] [] raw_t
2.196 + |> Thm.close_derivation;
2.197 + in
2.198 + mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
2.199 + |> K |> Goal.prove lthy [] [] t
2.200 + |> Thm.close_derivation
2.201 + |> single
2.202 + end)
2.203 end)
2.204 end;
2.205
2.206 @@ -1120,13 +1137,13 @@
2.207 (goalss, after_qed, lthy')
2.208 end;
2.209
2.210 -fun add_primcorec_ursive_cmd maybe_tac seq (raw_fixes, raw_specs') lthy =
2.211 +fun add_primcorec_ursive_cmd maybe_tac opts (raw_fixes, raw_specs') lthy =
2.212 let
2.213 val (raw_specs, maybe_of_specs) =
2.214 split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy));
2.215 val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy;
2.216 in
2.217 - add_primcorec_ursive maybe_tac seq fixes specs maybe_of_specs lthy
2.218 + add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy
2.219 handle ERROR str => primcorec_error str
2.220 end
2.221 handle Primcorec_Error (str, eqns) =>