136 (** datatypes **) |
136 (** datatypes **) |
137 |
137 |
138 (* definitional scheme for random instances on datatypes *) |
138 (* definitional scheme for random instances on datatypes *) |
139 |
139 |
140 (*FIXME avoid this low-level proving*) |
140 (*FIXME avoid this low-level proving*) |
141 val rct = Thm.cprop_of @{thm random_aux_rec} |> Thm.dest_arg |> Thm.dest_arg |
141 local |
142 |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_fun; |
142 |
143 fun dest_ctyp_nth k cT = nth (Thm.dest_ctyp cT) k; |
143 fun dest_ctyp_nth k cT = nth (Thm.dest_ctyp cT) k; |
144 val aT = rct |> Thm.ctyp_of_term |> dest_ctyp_nth 1; |
144 val eq = Thm.cprop_of @{thm random_aux_rec} |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_arg; |
|
145 val lhs = eq |> Thm.dest_arg1; |
|
146 val pt_random_aux = lhs |> Thm.dest_fun; |
|
147 val ct_k = lhs |> Thm.dest_arg; |
|
148 val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun; |
|
149 val aT = pt_random_aux |> Thm.ctyp_of_term |> dest_ctyp_nth 1; |
|
150 |
|
151 val rew_thms = map mk_meta_eq [@{thm code_numeral_zero_minus_one}, |
|
152 @{thm Suc_code_numeral_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}]; |
|
153 val rew_ts = map (Logic.dest_equals o Thm.prop_of) rew_thms; |
|
154 val rew_ss = HOL_ss addsimps rew_thms; |
|
155 |
|
156 in |
145 |
157 |
146 fun random_aux_primrec eq lthy = |
158 fun random_aux_primrec eq lthy = |
147 let |
159 let |
148 val thy = ProofContext.theory_of lthy; |
160 val thy = ProofContext.theory_of lthy; |
149 val rews = map mk_meta_eq [@{thm code_numeral_zero_minus_one}, |
161 val ((t_random_aux as Free (random_aux, T)) $ (t_k as Free (v, _)), proto_t_rhs) = |
150 @{thm Suc_code_numeral_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}]; |
162 (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; |
151 val (rt as Free (random_aux, T)) $ (vt as Free (v, _)) = |
|
152 (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; |
|
153 val Type (_, [_, iT]) = T; |
163 val Type (_, [_, iT]) = T; |
154 val icT = Thm.ctyp_of thy iT; |
164 val icT = Thm.ctyp_of thy iT; |
|
165 val cert = Thm.cterm_of thy; |
|
166 val inst = Thm.instantiate_cterm ([(aT, icT)], []); |
155 fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t); |
167 fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t); |
156 val eqs0 = [subst_v @{term "0::code_numeral"} eq, subst_v (@{term "Suc_code_numeral"} $ vt) eq]; |
168 val t_rhs = lambda t_k proto_t_rhs; |
157 val eqs1 = map (Pattern.rewrite_term thy (map (Logic.dest_equals o Thm.prop_of) rews) []) eqs0 |
169 val eqs0 = [subst_v @{term "0::code_numeral"} eq, subst_v (@{term "Suc_code_numeral"} $ t_k) eq]; |
|
170 val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0; |
158 val ((_, eqs2), lthy') = PrimrecPackage.add_primrec_simple |
171 val ((_, eqs2), lthy') = PrimrecPackage.add_primrec_simple |
159 [((Binding.name random_aux, T), NoSyn)] eqs1 lthy; |
172 [((Binding.name random_aux, T), NoSyn)] eqs1 lthy; |
160 val eq_tac = ALLGOALS Goal.conjunction_tac THEN ALLGOALS (simp_tac (HOL_ss addsimps rews)) |
173 val eq_tac = ALLGOALS Goal.conjunction_tac THEN ALLGOALS (simp_tac rew_ss) |
161 THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2))); |
174 THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2))); |
162 val eqs3 = Goal.prove_multi lthy' [v] [] eqs0 (K eq_tac); |
175 val eqs3 = Goal.prove_multi lthy' [v] [] eqs0 (K eq_tac); |
163 val rct' = Thm.instantiate_cterm ([(aT, icT)], []) rct |
176 val cT_random_aux = inst pt_random_aux; |
|
177 val cT_rhs = inst pt_rhs; |
164 val rule = @{thm random_aux_rec} |
178 val rule = @{thm random_aux_rec} |
165 |> Drule.instantiate ([(aT, icT)], [(rct', Thm.cterm_of thy rt)]) |
179 |> Drule.instantiate ([(aT, icT)], |
166 |> (fn thm => thm OF eqs3) |
180 [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]) |
|
181 |> (fn thm => thm OF eqs3); |
167 val tac = ALLGOALS (rtac rule); |
182 val tac = ALLGOALS (rtac rule); |
168 val simp = Goal.prove lthy' [v] [] eq (K tac); |
183 val simp = Goal.prove lthy' [v] [] eq (K tac); |
169 in (simp, lthy') end; |
184 in (simp, lthy') end; |
|
185 |
|
186 end; |
170 |
187 |
171 fun random_aux_primrec_multi prefix [eq] lthy = |
188 fun random_aux_primrec_multi prefix [eq] lthy = |
172 lthy |
189 lthy |
173 |> random_aux_primrec eq |
190 |> random_aux_primrec eq |
174 |>> (fn simp => [simp]) |
191 |>> (fn simp => [simp]) |