--- a/src/Pure/conjunction.ML Tue Jun 19 23:15:47 2007 +0200
+++ b/src/Pure/conjunction.ML Tue Jun 19 23:15:49 2007 +0200
@@ -10,43 +10,46 @@
val conjunction: cterm
val mk_conjunction: cterm * cterm -> cterm
val mk_conjunction_list: cterm list -> cterm
+ val mk_conjunction_balanced: cterm list -> cterm
val dest_conjunction: cterm -> cterm * cterm
val cong: thm -> thm -> thm
- val conv: int -> (int -> cterm -> thm) -> cterm -> thm
+ val convs: (cterm -> thm) -> cterm -> thm
val conjunctionD1: thm
val conjunctionD2: thm
val conjunctionI: thm
val intr: thm -> thm -> thm
val intr_list: thm list -> thm
+ val intr_balanced: thm list -> thm
val elim: thm -> thm * thm
val elim_list: thm -> thm list
- val elim_precise: int list -> thm -> thm list list
- val curry: int -> thm -> thm
- val uncurry: int -> thm -> thm
- val split_defined: int -> thm -> thm * thm list
+ val elim_balanced: int -> thm -> thm list
+ val curry_balanced: int -> thm -> thm
+ val uncurry_balanced: int -> thm -> thm
end;
structure Conjunction: CONJUNCTION =
struct
-
(** abstract syntax **)
fun read s = Thm.read_cterm ProtoPure.thy (s, propT);
val cert = Thm.cterm_of ProtoPure.thy;
+val true_prop = cert Logic.true_prop;
val conjunction = cert Logic.conjunction;
+
fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
-val true_prop = read "!!dummy. PROP dummy ==> PROP dummy";
-
fun mk_conjunction_list [] = true_prop
| mk_conjunction_list ts = foldr1 mk_conjunction ts;
+fun mk_conjunction_balanced [] = true_prop
+ | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
+
fun dest_conjunction ct =
(case Thm.term_of ct of
(Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
- | _ => raise TERM ("dest_conjunction", [term_of ct]));
+ | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
@@ -54,20 +57,12 @@
(* conversion *)
-(*rewrite the A's in A1 && ... && An*)
-
val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
-fun conv 0 _ = reflexive
- | conv n cv =
- let
- fun cnv i ct =
- if i = n then cv i ct
- else
- (case try dest_conjunction ct of
- NONE => cv i ct
- | SOME (A, B) => cong (cv i A) (cnv (i + 1) B));
- in cnv 1 end;
+fun convs cv ct =
+ (case try dest_conjunction ct of
+ NONE => cv ct
+ | SOME (A, B) => cong (convs cv A) (convs cv B));
(* intro/elim *)
@@ -98,6 +93,7 @@
(Thm.forall_intr C (Thm.implies_intr ABC
(Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
+
fun intr tha thb =
Thm.implies_elim
(Thm.implies_elim
@@ -105,9 +101,6 @@
tha)
thb;
-fun intr_list [] = asm_rl
- | intr_list ths = foldr1 (uncurry intr) ths;
-
fun elim th =
let
val (A, B) = dest_conjunction (Thm.cprop_of th)
@@ -118,36 +111,34 @@
Thm.implies_elim (inst conjunctionD2) th)
end;
-(*((A && B) && C) && D && E -- flat*)
-fun elim_list th =
+end;
+
+
+(* multiple conjuncts *)
+
+fun intr_list [] = asm_rl
+ | intr_list ths = foldr1 (uncurry intr) ths;
+
+fun intr_balanced [] = asm_rl
+ | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
+
+fun elim_list th = (* FIXME improper!? rename to "elims" *)
let val (th1, th2) = elim th
in elim_list th1 @ elim_list th2 end handle THM _ => [th];
-(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
-fun elim_precise spans =
- let
- fun elm 0 _ = []
- | elm 1 th = [th]
- | elm n th =
- let val (th1, th2) = elim th
- in th1 :: elm (n - 1) th2 end;
- fun elms (0 :: ns) ths = [] :: elms ns ths
- | elms (n :: ns) (th :: ths) = elm n th :: elms ns ths
- | elms _ _ = [];
- in elms spans o elm (length (filter_out (equal 0) spans)) end;
-
-end;
+fun elim_balanced 0 _ = []
+ | elim_balanced n th = BalancedTree.dest elim n th;
(* currying *)
local
-fun conjs m =
- let val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto m)
- in (As, Logic.mk_conjunction_list As) end;
+fun conjs n =
+ let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n)
+ in (As, mk_conjunction_balanced As) end;
-val B = Free ("B", propT);
+val B = cert (Free ("B", propT));
fun comp_rule th rule =
Thm.adjust_maxidx_thm ~1 (th COMP
@@ -160,64 +151,35 @@
-----------------------
A1 ==> ... ==> An ==> B
*)
-fun curry n th =
- let
- val k =
- (case try Logic.dest_implies (Thm.prop_of th) of
- NONE => 0
- | SOME (prem, _) => length (Logic.dest_conjunction_list prem));
- val m = if n = ~1 then k else Int.min (n, k);
- in
- if m < 2 then th
- else
- let
- val (As, C) = conjs m;
- val cAs = map cert As;
- val D = Logic.mk_implies (Logic.mk_conjunction_list As, B) |> cert;
- in
- comp_rule th
- (Thm.implies_elim (Thm.assume D) (intr_list (map Thm.assume cAs))
- |> Drule.implies_intr_list (D :: cAs))
- end
- end;
+fun curry_balanced n th =
+ if n < 2 then th
+ else
+ let
+ val (As, C) = conjs n;
+ val D = Drule.mk_implies (C, B);
+ in
+ comp_rule th
+ (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As))
+ |> Drule.implies_intr_list (D :: As))
+ end;
(*
A1 ==> ... ==> An ==> B
-----------------------
- A1 && ... && An ==> B
+ A1 && ... && An ==> B
*)
-fun uncurry n th =
- let
- val k = Thm.nprems_of th;
- val m = if n = ~1 then k else Int.min (n, k);
- in
- if m < 2 then th
- else
- let
- val (As, C) = conjs m ||> cert;
- val D = Logic.list_implies (As, B) |> cert;
- in
- comp_rule th
- (Drule.implies_elim_list (Thm.assume D) (elim_list (Thm.assume C))
- |> Drule.implies_intr_list [D, C])
- end
- end;
+fun uncurry_balanced n th =
+ if n < 2 then th
+ else
+ let
+ val (As, C) = conjs n;
+ val D = Drule.list_implies (As, B);
+ in
+ comp_rule th
+ (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C))
+ |> Drule.implies_intr_list [D, C])
+ end;
end;
-
-(* defined conjunctions *)
-
-fun project th 1 = (th RS conjunctionD1 handle THM _ => th)
- | project th k = project (th RS conjunctionD2) (k - 1);
-
-fun split_defined n eq =
- let
- val intro =
- (eq RS Drule.equal_elim_rule2)
- |> curry n
- |> n = 0 ? Thm.eq_assumption 1;
- val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
- in (intro, dests) end;
-
end;