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