29 expands: thm list, |
29 expands: thm list, |
30 case_conv_ifs: thm list}; |
30 case_conv_ifs: thm list}; |
31 |
31 |
32 val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar |
32 val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar |
33 val ctr_sugar_of: Proof.context -> string -> ctr_sugar option |
33 val ctr_sugar_of: Proof.context -> string -> ctr_sugar option |
|
34 val ctr_sugars_of: Proof.context -> ctr_sugar list |
34 |
35 |
35 val rep_compat_prefix: string |
36 val rep_compat_prefix: string |
36 |
37 |
37 val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list |
38 val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list |
38 val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list |
39 val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list |
78 sel_thmss: thm list list, |
79 sel_thmss: thm list list, |
79 disc_exhausts: thm list, |
80 disc_exhausts: thm list, |
80 collapses: thm list, |
81 collapses: thm list, |
81 expands: thm list, |
82 expands: thm list, |
82 case_conv_ifs: thm list}; |
83 case_conv_ifs: thm list}; |
|
84 |
|
85 fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar, |
|
86 {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) = |
|
87 ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2; |
83 |
88 |
84 fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, |
89 fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, |
85 case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss, |
90 case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss, |
86 disc_exhausts, collapses, expands, case_conv_ifs} = |
91 disc_exhausts, collapses, expands, case_conv_ifs} = |
87 {ctrs = map (Morphism.term phi) ctrs, |
92 {ctrs = map (Morphism.term phi) ctrs, |
103 disc_exhausts = map (Morphism.thm phi) disc_exhausts, |
108 disc_exhausts = map (Morphism.thm phi) disc_exhausts, |
104 collapses = map (Morphism.thm phi) collapses, |
109 collapses = map (Morphism.thm phi) collapses, |
105 expands = map (Morphism.thm phi) expands, |
110 expands = map (Morphism.thm phi) expands, |
106 case_conv_ifs = map (Morphism.thm phi) case_conv_ifs}; |
111 case_conv_ifs = map (Morphism.thm phi) case_conv_ifs}; |
107 |
112 |
108 fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar, |
113 val transfer_ctr_sugar = |
109 {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) = |
114 morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of; |
110 ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2; |
|
111 |
115 |
112 structure Data = Generic_Data |
116 structure Data = Generic_Data |
113 ( |
117 ( |
114 type T = ctr_sugar Symtab.table; |
118 type T = ctr_sugar Symtab.table; |
115 val empty = Symtab.empty; |
119 val empty = Symtab.empty; |
117 val merge = Symtab.merge eq_ctr_sugar; |
121 val merge = Symtab.merge eq_ctr_sugar; |
118 ); |
122 ); |
119 |
123 |
120 fun ctr_sugar_of ctxt = |
124 fun ctr_sugar_of ctxt = |
121 Symtab.lookup (Data.get (Context.Proof ctxt)) |
125 Symtab.lookup (Data.get (Context.Proof ctxt)) |
122 #> Option.map (morph_ctr_sugar |
126 #> Option.map (transfer_ctr_sugar ctxt); |
123 (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt)))); |
127 |
|
128 fun ctr_sugars_of ctxt = |
|
129 Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) []; |
124 |
130 |
125 fun register_ctr_sugar key ctr_sugar = |
131 fun register_ctr_sugar key ctr_sugar = |
126 Local_Theory.declaration {syntax = false, pervasive = true} |
132 Local_Theory.declaration {syntax = false, pervasive = true} |
127 (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar))); |
133 (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar))); |
128 |
134 |