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