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