1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Nov 11 17:34:44 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,986 +0,0 @@
1.4 -(* Title: HOL/BNF/Tools/bnf_fp_rec_sugar.ML
1.5 - Author: Lorenz Panny, TU Muenchen
1.6 - Copyright 2013
1.7 -
1.8 -Recursor and corecursor sugar.
1.9 -*)
1.10 -
1.11 -signature BNF_FP_REC_SUGAR =
1.12 -sig
1.13 - val add_primrec: (binding * typ option * mixfix) list ->
1.14 - (Attrib.binding * term) list -> local_theory -> (term list * thm list list) * local_theory
1.15 - val add_primrec_cmd: (binding * string option * mixfix) list ->
1.16 - (Attrib.binding * string) list -> local_theory -> (term list * thm list list) * local_theory
1.17 - val add_primrec_global: (binding * typ option * mixfix) list ->
1.18 - (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory
1.19 - val add_primrec_overloaded: (string * (string * typ) * bool) list ->
1.20 - (binding * typ option * mixfix) list ->
1.21 - (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory
1.22 - val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
1.23 - local_theory -> (string list * (term list * (int list list * thm list list))) * local_theory
1.24 - val add_primcorecursive_cmd: bool ->
1.25 - (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
1.26 - Proof.context -> Proof.state
1.27 - val add_primcorec_cmd: bool ->
1.28 - (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
1.29 - local_theory -> local_theory
1.30 -end;
1.31 -
1.32 -structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR =
1.33 -struct
1.34 -
1.35 -open BNF_Util
1.36 -open BNF_FP_Util
1.37 -open BNF_FP_Rec_Sugar_Util
1.38 -open BNF_FP_Rec_Sugar_Tactics
1.39 -
1.40 -val codeN = "code"
1.41 -val ctrN = "ctr"
1.42 -val discN = "disc"
1.43 -val selN = "sel"
1.44 -
1.45 -val nitpick_attrs = @{attributes [nitpick_simp]};
1.46 -val simp_attrs = @{attributes [simp]};
1.47 -val code_nitpick_attrs = Code.add_default_eqn_attrib :: nitpick_attrs;
1.48 -val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs;
1.49 -
1.50 -exception Primrec_Error of string * term list;
1.51 -
1.52 -fun primrec_error str = raise Primrec_Error (str, []);
1.53 -fun primrec_error_eqn str eqn = raise Primrec_Error (str, [eqn]);
1.54 -fun primrec_error_eqns str eqns = raise Primrec_Error (str, eqns);
1.55 -
1.56 -fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x);
1.57 -
1.58 -val free_name = try (fn Free (v, _) => v);
1.59 -val const_name = try (fn Const (v, _) => v);
1.60 -val undef_const = Const (@{const_name undefined}, dummyT);
1.61 -
1.62 -fun permute_args n t = list_comb (t, map Bound (0 :: (n downto 1)))
1.63 - |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n);
1.64 -val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
1.65 -fun drop_All t = subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
1.66 - strip_qnt_body @{const_name all} t)
1.67 -fun abstract vs =
1.68 - let fun a n (t $ u) = a n t $ a n u
1.69 - | a n (Abs (v, T, b)) = Abs (v, T, a (n + 1) b)
1.70 - | a n t = let val idx = find_index (equal t) vs in
1.71 - if idx < 0 then t else Bound (n + idx) end
1.72 - in a 0 end;
1.73 -fun mk_prod1 Ts (t, u) = HOLogic.pair_const (fastype_of1 (Ts, t)) (fastype_of1 (Ts, u)) $ t $ u;
1.74 -fun mk_tuple1 Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 Ts));
1.75 -
1.76 -fun get_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes
1.77 - |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
1.78 - |> map_filter I;
1.79 -
1.80 -
1.81 -(* Primrec *)
1.82 -
1.83 -type eqn_data = {
1.84 - fun_name: string,
1.85 - rec_type: typ,
1.86 - ctr: term,
1.87 - ctr_args: term list,
1.88 - left_args: term list,
1.89 - right_args: term list,
1.90 - res_type: typ,
1.91 - rhs_term: term,
1.92 - user_eqn: term
1.93 -};
1.94 -
1.95 -fun dissect_eqn lthy fun_names eqn' =
1.96 - let
1.97 - val eqn = drop_All eqn' |> HOLogic.dest_Trueprop
1.98 - handle TERM _ =>
1.99 - primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
1.100 - val (lhs, rhs) = HOLogic.dest_eq eqn
1.101 - handle TERM _ =>
1.102 - primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
1.103 - val (fun_name, args) = strip_comb lhs
1.104 - |>> (fn x => if is_Free x then fst (dest_Free x)
1.105 - else primrec_error_eqn "malformed function equation (does not start with free)" eqn);
1.106 - val (left_args, rest) = take_prefix is_Free args;
1.107 - val (nonfrees, right_args) = take_suffix is_Free rest;
1.108 - val num_nonfrees = length nonfrees;
1.109 - val _ = num_nonfrees = 1 orelse if num_nonfrees = 0 then
1.110 - primrec_error_eqn "constructor pattern missing in left-hand side" eqn else
1.111 - primrec_error_eqn "more than one non-variable argument in left-hand side" eqn;
1.112 - val _ = member (op =) fun_names fun_name orelse
1.113 - primrec_error_eqn "malformed function equation (does not start with function name)" eqn
1.114 -
1.115 - val (ctr, ctr_args) = strip_comb (the_single nonfrees);
1.116 - val _ = try (num_binder_types o fastype_of) ctr = SOME (length ctr_args) orelse
1.117 - primrec_error_eqn "partially applied constructor in pattern" eqn;
1.118 - val _ = let val d = duplicates (op =) (left_args @ ctr_args @ right_args) in null d orelse
1.119 - primrec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^
1.120 - "\" in left-hand side") eqn end;
1.121 - val _ = forall is_Free ctr_args orelse
1.122 - primrec_error_eqn "non-primitive pattern in left-hand side" eqn;
1.123 - val _ =
1.124 - let val b = fold_aterms (fn x as Free (v, _) =>
1.125 - if (not (member (op =) (left_args @ ctr_args @ right_args) x) andalso
1.126 - not (member (op =) fun_names v) andalso
1.127 - not (Variable.is_fixed lthy v)) then cons x else I | _ => I) rhs []
1.128 - in
1.129 - null b orelse
1.130 - primrec_error_eqn ("extra variable(s) in right-hand side: " ^
1.131 - commas (map (Syntax.string_of_term lthy) b)) eqn
1.132 - end;
1.133 - in
1.134 - {fun_name = fun_name,
1.135 - rec_type = body_type (type_of ctr),
1.136 - ctr = ctr,
1.137 - ctr_args = ctr_args,
1.138 - left_args = left_args,
1.139 - right_args = right_args,
1.140 - res_type = map fastype_of (left_args @ right_args) ---> fastype_of rhs,
1.141 - rhs_term = rhs,
1.142 - user_eqn = eqn'}
1.143 - end;
1.144 -
1.145 -fun rewrite_map_arg get_ctr_pos rec_type res_type =
1.146 - let
1.147 - val pT = HOLogic.mk_prodT (rec_type, res_type);
1.148 -
1.149 - val maybe_suc = Option.map (fn x => x + 1);
1.150 - fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const pT)
1.151 - | subst d (Abs (v, T, b)) = Abs (v, if d = SOME ~1 then pT else T, subst (maybe_suc d) b)
1.152 - | subst d t =
1.153 - let
1.154 - val (u, vs) = strip_comb t;
1.155 - val ctr_pos = try (get_ctr_pos o the) (free_name u) |> the_default ~1;
1.156 - in
1.157 - if ctr_pos >= 0 then
1.158 - if d = SOME ~1 andalso length vs = ctr_pos then
1.159 - list_comb (permute_args ctr_pos (snd_const pT), vs)
1.160 - else if length vs > ctr_pos andalso is_some d
1.161 - andalso d = try (fn Bound n => n) (nth vs ctr_pos) then
1.162 - list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs))
1.163 - else
1.164 - primrec_error_eqn ("recursive call not directly applied to constructor argument") t
1.165 - else if d = SOME ~1 andalso const_name u = SOME @{const_name comp} then
1.166 - list_comb (map_types (K dummyT) u, map2 subst [NONE, d] vs)
1.167 - else
1.168 - list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs)
1.169 - end
1.170 - in
1.171 - subst (SOME ~1)
1.172 - end;
1.173 -
1.174 -fun subst_rec_calls lthy get_ctr_pos has_call ctr_args direct_calls indirect_calls t =
1.175 - let
1.176 - fun subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
1.177 - | subst bound_Ts (t as g' $ y) =
1.178 - let
1.179 - val maybe_direct_y' = AList.lookup (op =) direct_calls y;
1.180 - val maybe_indirect_y' = AList.lookup (op =) indirect_calls y;
1.181 - val (g, g_args) = strip_comb g';
1.182 - val ctr_pos = try (get_ctr_pos o the) (free_name g) |> the_default ~1;
1.183 - val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse
1.184 - primrec_error_eqn "too few arguments in recursive call" t;
1.185 - in
1.186 - if not (member (op =) ctr_args y) then
1.187 - pairself (subst bound_Ts) (g', y) |> (op $)
1.188 - else if ctr_pos >= 0 then
1.189 - list_comb (the maybe_direct_y', g_args)
1.190 - else if is_some maybe_indirect_y' then
1.191 - (if has_call g' then t else y)
1.192 - |> massage_indirect_rec_call lthy has_call
1.193 - (rewrite_map_arg get_ctr_pos) bound_Ts y (the maybe_indirect_y')
1.194 - |> (if has_call g' then I else curry (op $) g')
1.195 - else
1.196 - t
1.197 - end
1.198 - | subst _ t = t
1.199 - in
1.200 - subst [] t
1.201 - |> tap (fn u => has_call u andalso (* FIXME detect this case earlier *)
1.202 - primrec_error_eqn "recursive call not directly applied to constructor argument" t)
1.203 - end;
1.204 -
1.205 -fun build_rec_arg lthy (funs_data : eqn_data list list) has_call (ctr_spec : rec_ctr_spec)
1.206 - (maybe_eqn_data : eqn_data option) =
1.207 - if is_none maybe_eqn_data then undef_const else
1.208 - let
1.209 - val eqn_data = the maybe_eqn_data;
1.210 - val t = #rhs_term eqn_data;
1.211 - val ctr_args = #ctr_args eqn_data;
1.212 -
1.213 - val calls = #calls ctr_spec;
1.214 - val n_args = fold (curry (op +) o (fn Direct_Rec _ => 2 | _ => 1)) calls 0;
1.215 -
1.216 - val no_calls' = tag_list 0 calls
1.217 - |> map_filter (try (apsnd (fn No_Rec n => n | Direct_Rec (n, _) => n)));
1.218 - val direct_calls' = tag_list 0 calls
1.219 - |> map_filter (try (apsnd (fn Direct_Rec (_, n) => n)));
1.220 - val indirect_calls' = tag_list 0 calls
1.221 - |> map_filter (try (apsnd (fn Indirect_Rec n => n)));
1.222 -
1.223 - fun make_direct_type _ = dummyT; (* FIXME? *)
1.224 -
1.225 - val rec_res_type_list = map (fn (x :: _) => (#rec_type x, #res_type x)) funs_data;
1.226 -
1.227 - fun make_indirect_type (Type (Tname, Ts)) = Type (Tname, Ts |> map (fn T =>
1.228 - let val maybe_res_type = AList.lookup (op =) rec_res_type_list T in
1.229 - if is_some maybe_res_type
1.230 - then HOLogic.mk_prodT (T, the maybe_res_type)
1.231 - else make_indirect_type T end))
1.232 - | make_indirect_type T = T;
1.233 -
1.234 - val args = replicate n_args ("", dummyT)
1.235 - |> Term.rename_wrt_term t
1.236 - |> map Free
1.237 - |> fold (fn (ctr_arg_idx, arg_idx) =>
1.238 - nth_map arg_idx (K (nth ctr_args ctr_arg_idx)))
1.239 - no_calls'
1.240 - |> fold (fn (ctr_arg_idx, arg_idx) =>
1.241 - nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_direct_type)))
1.242 - direct_calls'
1.243 - |> fold (fn (ctr_arg_idx, arg_idx) =>
1.244 - nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_indirect_type)))
1.245 - indirect_calls';
1.246 -
1.247 - val fun_name_ctr_pos_list =
1.248 - map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data;
1.249 - val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1;
1.250 - val direct_calls = map (apfst (nth ctr_args) o apsnd (nth args)) direct_calls';
1.251 - val indirect_calls = map (apfst (nth ctr_args) o apsnd (nth args)) indirect_calls';
1.252 -
1.253 - val abstractions = args @ #left_args eqn_data @ #right_args eqn_data;
1.254 - in
1.255 - t
1.256 - |> subst_rec_calls lthy get_ctr_pos has_call ctr_args direct_calls indirect_calls
1.257 - |> fold_rev lambda abstractions
1.258 - end;
1.259 -
1.260 -fun build_defs lthy bs mxs (funs_data : eqn_data list list) (rec_specs : rec_spec list) has_call =
1.261 - let
1.262 - val n_funs = length funs_data;
1.263 -
1.264 - val ctr_spec_eqn_data_list' =
1.265 - (take n_funs rec_specs |> map #ctr_specs) ~~ funs_data
1.266 - |> maps (uncurry (finds (fn (x, y) => #ctr x = #ctr y))
1.267 - ##> (fn x => null x orelse
1.268 - primrec_error_eqns "excess equations in definition" (map #rhs_term x)) #> fst);
1.269 - val _ = ctr_spec_eqn_data_list' |> map (fn (_, x) => length x <= 1 orelse
1.270 - primrec_error_eqns ("multiple equations for constructor") (map #user_eqn x));
1.271 -
1.272 - val ctr_spec_eqn_data_list =
1.273 - ctr_spec_eqn_data_list' @ (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair []));
1.274 -
1.275 - val recs = take n_funs rec_specs |> map #recx;
1.276 - val rec_args = ctr_spec_eqn_data_list
1.277 - |> sort ((op <) o pairself (#offset o fst) |> make_ord)
1.278 - |> map (uncurry (build_rec_arg lthy funs_data has_call) o apsnd (try the_single));
1.279 - val ctr_poss = map (fn x =>
1.280 - if length (distinct ((op =) o pairself (length o #left_args)) x) <> 1 then
1.281 - primrec_error ("inconstant constructor pattern position for function " ^
1.282 - quote (#fun_name (hd x)))
1.283 - else
1.284 - hd x |> #left_args |> length) funs_data;
1.285 - in
1.286 - (recs, ctr_poss)
1.287 - |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
1.288 - |> Syntax.check_terms lthy
1.289 - |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs
1.290 - end;
1.291 -
1.292 -fun find_rec_calls has_call (eqn_data : eqn_data) =
1.293 - let
1.294 - fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg
1.295 - | find (t as _ $ _) ctr_arg =
1.296 - let
1.297 - val (f', args') = strip_comb t;
1.298 - val n = find_index (equal ctr_arg) args';
1.299 - in
1.300 - if n < 0 then
1.301 - find f' ctr_arg @ maps (fn x => find x ctr_arg) args'
1.302 - else
1.303 - let val (f, args) = chop n args' |>> curry list_comb f' in
1.304 - if has_call f then
1.305 - f :: maps (fn x => find x ctr_arg) args
1.306 - else
1.307 - find f ctr_arg @ maps (fn x => find x ctr_arg) args
1.308 - end
1.309 - end
1.310 - | find _ _ = [];
1.311 - in
1.312 - map (find (#rhs_term eqn_data)) (#ctr_args eqn_data)
1.313 - |> (fn [] => NONE | callss => SOME (#ctr eqn_data, callss))
1.314 - end;
1.315 -
1.316 -fun prepare_primrec fixes specs lthy =
1.317 - let
1.318 - val (bs, mxs) = map_split (apfst fst) fixes;
1.319 - val fun_names = map Binding.name_of bs;
1.320 - val eqns_data = map (dissect_eqn lthy fun_names) specs;
1.321 - val funs_data = eqns_data
1.322 - |> partition_eq ((op =) o pairself #fun_name)
1.323 - |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst
1.324 - |> map (fn (x, y) => the_single y handle List.Empty =>
1.325 - primrec_error ("missing equations for function " ^ quote x));
1.326 -
1.327 - val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
1.328 - val arg_Ts = map (#rec_type o hd) funs_data;
1.329 - val res_Ts = map (#res_type o hd) funs_data;
1.330 - val callssss = funs_data
1.331 - |> map (partition_eq ((op =) o pairself #ctr))
1.332 - |> map (maps (map_filter (find_rec_calls has_call)));
1.333 -
1.334 - val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy') =
1.335 - rec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
1.336 -
1.337 - val actual_nn = length funs_data;
1.338 -
1.339 - val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in
1.340 - map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
1.341 - primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy' ctr) ^
1.342 - " is not a constructor in left-hand side") user_eqn) eqns_data end;
1.343 -
1.344 - val defs = build_defs lthy' bs mxs funs_data rec_specs has_call;
1.345 -
1.346 - fun prove lthy def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec)
1.347 - (fun_data : eqn_data list) =
1.348 - let
1.349 - val def_thms = map (snd o snd) def_thms';
1.350 - val simp_thmss = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
1.351 - |> fst
1.352 - |> map_filter (try (fn (x, [y]) =>
1.353 - (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
1.354 - |> map (fn (user_eqn, num_extra_args, rec_thm) =>
1.355 - mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
1.356 - |> K |> Goal.prove lthy [] [] user_eqn);
1.357 - val poss = find_indices (fn (x, y) => #ctr x = #ctr y) fun_data eqns_data;
1.358 - in
1.359 - (poss, simp_thmss)
1.360 - end;
1.361 -
1.362 - val notes =
1.363 - (if n2m then map2 (fn name => fn thm =>
1.364 - (name, inductN, [thm], [])) fun_names (take actual_nn induct_thms) else [])
1.365 - |> map (fn (prefix, thmN, thms, attrs) =>
1.366 - ((Binding.qualify true prefix (Binding.name thmN), attrs), [(thms, [])]));
1.367 -
1.368 - val common_name = mk_common_name fun_names;
1.369 -
1.370 - val common_notes =
1.371 - (if n2m then [(inductN, [induct_thm], [])] else [])
1.372 - |> map (fn (thmN, thms, attrs) =>
1.373 - ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
1.374 - in
1.375 - (((fun_names, defs),
1.376 - fn lthy => fn defs =>
1.377 - split_list (map2 (prove lthy defs) (take actual_nn rec_specs) funs_data)),
1.378 - lthy' |> Local_Theory.notes (notes @ common_notes) |> snd)
1.379 - end;
1.380 -
1.381 -(* primrec definition *)
1.382 -
1.383 -fun add_primrec_simple fixes ts lthy =
1.384 - let
1.385 - val (((names, defs), prove), lthy) = prepare_primrec fixes ts lthy
1.386 - handle ERROR str => primrec_error str;
1.387 - in
1.388 - lthy
1.389 - |> fold_map Local_Theory.define defs
1.390 - |-> (fn defs => `(fn lthy => (names, (map fst defs, prove lthy defs))))
1.391 - end
1.392 - handle Primrec_Error (str, eqns) =>
1.393 - if null eqns
1.394 - then error ("primrec_new error:\n " ^ str)
1.395 - else error ("primrec_new error:\n " ^ str ^ "\nin\n " ^
1.396 - space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns));
1.397 -
1.398 -local
1.399 -
1.400 -fun gen_primrec prep_spec (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy =
1.401 - let
1.402 - val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
1.403 - val _ = null d orelse primrec_error ("duplicate function name(s): " ^ commas d);
1.404 -
1.405 - val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy);
1.406 -
1.407 - val mk_notes =
1.408 - flat ooo map3 (fn poss => fn prefix => fn thms =>
1.409 - let
1.410 - val (bs, attrss) = map_split (fst o nth specs) poss;
1.411 - val notes =
1.412 - map3 (fn b => fn attrs => fn thm =>
1.413 - ((Binding.qualify false prefix b, code_nitpick_simp_attrs @ attrs), [([thm], [])]))
1.414 - bs attrss thms;
1.415 - in
1.416 - ((Binding.qualify true prefix (Binding.name simpsN), []), [(thms, [])]) :: notes
1.417 - end);
1.418 - in
1.419 - lthy
1.420 - |> add_primrec_simple fixes (map snd specs)
1.421 - |-> (fn (names, (ts, (posss, simpss))) =>
1.422 - Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
1.423 - #> Local_Theory.notes (mk_notes posss names simpss)
1.424 - #>> pair ts o map snd)
1.425 - end;
1.426 -
1.427 -in
1.428 -
1.429 -val add_primrec = gen_primrec Specification.check_spec;
1.430 -val add_primrec_cmd = gen_primrec Specification.read_spec;
1.431 -
1.432 -end;
1.433 -
1.434 -fun add_primrec_global fixes specs thy =
1.435 - let
1.436 - val lthy = Named_Target.theory_init thy;
1.437 - val ((ts, simps), lthy') = add_primrec fixes specs lthy;
1.438 - val simps' = burrow (Proof_Context.export lthy' lthy) simps;
1.439 - in ((ts, simps'), Local_Theory.exit_global lthy') end;
1.440 -
1.441 -fun add_primrec_overloaded ops fixes specs thy =
1.442 - let
1.443 - val lthy = Overloading.overloading ops thy;
1.444 - val ((ts, simps), lthy') = add_primrec fixes specs lthy;
1.445 - val simps' = burrow (Proof_Context.export lthy' lthy) simps;
1.446 - in ((ts, simps'), Local_Theory.exit_global lthy') end;
1.447 -
1.448 -
1.449 -
1.450 -(* Primcorec *)
1.451 -
1.452 -type co_eqn_data_disc = {
1.453 - fun_name: string,
1.454 - fun_T: typ,
1.455 - fun_args: term list,
1.456 - ctr: term,
1.457 - ctr_no: int, (*###*)
1.458 - disc: term,
1.459 - prems: term list,
1.460 - auto_gen: bool,
1.461 - user_eqn: term
1.462 -};
1.463 -
1.464 -type co_eqn_data_sel = {
1.465 - fun_name: string,
1.466 - fun_T: typ,
1.467 - fun_args: term list,
1.468 - ctr: term,
1.469 - sel: term,
1.470 - rhs_term: term,
1.471 - user_eqn: term
1.472 -};
1.473 -
1.474 -datatype co_eqn_data =
1.475 - Disc of co_eqn_data_disc |
1.476 - Sel of co_eqn_data_sel;
1.477 -
1.478 -fun co_dissect_eqn_disc sequential fun_names (corec_specs : corec_spec list) prems' concl
1.479 - matchedsss =
1.480 - let
1.481 - fun find_subterm p = let (* FIXME \<exists>? *)
1.482 - fun f (t as u $ v) = if p t then SOME t else merge_options (f u, f v)
1.483 - | f t = if p t then SOME t else NONE
1.484 - in f end;
1.485 -
1.486 - val applied_fun = concl
1.487 - |> find_subterm (member ((op =) o apsnd SOME) fun_names o try (fst o dest_Free o head_of))
1.488 - |> the
1.489 - handle Option.Option => primrec_error_eqn "malformed discriminator equation" concl;
1.490 - val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free;
1.491 - val {ctr_specs, ...} = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name);
1.492 -
1.493 - val discs = map #disc ctr_specs;
1.494 - val ctrs = map #ctr ctr_specs;
1.495 - val not_disc = head_of concl = @{term Not};
1.496 - val _ = not_disc andalso length ctrs <> 2 andalso
1.497 - primrec_error_eqn "\<not>ed discriminator for a type with \<noteq> 2 constructors" concl;
1.498 - val disc = find_subterm (member (op =) discs o head_of) concl;
1.499 - val eq_ctr0 = concl |> perhaps (try (HOLogic.dest_not)) |> try (HOLogic.dest_eq #> snd)
1.500 - |> (fn SOME t => let val n = find_index (equal t) ctrs in
1.501 - if n >= 0 then SOME n else NONE end | _ => NONE);
1.502 - val _ = is_some disc orelse is_some eq_ctr0 orelse
1.503 - primrec_error_eqn "no discriminator in equation" concl;
1.504 - val ctr_no' =
1.505 - if is_none disc then the eq_ctr0 else find_index (equal (head_of (the disc))) discs;
1.506 - val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
1.507 - val ctr = #ctr (nth ctr_specs ctr_no);
1.508 -
1.509 - val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_;
1.510 - val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default [];
1.511 - val prems = map (abstract (List.rev fun_args)) prems';
1.512 - val real_prems =
1.513 - (if catch_all orelse sequential then maps negate_disj matchedss else []) @
1.514 - (if catch_all then [] else prems);
1.515 -
1.516 - val matchedsss' = AList.delete (op =) fun_name matchedsss
1.517 - |> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [real_prems]);
1.518 -
1.519 - val user_eqn =
1.520 - (real_prems, betapply (#disc (nth ctr_specs ctr_no), applied_fun))
1.521 - |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop
1.522 - |> Logic.list_implies;
1.523 - in
1.524 - (Disc {
1.525 - fun_name = fun_name,
1.526 - fun_T = fun_T,
1.527 - fun_args = fun_args,
1.528 - ctr = ctr,
1.529 - ctr_no = ctr_no,
1.530 - disc = #disc (nth ctr_specs ctr_no),
1.531 - prems = real_prems,
1.532 - auto_gen = catch_all,
1.533 - user_eqn = user_eqn
1.534 - }, matchedsss')
1.535 - end;
1.536 -
1.537 -fun co_dissect_eqn_sel fun_names (corec_specs : corec_spec list) eqn' of_spec eqn =
1.538 - let
1.539 - val (lhs, rhs) = HOLogic.dest_eq eqn
1.540 - handle TERM _ =>
1.541 - primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn;
1.542 - val sel = head_of lhs;
1.543 - val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free
1.544 - handle TERM _ =>
1.545 - primrec_error_eqn "malformed selector argument in left-hand side" eqn;
1.546 - val corec_spec = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name)
1.547 - handle Option.Option => primrec_error_eqn "malformed selector argument in left-hand side" eqn;
1.548 - val ctr_spec =
1.549 - if is_some of_spec
1.550 - then the (find_first (equal (the of_spec) o #ctr) (#ctr_specs corec_spec))
1.551 - else #ctr_specs corec_spec |> filter (exists (equal sel) o #sels) |> the_single
1.552 - handle List.Empty => primrec_error_eqn "ambiguous selector - use \"of\"" eqn;
1.553 - val user_eqn = drop_All eqn';
1.554 - in
1.555 - Sel {
1.556 - fun_name = fun_name,
1.557 - fun_T = fun_T,
1.558 - fun_args = fun_args,
1.559 - ctr = #ctr ctr_spec,
1.560 - sel = sel,
1.561 - rhs_term = rhs,
1.562 - user_eqn = user_eqn
1.563 - }
1.564 - end;
1.565 -
1.566 -fun co_dissect_eqn_ctr sequential fun_names (corec_specs : corec_spec list) eqn' imp_prems imp_rhs
1.567 - matchedsss =
1.568 - let
1.569 - val (lhs, rhs) = HOLogic.dest_eq imp_rhs;
1.570 - val fun_name = head_of lhs |> fst o dest_Free;
1.571 - val {ctr_specs, ...} = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name);
1.572 - val (ctr, ctr_args) = strip_comb rhs;
1.573 - val {disc, sels, ...} = the (find_first (equal ctr o #ctr) ctr_specs)
1.574 - handle Option.Option => primrec_error_eqn "not a constructor" ctr;
1.575 -
1.576 - val disc_imp_rhs = betapply (disc, lhs);
1.577 - val (maybe_eqn_data_disc, matchedsss') = if length ctr_specs = 1
1.578 - then (NONE, matchedsss)
1.579 - else apfst SOME (co_dissect_eqn_disc
1.580 - sequential fun_names corec_specs imp_prems disc_imp_rhs matchedsss);
1.581 -
1.582 - val sel_imp_rhss = (sels ~~ ctr_args)
1.583 - |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg));
1.584 -
1.585 -(*
1.586 -val _ = tracing ("reduced\n " ^ Syntax.string_of_term @{context} imp_rhs ^ "\nto\n \<cdot> " ^
1.587 - (is_some maybe_eqn_data_disc ? K (Syntax.string_of_term @{context} disc_imp_rhs ^ "\n \<cdot> ")) "" ^
1.588 - space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) sel_imp_rhss));
1.589 -*)
1.590 -
1.591 - val eqns_data_sel =
1.592 - map (co_dissect_eqn_sel fun_names corec_specs eqn' (SOME ctr)) sel_imp_rhss;
1.593 - in
1.594 - (the_list maybe_eqn_data_disc @ eqns_data_sel, matchedsss')
1.595 - end;
1.596 -
1.597 -fun co_dissect_eqn sequential fun_names (corec_specs : corec_spec list) eqn' of_spec matchedsss =
1.598 - let
1.599 - val eqn = drop_All eqn'
1.600 - handle TERM _ => primrec_error_eqn "malformed function equation" eqn';
1.601 - val (imp_prems, imp_rhs) = Logic.strip_horn eqn
1.602 - |> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop;
1.603 -
1.604 - val head = imp_rhs
1.605 - |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq))
1.606 - |> head_of;
1.607 -
1.608 - val maybe_rhs = imp_rhs |> perhaps (try (HOLogic.dest_not)) |> try (snd o HOLogic.dest_eq);
1.609 -
1.610 - val discs = maps #ctr_specs corec_specs |> map #disc;
1.611 - val sels = maps #ctr_specs corec_specs |> maps #sels;
1.612 - val ctrs = maps #ctr_specs corec_specs |> map #ctr;
1.613 - in
1.614 - if member (op =) discs head orelse
1.615 - is_some maybe_rhs andalso
1.616 - member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then
1.617 - co_dissect_eqn_disc sequential fun_names corec_specs imp_prems imp_rhs matchedsss
1.618 - |>> single
1.619 - else if member (op =) sels head then
1.620 - ([co_dissect_eqn_sel fun_names corec_specs eqn' of_spec imp_rhs], matchedsss)
1.621 - else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
1.622 - co_dissect_eqn_ctr sequential fun_names corec_specs eqn' imp_prems imp_rhs matchedsss
1.623 - else
1.624 - primrec_error_eqn "malformed function equation" eqn
1.625 - end;
1.626 -
1.627 -fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)
1.628 - ({fun_args, ctr_no, prems, ...} : co_eqn_data_disc) =
1.629 - if is_none (#pred (nth ctr_specs ctr_no)) then I else
1.630 - mk_conjs prems
1.631 - |> curry subst_bounds (List.rev fun_args)
1.632 - |> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args)
1.633 - |> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
1.634 -
1.635 -fun build_corec_arg_no_call (sel_eqns : co_eqn_data_sel list) sel =
1.636 - find_first (equal sel o #sel) sel_eqns
1.637 - |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple fun_args rhs_term)
1.638 - |> the_default undef_const
1.639 - |> K;
1.640 -
1.641 -fun build_corec_args_direct_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
1.642 - let
1.643 - val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
1.644 - in
1.645 - if is_none maybe_sel_eqn then (I, I, I) else
1.646 - let
1.647 - val {fun_args, rhs_term, ... } = the maybe_sel_eqn;
1.648 - fun rewrite_q _ t = if has_call t then @{term False} else @{term True};
1.649 - fun rewrite_g _ t = if has_call t then undef_const else t;
1.650 - fun rewrite_h bound_Ts t =
1.651 - if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const;
1.652 - fun massage f t = massage_direct_corec_call lthy has_call f [] rhs_term |> abs_tuple fun_args;
1.653 - in
1.654 - (massage rewrite_q,
1.655 - massage rewrite_g,
1.656 - massage rewrite_h)
1.657 - end
1.658 - end;
1.659 -
1.660 -fun build_corec_arg_indirect_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
1.661 - let
1.662 - val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
1.663 - in
1.664 - if is_none maybe_sel_eqn then I else
1.665 - let
1.666 - val {fun_args, rhs_term, ...} = the maybe_sel_eqn;
1.667 - fun rewrite bound_Ts U T (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) U T b)
1.668 - | rewrite bound_Ts U T (t as _ $ _) =
1.669 - let val (u, vs) = strip_comb t in
1.670 - if is_Free u andalso has_call u then
1.671 - Inr_const U T $ mk_tuple1 bound_Ts vs
1.672 - else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
1.673 - map (rewrite bound_Ts U T) vs |> chop 1 |>> HOLogic.mk_split o the_single |> list_comb
1.674 - else
1.675 - list_comb (rewrite bound_Ts U T u, map (rewrite bound_Ts U T) vs)
1.676 - end
1.677 - | rewrite _ U T t =
1.678 - if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
1.679 - fun massage t =
1.680 - massage_indirect_corec_call lthy has_call rewrite [] (range_type (fastype_of t)) rhs_term
1.681 - |> abs_tuple fun_args;
1.682 - in
1.683 - massage
1.684 - end
1.685 - end;
1.686 -
1.687 -fun build_corec_args_sel lthy has_call (all_sel_eqns : co_eqn_data_sel list)
1.688 - (ctr_spec : corec_ctr_spec) =
1.689 - let val sel_eqns = filter (equal (#ctr ctr_spec) o #ctr) all_sel_eqns in
1.690 - if null sel_eqns then I else
1.691 - let
1.692 - val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
1.693 -
1.694 - val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
1.695 - val direct_calls' = map_filter (try (apsnd (fn Direct_Corec n => n))) sel_call_list;
1.696 - val indirect_calls' = map_filter (try (apsnd (fn Indirect_Corec n => n))) sel_call_list;
1.697 - in
1.698 - I
1.699 - #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls'
1.700 - #> fold (fn (sel, (q, g, h)) =>
1.701 - let val (fq, fg, fh) = build_corec_args_direct_call lthy has_call sel_eqns sel in
1.702 - nth_map q fq o nth_map g fg o nth_map h fh end) direct_calls'
1.703 - #> fold (fn (sel, n) => nth_map n
1.704 - (build_corec_arg_indirect_call lthy has_call sel_eqns sel)) indirect_calls'
1.705 - end
1.706 - end;
1.707 -
1.708 -fun co_build_defs lthy bs mxs has_call arg_Tss (corec_specs : corec_spec list)
1.709 - (disc_eqnss : co_eqn_data_disc list list) (sel_eqnss : co_eqn_data_sel list list) =
1.710 - let
1.711 - val corec_specs' = take (length bs) corec_specs;
1.712 - val corecs = map #corec corec_specs';
1.713 - val ctr_specss = map #ctr_specs corec_specs';
1.714 - val corec_args = hd corecs
1.715 - |> fst o split_last o binder_types o fastype_of
1.716 - |> map (Const o pair @{const_name undefined})
1.717 - |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
1.718 - |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;
1.719 - fun currys [] t = t
1.720 - | currys Ts t = t $ mk_tuple1 (List.rev Ts) (map Bound (length Ts - 1 downto 0))
1.721 - |> fold_rev (Term.abs o pair Name.uu) Ts;
1.722 -
1.723 -(*
1.724 -val _ = tracing ("corecursor arguments:\n \<cdot> " ^
1.725 - space_implode "\n \<cdot> " (map (Syntax.string_of_term lthy) corec_args));
1.726 -*)
1.727 -
1.728 - val exclss' =
1.729 - disc_eqnss
1.730 - |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x))
1.731 - #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs [])
1.732 - #> maps (uncurry (map o pair)
1.733 - #> map (fn ((fun_args, c, x, a), (_, c', y, a')) =>
1.734 - ((c, c', a orelse a'), (x, s_not (mk_conjs y)))
1.735 - ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop
1.736 - ||> Logic.list_implies
1.737 - ||> curry Logic.list_all (map dest_Free fun_args))))
1.738 - in
1.739 - map (list_comb o rpair corec_args) corecs
1.740 - |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
1.741 - |> map2 currys arg_Tss
1.742 - |> Syntax.check_terms lthy
1.743 - |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs
1.744 - |> rpair exclss'
1.745 - end;
1.746 -
1.747 -fun mk_real_disc_eqns fun_binding arg_Ts ({ctr_specs, ...} : corec_spec)
1.748 - (sel_eqns : co_eqn_data_sel list) (disc_eqns : co_eqn_data_disc list) =
1.749 - if length disc_eqns <> length ctr_specs - 1 then disc_eqns else
1.750 - let
1.751 - val n = 0 upto length ctr_specs
1.752 - |> the o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns));
1.753 - val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns)
1.754 - |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options;
1.755 - val extra_disc_eqn = {
1.756 - fun_name = Binding.name_of fun_binding,
1.757 - fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))),
1.758 - fun_args = fun_args,
1.759 - ctr = #ctr (nth ctr_specs n),
1.760 - ctr_no = n,
1.761 - disc = #disc (nth ctr_specs n),
1.762 - prems = maps (negate_conj o #prems) disc_eqns,
1.763 - auto_gen = true,
1.764 - user_eqn = undef_const};
1.765 - in
1.766 - chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
1.767 - end;
1.768 -
1.769 -fun add_primcorec simple sequential fixes specs of_specs lthy =
1.770 - let
1.771 - val (bs, mxs) = map_split (apfst fst) fixes;
1.772 - val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
1.773 -
1.774 - val callssss = []; (* FIXME *)
1.775 -
1.776 - val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
1.777 - strong_coinduct_thms), lthy') =
1.778 - corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
1.779 -
1.780 - val actual_nn = length bs;
1.781 - val fun_names = map Binding.name_of bs;
1.782 - val corec_specs = take actual_nn corec_specs'; (*###*)
1.783 -
1.784 - val eqns_data =
1.785 - fold_map2 (co_dissect_eqn sequential fun_names corec_specs) (map snd specs) of_specs []
1.786 - |> flat o fst;
1.787 -
1.788 - val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
1.789 - |> partition_eq ((op =) o pairself #fun_name)
1.790 - |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
1.791 - |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);
1.792 - val _ = disc_eqnss' |> map (fn x =>
1.793 - let val d = duplicates ((op =) o pairself #ctr_no) x in null d orelse
1.794 - primrec_error_eqns "excess discriminator equations in definition"
1.795 - (maps (fn t => filter (equal (#ctr_no t) o #ctr_no) x) d |> map #user_eqn) end);
1.796 -
1.797 - val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
1.798 - |> partition_eq ((op =) o pairself #fun_name)
1.799 - |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
1.800 - |> map (flat o snd);
1.801 -
1.802 - val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
1.803 - val arg_Tss = map (binder_types o snd o fst) fixes;
1.804 - val disc_eqnss = map5 mk_real_disc_eqns bs arg_Tss corec_specs sel_eqnss disc_eqnss';
1.805 - val (defs, exclss') =
1.806 - co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
1.807 -
1.808 - fun excl_tac (c, c', a) =
1.809 - if a orelse c = c' orelse sequential then
1.810 - SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy [])))
1.811 - else if simple then
1.812 - SOME (K (auto_tac lthy))
1.813 - else
1.814 - NONE;
1.815 -
1.816 -(*
1.817 -val _ = tracing ("exclusiveness properties:\n \<cdot> " ^
1.818 - space_implode "\n \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) exclss'));
1.819 -*)
1.820 -
1.821 - val exclss'' = exclss' |> map (map (fn (idx, t) =>
1.822 - (idx, (Option.map (Goal.prove lthy [] [] t) (excl_tac idx), t))));
1.823 - val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
1.824 - val (obligation_idxss, obligationss) = exclss''
1.825 - |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
1.826 - |> split_list o map split_list;
1.827 -
1.828 - fun prove thmss' def_thms' lthy =
1.829 - let
1.830 - val def_thms = map (snd o snd) def_thms';
1.831 -
1.832 - val exclss' = map (op ~~) (obligation_idxss ~~ thmss');
1.833 - fun mk_exclsss excls n =
1.834 - (excls, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1))
1.835 - |-> fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])));
1.836 - val exclssss = (exclss' ~~ taut_thmss |> map (op @), fun_names ~~ corec_specs)
1.837 - |-> map2 (fn excls => fn (_, {ctr_specs, ...}) => mk_exclsss excls (length ctr_specs));
1.838 -
1.839 - fun prove_disc ({ctr_specs, ...} : corec_spec) exclsss
1.840 - ({fun_name, fun_T, fun_args, ctr_no, prems, ...} : co_eqn_data_disc) =
1.841 - if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then [] else
1.842 - let
1.843 - val {disc_corec, ...} = nth ctr_specs ctr_no;
1.844 - val k = 1 + ctr_no;
1.845 - val m = length prems;
1.846 - val t =
1.847 - list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0))
1.848 - |> curry betapply (#disc (nth ctr_specs ctr_no)) (*###*)
1.849 - |> HOLogic.mk_Trueprop
1.850 - |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
1.851 - |> curry Logic.list_all (map dest_Free fun_args);
1.852 - in
1.853 - mk_primcorec_disc_tac lthy def_thms disc_corec k m exclsss
1.854 - |> K |> Goal.prove lthy [] [] t
1.855 - |> pair (#disc (nth ctr_specs ctr_no))
1.856 - |> single
1.857 - end;
1.858 -
1.859 - fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
1.860 - : corec_spec) (disc_eqns : co_eqn_data_disc list) exclsss
1.861 - ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, ...} : co_eqn_data_sel) =
1.862 - let
1.863 - val SOME ctr_spec = find_first (equal ctr o #ctr) ctr_specs;
1.864 - val ctr_no = find_index (equal ctr o #ctr) ctr_specs;
1.865 - val prems = the_default (maps (negate_conj o #prems) disc_eqns)
1.866 - (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
1.867 - val sel_corec = find_index (equal sel) (#sels ctr_spec)
1.868 - |> nth (#sel_corecs ctr_spec);
1.869 - val k = 1 + ctr_no;
1.870 - val m = length prems;
1.871 - val t =
1.872 - list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0))
1.873 - |> curry betapply sel
1.874 - |> rpair (abstract (List.rev fun_args) rhs_term)
1.875 - |> HOLogic.mk_Trueprop o HOLogic.mk_eq
1.876 - |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
1.877 - |> curry Logic.list_all (map dest_Free fun_args);
1.878 - val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
1.879 - in
1.880 - mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
1.881 - nested_map_idents nested_map_comps sel_corec k m exclsss
1.882 - |> K |> Goal.prove lthy [] [] t
1.883 - |> pair sel
1.884 - end;
1.885 -
1.886 - fun prove_ctr disc_alist sel_alist (disc_eqns : co_eqn_data_disc list)
1.887 - (sel_eqns : co_eqn_data_sel list) ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) =
1.888 - if not (exists (equal ctr o #ctr) disc_eqns)
1.889 - andalso not (exists (equal ctr o #ctr) sel_eqns)
1.890 - orelse (* don't try to prove theorems when some sel_eqns are missing *)
1.891 - filter (equal ctr o #ctr) sel_eqns
1.892 - |> fst o finds ((op =) o apsnd #sel) sels
1.893 - |> exists (null o snd)
1.894 - then [] else
1.895 - let
1.896 - val (fun_name, fun_T, fun_args, prems) =
1.897 - (find_first (equal ctr o #ctr) disc_eqns, find_first (equal ctr o #ctr) sel_eqns)
1.898 - |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x))
1.899 - ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, []))
1.900 - |> the o merge_options;
1.901 - val m = length prems;
1.902 - val t = filter (equal ctr o #ctr) sel_eqns
1.903 - |> fst o finds ((op =) o apsnd #sel) sels
1.904 - |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
1.905 - |> curry list_comb ctr
1.906 - |> curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
1.907 - map Bound (length fun_args - 1 downto 0)))
1.908 - |> HOLogic.mk_Trueprop
1.909 - |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
1.910 - |> curry Logic.list_all (map dest_Free fun_args);
1.911 - val maybe_disc_thm = AList.lookup (op =) disc_alist disc;
1.912 - val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist);
1.913 - in
1.914 - mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms
1.915 - |> K |> Goal.prove lthy [] [] t
1.916 - |> single
1.917 - end;
1.918 -
1.919 - val disc_alists = map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss;
1.920 - val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss;
1.921 -
1.922 - val disc_thmss = map (map snd) disc_alists;
1.923 - val sel_thmss = map (map snd) sel_alists;
1.924 - val ctr_thmss = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss
1.925 - (map #ctr_specs corec_specs);
1.926 -
1.927 - val simp_thmss = map2 append disc_thmss sel_thmss
1.928 -
1.929 - val common_name = mk_common_name fun_names;
1.930 -
1.931 - val notes =
1.932 - [(coinductN, map (if n2m then single else K []) coinduct_thms, []),
1.933 - (codeN, ctr_thmss(*FIXME*), code_nitpick_attrs),
1.934 - (ctrN, ctr_thmss, []),
1.935 - (discN, disc_thmss, simp_attrs),
1.936 - (selN, sel_thmss, simp_attrs),
1.937 - (simpsN, simp_thmss, []),
1.938 - (strong_coinductN, map (if n2m then single else K []) strong_coinduct_thms, [])]
1.939 - |> maps (fn (thmN, thmss, attrs) =>
1.940 - map2 (fn fun_name => fn thms =>
1.941 - ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]))
1.942 - fun_names (take actual_nn thmss))
1.943 - |> filter_out (null o fst o hd o snd);
1.944 -
1.945 - val common_notes =
1.946 - [(coinductN, if n2m then [coinduct_thm] else [], []),
1.947 - (strong_coinductN, if n2m then [strong_coinduct_thm] else [], [])]
1.948 - |> filter_out (null o #2)
1.949 - |> map (fn (thmN, thms, attrs) =>
1.950 - ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
1.951 - in
1.952 - lthy |> Local_Theory.notes (notes @ common_notes) |> snd
1.953 - end;
1.954 -
1.955 - fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
1.956 -
1.957 - val _ = if not simple orelse forall null obligationss then () else
1.958 - primrec_error "need exclusiveness proofs - use primcorecursive instead of primcorec";
1.959 - in
1.960 - if simple then
1.961 - lthy'
1.962 - |> after_qed (map (fn [] => []) obligationss)
1.963 - |> pair NONE o SOME
1.964 - else
1.965 - lthy'
1.966 - |> Proof.theorem NONE after_qed obligationss
1.967 - |> Proof.refine (Method.primitive_text I)
1.968 - |> Seq.hd
1.969 - |> rpair NONE o SOME
1.970 - end;
1.971 -
1.972 -fun add_primcorec_ursive_cmd simple seq (raw_fixes, raw_specs') lthy =
1.973 - let
1.974 - val (raw_specs, of_specs) = split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy));
1.975 - val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy;
1.976 - in
1.977 - add_primcorec simple seq fixes specs of_specs lthy
1.978 - handle ERROR str => primrec_error str
1.979 - end
1.980 - handle Primrec_Error (str, eqns) =>
1.981 - if null eqns
1.982 - then error ("primcorec error:\n " ^ str)
1.983 - else error ("primcorec error:\n " ^ str ^ "\nin\n " ^
1.984 - space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns));
1.985 -
1.986 -val add_primcorecursive_cmd = (the o fst) ooo add_primcorec_ursive_cmd false;
1.987 -val add_primcorec_cmd = (the o snd) ooo add_primcorec_ursive_cmd true;
1.988 -
1.989 -end;