|
70525
|
1 |
(* Title: HOL/ex/Join_Theory.thy
|
|
|
2 |
Author: Makarius
|
|
|
3 |
*)
|
|
|
4 |
|
|
|
5 |
section \<open>Join theory content from independent (parallel) specifications\<close>
|
|
|
6 |
|
|
|
7 |
theory Join_Theory
|
|
|
8 |
imports Main
|
|
|
9 |
begin
|
|
|
10 |
|
|
|
11 |
subsection \<open>Example template\<close>
|
|
|
12 |
|
|
|
13 |
definition "test = True"
|
|
|
14 |
lemma test: "test" by (simp add: test_def)
|
|
|
15 |
|
|
|
16 |
|
|
|
17 |
subsection \<open>Specification as Isabelle/ML function\<close>
|
|
|
18 |
|
|
|
19 |
ML \<open>
|
|
|
20 |
fun spec i lthy =
|
|
|
21 |
let
|
|
|
22 |
val b = Binding.name ("test" ^ string_of_int i)
|
|
|
23 |
val ((t, (_, def)), lthy') = lthy
|
|
|
24 |
|> Local_Theory.define ((b, NoSyn), ((Binding.empty, []), \<^term>\<open>True\<close>));
|
|
|
25 |
val th =
|
|
|
26 |
Goal.prove lthy' [] [] (HOLogic.mk_Trueprop t)
|
|
|
27 |
(fn {context = goal_ctxt, ...} => asm_full_simp_tac (goal_ctxt addsimps [def]) 1);
|
|
|
28 |
val (_, lthy'') = lthy' |> Local_Theory.note ((b, []), [th]);
|
|
|
29 |
in lthy'' end;
|
|
|
30 |
\<close>
|
|
|
31 |
|
|
|
32 |
|
|
|
33 |
subsection \<open>Example application\<close>
|
|
|
34 |
|
|
|
35 |
setup \<open>
|
|
|
36 |
fn thy =>
|
|
|
37 |
let val forked_thys = Par_List.map (fn i => Named_Target.theory_map (spec i) thy) (1 upto 10)
|
|
77895
|
38 |
in Context.join_thys forked_thys end
|
|
70525
|
39 |
\<close>
|
|
|
40 |
|
|
|
41 |
term test1
|
|
|
42 |
thm test1
|
|
|
43 |
|
|
|
44 |
term test10
|
|
|
45 |
thm test10
|
|
|
46 |
|
|
|
47 |
end
|