1(* Title: HOL/Tools/BNF/bnf_gfp_rec_sugar.ML 2 Author: Lorenz Panny, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 Copyright 2013 5 6Corecursor sugar ("primcorec" and "primcorecursive"). 7*) 8 9signature BNF_GFP_REC_SUGAR = 10sig 11 datatype corec_option = 12 Plugins_Option of Proof.context -> Plugin_Name.filter | 13 Sequential_Option | 14 Exhaustive_Option | 15 Transfer_Option 16 17 datatype corec_call = 18 Dummy_No_Corec of int | 19 No_Corec of int | 20 Mutual_Corec of int * int * int | 21 Nested_Corec of int 22 23 type corec_ctr_spec = 24 {ctr: term, 25 disc: term, 26 sels: term list, 27 pred: int option, 28 calls: corec_call list, 29 discI: thm, 30 sel_thms: thm list, 31 distinct_discss: thm list list, 32 collapse: thm, 33 corec_thm: thm, 34 corec_disc: thm, 35 corec_sels: thm list} 36 37 type corec_spec = 38 {T: typ, 39 corec: term, 40 exhaust_discs: thm list, 41 sel_defs: thm list, 42 fp_nesting_maps: thm list, 43 fp_nesting_map_ident0s: thm list, 44 fp_nesting_map_comps: thm list, 45 ctr_specs: corec_ctr_spec list} 46 47 val abstract_over_list: term list -> term -> term 48 val abs_tuple_balanced: term list -> term -> term 49 50 val mk_conjs: term list -> term 51 val mk_disjs: term list -> term 52 val mk_dnf: term list list -> term 53 val conjuncts_s: term -> term list 54 val s_not: term -> term 55 val s_not_conj: term list -> term list 56 val s_conjs: term list -> term 57 val s_disjs: term list -> term 58 val s_dnf: term list list -> term list 59 60 val case_of: Proof.context -> string -> (string * bool) option 61 val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list -> 62 term -> 'a -> 'a 63 val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) -> 64 (typ list -> term -> unit) -> (typ list -> term -> term) -> typ list -> term -> term 65 val massage_nested_corec_call: Proof.context -> (term -> bool) -> 66 (typ list -> typ -> typ -> term -> term) -> (typ list -> typ -> typ -> term -> term) -> 67 typ list -> typ -> typ -> term -> term 68 val expand_to_ctr_term: Proof.context -> typ -> term -> term 69 val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) -> 70 typ list -> term -> term 71 val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) -> 72 typ list -> term -> 'a -> 'a 73 val case_thms_of_term: Proof.context -> term -> 74 thm list * thm list * thm list * thm list * thm list 75 val map_thms_of_type: Proof.context -> typ -> thm list 76 77 val corec_specs_of: binding list -> typ list -> typ list -> term list -> 78 (term * term list list) list list -> local_theory -> 79 corec_spec list * typ list * thm * thm * thm list * thm list * (Token.src list * Token.src list) 80 * bool * local_theory 81 82 val gfp_rec_sugar_interpretation: string -> 83 (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory 84 85 val primcorec_ursive: bool -> bool -> corec_option list -> ((binding * typ) * mixfix) list -> 86 ((binding * Token.T list list) * term) list -> term option list -> Proof.context -> 87 (term * 'a list) list list * (thm list list -> local_theory -> local_theory) * local_theory 88 val primcorec_ursive_cmd: bool -> bool -> corec_option list -> 89 (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list -> 90 Proof.context -> 91 (term * 'a list) list list * (thm list list -> local_theory -> local_theory) * local_theory 92 val primcorecursive_cmd: bool -> corec_option list -> 93 (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list -> 94 Proof.context -> Proof.state 95 val primcorec_cmd: bool -> corec_option list -> 96 (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list -> 97 local_theory -> local_theory 98end; 99 100structure BNF_GFP_Rec_Sugar : BNF_GFP_REC_SUGAR = 101struct 102 103open Ctr_Sugar_General_Tactics 104open Ctr_Sugar 105open BNF_Util 106open BNF_Def 107open BNF_FP_Util 108open BNF_FP_Def_Sugar 109open BNF_FP_N2M_Sugar 110open BNF_FP_Rec_Sugar_Util 111open BNF_FP_Rec_Sugar_Transfer 112open BNF_GFP_Rec_Sugar_Tactics 113 114val codeN = "code"; 115val ctrN = "ctr"; 116val discN = "disc"; 117val disc_iffN = "disc_iff"; 118val excludeN = "exclude"; 119val selN = "sel"; 120 121val nitpicksimp_attrs = @{attributes [nitpick_simp]}; 122val simp_attrs = @{attributes [simp]}; 123 124fun use_primcorecursive () = 125 error ("\"auto\" failed (try " ^ quote (#1 \<^command_keyword>\<open>primcorecursive\<close>) ^ " instead of " ^ 126 quote (#1 \<^command_keyword>\<open>primcorec\<close>) ^ ")"); 127 128datatype corec_option = 129 Plugins_Option of Proof.context -> Plugin_Name.filter | 130 Sequential_Option | 131 Exhaustive_Option | 132 Transfer_Option; 133 134datatype corec_call = 135 Dummy_No_Corec of int | 136 No_Corec of int | 137 Mutual_Corec of int * int * int | 138 Nested_Corec of int; 139 140type basic_corec_ctr_spec = 141 {ctr: term, 142 disc: term, 143 sels: term list}; 144 145type corec_ctr_spec = 146 {ctr: term, 147 disc: term, 148 sels: term list, 149 pred: int option, 150 calls: corec_call list, 151 discI: thm, 152 sel_thms: thm list, 153 distinct_discss: thm list list, 154 collapse: thm, 155 corec_thm: thm, 156 corec_disc: thm, 157 corec_sels: thm list}; 158 159type corec_spec = 160 {T: typ, 161 corec: term, 162 exhaust_discs: thm list, 163 sel_defs: thm list, 164 fp_nesting_maps: thm list, 165 fp_nesting_map_ident0s: thm list, 166 fp_nesting_map_comps: thm list, 167 ctr_specs: corec_ctr_spec list}; 168 169exception NO_MAP of term; 170 171fun abstract_over_list rev_vs = 172 let 173 val vs = rev rev_vs; 174 175 fun abs n (t $ u) = abs n t $ abs n u 176 | abs n (Abs (s, T, t)) = Abs (s, T, abs (n + 1) t) 177 | abs n t = 178 let val j = find_index (curry (op =) t) vs in 179 if j < 0 then t else Bound (n + j) 180 end; 181 in 182 abs 0 183 end; 184 185val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced; 186 187fun curried_type (Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>prod\<close>, Ts), T])) = 188 Ts ---> T; 189 190fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs); 191 192val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^const>\<open>True\<close>; 193val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^const>\<open>False\<close>; 194val mk_dnf = mk_disjs o map mk_conjs; 195 196val conjuncts_s = filter_out (curry (op aconv) \<^const>\<open>True\<close>) o HOLogic.conjuncts; 197 198fun s_not \<^const>\<open>True\<close> = \<^const>\<open>False\<close> 199 | s_not \<^const>\<open>False\<close> = \<^const>\<open>True\<close> 200 | s_not (\<^const>\<open>Not\<close> $ t) = t 201 | s_not (\<^const>\<open>conj\<close> $ t $ u) = \<^const>\<open>disj\<close> $ s_not t $ s_not u 202 | s_not (\<^const>\<open>disj\<close> $ t $ u) = \<^const>\<open>conj\<close> $ s_not t $ s_not u 203 | s_not t = \<^const>\<open>Not\<close> $ t; 204 205val s_not_conj = conjuncts_s o s_not o mk_conjs; 206 207fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^const>\<open>False\<close>] else cs; 208fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs; 209 210fun propagate_units css = 211 (case List.partition (can the_single) css of 212 ([], _) => css 213 | ([u] :: uss, css') => 214 [u] :: propagate_units (map (propagate_unit_neg (s_not u)) 215 (map (propagate_unit_pos u) (uss @ css')))); 216 217fun s_conjs cs = 218 if member (op aconv) cs \<^const>\<open>False\<close> then \<^const>\<open>False\<close> 219 else mk_conjs (remove (op aconv) \<^const>\<open>True\<close> cs); 220 221fun s_disjs ds = 222 if member (op aconv) ds \<^const>\<open>True\<close> then \<^const>\<open>True\<close> 223 else mk_disjs (remove (op aconv) \<^const>\<open>False\<close> ds); 224 225fun s_dnf css0 = 226 let val css = propagate_units css0 in 227 if null css then 228 [\<^const>\<open>False\<close>] 229 else if exists null css then 230 [] 231 else 232 map (fn c :: cs => (c, cs)) css 233 |> AList.coalesce (op =) 234 |> map (fn (c, css) => c :: s_dnf css) 235 |> (fn [cs] => cs | css => [s_disjs (map s_conjs css)]) 236 end; 237 238fun fold_rev_let_if_case ctxt f bound_Ts = 239 let 240 val thy = Proof_Context.theory_of ctxt; 241 242 fun fld conds t = 243 (case Term.strip_comb t of 244 (Const (\<^const_name>\<open>Let\<close>, _), [_, _]) => fld conds (unfold_lets_splits t) 245 | (Const (\<^const_name>\<open>If\<close>, _), [cond, then_branch, else_branch]) => 246 fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch 247 | (Const (c, _), args as _ :: _ :: _) => 248 let val n = num_binder_types (Sign.the_const_type thy c) - 1 in 249 if n >= 0 andalso n < length args then 250 (case fastype_of1 (bound_Ts, nth args n) of 251 Type (s, Ts) => 252 (case dest_case ctxt s Ts t of 253 SOME ({split_sels = _ :: _, ...}, conds', branches) => 254 fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches) 255 | _ => f conds t) 256 | _ => f conds t) 257 else 258 f conds t 259 end 260 | _ => f conds t); 261 in 262 fld [] 263 end; 264 265fun case_of ctxt s = 266 (case ctr_sugar_of ctxt s of 267 SOME {casex = Const (s', _), split_sels, ...} => SOME (s', not (null split_sels)) 268 | _ => NONE); 269 270fun massage_let_if_case ctxt has_call massage_leaf unexpected_call unsupported_case bound_Ts t0 = 271 let 272 val thy = Proof_Context.theory_of ctxt; 273 274 fun check_no_call bound_Ts t = if has_call t then unexpected_call bound_Ts t else (); 275 276 fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t 277 | massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m - 1) t) 278 | massage_abs bound_Ts m t = 279 let val T = domain_type (fastype_of1 (bound_Ts, t)) in 280 Abs (Name.uu, T, massage_abs (T :: bound_Ts) (m - 1) (incr_boundvars 1 t $ Bound 0)) 281 end 282 and massage_rec bound_Ts t = 283 let val typof = curry fastype_of1 bound_Ts in 284 (case Term.strip_comb t of 285 (Const (\<^const_name>\<open>Let\<close>, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t) 286 | (Const (\<^const_name>\<open>If\<close>, _), obj :: (branches as [_, _])) => 287 (case List.partition Term.is_dummy_pattern (map (massage_rec bound_Ts) branches) of 288 (dummy_branch' :: _, []) => dummy_branch' 289 | (_, [branch']) => branch' 290 | (_, branches') => 291 Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj, 292 branches')) 293 | (c as Const (\<^const_name>\<open>case_prod\<close>, _), arg :: args) => 294 massage_rec bound_Ts 295 (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args))) 296 | (Const (c, _), args as _ :: _ :: _) => 297 (case try strip_fun_type (Sign.the_const_type thy c) of 298 SOME (gen_branch_Ts, gen_body_fun_T) => 299 let 300 val gen_branch_ms = map num_binder_types gen_branch_Ts; 301 val n = length gen_branch_ms; 302 in 303 if n < length args then 304 (case gen_body_fun_T of 305 Type (_, [Type (T_name, _), _]) => 306 (case case_of ctxt T_name of 307 SOME (c', has_split_sels) => 308 if c' = c then 309 if has_split_sels then 310 let 311 val (branches, obj_leftovers) = chop n args; 312 val branches' = map2 (massage_abs bound_Ts) gen_branch_ms branches; 313 val branch_Ts' = map typof branches'; 314 val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts')); 315 val casex' = 316 Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T'); 317 in 318 Term.list_comb (casex', 319 branches' @ tap (List.app (check_no_call bound_Ts)) obj_leftovers) 320 end 321 else 322 unsupported_case bound_Ts t 323 else 324 massage_leaf bound_Ts t 325 | NONE => massage_leaf bound_Ts t) 326 | _ => massage_leaf bound_Ts t) 327 else 328 massage_leaf bound_Ts t 329 end 330 | NONE => massage_leaf bound_Ts t) 331 | _ => massage_leaf bound_Ts t) 332 end; 333 in 334 massage_rec bound_Ts t0 335 |> Term.map_aterms (fn t => 336 if Term.is_dummy_pattern t then Const (\<^const_name>\<open>undefined\<close>, fastype_of t) else t) 337 end; 338 339fun massage_let_if_case_corec ctxt has_call massage_leaf bound_Ts t0 = 340 massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call_in ctxt [t0])) 341 (K (unsupported_case_around_corec_call ctxt [t0])) bound_Ts t0; 342 343fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 = 344 let 345 fun check_no_call t = if has_call t then unexpected_corec_call_in ctxt [t0] t else (); 346 347 fun massage_mutual_call bound_Ts (Type (\<^type_name>\<open>fun\<close>, [_, U2])) 348 (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) t = 349 Abs (Name.uu, T1, massage_mutual_call (T1 :: bound_Ts) U2 T2 (incr_boundvars 1 t $ Bound 0)) 350 | massage_mutual_call bound_Ts U T t = 351 (if has_call t then massage_call else massage_noncall) bound_Ts U T t; 352 353 fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t = 354 (case try (dest_map ctxt s) t of 355 SOME (map0, fs) => 356 let 357 val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t)); 358 val map' = mk_map (length fs) dom_Ts Us map0; 359 val fs' = 360 map_flattened_map_args ctxt s (@{map 3} (massage_map_or_map_arg bound_Ts) Us Ts) fs; 361 in 362 Term.list_comb (map', fs') 363 end 364 | NONE => raise NO_MAP t) 365 | massage_map _ _ _ t = raise NO_MAP t 366 and massage_map_or_map_arg bound_Ts U T t = 367 if T = U then 368 tap check_no_call t 369 else 370 massage_map bound_Ts U T t 371 handle NO_MAP _ => massage_mutual_fun bound_Ts U T t 372 and massage_mutual_fun bound_Ts U T t = 373 let 374 val j = Term.maxidx_of_term t + 1; 375 val var = Var ((Name.uu, j), domain_type (fastype_of1 (bound_Ts, t))); 376 377 fun massage_body () = 378 Term.lambda var (Term.incr_boundvars 1 (massage_any_call bound_Ts U T 379 (betapply (t, var)))); 380 in 381 (case t of 382 Const (\<^const_name>\<open>comp\<close>, _) $ t1 $ t2 => 383 if has_call t2 then massage_body () 384 else mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, t2) 385 | _ => massage_body ()) 386 end 387 and massage_any_call bound_Ts U T = 388 massage_let_if_case_corec ctxt has_call (fn bound_Ts => fn t => 389 if has_call t then 390 (case U of 391 Type (s, Us) => 392 (case try (dest_ctr ctxt s) t of 393 SOME (f, args) => 394 let 395 val typof = curry fastype_of1 bound_Ts; 396 val f' = mk_ctr Us f 397 val f'_T = typof f'; 398 val arg_Ts = map typof args; 399 in 400 Term.list_comb (f', 401 @{map 3} (massage_any_call bound_Ts) (binder_types f'_T) arg_Ts args) 402 end 403 | NONE => 404 (case t of 405 Const (\<^const_name>\<open>case_prod\<close>, _) $ t' => 406 let 407 val U' = curried_type U; 408 val T' = curried_type T; 409 in 410 Const (\<^const_name>\<open>case_prod\<close>, U' --> U) $ massage_any_call bound_Ts U' T' t' 411 end 412 | t1 $ t2 => 413 (if has_call t2 then 414 massage_mutual_call bound_Ts U T t 415 else 416 massage_map bound_Ts U T t1 $ t2 417 handle NO_MAP _ => massage_mutual_call bound_Ts U T t) 418 | Abs (s, T', t') => 419 Abs (s, T', massage_any_call (T' :: bound_Ts) (range_type U) (range_type T) t') 420 | _ => massage_mutual_call bound_Ts U T t)) 421 | _ => ill_formed_corec_call ctxt t) 422 else 423 massage_noncall bound_Ts U T t) bound_Ts; 424 in 425 (if has_call t0 then massage_any_call else massage_noncall) bound_Ts U T t0 426 end; 427 428fun expand_to_ctr_term ctxt (T as Type (s, Ts)) t = 429 (case ctr_sugar_of ctxt s of 430 SOME {ctrs, casex, ...} => Term.list_comb (mk_case Ts T casex, map (mk_ctr Ts) ctrs) $ t 431 | NONE => raise Fail "expand_to_ctr_term"); 432 433fun expand_corec_code_rhs ctxt has_call bound_Ts t = 434 (case fastype_of1 (bound_Ts, t) of 435 T as Type (s, _) => 436 massage_let_if_case_corec ctxt has_call (fn _ => fn t => 437 if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt T t) bound_Ts t 438 | _ => raise Fail "expand_corec_code_rhs"); 439 440fun massage_corec_code_rhs ctxt massage_ctr = 441 massage_let_if_case_corec ctxt (K false) 442 (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb); 443 444fun fold_rev_corec_code_rhs ctxt f = 445 fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb); 446 447fun case_thms_of_term ctxt t = 448 let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in 449 (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #exhaust_discs ctr_sugars, 450 maps #split_sels ctr_sugars, maps #split_sel_asms ctr_sugars) 451 end; 452 453fun basic_corec_specs_of ctxt res_T = 454 (case res_T of 455 Type (T_name, _) => 456 (case Ctr_Sugar.ctr_sugar_of ctxt T_name of 457 NONE => not_codatatype ctxt res_T 458 | SOME {T = fpT, ctrs, discs, selss, ...} => 459 let 460 val thy = Proof_Context.theory_of ctxt; 461 462 val As_rho = tvar_subst thy [fpT] [res_T]; 463 val substA = Term.subst_TVars As_rho; 464 465 fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels}; 466 in 467 @{map 3} mk_spec ctrs discs selss 468 handle ListPair.UnequalLengths => not_codatatype ctxt res_T 469 end) 470 | _ => not_codatatype ctxt res_T); 471 472fun map_thms_of_type ctxt (Type (s, _)) = 473 (case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => []) 474 | map_thms_of_type _ _ = []; 475 476structure GFP_Rec_Sugar_Plugin = Plugin(type T = fp_rec_sugar); 477 478fun gfp_rec_sugar_interpretation name f = 479 GFP_Rec_Sugar_Plugin.interpretation name (fn fp_rec_sugar => fn lthy => 480 f (transfer_fp_rec_sugar (Proof_Context.theory_of lthy) fp_rec_sugar) lthy); 481 482val interpret_gfp_rec_sugar = GFP_Rec_Sugar_Plugin.data; 483 484fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 = 485 let 486 val thy = Proof_Context.theory_of lthy0; 487 488 val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs, 489 fp_co_induct_sugar = SOME {common_co_inducts = common_coinduct_thms, ...}, ...} :: _, 490 (_, gfp_sugar_thms)), lthy) = 491 nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0; 492 493 val coinduct_attrs_pair = 494 (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], [])); 495 496 val perm_fp_sugars = sort (int_ord o apply2 #fp_res_index) fp_sugars; 497 498 val indices = map #fp_res_index fp_sugars; 499 val perm_indices = map #fp_res_index perm_fp_sugars; 500 501 val perm_fpTs = map #T perm_fp_sugars; 502 val perm_ctrXs_Tsss' = 503 map (repair_nullary_single_ctr o #ctrXs_Tss o #fp_ctr_sugar) perm_fp_sugars; 504 505 val nn0 = length res_Ts; 506 val nn = length perm_fpTs; 507 val kks = 0 upto nn - 1; 508 val perm_ns' = map length perm_ctrXs_Tsss'; 509 510 val perm_Ts = map #T perm_fp_sugars; 511 val perm_Xs = map #X perm_fp_sugars; 512 val perm_Cs = 513 map (domain_type o body_fun_type o fastype_of o #co_rec o the o #fp_co_induct_sugar) 514 perm_fp_sugars; 515 val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs); 516 517 fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)] 518 | zip_corecT U = 519 (case AList.lookup (op =) Xs_TCs U of 520 SOME (T, C) => [T, C] 521 | NONE => [U]); 522 523 val perm_p_Tss = mk_corec_p_pred_types perm_Cs perm_ns'; 524 val perm_f_Tssss = 525 map2 (fn C => map (map (map (curry (op -->) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss'; 526 val perm_q_Tssss = 527 map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) perm_f_Tssss; 528 529 val (perm_p_hss, h) = indexedd perm_p_Tss 0; 530 val (perm_q_hssss, h') = indexedddd perm_q_Tssss h; 531 val (perm_f_hssss, _) = indexedddd perm_f_Tssss h'; 532 533 val fun_arg_hs = 534 flat (@{map 3} flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss); 535 536 fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs; 537 fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs; 538 539 val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms; 540 541 val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss); 542 val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss); 543 val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss); 544 545 val f_Tssss = unpermute perm_f_Tssss; 546 val fpTs = unpermute perm_fpTs; 547 val Cs = unpermute perm_Cs; 548 549 val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts; 550 val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts; 551 552 val substA = Term.subst_TVars As_rho; 553 val substAT = Term.typ_subst_TVars As_rho; 554 val substCT = Term.typ_subst_TVars Cs_rho; 555 556 val perm_Cs' = map substCT perm_Cs; 557 558 fun call_of nullary [] [g_i] [Type (\<^type_name>\<open>fun\<close>, [_, T])] = 559 (if exists_subtype_in Cs T then Nested_Corec 560 else if nullary then Dummy_No_Corec 561 else No_Corec) g_i 562 | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i'); 563 564 fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms distinct_discss collapse 565 corec_thm corec_disc corec_sels = 566 let val nullary = not (can dest_funT (fastype_of ctr)) in 567 {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io, 568 calls = @{map 3} (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms, 569 distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm, 570 corec_disc = corec_disc, corec_sels = corec_sels} 571 end; 572 573 fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...} 574 : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss = 575 let val p_ios = map SOME p_is @ [NONE] in 576 @{map 14} mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss 577 distinct_discsss collapses corec_thms corec_discs corec_selss 578 end; 579 580 fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, 581 fp_co_induct_sugar = SOME {co_rec = corec, co_rec_thms = corec_thms, 582 co_rec_discs = corec_discs, co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss 583 f_isss f_Tsss = 584 {T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, 585 exhaust_discs = exhaust_discs, sel_defs = sel_defs, 586 fp_nesting_maps = maps (map_thms_of_type lthy o T_of_bnf) fp_nesting_bnfs, 587 fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs, 588 fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs, 589 ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs 590 corec_selss}; 591 in 592 (@{map 5} mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts, 593 co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms, 594 co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss, coinduct_attrs_pair, 595 is_some gfp_sugar_thms, lthy) 596 end; 597 598val undef_const = Const (\<^const_name>\<open>undefined\<close>, dummyT); 599 600type coeqn_data_disc = 601 {fun_name: string, 602 fun_T: typ, 603 fun_args: term list, 604 ctr: term, 605 ctr_no: int, 606 disc: term, 607 prems: term list, 608 auto_gen: bool, 609 ctr_rhs_opt: term option, 610 code_rhs_opt: term option, 611 eqn_pos: int, 612 user_eqn: term}; 613 614type coeqn_data_sel = 615 {fun_name: string, 616 fun_T: typ, 617 fun_args: term list, 618 ctr: term, 619 sel: term, 620 rhs_term: term, 621 ctr_rhs_opt: term option, 622 code_rhs_opt: term option, 623 eqn_pos: int, 624 user_eqn: term}; 625 626fun ctr_sel_of ({ctr, sel, ...} : coeqn_data_sel) = (ctr, sel); 627 628datatype coeqn_data = 629 Disc of coeqn_data_disc | 630 Sel of coeqn_data_sel; 631 632fun is_free_in frees (Free (s, _)) = member (op =) frees s 633 | is_free_in _ _ = false; 634 635fun is_catch_all_prem (Free (s, _)) = s = Name.uu_ 636 | is_catch_all_prem _ = false; 637 638fun add_extra_frees ctxt frees names = 639 fold_aterms (fn x as Free (s, _) => 640 (not (member (op =) frees x) andalso not (member (op =) names s) andalso 641 not (Variable.is_fixed ctxt s) andalso not (is_catch_all_prem x)) 642 ? cons x | _ => I); 643 644fun check_extra_frees ctxt frees names t = 645 let val bads = add_extra_frees ctxt frees names t [] in 646 null bads orelse extra_variable_in_rhs ctxt [t] (hd bads) 647 end; 648 649fun check_fun_args ctxt eqn fun_args = 650 (check_duplicate_variables_in_lhs ctxt [eqn] fun_args; 651 check_all_fun_arg_frees ctxt [eqn] fun_args); 652 653fun dissect_coeqn_disc ctxt fun_names sequentials 654 (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos ctr_rhs_opt code_rhs_opt prems0 655 concl matchedsss = 656 let 657 fun find_subterm p = 658 let (* FIXME \<exists>? *) 659 fun find (t as u $ v) = if p t then SOME t else merge_options (find u, find v) 660 | find t = if p t then SOME t else NONE; 661 in find end; 662 663 val applied_fun = concl 664 |> find_subterm (member (op = o apsnd SOME) fun_names o try (fst o dest_Free o head_of)) 665 |> the 666 handle Option.Option => error_at ctxt [concl] "Ill-formed discriminator formula"; 667 val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free; 668 669 val _ = check_fun_args ctxt concl fun_args; 670 671 val bads = filter (Term.exists_subterm (is_free_in fun_names)) prems0; 672 val _ = null bads orelse unexpected_rec_call_in ctxt [] (hd bads); 673 674 val (sequential, basic_ctr_specs) = 675 the (AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name); 676 677 val discs = map #disc basic_ctr_specs; 678 val ctrs = map #ctr basic_ctr_specs; 679 val not_disc = head_of concl = \<^term>\<open>Not\<close>; 680 val _ = not_disc andalso length ctrs <> 2 andalso 681 error_at ctxt [concl] "Negated discriminator for a type with \<noteq> 2 constructors"; 682 val disc' = find_subterm (member (op =) discs o head_of) concl; 683 val eq_ctr0 = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd) 684 |> (fn SOME t => let val n = find_index (curry (op =) t) ctrs in 685 if n >= 0 then SOME n else NONE end | _ => NONE); 686 687 val _ = is_none disc' orelse perhaps (try HOLogic.dest_not) concl = the disc' orelse 688 error_at ctxt [concl] "Ill-formed discriminator formula"; 689 val _ = is_some disc' orelse is_some eq_ctr0 orelse 690 error_at ctxt [concl] "No discriminator in equation"; 691 692 val ctr_no' = 693 if is_none disc' then the eq_ctr0 else find_index (curry (op =) (head_of (the disc'))) discs; 694 val ctr_no = if not_disc then 1 - ctr_no' else ctr_no'; 695 val {ctr, disc, ...} = nth basic_ctr_specs ctr_no; 696 697 val catch_all = 698 (case prems0 of 699 [prem] => is_catch_all_prem prem 700 | _ => 701 if exists is_catch_all_prem prems0 then error_at ctxt [concl] "Superfluous premises" 702 else false); 703 val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default []; 704 val prems = map (abstract_over_list fun_args) prems0; 705 val actual_prems = 706 (if catch_all orelse sequential then maps s_not_conj matchedss else []) @ 707 (if catch_all then [] else prems); 708 709 val matchedsss' = AList.delete (op =) fun_name matchedsss 710 |> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [actual_prems]); 711 712 val user_eqn = 713 (actual_prems, concl) 714 |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract_over_list fun_args 715 |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies; 716 717 val _ = check_extra_frees ctxt fun_args fun_names user_eqn; 718 in 719 (Disc {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no, 720 disc = disc, prems = actual_prems, auto_gen = catch_all, ctr_rhs_opt = ctr_rhs_opt, 721 code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = user_eqn}, 722 matchedsss') 723 end; 724 725fun dissect_coeqn_sel ctxt fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos 726 ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn = 727 let 728 val (lhs, rhs) = HOLogic.dest_eq eqn 729 handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn]; 730 731 val sel = head_of lhs; 732 val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free 733 handle TERM _ => error_at ctxt [eqn] "Ill-formed selector argument in left-hand side"; 734 val _ = check_fun_args ctxt eqn fun_args; 735 736 val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name) 737 handle Option.Option => error_at ctxt [eqn] "Ill-formed selector argument in left-hand side"; 738 val {ctr, ...} = 739 (case of_spec_opt of 740 SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs) 741 | NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single 742 handle List.Empty => error_at ctxt [eqn] "Ambiguous selector (without \"of\")"); 743 val user_eqn = drop_all eqn0; 744 745 val _ = check_extra_frees ctxt fun_args fun_names user_eqn; 746 in 747 Sel {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, sel = sel, 748 rhs_term = rhs, ctr_rhs_opt = ctr_rhs_opt, code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, 749 user_eqn = user_eqn} 750 end; 751 752fun dissect_coeqn_ctr ctxt fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) 753 eqn_pos eqn0 code_rhs_opt prems concl matchedsss = 754 let 755 val (lhs, rhs) = HOLogic.dest_eq concl; 756 val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; 757 758 val _ = check_fun_args ctxt concl fun_args; 759 val _ = check_extra_frees ctxt fun_args fun_names (drop_all eqn0); 760 761 val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name); 762 val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs); 763 val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs) 764 handle Option.Option => not_constructor_in_rhs ctxt [] ctr; 765 766 val disc_concl = betapply (disc, lhs); 767 val (eqn_data_disc_opt, matchedsss') = 768 if null (tl basic_ctr_specs) andalso not (null sels) then 769 (NONE, matchedsss) 770 else 771 apfst SOME (dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos 772 (SOME (abstract_over_list fun_args rhs)) code_rhs_opt prems disc_concl matchedsss); 773 774 val sel_concls = sels ~~ ctr_args 775 |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)) 776 handle ListPair.UnequalLengths => partially_applied_ctr_in_rhs ctxt [rhs]; 777 778 val eqns_data_sel = 779 map (dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos 780 (SOME (abstract_over_list fun_args rhs)) code_rhs_opt eqn0 (SOME ctr)) 781 sel_concls; 782 in 783 (the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss') 784 end; 785 786fun dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss = 787 let 788 val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs ctxt has_call []); 789 val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; 790 791 val _ = check_fun_args ctxt concl fun_args; 792 val _ = check_extra_frees ctxt fun_args fun_names concl; 793 794 val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name); 795 796 val cond_ctrs = fold_rev_corec_code_rhs ctxt (fn cs => fn ctr => fn _ => 797 if member (op = o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs) 798 else not_constructor_in_rhs ctxt [] ctr) [] rhs' [] 799 |> AList.group (op =); 800 801 val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs); 802 val ctr_concls = cond_ctrs |> map (fn (ctr, _) => 803 binder_types (fastype_of ctr) 804 |> map_index (fn (n, T) => massage_corec_code_rhs ctxt (fn _ => fn ctr' => fn args => 805 if ctr' = ctr then nth args n else Term.dummy_pattern T) [] rhs') 806 |> curry Term.list_comb ctr 807 |> curry HOLogic.mk_eq lhs); 808 809 val bads = maps (filter (Term.exists_subterm (is_free_in fun_names))) ctr_premss; 810 val _ = null bads orelse unexpected_corec_call_in ctxt [eqn0] rhs; 811 812 val sequentials = replicate (length fun_names) false; 813 in 814 @{fold_map 2} (dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0 815 (SOME (abstract_over_list fun_args rhs))) 816 ctr_premss ctr_concls matchedsss 817 end; 818 819fun dissect_coeqn ctxt has_call fun_names sequentials 820 (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss = 821 let 822 val eqn = drop_all eqn0 823 handle TERM _ => ill_formed_formula ctxt eqn0; 824 val (prems, concl) = Logic.strip_horn eqn 825 |> map_prod (map HOLogic.dest_Trueprop) HOLogic.dest_Trueprop 826 handle TERM _ => ill_formed_equation ctxt eqn; 827 828 val head = concl 829 |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq)) 830 |> head_of; 831 832 val rhs_opt = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd); 833 834 fun check_num_args () = 835 is_none rhs_opt orelse not (can dest_funT (fastype_of (the rhs_opt))) orelse 836 missing_args_to_fun_on_lhs ctxt [eqn]; 837 838 val discs = maps (map #disc) basic_ctr_specss; 839 val sels = maps (maps #sels) basic_ctr_specss; 840 val ctrs = maps (map #ctr) basic_ctr_specss; 841 in 842 if member (op =) discs head orelse 843 (is_some rhs_opt andalso 844 member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso 845 member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt)) then 846 (dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl 847 matchedsss 848 |>> single) 849 else if member (op =) sels head then 850 (null prems orelse error_at ctxt [eqn] "Unexpected condition in selector formula"; 851 ([dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt 852 concl], matchedsss)) 853 else if is_some rhs_opt andalso is_Free head andalso is_free_in fun_names head then 854 if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then 855 (check_num_args (); 856 dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0 857 (if null prems then 858 SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0)))) 859 else 860 NONE) 861 prems concl matchedsss) 862 else if null prems then 863 (check_num_args (); 864 dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss 865 |>> flat) 866 else 867 error_at ctxt [eqn] "Cannot mix constructor and code views" 868 else if is_some rhs_opt then 869 error_at ctxt [eqn] ("Ill-formed equation head: " ^ quote (Syntax.string_of_term ctxt head)) 870 else 871 error_at ctxt [eqn] "Expected equation or discriminator formula" 872 end; 873 874fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list) 875 ({fun_args, ctr_no, prems, ...} : coeqn_data_disc) = 876 if is_none (#pred (nth ctr_specs ctr_no)) then 877 I 878 else 879 s_conjs prems 880 |> curry subst_bounds (List.rev fun_args) 881 |> abs_tuple_balanced fun_args 882 |> K |> nth_map (the (#pred (nth ctr_specs ctr_no))); 883 884fun build_corec_arg_no_call (sel_eqns : coeqn_data_sel list) sel = 885 find_first (curry (op =) sel o #sel) sel_eqns 886 |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple_balanced fun_args rhs_term) 887 |> the_default undef_const 888 |> K; 889 890fun build_corec_args_mutual_call ctxt has_call (sel_eqns : coeqn_data_sel list) sel = 891 (case find_first (curry (op =) sel o #sel) sel_eqns of 892 NONE => (I, I, I) 893 | SOME {fun_args, rhs_term, ... } => 894 let 895 val bound_Ts = List.rev (map fastype_of fun_args); 896 897 fun rewrite_stop _ t = if has_call t then \<^term>\<open>False\<close> else \<^term>\<open>True\<close>; 898 fun rewrite_end _ t = if has_call t then undef_const else t; 899 fun rewrite_cont bound_Ts t = 900 if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const; 901 fun massage f _ = massage_let_if_case_corec ctxt has_call f bound_Ts rhs_term 902 |> abs_tuple_balanced fun_args; 903 in 904 (massage rewrite_stop, massage rewrite_end, massage rewrite_cont) 905 end); 906 907fun build_corec_arg_nested_call ctxt has_call (sel_eqns : coeqn_data_sel list) sel = 908 (case find_first (curry (op =) sel o #sel) sel_eqns of 909 NONE => I 910 | SOME {fun_args, rhs_term, ...} => 911 let 912 fun massage_call bound_Ts U T t0 = 913 let 914 val U2 = 915 (case try dest_sumT U of 916 SOME (U1, U2) => if U1 = T then U2 else invalid_map ctxt [] t0 917 | NONE => invalid_map ctxt [] t0); 918 919 fun rewrite bound_Ts (Abs (s, T', t')) = Abs (s, T', rewrite (T' :: bound_Ts) t') 920 | rewrite bound_Ts (t as _ $ _) = 921 let val (u, vs) = strip_comb t in 922 if is_Free u andalso has_call u then 923 Inr_const T U2 $ mk_tuple1_balanced bound_Ts vs 924 else if try (fst o dest_Const) u = SOME \<^const_name>\<open>case_prod\<close> then 925 map (rewrite bound_Ts) vs |> chop 1 926 |>> HOLogic.mk_case_prod o the_single 927 |> Term.list_comb 928 else 929 Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs) 930 end 931 | rewrite _ t = 932 if is_Free t andalso has_call t then Inr_const T U2 $ HOLogic.unit else t; 933 in 934 rewrite bound_Ts t0 935 end; 936 937 fun massage_noncall U T t = 938 build_map ctxt [] [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t; 939 940 val bound_Ts = List.rev (map fastype_of fun_args); 941 in 942 fn t => 943 rhs_term 944 |> massage_nested_corec_call ctxt has_call massage_call (K massage_noncall) bound_Ts 945 (range_type (fastype_of t)) (fastype_of1 (bound_Ts, rhs_term)) 946 |> abs_tuple_balanced fun_args 947 end); 948 949fun build_corec_args_sel ctxt has_call (all_sel_eqns : coeqn_data_sel list) 950 (ctr_spec : corec_ctr_spec) = 951 (case filter (curry (op =) (#ctr ctr_spec) o #ctr) all_sel_eqns of 952 [] => I 953 | sel_eqns => 954 let 955 val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec; 956 val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list; 957 val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list; 958 val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list; 959 in 960 I 961 #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls' 962 #> fold (fn (sel, (q, g, h)) => 963 let val (fq, fg, fh) = build_corec_args_mutual_call ctxt has_call sel_eqns sel in 964 nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls' 965 #> fold (fn (sel, n) => nth_map n 966 (build_corec_arg_nested_call ctxt has_call sel_eqns sel)) nested_calls' 967 end); 968 969fun build_defs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list) 970 (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) = 971 let 972 val corecs = map #corec corec_specs; 973 val ctr_specss = map #ctr_specs corec_specs; 974 val corec_args = hd corecs 975 |> fst o split_last o binder_types o fastype_of 976 |> map (fn T => 977 if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, \<^term>\<open>False\<close>) 978 else Const (\<^const_name>\<open>undefined\<close>, T)) 979 |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss 980 |> fold2 (fold o build_corec_args_sel ctxt has_call) sel_eqnss ctr_specss; 981 982 val bad = fold (add_extra_frees ctxt [] []) corec_args []; 983 val _ = null bad orelse 984 (if exists has_call corec_args then nonprimitive_corec ctxt [] 985 else extra_variable_in_rhs ctxt [] (hd bad)); 986 987 val excludess' = 988 disc_eqnss 989 |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x)) 990 #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs []) 991 #> maps (uncurry (map o pair) 992 #> map (fn ((fun_args, c, x, a), (_, c', y, a')) => 993 ((c, c', a orelse a'), (x, s_not (s_conjs y))) 994 ||> map_prod (map HOLogic.mk_Trueprop) HOLogic.mk_Trueprop 995 ||> Logic.list_implies 996 ||> curry Logic.list_all (map dest_Free fun_args)))); 997 in 998 map (Term.list_comb o rpair corec_args) corecs 999 |> map2 abs_curried_balanced arg_Tss 1000 |> (fn ts => Syntax.check_terms ctxt ts 1001 handle ERROR _ => nonprimitive_corec ctxt []) 1002 |> @{map 3} (fn b => fn mx => fn t => 1003 ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) bs mxs 1004 |> rpair excludess' 1005 end; 1006 1007fun mk_actual_disc_eqns fun_binding arg_Ts exhaustive ({ctr_specs, ...} : corec_spec) 1008 (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) = 1009 let 1010 val fun_name = Binding.name_of fun_binding; 1011 val num_disc_eqns = length disc_eqns; 1012 val num_ctrs = length ctr_specs; 1013 in 1014 if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> num_ctrs - 1 then 1015 (num_disc_eqns > 0 orelse error ("Missing discriminator formula for " ^ quote fun_name); 1016 disc_eqns) 1017 else 1018 let 1019 val ctr_no = 0 upto length ctr_specs 1020 |> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns)); 1021 val {ctr, disc, ...} = nth ctr_specs ctr_no; 1022 val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns; 1023 1024 val fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))); 1025 val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns) 1026 |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options; 1027 val prems = maps (s_not_conj o #prems) disc_eqns; 1028 val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE; 1029 val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE; 1030 val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt 1031 |> the_default 100000; (* FIXME *) 1032 1033 val extra_disc_eqn = 1034 {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no, 1035 disc = disc, prems = prems, auto_gen = true, ctr_rhs_opt = ctr_rhs_opt, 1036 code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = undef_const}; 1037 in 1038 chop ctr_no disc_eqns ||> cons extra_disc_eqn |> op @ 1039 end 1040 end; 1041 1042fun find_corec_calls ctxt has_call (basic_ctr_specs : basic_corec_ctr_spec list) 1043 ({ctr, sel, rhs_term, ...} : coeqn_data_sel) = 1044 let 1045 val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs 1046 |> find_index (curry (op =) sel) o #sels o the; 1047 in 1048 K (if has_call rhs_term then fold_rev_let_if_case ctxt (K cons) [] rhs_term [] else []) 1049 |> nth_map sel_no |> AList.map_entry (op =) ctr 1050 end; 1051 1052fun applied_fun_of fun_name fun_T fun_args = 1053 Term.list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); 1054 1055fun is_trivial_implies thm = 1056 uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm)); 1057 1058fun primcorec_ursive int auto opts fixes specs of_specs_opt lthy = 1059 let 1060 val (bs, mxs) = map_split (apfst fst) fixes; 1061 val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list; 1062 val primcorec_types = map (#1 o dest_Type) res_Ts; 1063 1064 val _ = check_duplicate_const_names bs; 1065 val _ = List.app (uncurry (check_top_sort lthy)) (bs ~~ arg_Ts); 1066 1067 val actual_nn = length bs; 1068 1069 val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) 1070 |> the_default Plugin_Name.default_filter; 1071 val sequentials = replicate actual_nn (exists (can (fn Sequential_Option => ())) opts); 1072 val exhaustives = replicate actual_nn (exists (can (fn Exhaustive_Option => ())) opts); 1073 val transfers = replicate actual_nn (exists (can (fn Transfer_Option => ())) opts); 1074 1075 val fun_names = map Binding.name_of bs; 1076 val qualifys = map (fold_rev (uncurry Binding.qualify o swap) o Binding.path_of) bs; 1077 val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts; 1078 val frees = map (fst #>> Binding.name_of #> Free) fixes; 1079 val has_call = Term.exists_subterm (member (op =) frees); 1080 val eqns_data = 1081 @{fold_map 2} (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) 1082 (tag_list 0 (map snd specs)) of_specs_opt [] 1083 |> flat o fst; 1084 1085 val missing = fun_names 1086 |> filter (map (fn Disc x => #fun_name x | Sel x => #fun_name x) eqns_data 1087 |> not oo member (op =)); 1088 val _ = null missing orelse missing_equations_for_const (hd missing); 1089 1090 val callssss = 1091 map_filter (try (fn Sel x => x)) eqns_data 1092 |> partition_eq (op = o apply2 #fun_name) 1093 |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 1094 |> map (flat o snd) 1095 |> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss 1096 |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} => 1097 (ctr, map (K []) sels))) basic_ctr_specss); 1098 1099 val (corec_specs0, _, coinduct_thm, coinduct_strong_thm, coinduct_thms, coinduct_strong_thms, 1100 (coinduct_attrs, common_coinduct_attrs), n2m, lthy) = 1101 corec_specs_of bs arg_Ts res_Ts frees callssss lthy; 1102 val corec_specs = take actual_nn corec_specs0; 1103 val ctr_specss = map #ctr_specs corec_specs; 1104 1105 val disc_eqnss0 = map_filter (try (fn Disc x => x)) eqns_data 1106 |> partition_eq (op = o apply2 #fun_name) 1107 |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 1108 |> map (sort (op < o apply2 #ctr_no |> make_ord) o flat o snd); 1109 1110 val _ = disc_eqnss0 |> map (fn x => 1111 let val dups = duplicates (op = o apply2 #ctr_no) x in 1112 null dups orelse 1113 error_at lthy 1114 (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) dups 1115 |> map (fn {ctr_rhs_opt = SOME t, ...} => t | {user_eqn, ...} => user_eqn)) 1116 "Overspecified case(s)" 1117 end); 1118 1119 val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data 1120 |> partition_eq (op = o apply2 #fun_name) 1121 |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 1122 |> map (flat o snd); 1123 1124 val _ = sel_eqnss |> map (fn x => 1125 let val dups = duplicates (op = o apply2 ctr_sel_of) x in 1126 null dups orelse 1127 error_at lthy 1128 (maps (fn t => filter (curry (op =) (ctr_sel_of t) o ctr_sel_of) x) dups 1129 |> map (fn {ctr_rhs_opt = SOME t, ...} => t | {user_eqn, ...} => user_eqn)) 1130 "Overspecified case(s)" 1131 end); 1132 1133 val arg_Tss = map (binder_types o snd o fst) fixes; 1134 val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss 1135 disc_eqnss0; 1136 val (defs, excludess') = 1137 build_defs lthy bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss; 1138 1139 val tac_opts = 1140 map (fn {code_rhs_opt, ...} :: _ => 1141 if auto orelse is_some code_rhs_opt then SOME (auto_tac o #context) else NONE) disc_eqnss; 1142 1143 fun exclude_tac tac_opt sequential (c, c', a) = 1144 if a orelse c = c' orelse sequential then 1145 SOME (fn {context = ctxt, prems = _} => HEADGOAL (mk_primcorec_assumption_tac ctxt [])) 1146 else 1147 tac_opt; 1148 1149 val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) => 1150 (j, (Option.map (Goal.prove (*no sorry*) lthy [] [] goal #> Thm.close_derivation \<^here>) 1151 (exclude_tac tac_opt sequential j), goal)))) 1152 tac_opts sequentials excludess' 1153 handle ERROR _ => use_primcorecursive (); 1154 1155 val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess''; 1156 val (goal_idxss, exclude_goalss) = excludess'' 1157 |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd)) 1158 |> split_list o map split_list; 1159 1160 fun list_all_fun_args extras = 1161 map2 (fn [] => I 1162 | {fun_args, ...} :: _ => map (curry Logic.list_all (extras @ map dest_Free fun_args))) 1163 disc_eqnss; 1164 1165 val syntactic_exhaustives = 1166 map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns 1167 orelse exists #auto_gen disc_eqns) 1168 disc_eqnss; 1169 val de_facto_exhaustives = 1170 map2 (fn b => fn b' => b orelse b') exhaustives syntactic_exhaustives; 1171 1172 val nchotomy_goalss = 1173 map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems) 1174 de_facto_exhaustives disc_eqnss 1175 |> list_all_fun_args [] 1176 val nchotomy_taut_thmss = 1177 @{map 5} (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} => 1178 fn {code_rhs_opt, ...} :: _ => fn [] => K [] 1179 | [goal] => fn true => 1180 let 1181 val (_, _, arg_exhaust_discs, _, _) = 1182 case_thms_of_term lthy (the_default Term.dummy code_rhs_opt); 1183 in 1184 [Goal.prove (*no sorry*) lthy [] [] goal (fn {context = ctxt, ...} => 1185 mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs)) 1186 |> Thm.close_derivation \<^here>] 1187 handle ERROR _ => use_primcorecursive () 1188 end 1189 | false => 1190 (case tac_opt of 1191 SOME tac => [Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation \<^here>] 1192 | NONE => [])) 1193 tac_opts corec_specs disc_eqnss nchotomy_goalss syntactic_exhaustives; 1194 1195 val syntactic_exhaustives = 1196 map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns 1197 orelse exists #auto_gen disc_eqns) 1198 disc_eqnss; 1199 1200 val nchotomy_goalss = 1201 map2 (fn (NONE, false) => map (rpair []) | _ => K []) (tac_opts ~~ syntactic_exhaustives) 1202 nchotomy_goalss; 1203 1204 val goalss = nchotomy_goalss @ exclude_goalss; 1205 1206 fun prove thmss'' def_infos lthy = 1207 let 1208 val def_thms = map (snd o snd) def_infos; 1209 val ts = map fst def_infos; 1210 1211 val (nchotomy_thmss, exclude_thmss) = 1212 (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss''); 1213 1214 val ps = 1215 Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)]; 1216 1217 val exhaust_thmss = 1218 map2 (fn false => K [] 1219 | true => fn disc_eqns as {fun_args, ...} :: _ => 1220 let 1221 val p = Bound (length fun_args); 1222 fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); 1223 in 1224 [mk_imp_p (map (mk_imp_p o map HOLogic.mk_Trueprop o #prems) disc_eqns)] 1225 end) 1226 de_facto_exhaustives disc_eqnss 1227 |> list_all_fun_args ps 1228 |> @{map 3} (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K [] 1229 | [nchotomy_thm] => fn [goal] => 1230 [Goal.prove_sorry lthy [] [] goal 1231 (fn {context = ctxt, prems = _} => 1232 mk_primcorec_exhaust_tac ctxt 1233 ("" (* for "P" *) :: map (fst o dest_Free) fun_args) 1234 (length disc_eqns) nchotomy_thm) 1235 |> Thm.close_derivation \<^here>]) 1236 disc_eqnss nchotomy_thmss; 1237 val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss; 1238 1239 val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss); 1240 fun mk_excludesss excludes n = 1241 fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm]))) 1242 excludes (map (fn k => replicate k [asm_rl] @ replicate (n - k) []) (0 upto n - 1)); 1243 val excludessss = 1244 map2 (fn excludes => mk_excludesss excludes o length o #ctr_specs) 1245 (map2 append excludess' taut_thmss) corec_specs; 1246 1247 fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss 1248 ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) = 1249 if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), \<^term>\<open>\<lambda>x. x = x\<close>) then 1250 [] 1251 else 1252 let 1253 val {disc, corec_disc, ...} = nth ctr_specs ctr_no; 1254 val k = 1 + ctr_no; 1255 val m = length prems; 1256 val goal = 1257 applied_fun_of fun_name fun_T fun_args 1258 |> curry betapply disc 1259 |> HOLogic.mk_Trueprop 1260 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) 1261 |> curry Logic.list_all (map dest_Free fun_args); 1262 in 1263 if prems = [\<^term>\<open>False\<close>] then 1264 [] 1265 else 1266 Goal.prove_sorry lthy [] [] goal 1267 (fn {context = ctxt, prems = _} => 1268 mk_primcorec_disc_tac ctxt def_thms corec_disc k m excludesss) 1269 |> Thm.close_derivation \<^here> 1270 |> pair (#disc (nth ctr_specs ctr_no)) 1271 |> pair eqn_pos 1272 |> single 1273 end; 1274 1275 fun prove_sel ({sel_defs, fp_nesting_maps, fp_nesting_map_ident0s, fp_nesting_map_comps, 1276 ctr_specs, ...} : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss 1277 ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, code_rhs_opt, eqn_pos, ...} 1278 : coeqn_data_sel) = 1279 let 1280 val ctr_spec = the (find_first (curry (op =) ctr o #ctr) ctr_specs); 1281 val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs; 1282 val prems = the_default (maps (s_not_conj o #prems) disc_eqns) 1283 (find_first (curry (op =) ctr_no o #ctr_no) disc_eqns |> Option.map #prems); 1284 val corec_sel = find_index (curry (op =) sel) (#sels ctr_spec) 1285 |> nth (#corec_sels ctr_spec); 1286 val k = 1 + ctr_no; 1287 val m = length prems; 1288 val goal = 1289 applied_fun_of fun_name fun_T fun_args 1290 |> curry betapply sel 1291 |> rpair (abstract_over_list fun_args rhs_term) 1292 |> HOLogic.mk_Trueprop o HOLogic.mk_eq 1293 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) 1294 |> curry Logic.list_all (map dest_Free fun_args); 1295 val (distincts, _, _, split_sels, split_sel_asms) = case_thms_of_term lthy rhs_term; 1296 in 1297 Goal.prove_sorry lthy [] [] goal 1298 (fn {context = ctxt, prems = _} => 1299 mk_primcorec_sel_tac ctxt def_thms distincts split_sels split_sel_asms 1300 fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m 1301 excludesss) 1302 |> Thm.close_derivation \<^here> 1303 |> `(is_some code_rhs_opt ? Local_Defs.fold lthy sel_defs) (*mildly too aggressive*) 1304 |> pair sel 1305 |> pair eqn_pos 1306 end; 1307 1308 fun prove_ctr disc_alist sel_alist ({sel_defs, ...} : corec_spec) 1309 (disc_eqns : coeqn_data_disc list) (sel_eqns : coeqn_data_sel list) 1310 ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) = 1311 (* don't try to prove theorems when some sel_eqns are missing *) 1312 if not (exists (curry (op =) ctr o #ctr) disc_eqns) 1313 andalso not (exists (curry (op =) ctr o #ctr) sel_eqns) 1314 orelse 1315 filter (curry (op =) ctr o #ctr) sel_eqns 1316 |> fst o finds (op = o apsnd #sel) sels 1317 |> exists (null o snd) then 1318 [] 1319 else 1320 let 1321 val (fun_name, fun_T, fun_args, prems, ctr_rhs_opt, code_rhs_opt, eqn_pos) = 1322 (find_first (curry (op =) ctr o #ctr) disc_eqns, 1323 find_first (curry (op =) ctr o #ctr) sel_eqns) 1324 |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x, 1325 #ctr_rhs_opt x, #code_rhs_opt x, #eqn_pos x)) 1326 ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], 1327 #ctr_rhs_opt x, #code_rhs_opt x, #eqn_pos x)) 1328 |> the o merge_options; 1329 val m = length prems; 1330 val goal = 1331 (case ctr_rhs_opt of 1332 SOME rhs => rhs 1333 | NONE => 1334 filter (curry (op =) ctr o #ctr) sel_eqns 1335 |> fst o finds (op = o apsnd #sel) sels 1336 |> map (snd #> (fn [x] => (#fun_args x, #rhs_term x)) 1337 #-> abstract_over_list) 1338 |> curry Term.list_comb ctr) 1339 |> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args) 1340 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) 1341 |> curry Logic.list_all (map dest_Free fun_args); 1342 val disc_thm_opt = AList.lookup (op =) disc_alist disc; 1343 val sel_thms = map (snd o snd) (filter (member (op =) sels o fst) sel_alist); 1344 in 1345 if prems = [\<^term>\<open>False\<close>] then 1346 [] 1347 else 1348 Goal.prove_sorry lthy [] [] goal 1349 (fn {context = ctxt, prems = _} => 1350 mk_primcorec_ctr_tac ctxt m collapse disc_thm_opt sel_thms) 1351 |> is_some code_rhs_opt ? Local_Defs.fold lthy sel_defs (*mildly too aggressive*) 1352 |> Thm.close_derivation \<^here> 1353 |> pair ctr 1354 |> pair eqn_pos 1355 |> single 1356 end; 1357 1358 fun prove_code exhaustive (disc_eqns : coeqn_data_disc list) 1359 (sel_eqns : coeqn_data_sel list) nchotomys ctr_alist ctr_specs = 1360 let 1361 val fun_data_opt = 1362 (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns, 1363 find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns) 1364 |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x)) 1365 ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x)) 1366 |> merge_options; 1367 in 1368 (case fun_data_opt of 1369 NONE => [] 1370 | SOME (fun_name, fun_T, fun_args, rhs_opt) => 1371 let 1372 val bound_Ts = List.rev (map fastype_of fun_args); 1373 1374 val lhs = applied_fun_of fun_name fun_T fun_args; 1375 val rhs_info_opt = 1376 (case rhs_opt of 1377 SOME rhs => 1378 let 1379 val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs; 1380 val cond_ctrs = 1381 fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs []; 1382 val ctr_thms = 1383 map (the_default FalseE o AList.lookup (op =) ctr_alist o snd) cond_ctrs; 1384 in SOME (false, rhs, raw_rhs, ctr_thms) end 1385 | NONE => 1386 let 1387 fun prove_code_ctr ({ctr, sels, ...} : corec_ctr_spec) = 1388 if not (exists (curry (op =) ctr o fst) ctr_alist) then 1389 NONE 1390 else 1391 let 1392 val prems = find_first (curry (op =) ctr o #ctr) disc_eqns 1393 |> Option.map #prems |> the_default []; 1394 val t = 1395 filter (curry (op =) ctr o #ctr) sel_eqns 1396 |> fst o finds (op = o apsnd #sel) sels 1397 |> map (snd #> (fn [x] => (#fun_args x, #rhs_term x)) 1398 #-> abstract_over_list) 1399 |> curry Term.list_comb ctr; 1400 in 1401 SOME (prems, t) 1402 end; 1403 val ctr_conds_argss_opt = map prove_code_ctr ctr_specs; 1404 val exhaustive_code = 1405 exhaustive 1406 orelse exists (is_some andf (null o fst o the)) ctr_conds_argss_opt 1407 orelse forall is_some ctr_conds_argss_opt 1408 andalso exists #auto_gen disc_eqns; 1409 val rhs = 1410 (if exhaustive_code then 1411 split_last (map_filter I ctr_conds_argss_opt) ||> snd 1412 else 1413 Const (\<^const_name>\<open>Code.abort\<close>, \<^typ>\<open>String.literal\<close> --> 1414 (HOLogic.unitT --> body_type fun_T) --> body_type fun_T) $ 1415 HOLogic.mk_literal fun_name $ 1416 absdummy HOLogic.unitT (incr_boundvars 1 lhs) 1417 |> pair (map_filter I ctr_conds_argss_opt)) 1418 |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u) 1419 in 1420 SOME (exhaustive_code, rhs, rhs, map snd ctr_alist) 1421 end); 1422 in 1423 (case rhs_info_opt of 1424 NONE => [] 1425 | SOME (exhaustive_code, rhs, raw_rhs, ctr_thms) => 1426 let 1427 val ms = map (Logic.count_prems o Thm.prop_of) ctr_thms; 1428 val (raw_goal, goal) = (raw_rhs, rhs) 1429 |> apply2 (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args) 1430 #> abstract_over_list fun_args 1431 #> curry Logic.list_all (map dest_Free fun_args)); 1432 val (distincts, discIs, _, split_sels, split_sel_asms) = 1433 case_thms_of_term lthy raw_rhs; 1434 1435 val raw_code_thm = 1436 Goal.prove_sorry lthy [] [] raw_goal 1437 (fn {context = ctxt, prems = _} => 1438 mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms 1439 ms ctr_thms 1440 (if exhaustive_code then try the_single nchotomys else NONE)) 1441 |> Thm.close_derivation \<^here>; 1442 in 1443 Goal.prove_sorry lthy [] [] goal 1444 (fn {context = ctxt, prems = _} => 1445 mk_primcorec_code_tac ctxt distincts split_sels raw_code_thm) 1446 |> Thm.close_derivation \<^here> 1447 |> single 1448 end) 1449 end) 1450 end; 1451 1452 val disc_alistss = @{map 3} (map oo prove_disc) corec_specs excludessss disc_eqnss; 1453 val disc_alists = map (map snd o flat) disc_alistss; 1454 val sel_alists = @{map 4} (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss; 1455 val disc_thmss = map (map snd o sort_list_duplicates o flat) disc_alistss; 1456 val disc_thmsss' = map (map (map (snd o snd))) disc_alistss; 1457 val sel_thmss = map (map (fst o snd) o sort_list_duplicates) sel_alists; 1458 1459 fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss' 1460 (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms 1461 ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) = 1462 if null exhaust_thms orelse null disc_thms then 1463 [] 1464 else 1465 let 1466 val {disc, distinct_discss, ...} = nth ctr_specs ctr_no; 1467 val goal = 1468 mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args |> curry betapply disc, 1469 mk_conjs prems) 1470 |> curry Logic.list_all (map dest_Free fun_args); 1471 in 1472 Goal.prove_sorry lthy [] [] goal 1473 (fn {context = ctxt, prems = _} => 1474 mk_primcorec_disc_iff_tac ctxt (map (fst o dest_Free) exhaust_fun_args) 1475 (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)) 1476 |> Thm.close_derivation \<^here> 1477 |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule))) 1478 @{thms eqTrueE eq_False[THEN iffD1] notnotD} 1479 |> pair eqn_pos 1480 |> single 1481 end; 1482 1483 val disc_iff_thmss = @{map 6} (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss 1484 disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss 1485 |> map sort_list_duplicates; 1486 1487 val ctr_alists = @{map 6} (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists 1488 (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss; 1489 val ctr_thmss0 = map (map snd) ctr_alists; 1490 val ctr_thmss = map (map (snd o snd) o sort (int_ord o apply2 fst)) ctr_alists; 1491 1492 val code_thmss = 1493 @{map 6} prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss0 ctr_specss; 1494 1495 val disc_iff_or_disc_thmss = 1496 map2 (fn [] => I | disc_iffs => K disc_iffs) disc_iff_thmss disc_thmss; 1497 val simp_thmss = map2 append disc_iff_or_disc_thmss sel_thmss; 1498 1499 val common_name = mk_common_name fun_names; 1500 val common_qualify = fold_rev I qualifys; 1501 1502 val anonymous_notes = 1503 [(flat disc_iff_or_disc_thmss, simp_attrs)] 1504 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); 1505 1506 val common_notes = 1507 [(coinductN, if n2m then [coinduct_thm] else [], common_coinduct_attrs), 1508 (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], common_coinduct_attrs)] 1509 |> filter_out (null o #2) 1510 |> map (fn (thmN, thms, attrs) => 1511 ((common_qualify (Binding.qualify true common_name (Binding.name thmN)), attrs), 1512 [(thms, [])])); 1513 1514 val notes = 1515 [(coinductN, map (if n2m then single else K []) coinduct_thms, coinduct_attrs), 1516 (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms, 1517 coinduct_attrs), 1518 (codeN, code_thmss, nitpicksimp_attrs), 1519 (ctrN, ctr_thmss, []), 1520 (discN, disc_thmss, []), 1521 (disc_iffN, disc_iff_thmss, []), 1522 (excludeN, exclude_thmss, []), 1523 (exhaustN, nontriv_exhaust_thmss, []), 1524 (selN, sel_thmss, simp_attrs), 1525 (simpsN, simp_thmss, [])] 1526 |> maps (fn (thmN, thmss, attrs) => 1527 @{map 3} (fn fun_name => fn qualify => fn thms => 1528 ((qualify (Binding.qualify true fun_name (Binding.name thmN)), attrs), 1529 [(thms, [])])) 1530 fun_names qualifys (take actual_nn thmss)) 1531 |> filter_out (null o fst o hd o snd); 1532 1533 val fun_ts0 = map fst def_infos; 1534 in 1535 lthy 1536 |> Spec_Rules.add Binding.empty (Spec_Rules.equational_primcorec primcorec_types) 1537 fun_ts0 (flat sel_thmss) 1538 |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat ctr_thmss) 1539 |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat code_thmss) 1540 |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss)) 1541 |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) 1542 |> snd 1543 |> (fn lthy => 1544 let 1545 val phi = Local_Theory.target_morphism lthy; 1546 val Ts = take actual_nn (map #T corec_specs); 1547 val fp_rec_sugar = 1548 {transfers = transfers, fun_names = fun_names, funs = map (Morphism.term phi) ts, 1549 fun_defs = Morphism.fact phi def_thms, fpTs = Ts}; 1550 in 1551 interpret_gfp_rec_sugar plugins fp_rec_sugar lthy 1552 end) 1553 end; 1554 1555 fun after_qed thmss' = 1556 fold_map Local_Theory.define defs 1557 #> tap (uncurry (print_def_consts int)) 1558 #-> prove thmss'; 1559 in 1560 (goalss, after_qed, lthy) 1561 end; 1562 1563fun primcorec_ursive_cmd int auto opts (raw_fixes, raw_specs_of) lthy = 1564 let 1565 val (raw_specs, of_specs_opt) = 1566 split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy)); 1567 val (fixes, specs) = 1568 fst (Specification.read_multi_specs raw_fixes (map (fn spec => (spec, [], [])) raw_specs) lthy); 1569 in 1570 primcorec_ursive int auto opts fixes specs of_specs_opt lthy 1571 end; 1572 1573fun primcorecursive_cmd int = (fn (goalss, after_qed, lthy) => 1574 lthy 1575 |> Proof.theorem NONE after_qed goalss 1576 |> Proof.refine_singleton (Method.primitive_text (K I))) ooo 1577 primcorec_ursive_cmd int false; 1578 1579fun primcorec_cmd int = (fn (goalss, after_qed, lthy) => 1580 lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo 1581 primcorec_ursive_cmd int true; 1582 1583val corec_option_parser = Parse.group (K "option") 1584 (Plugin_Name.parse_filter >> Plugins_Option 1585 || Parse.reserved "sequential" >> K Sequential_Option 1586 || Parse.reserved "exhaustive" >> K Exhaustive_Option 1587 || Parse.reserved "transfer" >> K Transfer_Option); 1588 1589val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|" 1590 ((Parse.prop >> pair Binding.empty_atts) -- Scan.option (Parse.reserved "of" |-- Parse.const))); 1591 1592val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>primcorecursive\<close> 1593 "define primitive corecursive functions" 1594 ((Scan.optional (\<^keyword>\<open>(\<close> |-- 1595 Parse.!!! (Parse.list1 corec_option_parser) --| \<^keyword>\<open>)\<close>) []) -- 1596 (Parse.vars -- where_alt_props_of_parser) >> uncurry (primcorecursive_cmd true)); 1597 1598val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>primcorec\<close> 1599 "define primitive corecursive functions" 1600 ((Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 corec_option_parser) 1601 --| \<^keyword>\<open>)\<close>) []) -- 1602 (Parse.vars -- where_alt_props_of_parser) >> uncurry (primcorec_cmd true)); 1603 1604val _ = Theory.setup (gfp_rec_sugar_interpretation transfer_plugin 1605 gfp_rec_sugar_transfer_interpretation); 1606 1607end; 1608