1(* Title: Pure/conjunction.ML 2 Author: Makarius 3 4Meta-level conjunction. 5*) 6 7signature CONJUNCTION = 8sig 9 val conjunction: cterm 10 val mk_conjunction: cterm * cterm -> cterm 11 val mk_conjunction_balanced: cterm list -> cterm 12 val dest_conjunction: cterm -> cterm * cterm 13 val dest_conjunctions: cterm -> cterm list 14 val cong: thm -> thm -> thm 15 val convs: (cterm -> thm) -> cterm -> thm 16 val conjunctionD1: thm 17 val conjunctionD2: thm 18 val conjunctionI: thm 19 val intr: thm -> thm -> thm 20 val intr_balanced: thm list -> thm 21 val elim: thm -> thm * thm 22 val elim_conjunctions: thm -> thm list 23 val elim_balanced: int -> thm -> thm list 24 val curry_balanced: int -> thm -> thm 25 val uncurry_balanced: int -> thm -> thm 26end; 27 28structure Conjunction: CONJUNCTION = 29struct 30 31(** abstract syntax **) 32 33fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t; 34val read_prop = certify o Simple_Syntax.read_prop; 35 36val true_prop = certify Logic.true_prop; 37val conjunction = certify Logic.conjunction; 38 39fun mk_conjunction (A, B) = Thm.apply (Thm.apply conjunction A) B; 40 41fun mk_conjunction_balanced [] = true_prop 42 | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts; 43 44fun dest_conjunction ct = 45 (case Thm.term_of ct of 46 (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct 47 | _ => raise TERM ("dest_conjunction", [Thm.term_of ct])); 48 49fun dest_conjunctions ct = 50 (case try dest_conjunction ct of 51 NONE => [ct] 52 | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); 53 54 55 56(** derived rules **) 57 58(* conversion *) 59 60val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction); 61 62fun convs cv ct = 63 (case try dest_conjunction ct of 64 NONE => cv ct 65 | SOME (A, B) => cong (convs cv A) (convs cv B)); 66 67 68(* intro/elim *) 69 70local 71 72val A = read_prop "A" and vA = (("A", 0), propT); 73val B = read_prop "B" and vB = (("B", 0), propT); 74val C = read_prop "C"; 75val ABC = read_prop "A \<Longrightarrow> B \<Longrightarrow> C"; 76val A_B = read_prop "A &&& B"; 77 78val conjunction_def = 79 Thm.unvarify_axiom (Context.the_global_context ()) "Pure.conjunction_def"; 80 81fun conjunctionD which = 82 Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP 83 Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B)); 84 85in 86 87val conjunctionD1 = 88 Drule.store_standard_thm (Binding.make ("conjunctionD1", \<^here>)) (conjunctionD #1); 89 90val conjunctionD2 = 91 Drule.store_standard_thm (Binding.make ("conjunctionD2", \<^here>)) (conjunctionD #2); 92 93val conjunctionI = 94 Drule.store_standard_thm (Binding.make ("conjunctionI", \<^here>)) 95 (Drule.implies_intr_list [A, B] 96 (Thm.equal_elim 97 (Thm.symmetric conjunction_def) 98 (Thm.forall_intr C (Thm.implies_intr ABC 99 (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B]))))); 100 101 102fun intr tha thb = 103 Thm.implies_elim 104 (Thm.implies_elim 105 (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI) 106 tha) 107 thb; 108 109fun elim th = 110 let 111 val (A, B) = dest_conjunction (Thm.cprop_of th) 112 handle TERM (msg, _) => raise THM (msg, 0, [th]); 113 val inst = Thm.instantiate ([], [(vA, A), (vB, B)]); 114 in 115 (Thm.implies_elim (inst conjunctionD1) th, 116 Thm.implies_elim (inst conjunctionD2) th) 117 end; 118 119end; 120 121fun elim_conjunctions th = 122 (case try elim th of 123 NONE => [th] 124 | SOME (th1, th2) => elim_conjunctions th1 @ elim_conjunctions th2); 125 126 127(* balanced conjuncts *) 128 129fun intr_balanced [] = asm_rl 130 | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths; 131 132fun elim_balanced 0 _ = [] 133 | elim_balanced n th = Balanced_Tree.dest elim n th; 134 135 136(* currying *) 137 138local 139 140val bootstrap_thy = Context.the_global_context (); 141 142fun conjs n = 143 let 144 val As = 145 map (fn A => Thm.global_cterm_of bootstrap_thy (Free (A, propT))) 146 (Name.invent Name.context "A" n); 147 in (As, mk_conjunction_balanced As) end; 148 149val B = read_prop "B"; 150 151fun comp_rule th rule = 152 Thm.adjust_maxidx_thm ~1 (th COMP 153 (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1))); 154 155in 156 157(* 158 A1 &&& ... &&& An \<Longrightarrow> B 159 ----------------------- 160 A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B 161*) 162fun curry_balanced n th = 163 if n < 2 then th 164 else 165 let 166 val (As, C) = conjs n; 167 val D = Drule.mk_implies (C, B); 168 in 169 comp_rule th 170 (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As)) 171 |> Drule.implies_intr_list (D :: As)) 172 end; 173 174(* 175 A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B 176 ----------------------- 177 A1 &&& ... &&& An \<Longrightarrow> B 178*) 179fun uncurry_balanced n th = 180 if n < 2 then th 181 else 182 let 183 val (As, C) = conjs n; 184 val D = Drule.list_implies (As, B); 185 in 186 comp_rule th 187 (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C)) 188 |> Drule.implies_intr_list [D, C]) 189 end; 190 191end; 192 193end; 194