93 \end{minipage}\bigskip |
93 \end{minipage}\bigskip |
94 *}(*<*)oops(*>*) |
94 *}(*<*)oops(*>*) |
95 |
95 |
96 text {* \solution{ex:addconversion} *} |
96 text {* \solution{ex:addconversion} *} |
97 |
97 |
98 text {* |
98 ML{*fun add_simple_conv ctxt ctrm = |
99 (FIXME This solution works but is awkward.) |
99 let |
100 *} |
100 val trm = Thm.term_of ctrm |
|
101 in |
|
102 get_sum_thm ctxt trm (dest_sum trm) |
|
103 end |
101 |
104 |
102 ML{*fun add_conv ctxt ctrm = |
105 fun add_conv ctxt ctrm = |
103 (case Thm.term_of ctrm of |
106 (case Thm.term_of ctrm of |
104 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
107 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
105 (let |
108 (Conv.binop_conv (add_conv ctxt) |
106 val eq1 = Conv.binop_conv (add_conv ctxt) ctrm; |
109 then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm |
107 val ctrm' = Thm.rhs_of eq1; |
|
108 val trm' = Thm.term_of ctrm'; |
|
109 val eq2 = Conv.rewr_conv (get_sum_thm ctxt trm' (dest_sum trm')) ctrm' |
|
110 in |
|
111 Thm.transitive eq1 eq2 |
|
112 end) |
|
113 | _ $ _ => Conv.combination_conv |
110 | _ $ _ => Conv.combination_conv |
114 (add_conv ctxt) (add_conv ctxt) ctrm |
111 (add_conv ctxt) (add_conv ctxt) ctrm |
115 | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm |
112 | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm |
116 | _ => Conv.all_conv ctrm) |
113 | _ => Conv.all_conv ctrm) |
117 |
114 |