117 end; |
117 end; |
118 |
118 |
119 fun random_aux_primrec_multi auxname [eq] lthy = |
119 fun random_aux_primrec_multi auxname [eq] lthy = |
120 lthy |
120 lthy |
121 |> random_aux_primrec eq |
121 |> random_aux_primrec eq |
122 |>> (fn simp => [simp]) |
122 |>> single |
123 | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy = |
123 | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy = |
124 let |
124 let |
125 val thy = Proof_Context.theory_of lthy; |
125 val thy = Proof_Context.theory_of lthy; |
126 val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs; |
126 val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs; |
127 val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss; |
127 val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss; |
145 let |
145 let |
146 val proj_simps = map (snd o snd) proj_defs; |
146 val proj_simps = map (snd o snd) proj_defs; |
147 fun tac { context = ctxt, prems = _ } = |
147 fun tac { context = ctxt, prems = _ } = |
148 ALLGOALS (simp_tac (put_simpset HOL_ss ctxt addsimps proj_simps)) |
148 ALLGOALS (simp_tac (put_simpset HOL_ss ctxt addsimps proj_simps)) |
149 THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp]) |
149 THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp]) |
150 THEN ALLGOALS (simp_tac |
150 THEN ALLGOALS (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms fst_conv snd_conv})); |
151 (put_simpset HOL_ss ctxt addsimps [@{thm fst_conv}, @{thm snd_conv}])); |
|
152 in (map (fn prop => Goal.prove_sorry lthy [v] [] prop tac) eqs, lthy) end; |
151 in (map (fn prop => Goal.prove_sorry lthy [v] [] prop tac) eqs, lthy) end; |
153 in |
152 in |
154 lthy |
153 lthy |
155 |> random_aux_primrec aux_eq' |
154 |> random_aux_primrec aux_eq' |
156 ||>> fold_map Local_Theory.define proj_defs |
155 ||>> fold_map Local_Theory.define proj_defs |
157 |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs) |
156 |-> uncurry prove_eqs |
158 end; |
157 end; |
159 |
158 |
160 fun random_aux_specification prfx name eqs lthy = |
159 fun random_aux_specification prfx name eqs lthy = |
161 let |
160 let |
162 val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq |
161 val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq |
174 val b = Binding.conceal (Binding.qualify true prfx |
173 val b = Binding.conceal (Binding.qualify true prfx |
175 (Binding.qualify true name (Binding.name "simps"))); |
174 (Binding.qualify true name (Binding.name "simps"))); |
176 in |
175 in |
177 lthy |
176 lthy |
178 |> random_aux_primrec_multi (name ^ prfx) proto_eqs |
177 |> random_aux_primrec_multi (name ^ prfx) proto_eqs |
179 |-> (fn proto_simps => prove_simps proto_simps) |
178 |-> prove_simps |
180 |-> (fn simps => Local_Theory.note |
179 |-> (fn simps => Local_Theory.note |
181 ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps)) |
180 ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps)) |
182 |> snd |
181 |> snd |
183 end |
182 end |
184 |
183 |