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