1(* Title: HOL/Tools/inductive.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 4 5(Co)Inductive Definition module for HOL. 6 7Features: 8 * least or greatest fixedpoints 9 * mutually recursive definitions 10 * definitions involving arbitrary monotone operators 11 * automatically proves introduction and elimination rules 12 13 Introduction rules have the form 14 [| M Pj ti, ..., Q x, ... |] ==> Pk t 15 where M is some monotone operator (usually the identity) 16 Q x is any side condition on the free variables 17 ti, t are any terms 18 Pj, Pk are two of the predicates being defined in mutual recursion 19*) 20 21signature INDUCTIVE = 22sig 23 type result = 24 {preds: term list, elims: thm list, raw_induct: thm, 25 induct: thm, inducts: thm list, intrs: thm list, eqs: thm list} 26 val transform_result: morphism -> result -> result 27 type info = {names: string list, coind: bool} * result 28 val the_inductive: Proof.context -> term -> info 29 val the_inductive_global: Proof.context -> string -> info 30 val print_inductives: bool -> Proof.context -> unit 31 val get_monos: Proof.context -> thm list 32 val mono_add: attribute 33 val mono_del: attribute 34 val mk_cases_tac: Proof.context -> tactic 35 val mk_cases: Proof.context -> term -> thm 36 val inductive_forall_def: thm 37 val rulify: Proof.context -> thm -> thm 38 val inductive_cases: (Attrib.binding * term list) list -> local_theory -> 39 (string * thm list) list * local_theory 40 val inductive_cases_cmd: (Attrib.binding * string list) list -> local_theory -> 41 (string * thm list) list * local_theory 42 val ind_cases_rules: Proof.context -> 43 string list -> (binding * string option * mixfix) list -> thm list 44 val inductive_simps: (Attrib.binding * term list) list -> local_theory -> 45 (string * thm list) list * local_theory 46 val inductive_simps_cmd: (Attrib.binding * string list) list -> local_theory -> 47 (string * thm list) list * local_theory 48 type flags = 49 {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, 50 no_elim: bool, no_ind: bool, skip_mono: bool} 51 val add_inductive: 52 flags -> ((binding * typ) * mixfix) list -> 53 (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> 54 result * local_theory 55 val add_inductive_cmd: bool -> bool -> 56 (binding * string option * mixfix) list -> 57 (binding * string option * mixfix) list -> 58 Specification.multi_specs_cmd -> 59 (Facts.ref * Token.src list) list -> 60 local_theory -> result * local_theory 61 val arities_of: thm -> (string * int) list 62 val params_of: thm -> term list 63 val partition_rules: thm -> thm list -> (string * thm list) list 64 val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list 65 val unpartition_rules: thm list -> (string * 'a list) list -> 'a list 66 val infer_intro_vars: theory -> thm -> int -> thm list -> term list list 67 val inductive_internals: bool Config.T 68 val select_disj_tac: Proof.context -> int -> int -> int -> tactic 69 type add_ind_def = 70 flags -> 71 term list -> (Attrib.binding * term) list -> thm list -> 72 term list -> (binding * mixfix) list -> 73 local_theory -> result * local_theory 74 val declare_rules: binding -> bool -> bool -> binding -> string list -> term list -> 75 thm list -> binding list -> Token.src list list -> (thm * string list * int) list -> 76 thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory 77 val add_ind_def: add_ind_def 78 val gen_add_inductive: add_ind_def -> flags -> 79 ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> 80 thm list -> local_theory -> result * local_theory 81 val gen_add_inductive_cmd: add_ind_def -> bool -> bool -> 82 (binding * string option * mixfix) list -> 83 (binding * string option * mixfix) list -> 84 Specification.multi_specs_cmd -> (Facts.ref * Token.src list) list -> 85 local_theory -> result * local_theory 86 val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser 87end; 88 89structure Inductive: INDUCTIVE = 90struct 91 92(** theory context references **) 93 94val inductive_forall_def = @{thm HOL.induct_forall_def}; 95val inductive_conj_def = @{thm HOL.induct_conj_def}; 96val inductive_conj = @{thms induct_conj}; 97val inductive_atomize = @{thms induct_atomize}; 98val inductive_rulify = @{thms induct_rulify}; 99val inductive_rulify_fallback = @{thms induct_rulify_fallback}; 100 101val simp_thms1 = 102 map mk_meta_eq 103 @{lemma "(\<not> True) = False" "(\<not> False) = True" 104 "(True \<longrightarrow> P) = P" "(False \<longrightarrow> P) = True" 105 "(P \<and> True) = P" "(True \<and> P) = P" 106 by (fact simp_thms)+}; 107 108val simp_thms2 = 109 map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms1; 110 111val simp_thms3 = 112 @{thms le_rel_bool_arg_iff if_False if_True conj_ac 113 le_fun_def le_bool_def sup_fun_def sup_bool_def simp_thms 114 if_bool_eq_disj all_simps ex_simps imp_conjL}; 115 116 117 118(** misc utilities **) 119 120val inductive_internals = Attrib.setup_config_bool \<^binding>\<open>inductive_internals\<close> (K false); 121 122fun message quiet_mode s = if quiet_mode then () else writeln s; 123 124fun clean_message ctxt quiet_mode s = 125 if Config.get ctxt quick_and_dirty then () else message quiet_mode s; 126 127fun coind_prefix true = "co" 128 | coind_prefix false = ""; 129 130fun log (b: int) m n = if m >= n then 0 else 1 + log b (b * m) n; 131 132fun make_bool_args f g [] i = [] 133 | make_bool_args f g (x :: xs) i = 134 (if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2); 135 136fun make_bool_args' xs = 137 make_bool_args (K \<^term>\<open>False\<close>) (K \<^term>\<open>True\<close>) xs; 138 139fun arg_types_of k c = drop k (binder_types (fastype_of c)); 140 141fun find_arg T x [] = raise Fail "find_arg" 142 | find_arg T x ((p as (_, (SOME _, _))) :: ps) = 143 apsnd (cons p) (find_arg T x ps) 144 | find_arg T x ((p as (U, (NONE, y))) :: ps) = 145 if (T: typ) = U then (y, (U, (SOME x, y)) :: ps) 146 else apsnd (cons p) (find_arg T x ps); 147 148fun make_args Ts xs = 149 map (fn (T, (NONE, ())) => Const (\<^const_name>\<open>undefined\<close>, T) | (_, (SOME t, ())) => t) 150 (fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts)); 151 152fun make_args' Ts xs Us = 153 fst (fold_map (fn T => find_arg T ()) Us (Ts ~~ map (pair NONE) xs)); 154 155fun dest_predicate cs params t = 156 let 157 val k = length params; 158 val (c, ts) = strip_comb t; 159 val (xs, ys) = chop k ts; 160 val i = find_index (fn c' => c' = c) cs; 161 in 162 if xs = params andalso i >= 0 then 163 SOME (c, i, ys, chop (length ys) (arg_types_of k c)) 164 else NONE 165 end; 166 167fun mk_names a 0 = [] 168 | mk_names a 1 = [a] 169 | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n); 170 171fun select_disj_tac ctxt = 172 let 173 fun tacs 1 1 = [] 174 | tacs _ 1 = [resolve_tac ctxt @{thms disjI1}] 175 | tacs n i = resolve_tac ctxt @{thms disjI2} :: tacs (n - 1) (i - 1); 176 in fn n => fn i => EVERY' (tacs n i) end; 177 178 179 180(** context data **) 181 182type result = 183 {preds: term list, elims: thm list, raw_induct: thm, 184 induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}; 185 186fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} = 187 let 188 val term = Morphism.term phi; 189 val thm = Morphism.thm phi; 190 val fact = Morphism.fact phi; 191 in 192 {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, 193 induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs} 194 end; 195 196type info = {names: string list, coind: bool} * result; 197 198val empty_infos = 199 Item_Net.init (op = o apply2 (#names o fst)) (#preds o snd) 200 201val empty_equations = 202 Item_Net.init Thm.eq_thm_prop 203 (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of); 204 205datatype data = Data of 206 {infos: info Item_Net.T, 207 monos: thm list, 208 equations: thm Item_Net.T}; 209 210fun make_data (infos, monos, equations) = 211 Data {infos = infos, monos = monos, equations = equations}; 212 213structure Data = Generic_Data 214( 215 type T = data; 216 val empty = make_data (empty_infos, [], empty_equations); 217 val extend = I; 218 fun merge (Data {infos = infos1, monos = monos1, equations = equations1}, 219 Data {infos = infos2, monos = monos2, equations = equations2}) = 220 make_data (Item_Net.merge (infos1, infos2), 221 Thm.merge_thms (monos1, monos2), 222 Item_Net.merge (equations1, equations2)); 223); 224 225fun map_data f = 226 Data.map (fn Data {infos, monos, equations} => make_data (f (infos, monos, equations))); 227 228fun rep_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data rep => rep); 229 230fun print_inductives verbose ctxt = 231 let 232 val {infos, monos, ...} = rep_data ctxt; 233 val space = Consts.space_of (Proof_Context.consts_of ctxt); 234 val consts = 235 Item_Net.content infos 236 |> maps (fn ({names, ...}, result) => map (rpair result) names) 237 in 238 [Pretty.block 239 (Pretty.breaks 240 (Pretty.str "(co)inductives:" :: 241 map (Pretty.mark_str o #1) 242 (Name_Space.markup_entries verbose ctxt space consts))), 243 Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)] 244 end |> Pretty.writeln_chunks; 245 246 247(* inductive info *) 248 249fun the_inductive ctxt term = 250 Item_Net.retrieve (#infos (rep_data ctxt)) term 251 |> the_single 252 |> apsnd (transform_result (Morphism.transfer_morphism' ctxt)) 253 254fun the_inductive_global ctxt name = 255 #infos (rep_data ctxt) 256 |> Item_Net.content 257 |> filter (fn ({names, ...}, _) => member op = names name) 258 |> the_single 259 |> apsnd (transform_result (Morphism.transfer_morphism' ctxt)) 260 261fun put_inductives info = 262 map_data (fn (infos, monos, equations) => 263 (Item_Net.update (apsnd (transform_result Morphism.trim_context_morphism) info) infos, 264 monos, equations)); 265 266 267(* monotonicity rules *) 268 269fun get_monos ctxt = 270 #monos (rep_data ctxt) 271 |> map (Thm.transfer' ctxt); 272 273fun mk_mono ctxt thm = 274 let 275 fun eq_to_mono thm' = thm' RS (thm' RS @{thm eq_to_mono}); 276 fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD}) 277 handle THM _ => thm RS @{thm le_boolD} 278 in 279 (case Thm.concl_of thm of 280 Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => eq_to_mono (HOLogic.mk_obj_eq thm) 281 | _ $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => eq_to_mono thm 282 | _ $ (Const (\<^const_name>\<open>Orderings.less_eq\<close>, _) $ _ $ _) => 283 dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL 284 (resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}])) thm)) 285 | _ => thm) 286 end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Thm.string_of_thm ctxt thm); 287 288val mono_add = 289 Thm.declaration_attribute (fn thm => fn context => 290 map_data (fn (infos, monos, equations) => 291 (infos, Thm.add_thm (Thm.trim_context (mk_mono (Context.proof_of context) thm)) monos, 292 equations)) context); 293 294val mono_del = 295 Thm.declaration_attribute (fn thm => fn context => 296 map_data (fn (infos, monos, equations) => 297 (infos, Thm.del_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context); 298 299val _ = 300 Theory.setup 301 (Attrib.setup \<^binding>\<open>mono\<close> (Attrib.add_del mono_add mono_del) 302 "declaration of monotonicity rule"); 303 304 305(* equations *) 306 307fun retrieve_equations ctxt = 308 Item_Net.retrieve (#equations (rep_data ctxt)) 309 #> map (Thm.transfer' ctxt); 310 311val equation_add_permissive = 312 Thm.declaration_attribute (fn thm => 313 map_data (fn (infos, monos, equations) => 314 (infos, monos, perhaps (try (Item_Net.update (Thm.trim_context thm))) equations))); 315 316 317 318(** process rules **) 319 320local 321 322fun err_in_rule ctxt name t msg = 323 error (cat_lines ["Ill-formed introduction rule " ^ Binding.print name, 324 Syntax.string_of_term ctxt t, msg]); 325 326fun err_in_prem ctxt name t p msg = 327 error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p, 328 "in introduction rule " ^ Binding.print name, Syntax.string_of_term ctxt t, msg]); 329 330val bad_concl = "Conclusion of introduction rule must be an inductive predicate"; 331 332val bad_ind_occ = "Inductive predicate occurs in argument of inductive predicate"; 333 334val bad_app = "Inductive predicate must be applied to parameter(s) "; 335 336fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize []; 337 338in 339 340fun check_rule ctxt cs params ((binding, att), rule) = 341 let 342 val params' = Term.variant_frees rule (Logic.strip_params rule); 343 val frees = rev (map Free params'); 344 val concl = subst_bounds (frees, Logic.strip_assums_concl rule); 345 val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule); 346 val rule' = Logic.list_implies (prems, concl); 347 val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems; 348 val arule = fold_rev (Logic.all o Free) params' (Logic.list_implies (aprems, concl)); 349 350 fun check_ind err t = 351 (case dest_predicate cs params t of 352 NONE => err (bad_app ^ 353 commas (map (Syntax.string_of_term ctxt) params)) 354 | SOME (_, _, ys, _) => 355 if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs 356 then err bad_ind_occ else ()); 357 358 fun check_prem' prem t = 359 if member (op =) cs (head_of t) then 360 check_ind (err_in_prem ctxt binding rule prem) t 361 else 362 (case t of 363 Abs (_, _, t) => check_prem' prem t 364 | t $ u => (check_prem' prem t; check_prem' prem u) 365 | _ => ()); 366 367 fun check_prem (prem, aprem) = 368 if can HOLogic.dest_Trueprop aprem then check_prem' prem prem 369 else err_in_prem ctxt binding rule prem "Non-atomic premise"; 370 371 val _ = 372 (case concl of 373 Const (\<^const_name>\<open>Trueprop\<close>, _) $ t => 374 if member (op =) cs (head_of t) then 375 (check_ind (err_in_rule ctxt binding rule') t; 376 List.app check_prem (prems ~~ aprems)) 377 else err_in_rule ctxt binding rule' bad_concl 378 | _ => err_in_rule ctxt binding rule' bad_concl); 379 in 380 ((binding, att), arule) 381 end; 382 383fun rulify ctxt = 384 hol_simplify ctxt inductive_conj 385 #> hol_simplify ctxt inductive_rulify 386 #> hol_simplify ctxt inductive_rulify_fallback 387 #> Simplifier.norm_hhf ctxt; 388 389end; 390 391 392 393(** proofs for (co)inductive predicates **) 394 395(* prove monotonicity *) 396 397fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt = 398 (message (quiet_mode orelse skip_mono andalso Config.get ctxt quick_and_dirty) 399 " Proving monotonicity ..."; 400 (if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt 401 [] [] 402 (HOLogic.mk_Trueprop 403 (Const (\<^const_name>\<open>Orderings.mono\<close>, (predT --> predT) --> HOLogic.boolT) $ fp_fun)) 404 (fn _ => EVERY [resolve_tac ctxt @{thms monoI} 1, 405 REPEAT (resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}] 1), 406 REPEAT (FIRST 407 [assume_tac ctxt 1, 408 resolve_tac ctxt (map (mk_mono ctxt) monos @ get_monos ctxt) 1, 409 eresolve_tac ctxt @{thms le_funE} 1, 410 dresolve_tac ctxt @{thms le_boolD} 1])])); 411 412 413(* prove introduction rules *) 414 415fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' = 416 let 417 val _ = clean_message ctxt quiet_mode " Proving the introduction rules ..."; 418 419 val unfold = funpow k (fn th => th RS fun_cong) 420 (mono RS (fp_def RS 421 (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold}))); 422 423 val rules = [refl, TrueI, @{lemma "\<not> False" by (rule notI)}, exI, conjI]; 424 425 val intrs = map_index (fn (i, intr) => 426 Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY 427 [rewrite_goals_tac ctxt rec_preds_defs, 428 resolve_tac ctxt [unfold RS iffD2] 1, 429 select_disj_tac ctxt (length intr_ts) (i + 1) 1, 430 (*Not ares_tac, since refl must be tried before any equality assumptions; 431 backtracking may occur if the premises have extra variables!*) 432 DEPTH_SOLVE_1 (resolve_tac ctxt rules 1 APPEND assume_tac ctxt 1)]) 433 |> singleton (Proof_Context.export ctxt ctxt')) intr_ts 434 435 in (intrs, unfold) end; 436 437 438(* prove elimination rules *) 439 440fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' = 441 let 442 val _ = clean_message ctxt quiet_mode " Proving the elimination rules ..."; 443 444 val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt; 445 val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); 446 447 fun dest_intr r = 448 (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))), 449 Logic.strip_assums_hyp r, Logic.strip_params r); 450 451 val intrs = map dest_intr intr_ts ~~ intr_names; 452 453 val rules1 = [disjE, exE, FalseE]; 454 val rules2 = [conjE, FalseE, @{lemma "\<not> True \<Longrightarrow> R" by (rule notE [OF _ TrueI])}]; 455 456 fun prove_elim c = 457 let 458 val Ts = arg_types_of (length params) c; 459 val (anames, ctxt'') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt'; 460 val frees = map Free (anames ~~ Ts); 461 462 fun mk_elim_prem ((_, _, us, _), ts, params') = 463 Logic.list_all (params', 464 Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq) 465 (frees ~~ us) @ ts, P)); 466 val c_intrs = filter (equal c o #1 o #1 o #1) intrs; 467 val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) :: 468 map mk_elim_prem (map #1 c_intrs) 469 in 470 (Goal.prove_sorry ctxt'' [] prems P 471 (fn {context = ctxt4, prems} => EVERY 472 [cut_tac (hd prems) 1, 473 rewrite_goals_tac ctxt4 rec_preds_defs, 474 dresolve_tac ctxt4 [unfold RS iffD1] 1, 475 REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules1)), 476 REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules2)), 477 EVERY (map (fn prem => 478 DEPTH_SOLVE_1 (assume_tac ctxt4 1 ORELSE 479 resolve_tac ctxt [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1)) 480 (tl prems))]) 481 |> singleton (Proof_Context.export ctxt'' ctxt'''), 482 map #2 c_intrs, length Ts) 483 end 484 485 in map prove_elim cs end; 486 487 488(* prove simplification equations *) 489 490fun prove_eqs quiet_mode cs params intr_ts intrs 491 (elims: (thm * bstring list * int) list) ctxt ctxt'' = (* FIXME ctxt'' ?? *) 492 let 493 val _ = clean_message ctxt quiet_mode " Proving the simplification rules ..."; 494 495 fun dest_intr r = 496 (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))), 497 Logic.strip_assums_hyp r, Logic.strip_params r); 498 val intr_ts' = map dest_intr intr_ts; 499 500 fun prove_eq c (elim: thm * 'a * 'b) = 501 let 502 val Ts = arg_types_of (length params) c; 503 val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt; 504 val frees = map Free (anames ~~ Ts); 505 val c_intrs = filter (equal c o #1 o #1 o #1) (intr_ts' ~~ intrs); 506 fun mk_intr_conj (((_, _, us, _), ts, params'), _) = 507 let 508 fun list_ex ([], t) = t 509 | list_ex ((a, T) :: vars, t) = 510 HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t)); 511 val conjs = map2 (curry HOLogic.mk_eq) frees us @ map HOLogic.dest_Trueprop ts; 512 in 513 list_ex (params', if null conjs then \<^term>\<open>True\<close> else foldr1 HOLogic.mk_conj conjs) 514 end; 515 val lhs = list_comb (c, params @ frees); 516 val rhs = 517 if null c_intrs then \<^term>\<open>False\<close> 518 else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs); 519 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 520 fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} => 521 select_disj_tac ctxt'' (length c_intrs) (i + 1) 1 THEN 522 EVERY (replicate (length params) (resolve_tac ctxt'' @{thms exI} 1)) THEN 523 (if null prems then resolve_tac ctxt'' @{thms TrueI} 1 524 else 525 let 526 val (prems', last_prem) = split_last prems; 527 in 528 EVERY (map (fn prem => 529 (resolve_tac ctxt'' @{thms conjI} 1 THEN resolve_tac ctxt'' [prem] 1)) prems') 530 THEN resolve_tac ctxt'' [last_prem] 1 531 end)) ctxt' 1; 532 fun prove_intr2 (((_, _, us, _), ts, params'), intr) = 533 EVERY (replicate (length params') (eresolve_tac ctxt' @{thms exE} 1)) THEN 534 (if null ts andalso null us then resolve_tac ctxt' [intr] 1 535 else 536 EVERY (replicate (length ts + length us - 1) (eresolve_tac ctxt' @{thms conjE} 1)) THEN 537 Subgoal.FOCUS_PREMS (fn {context = ctxt'', prems, ...} => 538 let 539 val (eqs, prems') = chop (length us) prems; 540 val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs; 541 in 542 rewrite_goal_tac ctxt'' rew_thms 1 THEN 543 resolve_tac ctxt'' [intr] 1 THEN 544 EVERY (map (fn p => resolve_tac ctxt'' [p] 1) prems') 545 end) ctxt' 1); 546 in 547 Goal.prove_sorry ctxt' [] [] eq (fn _ => 548 resolve_tac ctxt' @{thms iffI} 1 THEN 549 eresolve_tac ctxt' [#1 elim] 1 THEN 550 EVERY (map_index prove_intr1 c_intrs) THEN 551 (if null c_intrs then eresolve_tac ctxt' @{thms FalseE} 1 552 else 553 let val (c_intrs', last_c_intr) = split_last c_intrs in 554 EVERY (map (fn ci => eresolve_tac ctxt' @{thms disjE} 1 THEN prove_intr2 ci) c_intrs') 555 THEN prove_intr2 last_c_intr 556 end)) 557 |> rulify ctxt' 558 |> singleton (Proof_Context.export ctxt' ctxt'') 559 end; 560 in 561 map2 prove_eq cs elims 562 end; 563 564 565(* derivation of simplified elimination rules *) 566 567local 568 569(*delete needless equality assumptions*) 570val refl_thin = Goal.prove_global \<^theory>\<open>HOL\<close> [] [] \<^prop>\<open>\<And>P. a = a \<Longrightarrow> P \<Longrightarrow> P\<close> 571 (fn {context = ctxt, ...} => assume_tac ctxt 1); 572val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; 573fun elim_tac ctxt = REPEAT o eresolve_tac ctxt elim_rls; 574 575fun simp_case_tac ctxt i = 576 EVERY' [elim_tac ctxt, 577 asm_full_simp_tac ctxt, 578 elim_tac ctxt, 579 REPEAT o bound_hyp_subst_tac ctxt] i; 580 581in 582 583fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac ctxt; 584 585fun mk_cases ctxt prop = 586 let 587 fun err msg = 588 error (Pretty.string_of (Pretty.block 589 [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop])); 590 591 val elims = Induct.find_casesP ctxt prop; 592 593 val cprop = Thm.cterm_of ctxt prop; 594 fun mk_elim rl = 595 Thm.implies_intr cprop 596 (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl)) 597 |> singleton (Proof_Context.export (Proof_Context.augment prop ctxt) ctxt); 598 in 599 (case get_first (try mk_elim) elims of 600 SOME r => r 601 | NONE => err "Proposition not an inductive predicate:") 602 end; 603 604end; 605 606 607(* inductive_cases *) 608 609fun gen_inductive_cases prep_att prep_prop args lthy = 610 let 611 val thmss = 612 map snd args 613 |> burrow (grouped 10 Par_List.map_independent (mk_cases lthy o prep_prop lthy)); 614 val facts = 615 map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])])) 616 args thmss; 617 in lthy |> Local_Theory.notes facts end; 618 619val inductive_cases = gen_inductive_cases (K I) Syntax.check_prop; 620val inductive_cases_cmd = gen_inductive_cases Attrib.check_src Syntax.read_prop; 621 622 623(* ind_cases *) 624 625fun ind_cases_rules ctxt raw_props raw_fixes = 626 let 627 val (props, ctxt') = Specification.read_props raw_props raw_fixes ctxt; 628 val rules = Proof_Context.export ctxt' ctxt (map (mk_cases ctxt') props); 629 in rules end; 630 631val _ = 632 Theory.setup 633 (Method.setup \<^binding>\<open>ind_cases\<close> 634 (Scan.lift (Scan.repeat1 Parse.prop -- Parse.for_fixes) >> 635 (fn (props, fixes) => fn ctxt => 636 Method.erule ctxt 0 (ind_cases_rules ctxt props fixes))) 637 "case analysis for inductive definitions, based on simplified elimination rule"); 638 639 640(* derivation of simplified equation *) 641 642fun mk_simp_eq ctxt prop = 643 let 644 val thy = Proof_Context.theory_of ctxt; 645 val ctxt' = Proof_Context.augment prop ctxt; 646 val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of; 647 val substs = 648 retrieve_equations ctxt (HOLogic.dest_Trueprop prop) 649 |> map_filter 650 (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop) 651 (Vartab.empty, Vartab.empty), eq) 652 handle Pattern.MATCH => NONE); 653 val (subst, eq) = 654 (case substs of 655 [s] => s 656 | _ => error 657 ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique")); 658 val inst = 659 map (fn v => (fst v, Thm.cterm_of ctxt' (Envir.subst_term subst (Var v)))) 660 (Term.add_vars (lhs_of eq) []); 661 in 662 infer_instantiate ctxt' inst eq 663 |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt'))) 664 |> singleton (Proof_Context.export ctxt' ctxt) 665 end 666 667 668(* inductive simps *) 669 670fun gen_inductive_simps prep_att prep_prop args lthy = 671 let 672 val facts = args |> map (fn ((a, atts), props) => 673 ((a, map (prep_att lthy) atts), 674 map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props)); 675 in lthy |> Local_Theory.notes facts end; 676 677val inductive_simps = gen_inductive_simps (K I) Syntax.check_prop; 678val inductive_simps_cmd = gen_inductive_simps Attrib.check_src Syntax.read_prop; 679 680 681(* prove induction rule *) 682 683fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono 684 fp_def rec_preds_defs ctxt ctxt''' = (* FIXME ctxt''' ?? *) 685 let 686 val _ = clean_message ctxt quiet_mode " Proving the induction rule ..."; 687 688 (* predicates for induction rule *) 689 690 val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt; 691 val preds = 692 map2 (curry Free) pnames 693 (map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs); 694 695 (* transform an introduction rule into a premise for induction rule *) 696 697 fun mk_ind_prem r = 698 let 699 fun subst s = 700 (case dest_predicate cs params s of 701 SOME (_, i, ys, (_, Ts)) => 702 let 703 val k = length Ts; 704 val bs = map Bound (k - 1 downto 0); 705 val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs); 706 val Q = 707 fold_rev Term.abs (mk_names "x" k ~~ Ts) 708 (HOLogic.mk_binop \<^const_name>\<open>HOL.induct_conj\<close> 709 (list_comb (incr_boundvars k s, bs), P)); 710 in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end 711 | NONE => 712 (case s of 713 t $ u => (fst (subst t) $ fst (subst u), NONE) 714 | Abs (a, T, t) => (Abs (a, T, fst (subst t)), NONE) 715 | _ => (s, NONE))); 716 717 fun mk_prem s prems = 718 (case subst s of 719 (_, SOME (t, u)) => t :: u :: prems 720 | (t, _) => t :: prems); 721 722 val SOME (_, i, ys, _) = 723 dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); 724 in 725 fold_rev (Logic.all o Free) (Logic.strip_params r) 726 (Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem 727 (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []), 728 HOLogic.mk_Trueprop (list_comb (nth preds i, ys)))) 729 end; 730 731 val ind_prems = map mk_ind_prem intr_ts; 732 733 734 (* make conclusions for induction rules *) 735 736 val Tss = map (binder_types o fastype_of) preds; 737 val (xnames, ctxt'') = Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt'; 738 val mutual_ind_concl = 739 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 740 (map (fn (((xnames, Ts), c), P) => 741 let val frees = map Free (xnames ~~ Ts) 742 in HOLogic.mk_imp (list_comb (c, params @ frees), list_comb (P, frees)) end) 743 (unflat Tss xnames ~~ Tss ~~ cs ~~ preds))); 744 745 746 (* make predicate for instantiation of abstract induction rule *) 747 748 val ind_pred = 749 fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj 750 (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp) 751 (make_bool_args HOLogic.mk_not I bs i) 752 (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds)); 753 754 val ind_concl = 755 HOLogic.mk_Trueprop 756 (HOLogic.mk_binrel \<^const_name>\<open>Orderings.less_eq\<close> (rec_const, ind_pred)); 757 758 val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct}); 759 760 val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl 761 (fn {context = ctxt3, prems} => EVERY 762 [rewrite_goals_tac ctxt3 [inductive_conj_def], 763 DETERM (resolve_tac ctxt3 [raw_fp_induct] 1), 764 REPEAT (resolve_tac ctxt3 [@{thm le_funI}, @{thm le_boolI}] 1), 765 rewrite_goals_tac ctxt3 simp_thms2, 766 (*This disjE separates out the introduction rules*) 767 REPEAT (FIRSTGOAL (eresolve_tac ctxt3 [disjE, exE, FalseE])), 768 (*Now break down the individual cases. No disjE here in case 769 some premise involves disjunction.*) 770 REPEAT (FIRSTGOAL (eresolve_tac ctxt3 [conjE] ORELSE' bound_hyp_subst_tac ctxt3)), 771 REPEAT (FIRSTGOAL 772 (resolve_tac ctxt3 [conjI, impI] ORELSE' 773 (eresolve_tac ctxt3 [notE] THEN' assume_tac ctxt3))), 774 EVERY (map (fn prem => 775 DEPTH_SOLVE_1 (assume_tac ctxt3 1 ORELSE 776 resolve_tac ctxt3 777 [rewrite_rule ctxt3 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem, 778 conjI, refl] 1)) prems)]); 779 780 val lemma = Goal.prove_sorry ctxt'' [] [] 781 (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY 782 [rewrite_goals_tac ctxt3 rec_preds_defs, 783 REPEAT (EVERY 784 [REPEAT (resolve_tac ctxt3 [conjI, impI] 1), 785 REPEAT (eresolve_tac ctxt3 [@{thm le_funE}, @{thm le_boolE}] 1), 786 assume_tac ctxt3 1, 787 rewrite_goals_tac ctxt3 simp_thms1, 788 assume_tac ctxt3 1])]); 789 790 in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end; 791 792(* prove coinduction rule *) 793 794fun If_const T = Const (\<^const_name>\<open>If\<close>, HOLogic.boolT --> T --> T --> T); 795fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end; 796 797fun prove_coindrule quiet_mode preds cs argTs bs xs params intr_ts mono 798 fp_def rec_preds_defs ctxt ctxt''' = (* FIXME ctxt''' ?? *) 799 let 800 val _ = clean_message ctxt quiet_mode " Proving the coinduction rule ..."; 801 val n = length cs; 802 val (ns, xss) = map_split (fn pred => 803 make_args' argTs xs (arg_types_of (length params) pred) |> `length) preds; 804 val xTss = map (map fastype_of) xss; 805 val (Rs_names, names_ctxt) = Variable.variant_fixes (mk_names "X" n) ctxt; 806 val Rs = map2 (fn name => fn Ts => Free (name, Ts ---> \<^typ>\<open>bool\<close>)) Rs_names xTss; 807 val Rs_applied = map2 (curry list_comb) Rs xss; 808 val preds_applied = map2 (curry list_comb) (map (fn p => list_comb (p, params)) preds) xss; 809 val abstract_list = fold_rev (absfree o dest_Free); 810 val bss = map (make_bool_args 811 (fn b => HOLogic.mk_eq (b, \<^term>\<open>False\<close>)) 812 (fn b => HOLogic.mk_eq (b, \<^term>\<open>True\<close>)) bs) (0 upto n - 1); 813 val eq_undefinedss = map (fn ys => map (fn x => 814 HOLogic.mk_eq (x, Const (\<^const_name>\<open>undefined\<close>, fastype_of x))) 815 (subtract (op =) ys xs)) xss; 816 val R = 817 @{fold 3} (fn bs => fn eqs => fn R => fn t => if null bs andalso null eqs then R else 818 mk_If (Library.foldr1 HOLogic.mk_conj (bs @ eqs)) R t) 819 bss eq_undefinedss Rs_applied \<^term>\<open>False\<close> 820 |> abstract_list (bs @ xs); 821 822 fun subst t = 823 (case dest_predicate cs params t of 824 SOME (_, i, ts, (_, Us)) => 825 let 826 val l = length Us; 827 val bs = map Bound (l - 1 downto 0); 828 val args = map (incr_boundvars l) ts @ bs 829 in 830 HOLogic.mk_disj (list_comb (nth Rs i, args), 831 list_comb (nth preds i, params @ args)) 832 |> fold_rev absdummy Us 833 end 834 | NONE => 835 (case t of 836 t1 $ t2 => subst t1 $ subst t2 837 | Abs (x, T, u) => Abs (x, T, subst u) 838 | _ => t)); 839 840 fun mk_coind_prem r = 841 let 842 val SOME (_, i, ts, (Ts, _)) = 843 dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); 844 val ps = 845 map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @ 846 map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r); 847 in 848 (i, fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P)) 849 (Logic.strip_params r) 850 (if null ps then \<^term>\<open>True\<close> else foldr1 HOLogic.mk_conj ps)) 851 end; 852 853 fun mk_prem i Ps = Logic.mk_implies 854 ((nth Rs_applied i, Library.foldr1 HOLogic.mk_disj Ps) |> @{apply 2} HOLogic.mk_Trueprop) 855 |> fold_rev Logic.all (nth xss i); 856 857 val prems = map mk_coind_prem intr_ts |> AList.group (op =) |> sort (int_ord o apply2 fst) 858 |> map (uncurry mk_prem); 859 860 val concl = @{map 3} (fn xs => 861 Ctr_Sugar_Util.list_all_free xs oo curry HOLogic.mk_imp) xss Rs_applied preds_applied 862 |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop; 863 864 865 val pred_defs_sym = if null rec_preds_defs then [] else map2 (fn n => fn thm => 866 funpow n (fn thm => thm RS @{thm meta_fun_cong}) thm RS @{thm Pure.symmetric}) 867 ns rec_preds_defs; 868 val simps = simp_thms3 @ pred_defs_sym; 869 val simprocs = [Simplifier.the_simproc ctxt "HOL.defined_All"]; 870 val simplify = asm_full_simplify (Ctr_Sugar_Util.ss_only simps ctxt addsimprocs simprocs); 871 val coind = (mono RS (fp_def RS @{thm def_coinduct})) 872 |> infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt R)] 873 |> simplify; 874 fun idx_of t = find_index (fn R => 875 R = the_single (subtract (op =) (preds @ params) (map Free (Term.add_frees t [])))) Rs; 876 val coind_concls = HOLogic.dest_Trueprop (Thm.concl_of coind) |> HOLogic.dest_conj 877 |> map (fn t => (idx_of t, t)) |> sort (int_ord o @{apply 2} fst) |> map snd; 878 val reorder_bound_goals = map_filter (fn (t, u) => if t aconv u then NONE else 879 SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))) 880 ((HOLogic.dest_Trueprop concl |> HOLogic.dest_conj) ~~ coind_concls); 881 val reorder_bound_thms = map (fn goal => Goal.prove_sorry ctxt [] [] goal 882 (fn {context = ctxt, prems = _} => 883 HEADGOAL (EVERY' [resolve_tac ctxt [iffI], 884 REPEAT_DETERM o resolve_tac ctxt [allI, impI], 885 REPEAT_DETERM o dresolve_tac ctxt [spec], eresolve_tac ctxt [mp], assume_tac ctxt, 886 REPEAT_DETERM o resolve_tac ctxt [allI, impI], 887 REPEAT_DETERM o dresolve_tac ctxt [spec], eresolve_tac ctxt [mp], assume_tac ctxt]))) 888 reorder_bound_goals; 889 val coinduction = Goal.prove_sorry ctxt [] prems concl (fn {context = ctxt, prems = CIH} => 890 HEADGOAL (full_simp_tac 891 (Ctr_Sugar_Util.ss_only (simps @ reorder_bound_thms) ctxt addsimprocs simprocs) THEN' 892 resolve_tac ctxt [coind]) THEN 893 ALLGOALS (REPEAT_ALL_NEW (REPEAT_DETERM o resolve_tac ctxt [allI, impI, conjI] THEN' 894 REPEAT_DETERM o eresolve_tac ctxt [exE, conjE] THEN' 895 dresolve_tac ctxt (map simplify CIH) THEN' 896 REPEAT_DETERM o (assume_tac ctxt ORELSE' 897 eresolve_tac ctxt [conjE] ORELSE' dresolve_tac ctxt [spec, mp])))) 898 in 899 coinduction 900 |> length cs = 1 ? (Object_Logic.rulify ctxt #> rotate_prems ~1) 901 |> singleton (Proof_Context.export names_ctxt ctxt''') 902 end 903 904 905 906 907(** specification of (co)inductive predicates **) 908 909fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy = 910 let 911 val fp_name = if coind then \<^const_name>\<open>Inductive.gfp\<close> else \<^const_name>\<open>Inductive.lfp\<close>; 912 913 val argTs = fold (combine (op =) o arg_types_of (length params)) cs []; 914 val k = log 2 1 (length cs); 915 val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT; 916 val p :: xs = 917 map Free (Variable.variant_frees lthy intr_ts 918 (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs))); 919 val bs = 920 map Free (Variable.variant_frees lthy (p :: xs @ intr_ts) 921 (map (rpair HOLogic.boolT) (mk_names "b" k))); 922 923 fun subst t = 924 (case dest_predicate cs params t of 925 SOME (_, i, ts, (Ts, Us)) => 926 let 927 val l = length Us; 928 val zs = map Bound (l - 1 downto 0); 929 in 930 fold_rev (Term.abs o pair "z") Us 931 (list_comb (p, 932 make_bool_args' bs i @ make_args argTs 933 ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us)))) 934 end 935 | NONE => 936 (case t of 937 t1 $ t2 => subst t1 $ subst t2 938 | Abs (x, T, u) => Abs (x, T, subst u) 939 | _ => t)); 940 941 (* transform an introduction rule into a conjunction *) 942 (* [| p_i t; ... |] ==> p_j u *) 943 (* is transformed into *) 944 (* b_j & x_j = u & p b_j t & ... *) 945 946 fun transform_rule r = 947 let 948 val SOME (_, i, ts, (Ts, _)) = 949 dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); 950 val ps = 951 make_bool_args HOLogic.mk_not I bs i @ 952 map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @ 953 map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r); 954 in 955 fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P)) 956 (Logic.strip_params r) 957 (if null ps then \<^term>\<open>True\<close> else foldr1 HOLogic.mk_conj ps) 958 end; 959 960 (* make a disjunction of all introduction rules *) 961 962 val fp_fun = 963 fold_rev lambda (p :: bs @ xs) 964 (if null intr_ts then \<^term>\<open>False\<close> 965 else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)); 966 967 (* add definition of recursive predicates to theory *) 968 969 val is_auxiliary = length cs > 1; 970 971 val rec_binding = 972 if Binding.is_empty alt_name then Binding.conglomerate (map #1 cnames_syn) else alt_name; 973 val rec_name = Binding.name_of rec_binding; 974 975 val internals = Config.get lthy inductive_internals; 976 977 val ((rec_const, (_, fp_def)), lthy') = lthy 978 |> is_auxiliary ? Proof_Context.concealed 979 |> Local_Theory.define 980 ((rec_binding, case cnames_syn of [(_, mx)] => mx | _ => NoSyn), 981 ((Thm.make_def_binding internals rec_binding, @{attributes [nitpick_unfold]}), 982 fold_rev lambda params 983 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) 984 ||> Proof_Context.restore_naming lthy; 985 val fp_def' = 986 Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) 987 (Thm.cterm_of lthy' (list_comb (rec_const, params))); 988 val specs = 989 if is_auxiliary then 990 map_index (fn (i, ((b, mx), c)) => 991 let 992 val Ts = arg_types_of (length params) c; 993 val xs = 994 map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts)); 995 in 996 ((b, mx), 997 ((Thm.make_def_binding internals b, []), fold_rev lambda (params @ xs) 998 (list_comb (rec_const, params @ make_bool_args' bs i @ 999 make_args argTs (xs ~~ Ts))))) 1000 end) (cnames_syn ~~ cs) 1001 else []; 1002 val (consts_defs, lthy'') = lthy' 1003 |> fold_map Local_Theory.define specs; 1004 val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs); 1005 1006 val (_, ctxt'') = Variable.add_fixes (map (fst o dest_Free) params) lthy''; 1007 val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''; 1008 val (_, lthy''') = lthy'' 1009 |> Local_Theory.note 1010 ((if internals 1011 then Binding.qualify true rec_name (Binding.name "mono") 1012 else Binding.empty, []), 1013 Proof_Context.export ctxt'' lthy'' [mono]); 1014 in 1015 (lthy''', Proof_Context.transfer (Proof_Context.theory_of lthy''') ctxt'', 1016 rec_binding, mono, fp_def', map (#2 o #2) consts_defs, 1017 list_comb (rec_const, params), preds, argTs, bs, xs) 1018 end; 1019 1020fun declare_rules rec_binding coind no_ind spec_name cnames 1021 preds intrs intr_bindings intr_atts elims eqs raw_induct lthy = 1022 let 1023 val rec_name = Binding.name_of rec_binding; 1024 fun rec_qualified qualified = Binding.qualify qualified rec_name; 1025 val intr_names = map Binding.name_of intr_bindings; 1026 val ind_case_names = 1027 if forall (equal "") intr_names then [] 1028 else [Attrib.case_names intr_names]; 1029 val induct = 1030 if coind then 1031 (raw_induct, 1032 [Attrib.case_names [rec_name], 1033 Attrib.case_conclusion (rec_name, intr_names), 1034 Attrib.consumes (1 - Thm.nprems_of raw_induct), 1035 Attrib.internal (K (Induct.coinduct_pred (hd cnames)))]) 1036 else if no_ind orelse length cnames > 1 then 1037 (raw_induct, ind_case_names @ [Attrib.consumes (~ (Thm.nprems_of raw_induct))]) 1038 else 1039 (raw_induct RSN (2, rev_mp), 1040 ind_case_names @ [Attrib.consumes (~ (Thm.nprems_of raw_induct))]); 1041 1042 val (intrs', lthy1) = 1043 lthy |> 1044 Spec_Rules.add spec_name 1045 (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) preds intrs |> 1046 Local_Theory.notes 1047 (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ 1048 map (fn th => [([th], @{attributes [Pure.intro?]})]) intrs) |>> 1049 map (hd o snd); 1050 val (((_, elims'), (_, [induct'])), lthy2) = 1051 lthy1 |> 1052 Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> 1053 fold_map (fn (name, (elim, cases, k)) => 1054 Local_Theory.note 1055 ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"), 1056 ((if forall (equal "") cases then [] else [Attrib.case_names cases]) @ 1057 [Attrib.consumes (1 - Thm.nprems_of elim), Attrib.constraints k, 1058 Attrib.internal (K (Induct.cases_pred name))] @ @{attributes [Pure.elim?]})), 1059 [elim]) #> 1060 apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>> 1061 Local_Theory.note 1062 ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), #2 induct), 1063 [rulify lthy1 (#1 induct)]); 1064 1065 val (eqs', lthy3) = lthy2 |> 1066 fold_map (fn (name, eq) => Local_Theory.note 1067 ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), 1068 [Attrib.internal (K equation_add_permissive)]), [eq]) 1069 #> apfst (hd o snd)) 1070 (if null eqs then [] else (cnames ~~ eqs)) 1071 val (inducts, lthy4) = 1072 if no_ind orelse coind then ([], lthy3) 1073 else 1074 let val inducts = cnames ~~ Project_Rule.projects lthy3 (1 upto length cnames) induct' in 1075 lthy3 |> 1076 Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []), 1077 inducts |> map (fn (name, th) => ([th], 1078 ind_case_names @ 1079 [Attrib.consumes (1 - Thm.nprems_of th), 1080 Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd 1081 end; 1082 in (intrs', elims', eqs', induct', inducts, lthy4) end; 1083 1084type flags = 1085 {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, 1086 no_elim: bool, no_ind: bool, skip_mono: bool}; 1087 1088type add_ind_def = 1089 flags -> 1090 term list -> (Attrib.binding * term) list -> thm list -> 1091 term list -> (binding * mixfix) list -> 1092 local_theory -> result * local_theory; 1093 1094fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono} 1095 cs intros monos params cnames_syn lthy = 1096 let 1097 val _ = null cnames_syn andalso error "No inductive predicates given"; 1098 val names = map (Binding.name_of o fst) cnames_syn; 1099 val _ = message (quiet_mode andalso not verbose) 1100 ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names); 1101 1102 val spec_name = Binding.conglomerate (map #1 cnames_syn); 1103 val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn; (* FIXME *) 1104 val ((intr_names, intr_atts), intr_ts) = 1105 apfst split_list (split_list (map (check_rule lthy cs params) intros)); 1106 1107 val (lthy1, lthy2, rec_binding, mono, fp_def, rec_preds_defs, rec_const, preds, 1108 argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts 1109 monos params cnames_syn lthy; 1110 1111 val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs) 1112 intr_ts rec_preds_defs lthy2 lthy1; 1113 val elims = 1114 if no_elim then [] 1115 else 1116 prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names) 1117 unfold rec_preds_defs lthy2 lthy1; 1118 val raw_induct = zero_var_indexes 1119 (if no_ind then Drule.asm_rl 1120 else if coind then 1121 prove_coindrule quiet_mode preds cs argTs bs xs params intr_ts mono fp_def 1122 rec_preds_defs lthy2 lthy1 1123 else 1124 prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def 1125 rec_preds_defs lthy2 lthy1); 1126 1127 val eqs = 1128 if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1; 1129 1130 val elims' = map (fn (th, ns, i) => (rulify lthy1 th, ns, i)) elims; 1131 val intrs' = map (rulify lthy1) intrs; 1132 1133 val (intrs'', elims'', eqs', induct, inducts, lthy3) = 1134 declare_rules rec_binding coind no_ind 1135 spec_name cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1; 1136 1137 val result = 1138 {preds = preds, 1139 intrs = intrs'', 1140 elims = elims'', 1141 raw_induct = rulify lthy3 raw_induct, 1142 induct = induct, 1143 inducts = inducts, 1144 eqs = eqs'}; 1145 1146 val lthy4 = lthy3 1147 |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => 1148 let val result' = transform_result phi result; 1149 in put_inductives ({names = cnames, coind = coind}, result') end); 1150 in (result, lthy4) end; 1151 1152 1153(* external interfaces *) 1154 1155fun gen_add_inductive mk_def 1156 flags cnames_syn pnames spec monos lthy = 1157 let 1158 1159 (* abbrevs *) 1160 1161 val (_, ctxt1) = Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn) lthy; 1162 1163 fun get_abbrev ((name, atts), t) = 1164 if can (Logic.strip_assums_concl #> Logic.dest_equals) t then 1165 let 1166 val _ = Binding.is_empty name andalso null atts orelse 1167 error "Abbreviations may not have names or attributes"; 1168 val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 (K []) t)); 1169 val var = 1170 (case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of 1171 NONE => error ("Undeclared head of abbreviation " ^ quote x) 1172 | SOME ((b, T'), mx) => 1173 if T <> T' then error ("Bad type specification for abbreviation " ^ quote x) 1174 else (b, mx)); 1175 in SOME (var, rhs) end 1176 else NONE; 1177 1178 val abbrevs = map_filter get_abbrev spec; 1179 val bs = map (Binding.name_of o fst o fst) abbrevs; 1180 1181 1182 (* predicates *) 1183 1184 val pre_intros = filter_out (is_some o get_abbrev) spec; 1185 val cnames_syn' = filter_out (member (op =) bs o Binding.name_of o fst o fst) cnames_syn; 1186 val cs = map (Free o apfst Binding.name_of o fst) cnames_syn'; 1187 val ps = map Free pnames; 1188 1189 val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn'); 1190 val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs; 1191 val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy; 1192 1193 fun close_rule r = 1194 fold (Logic.all o Free) (fold_aterms 1195 (fn t as Free (v as (s, _)) => 1196 if Variable.is_fixed ctxt1 s orelse 1197 member (op =) ps t then I else insert (op =) v 1198 | _ => I) r []) r; 1199 1200 val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros; 1201 val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn'; 1202 in 1203 lthy 1204 |> mk_def flags cs intros monos ps preds 1205 ||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs 1206 end; 1207 1208fun gen_add_inductive_cmd mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy = 1209 let 1210 val ((vars, intrs), _) = lthy 1211 |> Proof_Context.set_mode Proof_Context.mode_abbrev 1212 |> Specification.read_multi_specs (cnames_syn @ pnames_syn) intro_srcs; 1213 val (cs, ps) = chop (length cnames_syn) vars; 1214 val monos = Attrib.eval_thms lthy raw_monos; 1215 val flags = 1216 {quiet_mode = false, verbose = verbose, alt_name = Binding.empty, 1217 coind = coind, no_elim = false, no_ind = false, skip_mono = false}; 1218 in 1219 lthy 1220 |> gen_add_inductive mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos 1221 end; 1222 1223val add_inductive = gen_add_inductive add_ind_def; 1224val add_inductive_cmd = gen_add_inductive_cmd add_ind_def; 1225 1226 1227(* read off arities of inductive predicates from raw induction rule *) 1228fun arities_of induct = 1229 map (fn (_ $ t $ u) => 1230 (fst (dest_Const (head_of t)), length (snd (strip_comb u)))) 1231 (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct))); 1232 1233(* read off parameters of inductive predicate from raw induction rule *) 1234fun params_of induct = 1235 let 1236 val (_ $ t $ u :: _) = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct)); 1237 val (_, ts) = strip_comb t; 1238 val (_, us) = strip_comb u; 1239 in 1240 List.take (ts, length ts - length us) 1241 end; 1242 1243val pname_of_intr = 1244 Thm.concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const #> fst; 1245 1246(* partition introduction rules according to predicate name *) 1247fun gen_partition_rules f induct intros = 1248 fold_rev (fn r => AList.map_entry op = (pname_of_intr (f r)) (cons r)) intros 1249 (map (rpair [] o fst) (arities_of induct)); 1250 1251val partition_rules = gen_partition_rules I; 1252fun partition_rules' induct = gen_partition_rules fst induct; 1253 1254fun unpartition_rules intros xs = 1255 fold_map (fn r => AList.map_entry_yield op = (pname_of_intr r) 1256 (fn x :: xs => (x, xs)) #>> the) intros xs |> fst; 1257 1258(* infer order of variables in intro rules from order of quantifiers in elim rule *) 1259fun infer_intro_vars thy elim arity intros = 1260 let 1261 val _ :: cases = Thm.prems_of elim; 1262 val used = map (fst o fst) (Term.add_vars (Thm.prop_of elim) []); 1263 fun mtch (t, u) = 1264 let 1265 val params = Logic.strip_params t; 1266 val vars = 1267 map (Var o apfst (rpair 0)) 1268 (Name.variant_list used (map fst params) ~~ map snd params); 1269 val ts = 1270 map (curry subst_bounds (rev vars)) 1271 (List.drop (Logic.strip_assums_hyp t, arity)); 1272 val us = Logic.strip_imp_prems u; 1273 val tab = 1274 fold (Pattern.first_order_match thy) (ts ~~ us) (Vartab.empty, Vartab.empty); 1275 in 1276 map (Envir.subst_term tab) vars 1277 end 1278 in 1279 map (mtch o apsnd Thm.prop_of) (cases ~~ intros) 1280 end; 1281 1282 1283 1284(** outer syntax **) 1285 1286fun gen_ind_decl mk_def coind = 1287 Parse.vars -- Parse.for_fixes -- 1288 Scan.optional Parse_Spec.where_multi_specs [] -- 1289 Scan.optional (\<^keyword>\<open>monos\<close> |-- Parse.!!! Parse.thms1) [] 1290 >> (fn (((preds, params), specs), monos) => 1291 (snd o gen_add_inductive_cmd mk_def true coind preds params specs monos)); 1292 1293val ind_decl = gen_ind_decl add_ind_def; 1294 1295val _ = 1296 Outer_Syntax.local_theory \<^command_keyword>\<open>inductive\<close> "define inductive predicates" 1297 (ind_decl false); 1298 1299val _ = 1300 Outer_Syntax.local_theory \<^command_keyword>\<open>coinductive\<close> "define coinductive predicates" 1301 (ind_decl true); 1302 1303val _ = 1304 Outer_Syntax.local_theory \<^command_keyword>\<open>inductive_cases\<close> 1305 "create simplified instances of elimination rules" 1306 (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo inductive_cases_cmd)); 1307 1308val _ = 1309 Outer_Syntax.local_theory \<^command_keyword>\<open>inductive_simps\<close> 1310 "create simplification rules for inductive predicates" 1311 (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo inductive_simps_cmd)); 1312 1313val _ = 1314 Outer_Syntax.command \<^command_keyword>\<open>print_inductives\<close> 1315 "print (co)inductive definitions and monotonicity rules" 1316 (Parse.opt_bang >> (fn b => Toplevel.keep (print_inductives b o Toplevel.context_of))); 1317 1318end; 1319