29 *) |
29 *) |
30 |
30 |
31 signature INDUCTIVE_PACKAGE = |
31 signature INDUCTIVE_PACKAGE = |
32 sig |
32 sig |
33 val quiet_mode: bool ref |
33 val quiet_mode: bool ref |
|
34 val unify_consts: Sign.sg -> term list -> term list -> term list * term list |
34 val get_inductive: theory -> string -> |
35 val get_inductive: theory -> string -> |
35 {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, |
36 {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, |
36 induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
37 induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
37 val print_inductives: theory -> unit |
38 val print_inductives: theory -> unit |
38 val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> |
39 val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> |
60 |
61 |
61 fun coind_prefix true = "co" |
62 fun coind_prefix true = "co" |
62 | coind_prefix false = ""; |
63 | coind_prefix false = ""; |
63 |
64 |
64 |
65 |
|
66 (* the following code ensures that each recursive set *) |
|
67 (* always has the same type in all introduction rules *) |
|
68 |
|
69 fun unify_consts sign cs intr_ts = |
|
70 (let |
|
71 val {tsig, ...} = Sign.rep_sg sign; |
|
72 val add_term_consts_2 = |
|
73 foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs); |
|
74 fun varify (t, (i, ts)) = |
|
75 let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, [])) |
|
76 in (maxidx_of_term t', t'::ts) end; |
|
77 val (i, cs') = foldr varify (cs, (~1, [])); |
|
78 val (i', intr_ts') = foldr varify (intr_ts, (i, [])); |
|
79 val rec_consts = foldl add_term_consts_2 ([], cs'); |
|
80 val intr_consts = foldl add_term_consts_2 ([], intr_ts'); |
|
81 fun unify (env, (cname, cT)) = |
|
82 let val consts = map snd (filter (fn c => fst c = cname) intr_consts) |
|
83 in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp)) |
|
84 (env, (replicate (length consts) cT) ~~ consts) |
|
85 end; |
|
86 val (env, _) = foldl unify (([], i'), rec_consts); |
|
87 fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T |
|
88 in if T = T' then T else typ_subst_TVars_2 env T' end; |
|
89 val subst = fst o Type.freeze_thaw o |
|
90 (map_term_types (typ_subst_TVars_2 env)) |
|
91 |
|
92 in (map subst cs', map subst intr_ts') |
|
93 end) handle Type.TUNIFY => |
|
94 (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts)); |
|
95 |
|
96 |
65 (* misc *) |
97 (* misc *) |
66 |
98 |
67 (*For proving monotonicity of recursion operator*) |
99 (*For proving monotonicity of recursion operator*) |
68 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
100 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
69 ex_mono, Collect_mono, in_mono, vimage_mono]; |
101 ex_mono, Collect_mono, in_mono, vimage_mono]; |
654 |
688 |
655 val atts = map (Attrib.global_attribute thy) srcs; |
689 val atts = map (Attrib.global_attribute thy) srcs; |
656 val intr_names = map (fst o fst) intro_srcs; |
690 val intr_names = map (fst o fst) intro_srcs; |
657 val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs; |
691 val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs; |
658 val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; |
692 val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; |
659 |
693 val (cs', intr_ts') = unify_consts sign cs intr_ts; |
660 (* the following code ensures that each recursive set *) |
|
661 (* always has the same type in all introduction rules *) |
|
662 |
|
663 val {tsig, ...} = Sign.rep_sg sign; |
|
664 val add_term_consts_2 = |
|
665 foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs); |
|
666 fun varify (t, (i, ts)) = |
|
667 let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, [])) |
|
668 in (maxidx_of_term t', t'::ts) end; |
|
669 val (i, cs') = foldr varify (cs, (~1, [])); |
|
670 val (i', intr_ts') = foldr varify (intr_ts, (i, [])); |
|
671 val rec_consts = foldl add_term_consts_2 ([], cs'); |
|
672 val intr_consts = foldl add_term_consts_2 ([], intr_ts'); |
|
673 fun unify (env, (cname, cT)) = |
|
674 let val consts = map snd (filter (fn c => fst c = cname) intr_consts) |
|
675 in (foldl (fn ((env', j'), Tp) => Type.unify tsig j' env' Tp) |
|
676 (env, (replicate (length consts) cT) ~~ consts)) handle _ => |
|
677 error ("Occurrences of constant '" ^ cname ^ |
|
678 "' have incompatible types") |
|
679 end; |
|
680 val (env, _) = foldl unify (([], i'), rec_consts); |
|
681 fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T |
|
682 in if T = T' then T else typ_subst_TVars_2 env T' end; |
|
683 val subst = fst o Type.freeze_thaw o |
|
684 (map_term_types (typ_subst_TVars_2 env)); |
|
685 val cs'' = map subst cs'; |
|
686 val intr_ts'' = map subst intr_ts'; |
|
687 |
694 |
688 val ((thy', con_defs), monos) = thy |
695 val ((thy', con_defs), monos) = thy |
689 |> IsarThy.apply_theorems raw_monos |
696 |> IsarThy.apply_theorems raw_monos |
690 |> apfst (IsarThy.apply_theorems raw_con_defs); |
697 |> apfst (IsarThy.apply_theorems raw_con_defs); |
691 in |
698 in |
692 add_inductive_i verbose false "" coind false false cs'' |
699 add_inductive_i verbose false "" coind false false cs' |
693 atts ((intr_names ~~ intr_ts'') ~~ intr_atts) monos con_defs thy' |
700 atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' |
694 end; |
701 end; |
695 |
702 |
696 |
703 |
697 |
704 |
698 (** package setup **) |
705 (** package setup **) |