91 simple_pinducts : thm list, |
91 simple_pinducts : thm list, |
92 cases : thm, |
92 cases : thm, |
93 termination : thm, |
93 termination : thm, |
94 domintros : thm list option} |
94 domintros : thm list option} |
95 |
95 |
96 fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts, |
96 fun transform_function_data ({add_simps, case_names, fs, R, psimps, pinducts, |
97 simps, inducts, termination, defname, is_partial} : info) phi = |
97 simps, inducts, termination, defname, is_partial} : info) phi = |
98 let |
98 let |
99 val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi |
99 val term = Morphism.term phi |
|
100 val thm = Morphism.thm phi |
|
101 val fact = Morphism.fact phi |
100 val name = Binding.name_of o Morphism.binding phi o Binding.name |
102 val name = Binding.name_of o Morphism.binding phi o Binding.name |
101 in |
103 in |
102 { add_simps = add_simps, case_names = case_names, |
104 { add_simps = add_simps, case_names = case_names, |
103 fs = map term fs, R = term R, psimps = fact psimps, |
105 fs = map term fs, R = term R, psimps = fact psimps, |
104 pinducts = fact pinducts, simps = Option.map fact simps, |
106 pinducts = fact pinducts, simps = Option.map fact simps, |
130 val thy = Proof_Context.theory_of ctxt |
132 val thy = Proof_Context.theory_of ctxt |
131 val ct = cterm_of thy t |
133 val ct = cterm_of thy t |
132 val inst_morph = lift_morphism thy o Thm.instantiate |
134 val inst_morph = lift_morphism thy o Thm.instantiate |
133 |
135 |
134 fun match (trm, data) = |
136 fun match (trm, data) = |
135 SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) |
137 SOME (transform_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) |
136 handle Pattern.MATCH => NONE |
138 handle Pattern.MATCH => NONE |
137 in |
139 in |
138 get_first match (Item_Net.retrieve (get_function ctxt) t) |
140 get_first match (Item_Net.retrieve (get_function ctxt) t) |
139 end |
141 end |
140 |
142 |