equal
deleted
inserted
replaced
84 val mk_full_horn: (string * typ) list -> term list -> term -> term |
84 val mk_full_horn: (string * typ) list -> term list -> term -> term |
85 |
85 |
86 (* datatype operations *) |
86 (* datatype operations *) |
87 type cns_info = (term * typ * typ list * bool list) list |
87 type cns_info = (term * typ * typ list * bool list) list |
88 |
88 |
89 val all_dtyp_constrs_types: Datatype_Aux.descr -> cns_info list |
89 val all_dtyp_constrs_types: Old_Datatype_Aux.descr -> cns_info list |
90 |
90 |
91 (* tactics for function package *) |
91 (* tactics for function package *) |
92 val size_ss: simpset |
92 val size_ss: simpset |
93 val pat_completeness_simp: thm list -> Proof.context -> tactic |
93 val pat_completeness_simp: thm list -> Proof.context -> tactic |
94 val prove_termination_ind: Proof.context -> int -> tactic |
94 val prove_termination_ind: Proof.context -> int -> tactic |
331 corresponding type and types of arguments *) |
331 corresponding type and types of arguments *) |
332 fun all_dtyp_constrs_types descr = |
332 fun all_dtyp_constrs_types descr = |
333 let |
333 let |
334 fun aux ((ty_name, vs), (cname, args)) = |
334 fun aux ((ty_name, vs), (cname, args)) = |
335 let |
335 let |
336 val vs_tys = map (Datatype_Aux.typ_of_dtyp descr) vs |
336 val vs_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) vs |
337 val ty = Type (ty_name, vs_tys) |
337 val ty = Type (ty_name, vs_tys) |
338 val arg_tys = map (Datatype_Aux.typ_of_dtyp descr) args |
338 val arg_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) args |
339 val is_rec = map Datatype_Aux.is_rec_type args |
339 val is_rec = map Old_Datatype_Aux.is_rec_type args |
340 in |
340 in |
341 (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) |
341 (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) |
342 end |
342 end |
343 in |
343 in |
344 map (map aux) (all_dtyp_constrs_info descr) |
344 map (map aux) (all_dtyp_constrs_info descr) |
449 let |
449 let |
450 val monos = Inductive.get_monos ctxt |
450 val monos = Inductive.get_monos ctxt |
451 val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} |
451 val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} |
452 in |
452 in |
453 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
453 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
454 REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac monos)), |
454 REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)), |
455 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] |
455 REPEAT_DETERM (rtac impI 1 THEN (assume_tac ctxt 1 ORELSE tac))] |
456 end |
456 end |
457 |
457 |
458 fun map_thm ctxt f tac thm = |
458 fun map_thm ctxt f tac thm = |
459 let |
459 let |
460 val opt_goal_trm = map_term f (prop_of thm) |
460 val opt_goal_trm = map_term f (Thm.prop_of thm) |
461 in |
461 in |
462 case opt_goal_trm of |
462 case opt_goal_trm of |
463 NONE => thm |
463 NONE => thm |
464 | SOME goal => |
464 | SOME goal => |
465 Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) |
465 Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) |
493 |
493 |
494 (* transforms a theorem into one of the object logic *) |
494 (* transforms a theorem into one of the object logic *) |
495 fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars; |
495 fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars; |
496 fun atomize_rule ctxt i thm = |
496 fun atomize_rule ctxt i thm = |
497 Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm |
497 Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm |
498 fun atomize_concl ctxt thm = atomize_rule ctxt (length (prems_of thm)) thm |
498 fun atomize_concl ctxt thm = atomize_rule ctxt (length (Thm.prems_of thm)) thm |
499 |
499 |
500 |
500 |
501 (* applies a tactic to a formula composed of conjunctions *) |
501 (* applies a tactic to a formula composed of conjunctions *) |
502 fun conj_tac tac i = |
502 fun conj_tac tac i = |
503 let |
503 let |