1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11(*
12   Decompose a meta-conjunction as a proper fact (list of theorems)
13*)
14
15theory Conjuncts
16imports Main
17begin
18
19ML\<open>
20
21structure Conjuncts =
22struct
23
24local
25
26  structure Data = Generic_Data
27  (
28    type T = thm;
29    val empty: T = Drule.dummy_thm;
30    val extend = I;
31    val merge : T * T -> T = (K Drule.dummy_thm);
32  );
33
34  fun elim_conjuncts thm =
35    case try Conjunction.elim thm of
36    SOME (thm', thm'') => elim_conjuncts thm' @ elim_conjuncts thm''
37    | NONE => if Thm.prop_of thm = Thm.prop_of (Drule.dummy_thm) then [] else [thm]
38
39  in
40
41  val _ = Context.>> (Context.map_theory (
42    (Attrib.setup @{binding "conjuncts"}
43      (Scan.lift (Args.mode "accumulate") >> (fn acc =>
44        if acc then
45        Thm.declaration_attribute (Data.map o (fn x => fn y => Conjunction.intr y x))
46        else
47        Thm.declaration_attribute Data.put))
48      "add meta_conjuncts to \"conjuncts\" named theorem") #>
49    Global_Theory.add_thms_dynamic (@{binding "conjuncts"}, elim_conjuncts o Data.get)))
50
51end
52
53end
54
55\<close>
56
57notepad begin
58
59  fix A B C D
60  assume ABC[conjuncts]: "(A &&& B) &&& (B &&& C)"
61  note ABC' = conjuncts
62
63  have "A" by (rule ABC')
64  have "B" by (rule \<open>B\<close>)
65  have "C" by (rule ABC'(4))
66
67  (* Disclaimer: only the last declared lemma is stored *)
68  assume ABCD[conjuncts]: "A &&& B" "C &&& D"
69  note CD = conjuncts
70
71  have "A" by ((rule CD)?,rule ABC')
72  have "C" by (rule CD)
73
74
75
76  note ABCD(1)[conjuncts]
77  note AB = conjuncts
78
79  note ABCD(2)[conjuncts]
80  note CD = conjuncts
81
82  (* We can accumulate multi-thms, we just need to clear conjuncts first *)
83  note [[conjuncts]]
84
85  note ABCD[conjuncts (accumulate)]
86  note ABCD' = conjuncts
87
88end
89
90end
91