Meta-level conjunction.
authorwenzelm
Thu Apr 13 12:00:53 2006 +0200 (2006-04-13)
changeset 194164198e7698f6a
parent 19415 38d50affa48f
child 19417 3a9d25bdd7f4
Meta-level conjunction.
src/Pure/conjunction.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/conjunction.ML	Thu Apr 13 12:00:53 2006 +0200
     1.3 @@ -0,0 +1,206 @@
     1.4 +(*  Title:      Pure/conjunction.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Meta-level conjunction.
     1.9 +*)
    1.10 +
    1.11 +signature CONJUNCTION =
    1.12 +sig
    1.13 +  val conjunction: cterm
    1.14 +  val mk_conjunction: cterm * cterm -> cterm
    1.15 +  val dest_conjunction: cterm -> cterm * cterm
    1.16 +  val cong: thm -> thm -> thm
    1.17 +  val conv: int -> (int -> cterm -> thm) -> cterm -> thm
    1.18 +  val conjunctionD1: thm
    1.19 +  val conjunctionD2: thm
    1.20 +  val conjunctionI: thm
    1.21 +  val intr: thm -> thm -> thm
    1.22 +  val intr_list: thm list -> thm
    1.23 +  val elim: thm -> thm * thm
    1.24 +  val elim_list: thm -> thm list
    1.25 +  val elim_precise: int list -> thm -> thm list list
    1.26 +  val curry: int -> thm -> thm
    1.27 +  val uncurry: int -> thm -> thm
    1.28 +  val split_defined: int -> thm -> thm * thm list
    1.29 +end;
    1.30 +
    1.31 +structure Conjunction: CONJUNCTION =
    1.32 +struct
    1.33 +
    1.34 +
    1.35 +(** abstract syntax **)
    1.36 +
    1.37 +fun read s = Thm.read_cterm ProtoPure.thy (s, propT);
    1.38 +val cert = Thm.cterm_of ProtoPure.thy;
    1.39 +
    1.40 +val conjunction = cert Logic.conjunction;
    1.41 +fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
    1.42 +
    1.43 +fun dest_conjunction ct =
    1.44 +  (case Thm.term_of ct of
    1.45 +    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Drule.dest_binop ct
    1.46 +  | _ => raise TERM ("dest_conjunction", [term_of ct]));
    1.47 +
    1.48 +
    1.49 +
    1.50 +(** derived rules **)
    1.51 +
    1.52 +(* conversion *)
    1.53 +
    1.54 +(*rewrite the A's in A1 && ... && An*)
    1.55 +
    1.56 +val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
    1.57 +
    1.58 +fun conv 0 _ = reflexive
    1.59 +  | conv n cv =
    1.60 +      let
    1.61 +        fun cnv i ct =
    1.62 +          if i = n then cv i ct
    1.63 +          else
    1.64 +            (case try dest_conjunction ct of
    1.65 +              NONE => cv i ct
    1.66 +            | SOME (A, B) => cong (cv i A) (cnv (i + 1) B));
    1.67 +      in cnv 1 end;
    1.68 +
    1.69 +
    1.70 +(* intro/elim *)
    1.71 +
    1.72 +local
    1.73 +
    1.74 +val A = read "PROP A";
    1.75 +val B = read "PROP B";
    1.76 +val C = read "PROP C";
    1.77 +val ABC = read "PROP A ==> PROP B ==> PROP C";
    1.78 +val A_B = read "PROP ProtoPure.conjunction(A, B)"
    1.79 +
    1.80 +val conjunction_def = #1 (freeze_thaw ProtoPure.conjunction_def);
    1.81 +
    1.82 +fun conjunctionD which =
    1.83 +  Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
    1.84 +  Drule.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
    1.85 +
    1.86 +in
    1.87 +
    1.88 +val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
    1.89 +val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
    1.90 +
    1.91 +val conjunctionI = Drule.store_standard_thm "conjunctionI"
    1.92 +  (Drule.implies_intr_list [A, B]
    1.93 +    (Thm.equal_elim
    1.94 +      (Thm.symmetric conjunction_def)
    1.95 +      (Thm.forall_intr C (Thm.implies_intr ABC
    1.96 +        (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
    1.97 +
    1.98 +fun intr tha thb = thb COMP (tha COMP Drule.incr_indexes2 tha thb conjunctionI);
    1.99 +
   1.100 +fun intr_list [] = asm_rl
   1.101 +  | intr_list ths = foldr1 (uncurry intr) ths;
   1.102 +
   1.103 +fun elim th =
   1.104 + (th COMP Drule.incr_indexes th conjunctionD1,
   1.105 +  th COMP Drule.incr_indexes th conjunctionD2);
   1.106 +
   1.107 +(*((A && B) && C) && D && E -- flat*)
   1.108 +fun elim_list th =
   1.109 +  let val (th1, th2) = elim th
   1.110 +  in elim_list th1 @ elim_list th2 end handle THM _ => [th];
   1.111 +
   1.112 +(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
   1.113 +fun elim_precise spans =
   1.114 +  let
   1.115 +    fun elm 0 _ = []
   1.116 +      | elm 1 th = [th]
   1.117 +      | elm n th =
   1.118 +          let val (th1, th2) = elim th
   1.119 +          in th1 :: elm (n - 1) th2 end;
   1.120 +    fun elms (0 :: ns) ths = [] :: elms ns ths
   1.121 +      | elms (n :: ns) (th :: ths) = elm n th :: elms ns ths
   1.122 +      | elms _ _ = [];
   1.123 +  in elms spans o elm (length (filter_out (equal 0) spans)) end;
   1.124 +
   1.125 +end;
   1.126 +
   1.127 +
   1.128 +(* currying *)
   1.129 +
   1.130 +local
   1.131 +
   1.132 +fun conjs m =
   1.133 +  let val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto m)
   1.134 +  in (As, Logic.mk_conjunction_list As) end;
   1.135 +
   1.136 +val B = Free ("B", propT);
   1.137 +
   1.138 +fun comp_rule th rule =
   1.139 +  Thm.adjust_maxidx_thm (th COMP
   1.140 +    (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
   1.141 +
   1.142 +in
   1.143 +
   1.144 +(*
   1.145 +   A1 && ... && An ==> B
   1.146 +  -----------------------
   1.147 +  A1 ==> ... ==> An ==> B
   1.148 +*)
   1.149 +fun curry n th =
   1.150 +  let
   1.151 +    val k =
   1.152 +      (case try Logic.dest_implies (Thm.prop_of th) of
   1.153 +        NONE => 0
   1.154 +      | SOME (prem, _) => length (Logic.dest_conjunction_list prem));
   1.155 +    val m = if n = ~1 then k else Int.min (n, k);
   1.156 +  in
   1.157 +    if m < 2 then th
   1.158 +    else
   1.159 +      let
   1.160 +        val (As, C) = conjs m;
   1.161 +        val cAs = map cert As;
   1.162 +        val D = Logic.mk_implies (Logic.mk_conjunction_list As, B) |> cert;
   1.163 +      in
   1.164 +        comp_rule th
   1.165 +          (Thm.implies_elim (Thm.assume D) (intr_list (map Thm.assume cAs))
   1.166 +            |> Drule.implies_intr_list (D :: cAs))
   1.167 +      end
   1.168 +  end;
   1.169 +
   1.170 +(*
   1.171 +  A1 ==> ... ==> An ==> B
   1.172 +  -----------------------
   1.173 +   A1 && ... && An ==> B
   1.174 +*)
   1.175 +fun uncurry n th =
   1.176 +  let
   1.177 +    val k = Thm.nprems_of th;
   1.178 +    val m = if n = ~1 then k else Int.min (n, k);
   1.179 +  in
   1.180 +    if m < 2 then th
   1.181 +    else
   1.182 +      let
   1.183 +        val (As, C) = conjs m ||> cert;
   1.184 +        val D = Logic.list_implies (As, B) |> cert;
   1.185 +      in
   1.186 +        comp_rule th
   1.187 +          (Drule.implies_elim_list (Thm.assume D) (elim_list (Thm.assume C))
   1.188 +            |> Drule.implies_intr_list [D, C])
   1.189 +      end
   1.190 +  end;
   1.191 +
   1.192 +end;
   1.193 +
   1.194 +
   1.195 +(* defined conjunctions *)
   1.196 +
   1.197 +fun project th 1 = (th RS conjunctionD1 handle THM _ => th)
   1.198 +  | project th k = project (th RS conjunctionD2) (k - 1);
   1.199 +
   1.200 +fun split_defined n eq =
   1.201 +  let
   1.202 +    val intro =
   1.203 +      (eq RS Drule.equal_elim_rule2)
   1.204 +      |> curry n
   1.205 +      |> K (n = 0) ? Thm.eq_assumption 1;
   1.206 +    val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
   1.207 +  in (intro, dests) end;
   1.208 +
   1.209 +end;