88 txt {* |
89 txt {* |
89 where the simproc produces the goal state |
90 where the simproc produces the goal state |
90 |
91 |
91 \begin{minipage}{\textwidth} |
92 \begin{minipage}{\textwidth} |
92 @{subgoals [display]} |
93 @{subgoals [display]} |
93 \end{minipage} |
94 \end{minipage}\bigskip |
|
95 *}(*<*)oops(*>*) |
|
96 |
|
97 text {* \solution{ex:addconversion} *} |
|
98 |
|
99 text {* |
|
100 (FIXME This solution works but is awkward.) |
|
101 *} |
|
102 |
|
103 ML{*fun add_conv ctxt ctrm = |
|
104 (case Thm.term_of ctrm of |
|
105 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
|
106 (let |
|
107 val eq1 = Conv.binop_conv (add_conv ctxt) ctrm; |
|
108 val ctrm' = Thm.rhs_of eq1; |
|
109 val trm' = Thm.term_of ctrm'; |
|
110 val eq2 = Conv.rewr_conv (get_sum_thm ctxt trm' (dest_sum trm')) ctrm' |
|
111 in |
|
112 Thm.transitive eq1 eq2 |
|
113 end) |
|
114 | _ $ _ => Conv.combination_conv |
|
115 (add_conv ctxt) (add_conv ctxt) ctrm |
|
116 | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm |
|
117 | _ => Conv.all_conv ctrm) |
|
118 |
|
119 val add_tac = CSUBGOAL (fn (goal, i) => |
|
120 let |
|
121 val ctxt = ProofContext.init (Thm.theory_of_cterm goal) |
|
122 in |
|
123 CONVERSION |
|
124 (Conv.params_conv ~1 (fn ctxt => |
|
125 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
|
126 Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i |
|
127 end)*} |
|
128 |
|
129 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
|
130 apply(tactic {* add_tac 1 *})? |
|
131 txt {* |
|
132 where the simproc produces the goal state |
|
133 |
|
134 \begin{minipage}{\textwidth} |
|
135 @{subgoals [display]} |
|
136 \end{minipage}\bigskip |
94 *}(*<*)oops(*>*) |
137 *}(*<*)oops(*>*) |
95 |
138 |
96 |
139 |
97 |
|
98 end |
140 end |