src/Pure/conjunction.ML
changeset 23422 4a368c087f58
parent 21565 bd28361f4c5b
child 23535 58147e5bd070
     1.1 --- a/src/Pure/conjunction.ML	Tue Jun 19 23:15:47 2007 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Tue Jun 19 23:15:49 2007 +0200
     1.3 @@ -10,43 +10,46 @@
     1.4    val conjunction: cterm
     1.5    val mk_conjunction: cterm * cterm -> cterm
     1.6    val mk_conjunction_list: cterm list -> cterm
     1.7 +  val mk_conjunction_balanced: cterm list -> cterm
     1.8    val dest_conjunction: cterm -> cterm * cterm
     1.9    val cong: thm -> thm -> thm
    1.10 -  val conv: int -> (int -> cterm -> thm) -> cterm -> thm
    1.11 +  val convs: (cterm -> thm) -> cterm -> thm
    1.12    val conjunctionD1: thm
    1.13    val conjunctionD2: thm
    1.14    val conjunctionI: thm
    1.15    val intr: thm -> thm -> thm
    1.16    val intr_list: thm list -> thm
    1.17 +  val intr_balanced: thm list -> thm
    1.18    val elim: thm -> thm * thm
    1.19    val elim_list: thm -> thm list
    1.20 -  val elim_precise: int list -> thm -> thm list list
    1.21 -  val curry: int -> thm -> thm
    1.22 -  val uncurry: int -> thm -> thm
    1.23 -  val split_defined: int -> thm -> thm * thm list
    1.24 +  val elim_balanced: int -> thm -> thm list
    1.25 +  val curry_balanced: int -> thm -> thm
    1.26 +  val uncurry_balanced: int -> thm -> thm
    1.27  end;
    1.28  
    1.29  structure Conjunction: CONJUNCTION =
    1.30  struct
    1.31  
    1.32 -
    1.33  (** abstract syntax **)
    1.34  
    1.35  fun read s = Thm.read_cterm ProtoPure.thy (s, propT);
    1.36  val cert = Thm.cterm_of ProtoPure.thy;
    1.37  
    1.38 +val true_prop = cert Logic.true_prop;
    1.39  val conjunction = cert Logic.conjunction;
    1.40 +
    1.41  fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
    1.42  
    1.43 -val true_prop = read "!!dummy. PROP dummy ==> PROP dummy";
    1.44 -
    1.45  fun mk_conjunction_list [] = true_prop
    1.46    | mk_conjunction_list ts = foldr1 mk_conjunction ts;
    1.47  
    1.48 +fun mk_conjunction_balanced [] = true_prop
    1.49 +  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
    1.50 +
    1.51  fun dest_conjunction ct =
    1.52    (case Thm.term_of ct of
    1.53      (Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    1.54 -  | _ => raise TERM ("dest_conjunction", [term_of ct]));
    1.55 +  | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
    1.56  
    1.57  
    1.58  
    1.59 @@ -54,20 +57,12 @@
    1.60  
    1.61  (* conversion *)
    1.62  
    1.63 -(*rewrite the A's in A1 && ... && An*)
    1.64 -
    1.65  val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
    1.66  
    1.67 -fun conv 0 _ = reflexive
    1.68 -  | conv n cv =
    1.69 -      let
    1.70 -        fun cnv i ct =
    1.71 -          if i = n then cv i ct
    1.72 -          else
    1.73 -            (case try dest_conjunction ct of
    1.74 -              NONE => cv i ct
    1.75 -            | SOME (A, B) => cong (cv i A) (cnv (i + 1) B));
    1.76 -      in cnv 1 end;
    1.77 +fun convs cv ct =
    1.78 +  (case try dest_conjunction ct of
    1.79 +    NONE => cv ct
    1.80 +  | SOME (A, B) => cong (convs cv A) (convs cv B));
    1.81  
    1.82  
    1.83  (* intro/elim *)
    1.84 @@ -98,6 +93,7 @@
    1.85        (Thm.forall_intr C (Thm.implies_intr ABC
    1.86          (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
    1.87  
    1.88 +
    1.89  fun intr tha thb =
    1.90    Thm.implies_elim
    1.91      (Thm.implies_elim
    1.92 @@ -105,9 +101,6 @@
    1.93      tha)
    1.94    thb;
    1.95  
    1.96 -fun intr_list [] = asm_rl
    1.97 -  | intr_list ths = foldr1 (uncurry intr) ths;
    1.98 -
    1.99  fun elim th =
   1.100    let
   1.101      val (A, B) = dest_conjunction (Thm.cprop_of th)
   1.102 @@ -118,36 +111,34 @@
   1.103      Thm.implies_elim (inst conjunctionD2) th)
   1.104    end;
   1.105  
   1.106 -(*((A && B) && C) && D && E -- flat*)
   1.107 -fun elim_list th =
   1.108 +end;
   1.109 +
   1.110 +
   1.111 +(* multiple conjuncts *)
   1.112 +
   1.113 +fun intr_list [] = asm_rl
   1.114 +  | intr_list ths = foldr1 (uncurry intr) ths;
   1.115 +
   1.116 +fun intr_balanced [] = asm_rl
   1.117 +  | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
   1.118 +
   1.119 +fun elim_list th =   (* FIXME improper!? rename to "elims" *)
   1.120    let val (th1, th2) = elim th
   1.121    in elim_list th1 @ elim_list th2 end handle THM _ => [th];
   1.122  
   1.123 -(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
   1.124 -fun elim_precise spans =
   1.125 -  let
   1.126 -    fun elm 0 _ = []
   1.127 -      | elm 1 th = [th]
   1.128 -      | elm n th =
   1.129 -          let val (th1, th2) = elim th
   1.130 -          in th1 :: elm (n - 1) th2 end;
   1.131 -    fun elms (0 :: ns) ths = [] :: elms ns ths
   1.132 -      | elms (n :: ns) (th :: ths) = elm n th :: elms ns ths
   1.133 -      | elms _ _ = [];
   1.134 -  in elms spans o elm (length (filter_out (equal 0) spans)) end;
   1.135 -
   1.136 -end;
   1.137 +fun elim_balanced 0 _ = []
   1.138 +  | elim_balanced n th = BalancedTree.dest elim n th;
   1.139  
   1.140  
   1.141  (* currying *)
   1.142  
   1.143  local
   1.144  
   1.145 -fun conjs m =
   1.146 -  let val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto m)
   1.147 -  in (As, Logic.mk_conjunction_list As) end;
   1.148 +fun conjs n =
   1.149 +  let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n)
   1.150 +  in (As, mk_conjunction_balanced As) end;
   1.151  
   1.152 -val B = Free ("B", propT);
   1.153 +val B = cert (Free ("B", propT));
   1.154  
   1.155  fun comp_rule th rule =
   1.156    Thm.adjust_maxidx_thm ~1 (th COMP
   1.157 @@ -160,64 +151,35 @@
   1.158    -----------------------
   1.159    A1 ==> ... ==> An ==> B
   1.160  *)
   1.161 -fun curry n th =
   1.162 -  let
   1.163 -    val k =
   1.164 -      (case try Logic.dest_implies (Thm.prop_of th) of
   1.165 -        NONE => 0
   1.166 -      | SOME (prem, _) => length (Logic.dest_conjunction_list prem));
   1.167 -    val m = if n = ~1 then k else Int.min (n, k);
   1.168 -  in
   1.169 -    if m < 2 then th
   1.170 -    else
   1.171 -      let
   1.172 -        val (As, C) = conjs m;
   1.173 -        val cAs = map cert As;
   1.174 -        val D = Logic.mk_implies (Logic.mk_conjunction_list As, B) |> cert;
   1.175 -      in
   1.176 -        comp_rule th
   1.177 -          (Thm.implies_elim (Thm.assume D) (intr_list (map Thm.assume cAs))
   1.178 -            |> Drule.implies_intr_list (D :: cAs))
   1.179 -      end
   1.180 -  end;
   1.181 +fun curry_balanced n th =
   1.182 +  if n < 2 then th
   1.183 +  else
   1.184 +    let
   1.185 +      val (As, C) = conjs n;
   1.186 +      val D = Drule.mk_implies (C, B);
   1.187 +    in
   1.188 +      comp_rule th
   1.189 +        (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As))
   1.190 +          |> Drule.implies_intr_list (D :: As))
   1.191 +    end;
   1.192  
   1.193  (*
   1.194    A1 ==> ... ==> An ==> B
   1.195    -----------------------
   1.196 -   A1 && ... && An ==> B
   1.197 +  A1 && ... && An ==> B
   1.198  *)
   1.199 -fun uncurry n th =
   1.200 -  let
   1.201 -    val k = Thm.nprems_of th;
   1.202 -    val m = if n = ~1 then k else Int.min (n, k);
   1.203 -  in
   1.204 -    if m < 2 then th
   1.205 -    else
   1.206 -      let
   1.207 -        val (As, C) = conjs m ||> cert;
   1.208 -        val D = Logic.list_implies (As, B) |> cert;
   1.209 -      in
   1.210 -        comp_rule th
   1.211 -          (Drule.implies_elim_list (Thm.assume D) (elim_list (Thm.assume C))
   1.212 -            |> Drule.implies_intr_list [D, C])
   1.213 -      end
   1.214 -  end;
   1.215 +fun uncurry_balanced n th =
   1.216 +  if n < 2 then th
   1.217 +  else
   1.218 +    let
   1.219 +      val (As, C) = conjs n;
   1.220 +      val D = Drule.list_implies (As, B);
   1.221 +    in
   1.222 +      comp_rule th
   1.223 +        (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C))
   1.224 +          |> Drule.implies_intr_list [D, C])
   1.225 +    end;
   1.226  
   1.227  end;
   1.228  
   1.229 -
   1.230 -(* defined conjunctions *)
   1.231 -
   1.232 -fun project th 1 = (th RS conjunctionD1 handle THM _ => th)
   1.233 -  | project th k = project (th RS conjunctionD2) (k - 1);
   1.234 -
   1.235 -fun split_defined n eq =
   1.236 -  let
   1.237 -    val intro =
   1.238 -      (eq RS Drule.equal_elim_rule2)
   1.239 -      |> curry n
   1.240 -      |> n = 0 ? Thm.eq_assumption 1;
   1.241 -    val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
   1.242 -  in (intro, dests) end;
   1.243 -
   1.244  end;