removed obsolete ML files;
authorwenzelm
Fri Jun 02 18:15:38 2006 +0200 (2006-06-02)
changeset 197615cd82054c2c6
parent 19760 c7e9cc10acc8
child 19762 957bcf55c98f
removed obsolete ML files;
src/CTT/Arith.ML
src/CTT/Arith.thy
src/CTT/Bool.ML
src/CTT/Bool.thy
src/CTT/CTT.ML
src/CTT/CTT.thy
src/CTT/IsaMakefile
src/CTT/README.html
src/CTT/ROOT.ML
src/CTT/ex/Elimination.thy
src/CTT/ex/Equality.thy
src/CTT/ex/ROOT.ML
src/CTT/ex/Synthesis.thy
src/CTT/ex/Typechecking.thy
src/CTT/ex/elim.ML
src/CTT/ex/equal.ML
src/CTT/ex/synth.ML
src/CTT/ex/typechk.ML
src/CTT/rew.ML
     1.1 --- a/src/CTT/Arith.ML	Fri Jun 02 16:06:19 2006 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,422 +0,0 @@
     1.4 -(*  Title:      CTT/Arith.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8 -
     1.9 -Proofs about elementary arithmetic: addition, multiplication, etc.
    1.10 -Tests definitions and simplifier.
    1.11 -*)
    1.12 -
    1.13 -val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def];
    1.14 -
    1.15 -
    1.16 -(** Addition *)
    1.17 -
    1.18 -(*typing of add: short and long versions*)
    1.19 -
    1.20 -Goalw arith_defs "[| a:N;  b:N |] ==> a #+ b : N";
    1.21 -by (typechk_tac []) ;
    1.22 -qed "add_typing";
    1.23 -
    1.24 -Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N";
    1.25 -by (equal_tac []) ;
    1.26 -qed "add_typingL";
    1.27 -
    1.28 -
    1.29 -(*computation for add: 0 and successor cases*)
    1.30 -
    1.31 -Goalw arith_defs "b:N ==> 0 #+ b = b : N";
    1.32 -by (rew_tac []) ;
    1.33 -qed "addC0";
    1.34 -
    1.35 -Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
    1.36 -by (rew_tac []) ;
    1.37 -qed "addC_succ";
    1.38 -
    1.39 -
    1.40 -(** Multiplication *)
    1.41 -
    1.42 -(*typing of mult: short and long versions*)
    1.43 -
    1.44 -Goalw arith_defs "[| a:N;  b:N |] ==> a #* b : N";
    1.45 -by (typechk_tac [add_typing]) ;
    1.46 -qed "mult_typing";
    1.47 -
    1.48 -Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N";
    1.49 -by (equal_tac [add_typingL]) ;
    1.50 -qed "mult_typingL";
    1.51 -
    1.52 -(*computation for mult: 0 and successor cases*)
    1.53 -
    1.54 -Goalw arith_defs "b:N ==> 0 #* b = 0 : N";
    1.55 -by (rew_tac []) ;
    1.56 -qed "multC0";
    1.57 -
    1.58 -Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
    1.59 -by (rew_tac []) ;
    1.60 -qed "multC_succ";
    1.61 -
    1.62 -
    1.63 -(** Difference *)
    1.64 -
    1.65 -(*typing of difference*)
    1.66 -
    1.67 -Goalw arith_defs "[| a:N;  b:N |] ==> a - b : N";
    1.68 -by (typechk_tac []) ;
    1.69 -qed "diff_typing";
    1.70 -
    1.71 -Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a - b = c - d : N";
    1.72 -by (equal_tac []) ;
    1.73 -qed "diff_typingL";
    1.74 -
    1.75 -
    1.76 -
    1.77 -(*computation for difference: 0 and successor cases*)
    1.78 -
    1.79 -Goalw arith_defs "a:N ==> a - 0 = a : N";
    1.80 -by (rew_tac []) ;
    1.81 -qed "diffC0";
    1.82 -
    1.83 -(*Note: rec(a, 0, %z w.z) is pred(a). *)
    1.84 -
    1.85 -Goalw arith_defs "b:N ==> 0 - b = 0 : N";
    1.86 -by (NE_tac "b" 1);
    1.87 -by (hyp_rew_tac []) ;
    1.88 -qed "diff_0_eq_0";
    1.89 -
    1.90 -
    1.91 -(*Essential to simplify FIRST!!  (Else we get a critical pair)
    1.92 -  succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
    1.93 -Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N";
    1.94 -by (hyp_rew_tac []);
    1.95 -by (NE_tac "b" 1);
    1.96 -by (hyp_rew_tac []) ;
    1.97 -qed "diff_succ_succ";
    1.98 -
    1.99 -
   1.100 -
   1.101 -(*** Simplification *)
   1.102 -
   1.103 -val arith_typing_rls =
   1.104 -  [add_typing, mult_typing, diff_typing];
   1.105 -
   1.106 -val arith_congr_rls =
   1.107 -  [add_typingL, mult_typingL, diff_typingL];
   1.108 -
   1.109 -val congr_rls = arith_congr_rls@standard_congr_rls;
   1.110 -
   1.111 -val arithC_rls =
   1.112 -  [addC0, addC_succ,
   1.113 -   multC0, multC_succ,
   1.114 -   diffC0, diff_0_eq_0, diff_succ_succ];
   1.115 -
   1.116 -
   1.117 -structure Arith_simp_data: TSIMP_DATA =
   1.118 -  struct
   1.119 -  val refl              = refl_elem
   1.120 -  val sym               = sym_elem
   1.121 -  val trans             = trans_elem
   1.122 -  val refl_red          = refl_red
   1.123 -  val trans_red         = trans_red
   1.124 -  val red_if_equal      = red_if_equal
   1.125 -  val default_rls       = arithC_rls @ comp_rls
   1.126 -  val routine_tac       = routine_tac (arith_typing_rls @ routine_rls)
   1.127 -  end;
   1.128 -
   1.129 -structure Arith_simp = TSimpFun (Arith_simp_data);
   1.130 -
   1.131 -fun arith_rew_tac prems = make_rew_tac
   1.132 -    (Arith_simp.norm_tac(congr_rls, prems));
   1.133 -
   1.134 -fun hyp_arith_rew_tac prems = make_rew_tac
   1.135 -    (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems));
   1.136 -
   1.137 -
   1.138 -(**********
   1.139 -  Addition
   1.140 - **********)
   1.141 -
   1.142 -(*Associative law for addition*)
   1.143 -Goal "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
   1.144 -by (NE_tac "a" 1);
   1.145 -by (hyp_arith_rew_tac []) ;
   1.146 -qed "add_assoc";
   1.147 -
   1.148 -
   1.149 -(*Commutative law for addition.  Can be proved using three inductions.
   1.150 -  Must simplify after first induction!  Orientation of rewrites is delicate*)
   1.151 -Goal "[| a:N;  b:N |] ==> a #+ b = b #+ a : N";
   1.152 -by (NE_tac "a" 1);
   1.153 -by (hyp_arith_rew_tac []);
   1.154 -by (NE_tac "b" 2);
   1.155 -by (rtac sym_elem 1);
   1.156 -by (NE_tac "b" 1);
   1.157 -by (hyp_arith_rew_tac []) ;
   1.158 -qed "add_commute";
   1.159 -
   1.160 -
   1.161 -(****************
   1.162 -  Multiplication
   1.163 - ****************)
   1.164 -
   1.165 -(*Commutative law for multiplication
   1.166 -Goal "[| a:N;  b:N |] ==> a #* b = b #* a : N";
   1.167 -by (NE_tac "a" 1);
   1.168 -by (hyp_arith_rew_tac []);
   1.169 -by (NE_tac "b" 2);
   1.170 -by (rtac sym_elem 1);
   1.171 -by (NE_tac "b" 1);
   1.172 -by (hyp_arith_rew_tac []) ;
   1.173 -qed "mult_commute";   NEEDS COMMUTATIVE MATCHING
   1.174 -***************)
   1.175 -
   1.176 -(*right annihilation in product*)
   1.177 -Goal "a:N ==> a #* 0 = 0 : N";
   1.178 -by (NE_tac "a" 1);
   1.179 -by (hyp_arith_rew_tac []) ;
   1.180 -qed "mult_0_right";
   1.181 -
   1.182 -(*right successor law for multiplication*)
   1.183 -Goal "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
   1.184 -by (NE_tac "a" 1);
   1.185 -by (hyp_arith_rew_tac [add_assoc RS sym_elem]);
   1.186 -by (REPEAT (assume_tac 1
   1.187 -     ORELSE resolve_tac ([add_commute,mult_typingL,add_typingL]@ intrL_rls@
   1.188 -                         [refl_elem])   1)) ;
   1.189 -qed "mult_succ_right";
   1.190 -
   1.191 -(*Commutative law for multiplication*)
   1.192 -Goal "[| a:N;  b:N |] ==> a #* b = b #* a : N";
   1.193 -by (NE_tac "a" 1);
   1.194 -by (hyp_arith_rew_tac [mult_0_right, mult_succ_right]) ;
   1.195 -qed "mult_commute";
   1.196 -
   1.197 -(*addition distributes over multiplication*)
   1.198 -Goal "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N";
   1.199 -by (NE_tac "a" 1);
   1.200 -by (hyp_arith_rew_tac [add_assoc RS sym_elem]) ;
   1.201 -qed "add_mult_distrib";
   1.202 -
   1.203 -
   1.204 -(*Associative law for multiplication*)
   1.205 -Goal "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
   1.206 -by (NE_tac "a" 1);
   1.207 -by (hyp_arith_rew_tac [add_mult_distrib]) ;
   1.208 -qed "mult_assoc";
   1.209 -
   1.210 -
   1.211 -(************
   1.212 -  Difference
   1.213 - ************
   1.214 -
   1.215 -Difference on natural numbers, without negative numbers
   1.216 -  a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *)
   1.217 -
   1.218 -Goal "a:N ==> a - a = 0 : N";
   1.219 -by (NE_tac "a" 1);
   1.220 -by (hyp_arith_rew_tac []) ;
   1.221 -qed "diff_self_eq_0";
   1.222 -
   1.223 -
   1.224 -(*  [| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N  *)
   1.225 -val add_0_right = addC0 RSN (3, add_commute RS trans_elem);
   1.226 -
   1.227 -(*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
   1.228 -  An example of induction over a quantified formula (a product).
   1.229 -  Uses rewriting with a quantified, implicative inductive hypothesis.*)
   1.230 -Goal "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
   1.231 -by (NE_tac "b" 1);
   1.232 -(*strip one "universal quantifier" but not the "implication"*)
   1.233 -by (resolve_tac intr_rls 3);
   1.234 -(*case analysis on x in
   1.235 -    (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
   1.236 -by (NE_tac "x" 4 THEN assume_tac 4);
   1.237 -(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
   1.238 -by (rtac replace_type 5);
   1.239 -by (rtac replace_type 4);
   1.240 -by (arith_rew_tac []);
   1.241 -(*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
   1.242 -  Both follow by rewriting, (2) using quantified induction hyp*)
   1.243 -by (intr_tac[]);  (*strips remaining PRODs*)
   1.244 -by (hyp_arith_rew_tac [add_0_right]);
   1.245 -by (assume_tac 1);
   1.246 -qed "add_diff_inverse_lemma";
   1.247 -
   1.248 -
   1.249 -(*Version of above with premise   b-a=0   i.e.    a >= b.
   1.250 -  Using ProdE does not work -- for ?B(?a) is ambiguous.
   1.251 -  Instead, add_diff_inverse_lemma states the desired induction scheme;
   1.252 -    the use of RS below instantiates Vars in ProdE automatically. *)
   1.253 -Goal "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N";
   1.254 -by (rtac EqE 1);
   1.255 -by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
   1.256 -by (REPEAT (ares_tac [EqI] 1));
   1.257 -qed "add_diff_inverse";
   1.258 -
   1.259 -
   1.260 -(********************
   1.261 -  Absolute difference
   1.262 - ********************)
   1.263 -
   1.264 -(*typing of absolute difference: short and long versions*)
   1.265 -
   1.266 -Goalw arith_defs "[| a:N;  b:N |] ==> a |-| b : N";
   1.267 -by (typechk_tac []) ;
   1.268 -qed "absdiff_typing";
   1.269 -
   1.270 -Goalw arith_defs "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N";
   1.271 -by (equal_tac []) ;
   1.272 -qed "absdiff_typingL";
   1.273 -
   1.274 -Goalw [absdiff_def] "a:N ==> a |-| a = 0 : N";
   1.275 -by (arith_rew_tac [diff_self_eq_0]) ;
   1.276 -qed "absdiff_self_eq_0";
   1.277 -
   1.278 -Goalw [absdiff_def] "a:N ==> 0 |-| a = a : N";
   1.279 -by (hyp_arith_rew_tac []);
   1.280 -qed "absdiffC0";
   1.281 -
   1.282 -
   1.283 -Goalw [absdiff_def] "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N";
   1.284 -by (hyp_arith_rew_tac []) ;
   1.285 -qed "absdiff_succ_succ";
   1.286 -
   1.287 -(*Note how easy using commutative laws can be?  ...not always... *)
   1.288 -Goalw [absdiff_def] "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
   1.289 -by (rtac add_commute 1);
   1.290 -by (typechk_tac [diff_typing]);
   1.291 -qed "absdiff_commute";
   1.292 -
   1.293 -(*If a+b=0 then a=0.   Surprisingly tedious*)
   1.294 -Goal "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)";
   1.295 -by (NE_tac "a" 1);
   1.296 -by (rtac replace_type 3);
   1.297 -by (arith_rew_tac []);
   1.298 -by (intr_tac[]);  (*strips remaining PRODs*)
   1.299 -by (resolve_tac [ zero_ne_succ RS FE ] 2);
   1.300 -by (etac (EqE RS sym_elem) 3);
   1.301 -by (typechk_tac [add_typing]);
   1.302 -qed "add_eq0_lemma";
   1.303 -
   1.304 -(*Version of above with the premise  a+b=0.
   1.305 -  Again, resolution instantiates variables in ProdE *)
   1.306 -Goal "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N";
   1.307 -by (rtac EqE 1);
   1.308 -by (resolve_tac [add_eq0_lemma RS ProdE] 1);
   1.309 -by (rtac EqI 3);
   1.310 -by (typechk_tac []) ;
   1.311 -qed "add_eq0";
   1.312 -
   1.313 -(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
   1.314 -Goalw [absdiff_def]
   1.315 -    "[| a:N;  b:N;  a |-| b = 0 : N |] ==> \
   1.316 -\    ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)";
   1.317 -by (intr_tac[]);
   1.318 -by eqintr_tac;
   1.319 -by (rtac add_eq0 2);
   1.320 -by (rtac add_eq0 1);
   1.321 -by (resolve_tac [add_commute RS trans_elem] 6);
   1.322 -by (typechk_tac [diff_typing]);
   1.323 -qed "absdiff_eq0_lem";
   1.324 -
   1.325 -(*if  a |-| b = 0  then  a = b
   1.326 -  proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
   1.327 -Goal "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N";
   1.328 -by (rtac EqE 1);
   1.329 -by (resolve_tac [absdiff_eq0_lem RS SumE] 1);
   1.330 -by (TRYALL assume_tac);
   1.331 -by eqintr_tac;
   1.332 -by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
   1.333 -by (rtac EqE 3  THEN  assume_tac 3);
   1.334 -by (hyp_arith_rew_tac [add_0_right]);
   1.335 -qed "absdiff_eq0";
   1.336 -
   1.337 -(***********************
   1.338 -  Remainder and Quotient
   1.339 - ***********************)
   1.340 -
   1.341 -(*typing of remainder: short and long versions*)
   1.342 -
   1.343 -Goalw [mod_def] "[| a:N;  b:N |] ==> a mod b : N";
   1.344 -by (typechk_tac [absdiff_typing]) ;
   1.345 -qed "mod_typing";
   1.346 -
   1.347 -Goalw [mod_def] "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N";
   1.348 -by (equal_tac [absdiff_typingL]) ;
   1.349 -qed "mod_typingL";
   1.350 -
   1.351 -
   1.352 -(*computation for  mod : 0 and successor cases*)
   1.353 -
   1.354 -Goalw [mod_def]   "b:N ==> 0 mod b = 0 : N";
   1.355 -by (rew_tac [absdiff_typing]) ;
   1.356 -qed "modC0";
   1.357 -
   1.358 -Goalw [mod_def]
   1.359 -"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N";
   1.360 -by (rew_tac [absdiff_typing]) ;
   1.361 -qed "modC_succ";
   1.362 -
   1.363 -
   1.364 -(*typing of quotient: short and long versions*)
   1.365 -
   1.366 -Goalw [div_def]   "[| a:N;  b:N |] ==> a div b : N";
   1.367 -by (typechk_tac [absdiff_typing,mod_typing]) ;
   1.368 -qed "div_typing";
   1.369 -
   1.370 -Goalw [div_def] "[| a=c:N;  b=d:N |] ==> a div b = c div d : N";
   1.371 -by (equal_tac [absdiff_typingL, mod_typingL]);
   1.372 -qed "div_typingL";
   1.373 -
   1.374 -val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
   1.375 -
   1.376 -
   1.377 -(*computation for quotient: 0 and successor cases*)
   1.378 -
   1.379 -Goalw [div_def]   "b:N ==> 0 div b = 0 : N";
   1.380 -by (rew_tac [mod_typing, absdiff_typing]) ;
   1.381 -qed "divC0";
   1.382 -
   1.383 -Goalw [div_def]
   1.384 - "[| a:N;  b:N |] ==> succ(a) div b = \
   1.385 -\    rec(succ(a) mod b, succ(a div b), %x y. a div b) : N";
   1.386 -by (rew_tac [mod_typing]) ;
   1.387 -qed "divC_succ";
   1.388 -
   1.389 -
   1.390 -(*Version of above with same condition as the  mod  one*)
   1.391 -Goal "[| a:N;  b:N |] ==> \
   1.392 -\    succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N";
   1.393 -by (resolve_tac [ divC_succ RS trans_elem ] 1);
   1.394 -by (rew_tac(div_typing_rls @ [modC_succ]));
   1.395 -by (NE_tac "succ(a mod b)|-|b" 1);
   1.396 -by (rew_tac [mod_typing, div_typing, absdiff_typing]);
   1.397 -qed "divC_succ2";
   1.398 -
   1.399 -(*for case analysis on whether a number is 0 or a successor*)
   1.400 -Goal "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
   1.401 -\                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))";
   1.402 -by (NE_tac "a" 1);
   1.403 -by (rtac PlusI_inr 3);
   1.404 -by (rtac PlusI_inl 2);
   1.405 -by eqintr_tac;
   1.406 -by (equal_tac []) ;
   1.407 -qed "iszero_decidable";
   1.408 -
   1.409 -(*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   1.410 -Goal "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N";
   1.411 -by (NE_tac "a" 1);
   1.412 -by (arith_rew_tac (div_typing_rls@[modC0,modC_succ,divC0,divC_succ2]));
   1.413 -by (rtac EqE 1);
   1.414 -(*case analysis on   succ(u mod b)|-|b  *)
   1.415 -by (res_inst_tac [("a1", "succ(u mod b) |-| b")]
   1.416 -                 (iszero_decidable RS PlusE) 1);
   1.417 -by (etac SumE 3);
   1.418 -by (hyp_arith_rew_tac (div_typing_rls @
   1.419 -        [modC0,modC_succ, divC0, divC_succ2]));
   1.420 -(*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
   1.421 -by (resolve_tac [ add_typingL RS trans_elem ] 1);
   1.422 -by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
   1.423 -by (rtac refl_elem 3);
   1.424 -by (hyp_arith_rew_tac (div_typing_rls));
   1.425 -qed "mod_div_equality";
     2.1 --- a/src/CTT/Arith.thy	Fri Jun 02 16:06:19 2006 +0200
     2.2 +++ b/src/CTT/Arith.thy	Fri Jun 02 18:15:38 2006 +0200
     2.3 @@ -4,16 +4,13 @@
     2.4      Copyright   1991  University of Cambridge
     2.5  *)
     2.6  
     2.7 -header {* Arithmetic operators and their definitions *}
     2.8 +header {* Elementary arithmetic *}
     2.9  
    2.10  theory Arith
    2.11  imports Bool
    2.12  begin
    2.13  
    2.14 -text {*
    2.15 -  Proves about elementary arithmetic: addition, multiplication, etc.
    2.16 -  Tests definitions and simplifier.
    2.17 -*}
    2.18 +subsection {* Arithmetic operators and their definitions *}
    2.19  
    2.20  consts
    2.21    "#+"  :: "[i,i]=>i"   (infixr 65)
    2.22 @@ -37,6 +34,426 @@
    2.23    mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
    2.24    div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
    2.25  
    2.26 -ML {* use_legacy_bindings (the_context ()) *}
    2.27 +lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
    2.28 +
    2.29 +
    2.30 +subsection {* Proofs about elementary arithmetic: addition, multiplication, etc. *}
    2.31 +
    2.32 +(** Addition *)
    2.33 +
    2.34 +(*typing of add: short and long versions*)
    2.35 +
    2.36 +lemma add_typing: "[| a:N;  b:N |] ==> a #+ b : N"
    2.37 +apply (unfold arith_defs)
    2.38 +apply (tactic "typechk_tac []")
    2.39 +done
    2.40 +
    2.41 +lemma add_typingL: "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
    2.42 +apply (unfold arith_defs)
    2.43 +apply (tactic "equal_tac []")
    2.44 +done
    2.45 +
    2.46 +
    2.47 +(*computation for add: 0 and successor cases*)
    2.48 +
    2.49 +lemma addC0: "b:N ==> 0 #+ b = b : N"
    2.50 +apply (unfold arith_defs)
    2.51 +apply (tactic "rew_tac []")
    2.52 +done
    2.53 +
    2.54 +lemma addC_succ: "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
    2.55 +apply (unfold arith_defs)
    2.56 +apply (tactic "rew_tac []")
    2.57 +done
    2.58 +
    2.59 +
    2.60 +(** Multiplication *)
    2.61 +
    2.62 +(*typing of mult: short and long versions*)
    2.63 +
    2.64 +lemma mult_typing: "[| a:N;  b:N |] ==> a #* b : N"
    2.65 +apply (unfold arith_defs)
    2.66 +apply (tactic {* typechk_tac [thm "add_typing"] *})
    2.67 +done
    2.68 +
    2.69 +lemma mult_typingL: "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
    2.70 +apply (unfold arith_defs)
    2.71 +apply (tactic {* equal_tac [thm "add_typingL"] *})
    2.72 +done
    2.73 +
    2.74 +(*computation for mult: 0 and successor cases*)
    2.75 +
    2.76 +lemma multC0: "b:N ==> 0 #* b = 0 : N"
    2.77 +apply (unfold arith_defs)
    2.78 +apply (tactic "rew_tac []")
    2.79 +done
    2.80 +
    2.81 +lemma multC_succ: "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
    2.82 +apply (unfold arith_defs)
    2.83 +apply (tactic "rew_tac []")
    2.84 +done
    2.85 +
    2.86 +
    2.87 +(** Difference *)
    2.88 +
    2.89 +(*typing of difference*)
    2.90 +
    2.91 +lemma diff_typing: "[| a:N;  b:N |] ==> a - b : N"
    2.92 +apply (unfold arith_defs)
    2.93 +apply (tactic "typechk_tac []")
    2.94 +done
    2.95 +
    2.96 +lemma diff_typingL: "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
    2.97 +apply (unfold arith_defs)
    2.98 +apply (tactic "equal_tac []")
    2.99 +done
   2.100 +
   2.101 +
   2.102 +(*computation for difference: 0 and successor cases*)
   2.103 +
   2.104 +lemma diffC0: "a:N ==> a - 0 = a : N"
   2.105 +apply (unfold arith_defs)
   2.106 +apply (tactic "rew_tac []")
   2.107 +done
   2.108 +
   2.109 +(*Note: rec(a, 0, %z w.z) is pred(a). *)
   2.110 +
   2.111 +lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
   2.112 +apply (unfold arith_defs)
   2.113 +apply (tactic {* NE_tac "b" 1 *})
   2.114 +apply (tactic "hyp_rew_tac []")
   2.115 +done
   2.116 +
   2.117 +
   2.118 +(*Essential to simplify FIRST!!  (Else we get a critical pair)
   2.119 +  succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
   2.120 +lemma diff_succ_succ: "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
   2.121 +apply (unfold arith_defs)
   2.122 +apply (tactic "hyp_rew_tac []")
   2.123 +apply (tactic {* NE_tac "b" 1 *})
   2.124 +apply (tactic "hyp_rew_tac []")
   2.125 +done
   2.126 +
   2.127 +
   2.128 +subsection {* Simplification *}
   2.129 +
   2.130 +lemmas arith_typing_rls = add_typing mult_typing diff_typing
   2.131 +  and arith_congr_rls = add_typingL mult_typingL diff_typingL
   2.132 +lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls
   2.133 +
   2.134 +lemmas arithC_rls =
   2.135 +  addC0 addC_succ
   2.136 +  multC0 multC_succ
   2.137 +  diffC0 diff_0_eq_0 diff_succ_succ
   2.138 +
   2.139 +ML {*
   2.140 +
   2.141 +structure Arith_simp_data: TSIMP_DATA =
   2.142 +  struct
   2.143 +  val refl              = thm "refl_elem"
   2.144 +  val sym               = thm "sym_elem"
   2.145 +  val trans             = thm "trans_elem"
   2.146 +  val refl_red          = thm "refl_red"
   2.147 +  val trans_red         = thm "trans_red"
   2.148 +  val red_if_equal      = thm "red_if_equal"
   2.149 +  val default_rls       = thms "arithC_rls" @ thms "comp_rls"
   2.150 +  val routine_tac       = routine_tac (thms "arith_typing_rls" @ thms "routine_rls")
   2.151 +  end
   2.152 +
   2.153 +structure Arith_simp = TSimpFun (Arith_simp_data)
   2.154 +
   2.155 +local val congr_rls = thms "congr_rls" in
   2.156 +
   2.157 +fun arith_rew_tac prems = make_rew_tac
   2.158 +    (Arith_simp.norm_tac(congr_rls, prems))
   2.159 +
   2.160 +fun hyp_arith_rew_tac prems = make_rew_tac
   2.161 +    (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems))
   2.162  
   2.163  end
   2.164 +*}
   2.165 +
   2.166 +
   2.167 +subsection {* Addition *}
   2.168 +
   2.169 +(*Associative law for addition*)
   2.170 +lemma add_assoc: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
   2.171 +apply (tactic {* NE_tac "a" 1 *})
   2.172 +apply (tactic "hyp_arith_rew_tac []")
   2.173 +done
   2.174 +
   2.175 +
   2.176 +(*Commutative law for addition.  Can be proved using three inductions.
   2.177 +  Must simplify after first induction!  Orientation of rewrites is delicate*)
   2.178 +lemma add_commute: "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
   2.179 +apply (tactic {* NE_tac "a" 1 *})
   2.180 +apply (tactic "hyp_arith_rew_tac []")
   2.181 +apply (tactic {* NE_tac "b" 2 *})
   2.182 +apply (rule sym_elem)
   2.183 +apply (tactic {* NE_tac "b" 1 *})
   2.184 +apply (tactic "hyp_arith_rew_tac []")
   2.185 +done
   2.186 +
   2.187 +
   2.188 +subsection {* Multiplication *}
   2.189 +
   2.190 +(*right annihilation in product*)
   2.191 +lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
   2.192 +apply (tactic {* NE_tac "a" 1 *})
   2.193 +apply (tactic "hyp_arith_rew_tac []")
   2.194 +done
   2.195 +
   2.196 +(*right successor law for multiplication*)
   2.197 +lemma mult_succ_right: "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
   2.198 +apply (tactic {* NE_tac "a" 1 *})
   2.199 +apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
   2.200 +apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
   2.201 +done
   2.202 +
   2.203 +(*Commutative law for multiplication*)
   2.204 +lemma mult_commute: "[| a:N;  b:N |] ==> a #* b = b #* a : N"
   2.205 +apply (tactic {* NE_tac "a" 1 *})
   2.206 +apply (tactic {* hyp_arith_rew_tac [thm "mult_0_right", thm "mult_succ_right"] *})
   2.207 +done
   2.208 +
   2.209 +(*addition distributes over multiplication*)
   2.210 +lemma add_mult_distrib: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
   2.211 +apply (tactic {* NE_tac "a" 1 *})
   2.212 +apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
   2.213 +done
   2.214 +
   2.215 +(*Associative law for multiplication*)
   2.216 +lemma mult_assoc: "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
   2.217 +apply (tactic {* NE_tac "a" 1 *})
   2.218 +apply (tactic {* hyp_arith_rew_tac [thm "add_mult_distrib"] *})
   2.219 +done
   2.220 +
   2.221 +
   2.222 +subsection {* Difference *}
   2.223 +
   2.224 +text {*
   2.225 +Difference on natural numbers, without negative numbers
   2.226 +  a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *}
   2.227 +
   2.228 +lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
   2.229 +apply (tactic {* NE_tac "a" 1 *})
   2.230 +apply (tactic "hyp_arith_rew_tac []")
   2.231 +done
   2.232 +
   2.233 +
   2.234 +lemma add_0_right: "[| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N"
   2.235 +  by (rule addC0 [THEN [3] add_commute [THEN trans_elem]])
   2.236 +
   2.237 +(*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
   2.238 +  An example of induction over a quantified formula (a product).
   2.239 +  Uses rewriting with a quantified, implicative inductive hypothesis.*)
   2.240 +lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
   2.241 +apply (tactic {* NE_tac "b" 1 *})
   2.242 +(*strip one "universal quantifier" but not the "implication"*)
   2.243 +apply (rule_tac [3] intr_rls)
   2.244 +(*case analysis on x in
   2.245 +    (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
   2.246 +apply (tactic {* NE_tac "x" 4 *}, tactic "assume_tac 4")
   2.247 +(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
   2.248 +apply (rule_tac [5] replace_type)
   2.249 +apply (rule_tac [4] replace_type)
   2.250 +apply (tactic "arith_rew_tac []")
   2.251 +(*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
   2.252 +  Both follow by rewriting, (2) using quantified induction hyp*)
   2.253 +apply (tactic "intr_tac []") (*strips remaining PRODs*)
   2.254 +apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
   2.255 +apply assumption
   2.256 +done
   2.257 +
   2.258 +
   2.259 +(*Version of above with premise   b-a=0   i.e.    a >= b.
   2.260 +  Using ProdE does not work -- for ?B(?a) is ambiguous.
   2.261 +  Instead, add_diff_inverse_lemma states the desired induction scheme
   2.262 +    the use of RS below instantiates Vars in ProdE automatically. *)
   2.263 +lemma add_diff_inverse: "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N"
   2.264 +apply (rule EqE)
   2.265 +apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE])
   2.266 +apply (assumption | rule EqI)+
   2.267 +done
   2.268 +
   2.269 +
   2.270 +subsection {* Absolute difference *}
   2.271 +
   2.272 +(*typing of absolute difference: short and long versions*)
   2.273 +
   2.274 +lemma absdiff_typing: "[| a:N;  b:N |] ==> a |-| b : N"
   2.275 +apply (unfold arith_defs)
   2.276 +apply (tactic "typechk_tac []")
   2.277 +done
   2.278 +
   2.279 +lemma absdiff_typingL: "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
   2.280 +apply (unfold arith_defs)
   2.281 +apply (tactic "equal_tac []")
   2.282 +done
   2.283 +
   2.284 +lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
   2.285 +apply (unfold absdiff_def)
   2.286 +apply (tactic {* arith_rew_tac [thm "diff_self_eq_0"] *})
   2.287 +done
   2.288 +
   2.289 +lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
   2.290 +apply (unfold absdiff_def)
   2.291 +apply (tactic "hyp_arith_rew_tac []")
   2.292 +done
   2.293 +
   2.294 +
   2.295 +lemma absdiff_succ_succ: "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
   2.296 +apply (unfold absdiff_def)
   2.297 +apply (tactic "hyp_arith_rew_tac []")
   2.298 +done
   2.299 +
   2.300 +(*Note how easy using commutative laws can be?  ...not always... *)
   2.301 +lemma absdiff_commute: "[| a:N;  b:N |] ==> a |-| b = b |-| a : N"
   2.302 +apply (unfold absdiff_def)
   2.303 +apply (rule add_commute)
   2.304 +apply (tactic {* typechk_tac [thm "diff_typing"] *})
   2.305 +done
   2.306 +
   2.307 +(*If a+b=0 then a=0.   Surprisingly tedious*)
   2.308 +lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
   2.309 +apply (tactic {* NE_tac "a" 1 *})
   2.310 +apply (rule_tac [3] replace_type)
   2.311 +apply (tactic "arith_rew_tac []")
   2.312 +apply (tactic "intr_tac []") (*strips remaining PRODs*)
   2.313 +apply (rule_tac [2] zero_ne_succ [THEN FE])
   2.314 +apply (erule_tac [3] EqE [THEN sym_elem])
   2.315 +apply (tactic {* typechk_tac [thm "add_typing"] *})
   2.316 +done
   2.317 +
   2.318 +(*Version of above with the premise  a+b=0.
   2.319 +  Again, resolution instantiates variables in ProdE *)
   2.320 +lemma add_eq0: "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N"
   2.321 +apply (rule EqE)
   2.322 +apply (rule add_eq0_lemma [THEN ProdE])
   2.323 +apply (rule_tac [3] EqI)
   2.324 +apply (tactic "typechk_tac []")
   2.325 +done
   2.326 +
   2.327 +(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
   2.328 +lemma absdiff_eq0_lem:
   2.329 +    "[| a:N;  b:N;  a |-| b = 0 : N |] ==>
   2.330 +     ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
   2.331 +apply (unfold absdiff_def)
   2.332 +apply (tactic "intr_tac []")
   2.333 +apply (tactic eqintr_tac)
   2.334 +apply (rule_tac [2] add_eq0)
   2.335 +apply (rule add_eq0)
   2.336 +apply (rule_tac [6] add_commute [THEN trans_elem])
   2.337 +apply (tactic {* typechk_tac [thm "diff_typing"] *})
   2.338 +done
   2.339 +
   2.340 +(*if  a |-| b = 0  then  a = b
   2.341 +  proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
   2.342 +lemma absdiff_eq0: "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N"
   2.343 +apply (rule EqE)
   2.344 +apply (rule absdiff_eq0_lem [THEN SumE])
   2.345 +apply (tactic "TRYALL assume_tac")
   2.346 +apply (tactic eqintr_tac)
   2.347 +apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
   2.348 +apply (rule_tac [3] EqE, tactic "assume_tac 3")
   2.349 +apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
   2.350 +done
   2.351 +
   2.352 +
   2.353 +subsection {* Remainder and Quotient *}
   2.354 +
   2.355 +(*typing of remainder: short and long versions*)
   2.356 +
   2.357 +lemma mod_typing: "[| a:N;  b:N |] ==> a mod b : N"
   2.358 +apply (unfold mod_def)
   2.359 +apply (tactic {* typechk_tac [thm "absdiff_typing"] *})
   2.360 +done
   2.361 +
   2.362 +lemma mod_typingL: "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
   2.363 +apply (unfold mod_def)
   2.364 +apply (tactic {* equal_tac [thm "absdiff_typingL"] *})
   2.365 +done
   2.366 +
   2.367 +
   2.368 +(*computation for  mod : 0 and successor cases*)
   2.369 +
   2.370 +lemma modC0: "b:N ==> 0 mod b = 0 : N"
   2.371 +apply (unfold mod_def)
   2.372 +apply (tactic {* rew_tac [thm "absdiff_typing"] *})
   2.373 +done
   2.374 +
   2.375 +lemma modC_succ:
   2.376 +"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
   2.377 +apply (unfold mod_def)
   2.378 +apply (tactic {* rew_tac [thm "absdiff_typing"] *})
   2.379 +done
   2.380 +
   2.381 +
   2.382 +(*typing of quotient: short and long versions*)
   2.383 +
   2.384 +lemma div_typing: "[| a:N;  b:N |] ==> a div b : N"
   2.385 +apply (unfold div_def)
   2.386 +apply (tactic {* typechk_tac [thm "absdiff_typing", thm "mod_typing"] *})
   2.387 +done
   2.388 +
   2.389 +lemma div_typingL: "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
   2.390 +apply (unfold div_def)
   2.391 +apply (tactic {* equal_tac [thm "absdiff_typingL", thm "mod_typingL"] *})
   2.392 +done
   2.393 +
   2.394 +lemmas div_typing_rls = mod_typing div_typing absdiff_typing
   2.395 +
   2.396 +
   2.397 +(*computation for quotient: 0 and successor cases*)
   2.398 +
   2.399 +lemma divC0: "b:N ==> 0 div b = 0 : N"
   2.400 +apply (unfold div_def)
   2.401 +apply (tactic {* rew_tac [thm "mod_typing", thm "absdiff_typing"] *})
   2.402 +done
   2.403 +
   2.404 +lemma divC_succ:
   2.405 + "[| a:N;  b:N |] ==> succ(a) div b =
   2.406 +     rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
   2.407 +apply (unfold div_def)
   2.408 +apply (tactic {* rew_tac [thm "mod_typing"] *})
   2.409 +done
   2.410 +
   2.411 +
   2.412 +(*Version of above with same condition as the  mod  one*)
   2.413 +lemma divC_succ2: "[| a:N;  b:N |] ==>
   2.414 +     succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
   2.415 +apply (rule divC_succ [THEN trans_elem])
   2.416 +apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *})
   2.417 +apply (tactic {* NE_tac "succ (a mod b) |-|b" 1 *})
   2.418 +apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
   2.419 +done
   2.420 +
   2.421 +(*for case analysis on whether a number is 0 or a successor*)
   2.422 +lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) :
   2.423 +                      Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
   2.424 +apply (tactic {* NE_tac "a" 1 *})
   2.425 +apply (rule_tac [3] PlusI_inr)
   2.426 +apply (rule_tac [2] PlusI_inl)
   2.427 +apply (tactic eqintr_tac)
   2.428 +apply (tactic "equal_tac []")
   2.429 +done
   2.430 +
   2.431 +(*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   2.432 +lemma mod_div_equality: "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N"
   2.433 +apply (tactic {* NE_tac "a" 1 *})
   2.434 +apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
   2.435 +  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
   2.436 +apply (rule EqE)
   2.437 +(*case analysis on   succ(u mod b)|-|b  *)
   2.438 +apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
   2.439 +apply (erule_tac [3] SumE)
   2.440 +apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls" @
   2.441 +  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
   2.442 +(*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
   2.443 +apply (rule add_typingL [THEN trans_elem])
   2.444 +apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
   2.445 +apply (rule_tac [3] refl_elem)
   2.446 +apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls") *})
   2.447 +done
   2.448 +
   2.449 +end
     3.1 --- a/src/CTT/Bool.ML	Fri Jun 02 16:06:19 2006 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,58 +0,0 @@
     3.4 -(*  Title:      CTT/Bool
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1991  University of Cambridge
     3.8 -*)
     3.9 -
    3.10 -val bool_defs = [Bool_def,true_def,false_def,cond_def];
    3.11 -
    3.12 -(*Derivation of rules for the type Bool*)
    3.13 -
    3.14 -(*formation rule*)
    3.15 -Goalw bool_defs "Bool type";
    3.16 -by (typechk_tac []) ;
    3.17 -qed "boolF";
    3.18 -
    3.19 -
    3.20 -(*introduction rules for true, false*)
    3.21 -
    3.22 -Goalw bool_defs "true : Bool";
    3.23 -by (typechk_tac []) ;
    3.24 -qed "boolI_true";
    3.25 -
    3.26 -Goalw bool_defs "false : Bool";
    3.27 -by (typechk_tac []) ;
    3.28 -qed "boolI_false";
    3.29 -
    3.30 -(*elimination rule: typing of cond*)
    3.31 -Goalw bool_defs
    3.32 -    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)";
    3.33 -by (typechk_tac []);
    3.34 -by (ALLGOALS (etac TE));
    3.35 -by (typechk_tac []) ;
    3.36 -qed "boolE";
    3.37 -
    3.38 -Goalw bool_defs
    3.39 -    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] \
    3.40 -\    ==> cond(p,a,b) = cond(q,c,d) : C(p)";
    3.41 -by (rtac PlusEL 1);
    3.42 -by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ;
    3.43 -qed "boolEL";
    3.44 -
    3.45 -(*computation rules for true, false*)
    3.46 -
    3.47 -Goalw bool_defs
    3.48 -    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)";
    3.49 -by (resolve_tac comp_rls 1);
    3.50 -by (typechk_tac []);
    3.51 -by (ALLGOALS (etac TE));
    3.52 -by (typechk_tac []) ;
    3.53 -qed "boolC_true";
    3.54 -
    3.55 -Goalw bool_defs
    3.56 -    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)";
    3.57 -by (resolve_tac comp_rls 1);
    3.58 -by (typechk_tac []);
    3.59 -by (ALLGOALS (etac TE));
    3.60 -by (typechk_tac []) ;
    3.61 -qed "boolC_false";
     4.1 --- a/src/CTT/Bool.thy	Fri Jun 02 16:06:19 2006 +0200
     4.2 +++ b/src/CTT/Bool.thy	Fri Jun 02 18:15:38 2006 +0200
     4.3 @@ -8,20 +8,80 @@
     4.4  
     4.5  theory Bool
     4.6  imports CTT
     4.7 -uses "~~/src/Provers/typedsimp.ML" "rew.ML"
     4.8  begin
     4.9  
    4.10 -consts
    4.11 -  Bool        :: "t"
    4.12 -  true        :: "i"
    4.13 -  false       :: "i"
    4.14 -  cond        :: "[i,i,i]=>i"
    4.15 -defs
    4.16 -  Bool_def:   "Bool == T+T"
    4.17 -  true_def:   "true == inl(tt)"
    4.18 -  false_def:  "false == inr(tt)"
    4.19 -  cond_def:   "cond(a,b,c) == when(a, %u. b, %u. c)"
    4.20 +constdefs
    4.21 +  Bool :: "t"
    4.22 +  "Bool == T+T"
    4.23 +
    4.24 +  true :: "i"
    4.25 +  "true == inl(tt)"
    4.26 +
    4.27 +  false :: "i"
    4.28 +  "false == inr(tt)"
    4.29 +
    4.30 +  cond :: "[i,i,i]=>i"
    4.31 +  "cond(a,b,c) == when(a, %u. b, %u. c)"
    4.32 +
    4.33 +lemmas bool_defs = Bool_def true_def false_def cond_def
    4.34 +
    4.35 +
    4.36 +subsection {* Derivation of rules for the type Bool *}
    4.37 +
    4.38 +(*formation rule*)
    4.39 +lemma boolF: "Bool type"
    4.40 +apply (unfold bool_defs)
    4.41 +apply (tactic "typechk_tac []")
    4.42 +done
    4.43 +
    4.44 +
    4.45 +(*introduction rules for true, false*)
    4.46 +
    4.47 +lemma boolI_true: "true : Bool"
    4.48 +apply (unfold bool_defs)
    4.49 +apply (tactic "typechk_tac []")
    4.50 +done
    4.51 +
    4.52 +lemma boolI_false: "false : Bool"
    4.53 +apply (unfold bool_defs)
    4.54 +apply (tactic "typechk_tac []")
    4.55 +done
    4.56  
    4.57 -ML {* use_legacy_bindings (the_context ()) *}
    4.58 +(*elimination rule: typing of cond*)
    4.59 +lemma boolE: 
    4.60 +    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
    4.61 +apply (unfold bool_defs)
    4.62 +apply (tactic "typechk_tac []")
    4.63 +apply (erule_tac [!] TE)
    4.64 +apply (tactic "typechk_tac []")
    4.65 +done
    4.66 +
    4.67 +lemma boolEL: 
    4.68 +    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]  
    4.69 +     ==> cond(p,a,b) = cond(q,c,d) : C(p)"
    4.70 +apply (unfold bool_defs)
    4.71 +apply (rule PlusEL)
    4.72 +apply (erule asm_rl refl_elem [THEN TEL])+
    4.73 +done
    4.74 +
    4.75 +(*computation rules for true, false*)
    4.76 +
    4.77 +lemma boolC_true: 
    4.78 +    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
    4.79 +apply (unfold bool_defs)
    4.80 +apply (rule comp_rls)
    4.81 +apply (tactic "typechk_tac []")
    4.82 +apply (erule_tac [!] TE)
    4.83 +apply (tactic "typechk_tac []")
    4.84 +done
    4.85 +
    4.86 +lemma boolC_false: 
    4.87 +    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
    4.88 +apply (unfold bool_defs)
    4.89 +apply (rule comp_rls)
    4.90 +apply (tactic "typechk_tac []")
    4.91 +apply (erule_tac [!] TE)
    4.92 +apply (tactic "typechk_tac []")
    4.93 +done
    4.94  
    4.95  end
     5.1 --- a/src/CTT/CTT.ML	Fri Jun 02 16:06:19 2006 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,189 +0,0 @@
     5.4 -(*  Title:      CTT/CTT.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1991  University of Cambridge
     5.8 -
     5.9 -Tactics and derived rules for Constructive Type Theory
    5.10 -*)
    5.11 -
    5.12 -(*Formation rules*)
    5.13 -val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
    5.14 -and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
    5.15 -
    5.16 -
    5.17 -(*Introduction rules
    5.18 -  OMITTED: EqI, because its premise is an eqelem, not an elem*)
    5.19 -val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
    5.20 -and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];
    5.21 -
    5.22 -
    5.23 -(*Elimination rules
    5.24 -  OMITTED: EqE, because its conclusion is an eqelem,  not an elem
    5.25 -           TE, because it does not involve a constructor *)
    5.26 -val elim_rls = [NE, ProdE, SumE, PlusE, FE]
    5.27 -and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];
    5.28 -
    5.29 -(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
    5.30 -val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];
    5.31 -
    5.32 -(*rules with conclusion a:A, an elem judgement*)
    5.33 -val element_rls = intr_rls @ elim_rls;
    5.34 -
    5.35 -(*Definitions are (meta)equality axioms*)
    5.36 -val basic_defs = [fst_def,snd_def];
    5.37 -
    5.38 -(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
    5.39 -Goal "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
    5.40 -by (rtac sym_elem 1);
    5.41 -by (rtac SumIL 1);
    5.42 -by (ALLGOALS (rtac sym_elem ));
    5.43 -by (ALLGOALS assume_tac) ;
    5.44 -qed "SumIL2";
    5.45 -
    5.46 -val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
    5.47 -
    5.48 -(*Exploit p:Prod(A,B) to create the assumption z:B(a).
    5.49 -  A more natural form of product elimination. *)
    5.50 -val prems = Goal "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
    5.51 -\    |] ==> c(p`a): C(p`a)";
    5.52 -by (REPEAT (resolve_tac (ProdE::prems) 1)) ;
    5.53 -qed "subst_prodE";
    5.54 -
    5.55 -(** Tactics for type checking **)
    5.56 -
    5.57 -fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
    5.58 -  | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
    5.59 -  | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
    5.60 -  | is_rigid_elem _ = false;
    5.61 -
    5.62 -(*Try solving a:A or a=b:A by assumption provided a is rigid!*)
    5.63 -val test_assume_tac = SUBGOAL(fn (prem,i) =>
    5.64 -    if is_rigid_elem (Logic.strip_assums_concl prem)
    5.65 -    then  assume_tac i  else  no_tac);
    5.66 -
    5.67 -fun ASSUME tf i = test_assume_tac i  ORELSE  tf i;
    5.68 -
    5.69 -
    5.70 -(*For simplification: type formation and checking,
    5.71 -  but no equalities between terms*)
    5.72 -val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;
    5.73 -
    5.74 -fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
    5.75 -
    5.76 -
    5.77 -(*Solve all subgoals "A type" using formation rules. *)
    5.78 -val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
    5.79 -
    5.80 -
    5.81 -(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
    5.82 -fun typechk_tac thms =
    5.83 -  let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
    5.84 -  in  REPEAT_FIRST (ASSUME tac)  end;
    5.85 -
    5.86 -
    5.87 -(*Solve a:A (a flexible, A rigid) by introduction rules.
    5.88 -  Cannot use stringtrees (filt_resolve_tac) since
    5.89 -  goals like ?a:SUM(A,B) have a trivial head-string *)
    5.90 -fun intr_tac thms =
    5.91 -  let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
    5.92 -  in  REPEAT_FIRST (ASSUME tac)  end;
    5.93 -
    5.94 -
    5.95 -(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
    5.96 -fun equal_tac thms =
    5.97 -  let val rls = thms @ form_rls @ element_rls @ intrL_rls @
    5.98 -                elimL_rls @ [refl_elem]
    5.99 -  in  REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3))  end;
   5.100 -
   5.101 -(*** Simplification ***)
   5.102 -
   5.103 -(*To simplify the type in a goal*)
   5.104 -Goal "[| B = A;  a : A |] ==> a : B";
   5.105 -by (rtac equal_types 1);
   5.106 -by (rtac sym_type 2);
   5.107 -by (ALLGOALS assume_tac) ;
   5.108 -qed "replace_type";
   5.109 -
   5.110 -(*Simplify the parameter of a unary type operator.*)
   5.111 -val prems = Goal
   5.112 -     "[| a=c : A;  !!z. z:A ==> B(z) type |] ==> B(a)=B(c)";
   5.113 -by (rtac subst_typeL 1);
   5.114 -by (rtac refl_type 2);
   5.115 -by (ALLGOALS (resolve_tac prems));
   5.116 -by (assume_tac 1) ;
   5.117 -qed "subst_eqtyparg";
   5.118 -
   5.119 -(*Make a reduction rule for simplification.
   5.120 -  A goal a=c becomes b=c, by virtue of a=b *)
   5.121 -fun resolve_trans rl = rl RS trans_elem;
   5.122 -
   5.123 -(*Simplification rules for Constructive Type Theory*)
   5.124 -val reduction_rls = map resolve_trans comp_rls;
   5.125 -
   5.126 -(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
   5.127 -  Uses other intro rules to avoid changing flexible goals.*)
   5.128 -val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));
   5.129 -
   5.130 -(** Tactics that instantiate CTT-rules.
   5.131 -    Vars in the given terms will be incremented!
   5.132 -    The (rtac EqE i) lets them apply to equality judgements. **)
   5.133 -
   5.134 -fun NE_tac (sp: string) i =
   5.135 -  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;
   5.136 -
   5.137 -fun SumE_tac (sp: string) i =
   5.138 -  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;
   5.139 -
   5.140 -fun PlusE_tac (sp: string) i =
   5.141 -  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
   5.142 -
   5.143 -(** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
   5.144 -
   5.145 -(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
   5.146 -fun add_mp_tac i =
   5.147 -    rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i;
   5.148 -
   5.149 -(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   5.150 -fun mp_tac i = etac subst_prodE i  THEN  assume_tac i;
   5.151 -
   5.152 -(*"safe" when regarded as predicate calculus rules*)
   5.153 -val safe_brls = sort (make_ord lessb)
   5.154 -    [ (true,FE), (true,asm_rl),
   5.155 -      (false,ProdI), (true,SumE), (true,PlusE) ];
   5.156 -
   5.157 -val unsafe_brls =
   5.158 -    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
   5.159 -      (true,subst_prodE) ];
   5.160 -
   5.161 -(*0 subgoals vs 1 or more*)
   5.162 -val (safe0_brls, safep_brls) =
   5.163 -    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
   5.164 -
   5.165 -fun safestep_tac thms i =
   5.166 -    form_tac  ORELSE
   5.167 -    resolve_tac thms i  ORELSE
   5.168 -    biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
   5.169 -    DETERM (biresolve_tac safep_brls i);
   5.170 -
   5.171 -fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i);
   5.172 -
   5.173 -fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls;
   5.174 -
   5.175 -(*Fails unless it solves the goal!*)
   5.176 -fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);
   5.177 -
   5.178 -(** The elimination rules for fst/snd **)
   5.179 -
   5.180 -Goalw basic_defs "p : Sum(A,B) ==> fst(p) : A";
   5.181 -by (etac SumE 1);
   5.182 -by (assume_tac 1);
   5.183 -qed "SumE_fst";
   5.184 -
   5.185 -(*The first premise must be p:Sum(A,B) !!*)
   5.186 -val major::prems= Goalw basic_defs
   5.187 -    "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
   5.188 -\    |] ==> snd(p) : B(fst(p))";
   5.189 -by (rtac (major RS SumE) 1);
   5.190 -by (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1);
   5.191 -by (typechk_tac prems) ;
   5.192 -qed "SumE_snd";
     6.1 --- a/src/CTT/CTT.thy	Fri Jun 02 16:06:19 2006 +0200
     6.2 +++ b/src/CTT/CTT.thy	Fri Jun 02 18:15:38 2006 +0200
     6.3 @@ -8,6 +8,7 @@
     6.4  
     6.5  theory CTT
     6.6  imports Pure
     6.7 +uses "~~/src/Provers/typedsimp.ML" ("rew.ML")
     6.8  begin
     6.9  
    6.10  typedecl i
    6.11 @@ -57,36 +58,35 @@
    6.12    pair      :: "[i,i]=>i"           ("(1<_,/_>)")
    6.13  
    6.14  syntax
    6.15 -  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
    6.16 -  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
    6.17 -  "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
    6.18 -  "@*"      :: "[t,t]=>t"           ("(_ */ _)" [51,50] 50)
    6.19 -
    6.20 +  "_PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
    6.21 +  "_SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
    6.22  translations
    6.23 -  "PROD x:A. B" => "Prod(A, %x. B)"
    6.24 -  "A --> B"     => "Prod(A, %_. B)"
    6.25 -  "SUM x:A. B"  => "Sum(A, %x. B)"
    6.26 -  "A * B"       => "Sum(A, %_. B)"
    6.27 +  "PROD x:A. B" == "Prod(A, %x. B)"
    6.28 +  "SUM x:A. B"  == "Sum(A, %x. B)"
    6.29 +
    6.30 +abbreviation
    6.31 +  Arrow     :: "[t,t]=>t"           (infixr "-->" 30)
    6.32 +  "A --> B == PROD _:A. B"
    6.33 +  Times     :: "[t,t]=>t"           (infixr "*" 50)
    6.34 +  "A * B == SUM _:A. B"
    6.35  
    6.36 -print_translation {*
    6.37 -  [("Prod", dependent_tr' ("@PROD", "@-->")),
    6.38 -   ("Sum", dependent_tr' ("@SUM", "@*"))]
    6.39 -*}
    6.40 +const_syntax (xsymbols)
    6.41 +  Elem  ("(_ /\<in> _)" [10,10] 5)
    6.42 +  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    6.43 +  Arrow  (infixr "\<longrightarrow>" 30)
    6.44 +  Times  (infixr "\<times>" 50)
    6.45  
    6.46 +const_syntax (HTML output)
    6.47 +  Elem  ("(_ /\<in> _)" [10,10] 5)
    6.48 +  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    6.49 +  Times  (infixr "\<times>" 50)
    6.50  
    6.51  syntax (xsymbols)
    6.52 -  "@-->"    :: "[t,t]=>t"           ("(_ \<longrightarrow>/ _)" [31,30] 30)
    6.53 -  "@*"      :: "[t,t]=>t"           ("(_ \<times>/ _)"          [51,50] 50)
    6.54 -  Elem      :: "[i, t]=>prop"       ("(_ /\<in> _)" [10,10] 5)
    6.55 -  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    6.56    "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    6.57    "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    6.58    "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
    6.59  
    6.60  syntax (HTML output)
    6.61 -  "@*"      :: "[t,t]=>t"           ("(_ \<times>/ _)"          [51,50] 50)
    6.62 -  Elem      :: "[i, t]=>prop"       ("(_ /\<in> _)" [10,10] 5)
    6.63 -  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    6.64    "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    6.65    "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    6.66    "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
    6.67 @@ -273,6 +273,233 @@
    6.68    TEL: "[| p = q : T;  c = d : C(tt) |] ==> c = d : C(p)"
    6.69    TC: "p : T ==> p = tt : T"
    6.70  
    6.71 -ML {* use_legacy_bindings (the_context ()) *}
    6.72 +
    6.73 +subsection "Tactics and derived rules for Constructive Type Theory"
    6.74 +
    6.75 +(*Formation rules*)
    6.76 +lemmas form_rls = NF ProdF SumF PlusF EqF FF TF
    6.77 +  and formL_rls = ProdFL SumFL PlusFL EqFL
    6.78 +
    6.79 +(*Introduction rules
    6.80 +  OMITTED: EqI, because its premise is an eqelem, not an elem*)
    6.81 +lemmas intr_rls = NI0 NI_succ ProdI SumI PlusI_inl PlusI_inr TI
    6.82 +  and intrL_rls = NI_succL ProdIL SumIL PlusI_inlL PlusI_inrL
    6.83 +
    6.84 +(*Elimination rules
    6.85 +  OMITTED: EqE, because its conclusion is an eqelem,  not an elem
    6.86 +           TE, because it does not involve a constructor *)
    6.87 +lemmas elim_rls = NE ProdE SumE PlusE FE
    6.88 +  and elimL_rls = NEL ProdEL SumEL PlusEL FEL
    6.89 +
    6.90 +(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
    6.91 +lemmas comp_rls = NC0 NC_succ ProdC SumC PlusC_inl PlusC_inr
    6.92 +
    6.93 +(*rules with conclusion a:A, an elem judgement*)
    6.94 +lemmas element_rls = intr_rls elim_rls
    6.95 +
    6.96 +(*Definitions are (meta)equality axioms*)
    6.97 +lemmas basic_defs = fst_def snd_def
    6.98 +
    6.99 +(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
   6.100 +lemma SumIL2: "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
   6.101 +apply (rule sym_elem)
   6.102 +apply (rule SumIL)
   6.103 +apply (rule_tac [!] sym_elem)
   6.104 +apply assumption+
   6.105 +done
   6.106 +
   6.107 +lemmas intrL2_rls = NI_succL ProdIL SumIL2 PlusI_inlL PlusI_inrL
   6.108 +
   6.109 +(*Exploit p:Prod(A,B) to create the assumption z:B(a).
   6.110 +  A more natural form of product elimination. *)
   6.111 +lemma subst_prodE:
   6.112 +  assumes "p: Prod(A,B)"
   6.113 +    and "a: A"
   6.114 +    and "!!z. z: B(a) ==> c(z): C(z)"
   6.115 +  shows "c(p`a): C(p`a)"
   6.116 +apply (rule prems ProdE)+
   6.117 +done
   6.118 +
   6.119 +
   6.120 +subsection {* Tactics for type checking *}
   6.121 +
   6.122 +ML {*
   6.123 +
   6.124 +local
   6.125 +
   6.126 +fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
   6.127 +  | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
   6.128 +  | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
   6.129 +  | is_rigid_elem _ = false
   6.130 +
   6.131 +in
   6.132 +
   6.133 +(*Try solving a:A or a=b:A by assumption provided a is rigid!*)
   6.134 +val test_assume_tac = SUBGOAL(fn (prem,i) =>
   6.135 +    if is_rigid_elem (Logic.strip_assums_concl prem)
   6.136 +    then  assume_tac i  else  no_tac)
   6.137 +
   6.138 +fun ASSUME tf i = test_assume_tac i  ORELSE  tf i
   6.139 +
   6.140 +end;
   6.141 +
   6.142 +*}
   6.143 +
   6.144 +(*For simplification: type formation and checking,
   6.145 +  but no equalities between terms*)
   6.146 +lemmas routine_rls = form_rls formL_rls refl_type element_rls
   6.147 +
   6.148 +ML {*
   6.149 +local
   6.150 +  val routine_rls = thms "routine_rls";
   6.151 +  val form_rls = thms "form_rls";
   6.152 +  val intr_rls = thms "intr_rls";
   6.153 +  val element_rls = thms "element_rls";
   6.154 +  val equal_rls = form_rls @ element_rls @ thms "intrL_rls" @
   6.155 +    thms "elimL_rls" @ thms "refl_elem"
   6.156 +in
   6.157 +
   6.158 +fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
   6.159 +
   6.160 +(*Solve all subgoals "A type" using formation rules. *)
   6.161 +val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
   6.162 +
   6.163 +(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
   6.164 +fun typechk_tac thms =
   6.165 +  let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
   6.166 +  in  REPEAT_FIRST (ASSUME tac)  end
   6.167 +
   6.168 +(*Solve a:A (a flexible, A rigid) by introduction rules.
   6.169 +  Cannot use stringtrees (filt_resolve_tac) since
   6.170 +  goals like ?a:SUM(A,B) have a trivial head-string *)
   6.171 +fun intr_tac thms =
   6.172 +  let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
   6.173 +  in  REPEAT_FIRST (ASSUME tac)  end
   6.174 +
   6.175 +(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
   6.176 +fun equal_tac thms =
   6.177 +  REPEAT_FIRST (ASSUME (filt_resolve_tac (thms @ equal_rls) 3))
   6.178  
   6.179  end
   6.180 +
   6.181 +*}
   6.182 +
   6.183 +
   6.184 +subsection {* Simplification *}
   6.185 +
   6.186 +(*To simplify the type in a goal*)
   6.187 +lemma replace_type: "[| B = A;  a : A |] ==> a : B"
   6.188 +apply (rule equal_types)
   6.189 +apply (rule_tac [2] sym_type)
   6.190 +apply assumption+
   6.191 +done
   6.192 +
   6.193 +(*Simplify the parameter of a unary type operator.*)
   6.194 +lemma subst_eqtyparg:
   6.195 +  assumes "a=c : A"
   6.196 +    and "!!z. z:A ==> B(z) type"
   6.197 +  shows "B(a)=B(c)"
   6.198 +apply (rule subst_typeL)
   6.199 +apply (rule_tac [2] refl_type)
   6.200 +apply (rule prems)
   6.201 +apply assumption
   6.202 +done
   6.203 +
   6.204 +(*Simplification rules for Constructive Type Theory*)
   6.205 +lemmas reduction_rls = comp_rls [THEN trans_elem]
   6.206 +
   6.207 +ML {*
   6.208 +local
   6.209 +  val EqI = thm "EqI";
   6.210 +  val EqE = thm "EqE";
   6.211 +  val NE = thm "NE";
   6.212 +  val FE = thm "FE";
   6.213 +  val ProdI = thm "ProdI";
   6.214 +  val SumI = thm "SumI";
   6.215 +  val SumE = thm "SumE";
   6.216 +  val PlusE = thm "PlusE";
   6.217 +  val PlusI_inl = thm "PlusI_inl";
   6.218 +  val PlusI_inr = thm "PlusI_inr";
   6.219 +  val subst_prodE = thm "subst_prodE";
   6.220 +  val intr_rls = thms "intr_rls";
   6.221 +in
   6.222 +
   6.223 +(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
   6.224 +  Uses other intro rules to avoid changing flexible goals.*)
   6.225 +val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1))
   6.226 +
   6.227 +(** Tactics that instantiate CTT-rules.
   6.228 +    Vars in the given terms will be incremented!
   6.229 +    The (rtac EqE i) lets them apply to equality judgements. **)
   6.230 +
   6.231 +fun NE_tac (sp: string) i =
   6.232 +  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i
   6.233 +
   6.234 +fun SumE_tac (sp: string) i =
   6.235 +  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i
   6.236 +
   6.237 +fun PlusE_tac (sp: string) i =
   6.238 +  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i
   6.239 +
   6.240 +(** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
   6.241 +
   6.242 +(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
   6.243 +fun add_mp_tac i =
   6.244 +    rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i
   6.245 +
   6.246 +(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   6.247 +fun mp_tac i = etac subst_prodE i  THEN  assume_tac i
   6.248 +
   6.249 +(*"safe" when regarded as predicate calculus rules*)
   6.250 +val safe_brls = sort (make_ord lessb)
   6.251 +    [ (true,FE), (true,asm_rl),
   6.252 +      (false,ProdI), (true,SumE), (true,PlusE) ]
   6.253 +
   6.254 +val unsafe_brls =
   6.255 +    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
   6.256 +      (true,subst_prodE) ]
   6.257 +
   6.258 +(*0 subgoals vs 1 or more*)
   6.259 +val (safe0_brls, safep_brls) =
   6.260 +    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls
   6.261 +
   6.262 +fun safestep_tac thms i =
   6.263 +    form_tac  ORELSE
   6.264 +    resolve_tac thms i  ORELSE
   6.265 +    biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
   6.266 +    DETERM (biresolve_tac safep_brls i)
   6.267 +
   6.268 +fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i)
   6.269 +
   6.270 +fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls
   6.271 +
   6.272 +(*Fails unless it solves the goal!*)
   6.273 +fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
   6.274 +
   6.275 +end
   6.276 +*}
   6.277 +
   6.278 +use "rew.ML"
   6.279 +
   6.280 +
   6.281 +subsection {* The elimination rules for fst/snd *}
   6.282 +
   6.283 +lemma SumE_fst: "p : Sum(A,B) ==> fst(p) : A"
   6.284 +apply (unfold basic_defs)
   6.285 +apply (erule SumE)
   6.286 +apply assumption
   6.287 +done
   6.288 +
   6.289 +(*The first premise must be p:Sum(A,B) !!*)
   6.290 +lemma SumE_snd:
   6.291 +  assumes major: "p: Sum(A,B)"
   6.292 +    and "A type"
   6.293 +    and "!!x. x:A ==> B(x) type"
   6.294 +  shows "snd(p) : B(fst(p))"
   6.295 +  apply (unfold basic_defs)
   6.296 +  apply (rule major [THEN SumE])
   6.297 +  apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
   6.298 +  apply (tactic {* typechk_tac (thms "prems") *})
   6.299 +  done
   6.300 +
   6.301 +end
     7.1 --- a/src/CTT/IsaMakefile	Fri Jun 02 16:06:19 2006 +0200
     7.2 +++ b/src/CTT/IsaMakefile	Fri Jun 02 18:15:38 2006 +0200
     7.3 @@ -26,8 +26,8 @@
     7.4  Pure:
     7.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     7.6  
     7.7 -$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.ML Arith.thy \
     7.8 -  Bool.ML Bool.thy CTT.ML CTT.thy Main.thy ROOT.ML rew.ML
     7.9 +$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \
    7.10 +  Bool.thy CTT.thy Main.thy ROOT.ML rew.ML
    7.11  	@$(ISATOOL) usedir -b $(OUT)/Pure CTT
    7.12  
    7.13  
    7.14 @@ -35,8 +35,8 @@
    7.15  
    7.16  CTT-ex: CTT $(LOG)/CTT-ex.gz
    7.17  
    7.18 -$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/elim.ML ex/equal.ML \
    7.19 -  ex/synth.ML ex/typechk.ML
    7.20 +$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \
    7.21 +  ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy
    7.22  	@$(ISATOOL) usedir $(OUT)/CTT ex
    7.23  
    7.24  
     8.1 --- a/src/CTT/README.html	Fri Jun 02 16:06:19 2006 +0200
     8.2 +++ b/src/CTT/README.html	Fri Jun 02 18:15:38 2006 +0200
     8.3 @@ -13,10 +13,7 @@
     8.4  
     8.5  <H2>CTT: Constructive Type Theory</H2>
     8.6  
     8.7 -This directory contains the ML sources of the Isabelle system for
     8.8 -Constructive Type Theory (extensional equality, no universes).<p>
     8.9 -
    8.10 -The <tt>ex</tt> subdirectory contains some examples.<p>
    8.11 +This is a version of Constructive Type Theory (extensional equality, no universes).<p>
    8.12  
    8.13  Useful references on Constructive Type Theory:
    8.14  
     9.1 --- a/src/CTT/ROOT.ML	Fri Jun 02 16:06:19 2006 +0200
     9.2 +++ b/src/CTT/ROOT.ML	Fri Jun 02 18:15:38 2006 +0200
     9.3 @@ -1,15 +1,10 @@
     9.4 -(*  Title:      CTT/ROOT
     9.5 +(*  Title:      CTT/ROOT.ML
     9.6      ID:         $Id$
     9.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.8      Copyright   1991  University of Cambridge
     9.9 -
    9.10 -Adds Constructive Type Theory to a database containing pure Isabelle. 
    9.11 -Should be executed in the subdirectory CTT.
    9.12  *)
    9.13  
    9.14  val banner = "Constructive Type Theory";
    9.15  writeln banner;
    9.16  
    9.17  use_thy "Main";
    9.18 -
    9.19 -Goal "tt : T";  (*leave subgoal package empty*)
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/CTT/ex/Elimination.thy	Fri Jun 02 18:15:38 2006 +0200
    10.3 @@ -0,0 +1,194 @@
    10.4 +(*  Title:      CTT/ex/Elimination.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 +    Copyright   1991  University of Cambridge
    10.8 +
    10.9 +Some examples taken from P. Martin-L\"of, Intuitionistic type theory
   10.10 +        (Bibliopolis, 1984).
   10.11 +*)
   10.12 +
   10.13 +header "Examples with elimination rules"
   10.14 +
   10.15 +theory Elimination
   10.16 +imports CTT
   10.17 +begin
   10.18 +
   10.19 +text "This finds the functions fst and snd!"
   10.20 +
   10.21 +lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
   10.22 +apply (tactic {* pc_tac [] 1 *})
   10.23 +done
   10.24 +
   10.25 +lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
   10.26 +apply (tactic {* pc_tac [] 1 *})
   10.27 +back
   10.28 +done
   10.29 +
   10.30 +text "Double negation of the Excluded Middle"
   10.31 +lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
   10.32 +apply (tactic "intr_tac []")
   10.33 +apply (rule ProdE)
   10.34 +apply assumption
   10.35 +apply (tactic "pc_tac [] 1")
   10.36 +done
   10.37 +
   10.38 +lemma "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)"
   10.39 +apply (tactic "pc_tac [] 1")
   10.40 +done
   10.41 +(*The sequent version (ITT) could produce an interesting alternative
   10.42 +  by backtracking.  No longer.*)
   10.43 +
   10.44 +text "Binary sums and products"
   10.45 +lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
   10.46 +apply (tactic "pc_tac [] 1")
   10.47 +done
   10.48 +
   10.49 +(*A distributive law*)
   10.50 +lemma "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)"
   10.51 +apply (tactic "pc_tac [] 1")
   10.52 +done
   10.53 +
   10.54 +(*more general version, same proof*)
   10.55 +lemma
   10.56 +  assumes "A type"
   10.57 +    and "!!x. x:A ==> B(x) type"
   10.58 +    and "!!x. x:A ==> C(x) type"
   10.59 +  shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
   10.60 +apply (tactic {* pc_tac (thms "prems") 1 *})
   10.61 +done
   10.62 +
   10.63 +text "Construction of the currying functional"
   10.64 +lemma "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
   10.65 +apply (tactic "pc_tac [] 1")
   10.66 +done
   10.67 +
   10.68 +(*more general goal with same proof*)
   10.69 +lemma
   10.70 +  assumes "A type"
   10.71 +    and "!!x. x:A ==> B(x) type"
   10.72 +    and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
   10.73 +  shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
   10.74 +                      (PROD x:A . PROD y:B(x) . C(<x,y>))"
   10.75 +apply (tactic {* pc_tac (thms "prems") 1 *})
   10.76 +done
   10.77 +
   10.78 +text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
   10.79 +lemma "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
   10.80 +apply (tactic "pc_tac [] 1")
   10.81 +done
   10.82 +
   10.83 +(*more general goal with same proof*)
   10.84 +lemma
   10.85 +  assumes "A type"
   10.86 +    and "!!x. x:A ==> B(x) type"
   10.87 +    and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
   10.88 +  shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
   10.89 +        --> (PROD z : (SUM x:A . B(x)) . C(z))"
   10.90 +apply (tactic {* pc_tac (thms "prems") 1 *})
   10.91 +done
   10.92 +
   10.93 +text "Function application"
   10.94 +lemma "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B"
   10.95 +apply (tactic "pc_tac [] 1")
   10.96 +done
   10.97 +
   10.98 +text "Basic test of quantifier reasoning"
   10.99 +lemma
  10.100 +  assumes "A type"
  10.101 +    and "B type"
  10.102 +    and "!!x y.[| x:A;  y:B |] ==> C(x,y) type"
  10.103 +  shows
  10.104 +    "?a :     (SUM y:B . PROD x:A . C(x,y))
  10.105 +          --> (PROD x:A . SUM y:B . C(x,y))"
  10.106 +apply (tactic {* pc_tac (thms "prems") 1 *})
  10.107 +done
  10.108 +
  10.109 +text "Martin-Lof (1984) pages 36-7: the combinator S"
  10.110 +lemma
  10.111 +  assumes "A type"
  10.112 +    and "!!x. x:A ==> B(x) type"
  10.113 +    and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
  10.114 +  shows "?a :    (PROD x:A. PROD y:B(x). C(x,y))
  10.115 +             --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
  10.116 +apply (tactic {* pc_tac (thms "prems") 1 *})
  10.117 +done
  10.118 +
  10.119 +text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
  10.120 +lemma
  10.121 +  assumes "A type"
  10.122 +    and "B type"
  10.123 +    and "!!z. z: A+B ==> C(z) type"
  10.124 +  shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
  10.125 +          --> (PROD z: A+B. C(z))"
  10.126 +apply (tactic {* pc_tac (thms "prems") 1 *})
  10.127 +done
  10.128 +
  10.129 +(*towards AXIOM OF CHOICE*)
  10.130 +lemma [folded basic_defs]:
  10.131 +  "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
  10.132 +apply (tactic "pc_tac [] 1")
  10.133 +done
  10.134 +
  10.135 +
  10.136 +(*Martin-Lof (1984) page 50*)
  10.137 +text "AXIOM OF CHOICE!  Delicate use of elimination rules"
  10.138 +lemma
  10.139 +  assumes "A type"
  10.140 +    and "!!x. x:A ==> B(x) type"
  10.141 +    and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
  10.142 +  shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
  10.143 +                         (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
  10.144 +apply (tactic {* intr_tac (thms "prems") *})
  10.145 +apply (tactic "add_mp_tac 2")
  10.146 +apply (tactic "add_mp_tac 1")
  10.147 +apply (erule SumE_fst)
  10.148 +apply (rule replace_type)
  10.149 +apply (rule subst_eqtyparg)
  10.150 +apply (rule comp_rls)
  10.151 +apply (rule_tac [4] SumE_snd)
  10.152 +apply (tactic {* typechk_tac (thm "SumE_fst" :: thms "prems") *})
  10.153 +done
  10.154 +
  10.155 +text "Axiom of choice.  Proof without fst, snd.  Harder still!"
  10.156 +lemma [folded basic_defs]:
  10.157 +  assumes "A type"
  10.158 +    and "!!x. x:A ==> B(x) type"
  10.159 +    and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
  10.160 +  shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
  10.161 +                         (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
  10.162 +apply (tactic {* intr_tac (thms "prems") *})
  10.163 +(*Must not use add_mp_tac as subst_prodE hides the construction.*)
  10.164 +apply (rule ProdE [THEN SumE], assumption)
  10.165 +apply (tactic "TRYALL assume_tac")
  10.166 +apply (rule replace_type)
  10.167 +apply (rule subst_eqtyparg)
  10.168 +apply (rule comp_rls)
  10.169 +apply (erule_tac [4] ProdE [THEN SumE])
  10.170 +apply (tactic {* typechk_tac (thms "prems") *})
  10.171 +apply (rule replace_type)
  10.172 +apply (rule subst_eqtyparg)
  10.173 +apply (rule comp_rls)
  10.174 +apply (tactic {* typechk_tac (thms "prems") *})
  10.175 +apply assumption
  10.176 +done
  10.177 +
  10.178 +text "Example of sequent_style deduction"
  10.179 +(*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
  10.180 +    lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
  10.181 +lemma
  10.182 +  assumes "A type"
  10.183 +    and "B type"
  10.184 +    and "!!z. z:A*B ==> C(z) type"
  10.185 +  shows "?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))"
  10.186 +apply (rule intr_rls)
  10.187 +apply (tactic {* biresolve_tac safe_brls 2 *})
  10.188 +(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
  10.189 +apply (rule_tac [2] a = "y" in ProdE)
  10.190 +apply (tactic {* typechk_tac (thms "prems") *})
  10.191 +apply (rule SumE, assumption)
  10.192 +apply (tactic "intr_tac []")
  10.193 +apply (tactic "TRYALL assume_tac")
  10.194 +apply (tactic {* typechk_tac (thms "prems") *})
  10.195 +done
  10.196 +
  10.197 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/CTT/ex/Equality.thy	Fri Jun 02 18:15:38 2006 +0200
    11.3 @@ -0,0 +1,70 @@
    11.4 +(*  Title:      CTT/ex/Equality.thy
    11.5 +    ID:         $Id$
    11.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 +    Copyright   1991  University of Cambridge
    11.8 +*)
    11.9 +
   11.10 +header "Equality reasoning by rewriting"
   11.11 +
   11.12 +theory Equality
   11.13 +imports CTT
   11.14 +begin
   11.15 +
   11.16 +lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)"
   11.17 +apply (rule EqE)
   11.18 +apply (rule elim_rls, assumption)
   11.19 +apply (tactic "rew_tac []")
   11.20 +done
   11.21 +
   11.22 +lemma when_eq: "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B"
   11.23 +apply (rule EqE)
   11.24 +apply (rule elim_rls, assumption)
   11.25 +apply (tactic "rew_tac []")
   11.26 +done
   11.27 +
   11.28 +(*in the "rec" formulation of addition, 0+n=n *)
   11.29 +lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N"
   11.30 +apply (rule EqE)
   11.31 +apply (rule elim_rls, assumption)
   11.32 +apply (tactic "rew_tac []")
   11.33 +done
   11.34 +
   11.35 +(*the harder version, n+0=n: recursive, uses induction hypothesis*)
   11.36 +lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N"
   11.37 +apply (rule EqE)
   11.38 +apply (rule elim_rls, assumption)
   11.39 +apply (tactic "hyp_rew_tac []")
   11.40 +done
   11.41 +
   11.42 +(*Associativity of addition*)
   11.43 +lemma "[| a:N;  b:N;  c:N |]
   11.44 +      ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) =
   11.45 +          rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N"
   11.46 +apply (tactic {* NE_tac "a" 1 *})
   11.47 +apply (tactic "hyp_rew_tac []")
   11.48 +done
   11.49 +
   11.50 +(*Martin-Lof (1984) page 62: pairing is surjective*)
   11.51 +lemma "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)"
   11.52 +apply (rule EqE)
   11.53 +apply (rule elim_rls, assumption)
   11.54 +apply (tactic {* DEPTH_SOLVE_1 (rew_tac []) *}) (*!!!!!!!*)
   11.55 +done
   11.56 +
   11.57 +lemma "[| a : A;  b : B |] ==>
   11.58 +     (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
   11.59 +apply (tactic "rew_tac []")
   11.60 +done
   11.61 +
   11.62 +(*a contrived, complicated simplication, requires sum-elimination also*)
   11.63 +lemma "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =
   11.64 +      lam x. x  :  PROD x:(SUM y:N. N). (SUM y:N. N)"
   11.65 +apply (rule reduction_rls)
   11.66 +apply (rule_tac [3] intrL_rls)
   11.67 +apply (rule_tac [4] EqE)
   11.68 +apply (rule_tac [4] SumE, tactic "assume_tac 4")
   11.69 +(*order of unifiers is essential here*)
   11.70 +apply (tactic "rew_tac []")
   11.71 +done
   11.72 +
   11.73 +end
    12.1 --- a/src/CTT/ex/ROOT.ML	Fri Jun 02 16:06:19 2006 +0200
    12.2 +++ b/src/CTT/ex/ROOT.ML	Fri Jun 02 18:15:38 2006 +0200
    12.3 @@ -3,12 +3,10 @@
    12.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.5      Copyright   1991  University of Cambridge
    12.6  
    12.7 -Executes all examples for Constructive Type Theory. 
    12.8 +Examples for Constructive Type Theory. 
    12.9  *)
   12.10  
   12.11 -print_depth 2;  
   12.12 -
   12.13 -time_use "typechk.ML";
   12.14 -time_use "elim.ML";
   12.15 -time_use "equal.ML";
   12.16 -time_use "synth.ML";
   12.17 +use_thy "Typechecking";
   12.18 +use_thy "Elimination";
   12.19 +use_thy "Equality";
   12.20 +use_thy "Synthesis";
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/CTT/ex/Synthesis.thy	Fri Jun 02 18:15:38 2006 +0200
    13.3 @@ -0,0 +1,106 @@
    13.4 +(*  Title:      CTT/ex/Synthesis.thy
    13.5 +    ID:         $Id$
    13.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 +    Copyright   1991  University of Cambridge
    13.8 +*)
    13.9 +
   13.10 +header "Synthesis examples, using a crude form of narrowing"
   13.11 +
   13.12 +theory Synthesis
   13.13 +imports Arith
   13.14 +begin
   13.15 +
   13.16 +text "discovery of predecessor function"
   13.17 +lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)    
   13.18 +                  *  (PROD n:N. Eq(N, pred ` succ(n), n))"
   13.19 +apply (tactic "intr_tac []")
   13.20 +apply (tactic eqintr_tac)
   13.21 +apply (rule_tac [3] reduction_rls)
   13.22 +apply (rule_tac [5] comp_rls)
   13.23 +apply (tactic "rew_tac []")
   13.24 +done
   13.25 +
   13.26 +text "the function fst as an element of a function type"
   13.27 +lemma [folded basic_defs]:
   13.28 +  "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
   13.29 +apply (tactic "intr_tac []")
   13.30 +apply (tactic eqintr_tac)
   13.31 +apply (rule_tac [2] reduction_rls)
   13.32 +apply (rule_tac [4] comp_rls)
   13.33 +apply (tactic "typechk_tac []")
   13.34 +txt "now put in A everywhere"
   13.35 +apply assumption+
   13.36 +done
   13.37 +
   13.38 +text "An interesting use of the eliminator, when"
   13.39 +(*The early implementation of unification caused non-rigid path in occur check
   13.40 +  See following example.*)
   13.41 +lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)   
   13.42 +                   * Eq(?A, ?b(inr(i)), <succ(0), i>)"
   13.43 +apply (tactic "intr_tac []")
   13.44 +apply (tactic eqintr_tac)
   13.45 +apply (rule comp_rls)
   13.46 +apply (tactic "rew_tac []")
   13.47 +oops
   13.48 +
   13.49 +(*Here we allow the type to depend on i.  
   13.50 + This prevents the cycle in the first unification (no longer needed).  
   13.51 + Requires flex-flex to preserve the dependence.
   13.52 + Simpler still: make ?A into a constant type N*N.*)
   13.53 +lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
   13.54 +                  *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
   13.55 +oops
   13.56 +
   13.57 +text "A tricky combination of when and split"
   13.58 +(*Now handled easily, but caused great problems once*)
   13.59 +lemma [folded basic_defs]:
   13.60 +  "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)    
   13.61 +                           *  Eq(?A, ?b(inr(<i,j>)), j)"
   13.62 +apply (tactic "intr_tac []")
   13.63 +apply (tactic eqintr_tac)
   13.64 +apply (rule PlusC_inl [THEN trans_elem])
   13.65 +apply (rule_tac [4] comp_rls)
   13.66 +apply (rule_tac [7] reduction_rls)
   13.67 +apply (rule_tac [10] comp_rls)
   13.68 +apply (tactic "typechk_tac []")
   13.69 +oops
   13.70 +
   13.71 +(*similar but allows the type to depend on i and j*)
   13.72 +lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)  
   13.73 +                          *   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
   13.74 +oops
   13.75 +
   13.76 +(*similar but specifying the type N simplifies the unification problems*)
   13.77 +lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)   
   13.78 +                          *   Eq(N, ?b(inr(<i,j>)), j)"
   13.79 +oops
   13.80 +
   13.81 +
   13.82 +text "Deriving the addition operator"
   13.83 +lemma [folded arith_defs]:
   13.84 +  "?c : PROD n:N. Eq(N, ?f(0,n), n)   
   13.85 +                  *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
   13.86 +apply (tactic "intr_tac []")
   13.87 +apply (tactic eqintr_tac)
   13.88 +apply (rule comp_rls)
   13.89 +apply (tactic "rew_tac []")
   13.90 +oops
   13.91 +
   13.92 +text "The addition function -- using explicit lambdas"
   13.93 +lemma [folded arith_defs]:
   13.94 +  "?c : SUM plus : ?A .   
   13.95 +         PROD x:N. Eq(N, plus`0`x, x)   
   13.96 +                *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
   13.97 +apply (tactic "intr_tac []")
   13.98 +apply (tactic eqintr_tac)
   13.99 +apply (tactic "resolve_tac [TSimp.split_eqn] 3")
  13.100 +apply (tactic "SELECT_GOAL (rew_tac []) 4")
  13.101 +apply (tactic "resolve_tac [TSimp.split_eqn] 3")
  13.102 +apply (tactic "SELECT_GOAL (rew_tac []) 4")
  13.103 +apply (rule_tac [3] p = "y" in NC_succ)
  13.104 +  (**  by (resolve_tac comp_rls 3);  caused excessive branching  **)
  13.105 +apply (tactic "rew_tac []")
  13.106 +done
  13.107 +
  13.108 +end
  13.109 +
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/CTT/ex/Typechecking.thy	Fri Jun 02 18:15:38 2006 +0200
    14.3 @@ -0,0 +1,88 @@
    14.4 +(*  Title:      CTT/ex/Typechecking.thy
    14.5 +    ID:         $Id$
    14.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7 +    Copyright   1991  University of Cambridge
    14.8 +*)
    14.9 +
   14.10 +header "Easy examples: type checking and type deduction"
   14.11 +
   14.12 +theory Typechecking
   14.13 +imports CTT
   14.14 +begin
   14.15 +
   14.16 +subsection {* Single-step proofs: verifying that a type is well-formed *}
   14.17 +
   14.18 +lemma "?A type"
   14.19 +apply (rule form_rls)
   14.20 +done
   14.21 +
   14.22 +lemma "?A type"
   14.23 +apply (rule form_rls)
   14.24 +back
   14.25 +apply (rule form_rls)
   14.26 +apply (rule form_rls)
   14.27 +done
   14.28 +
   14.29 +lemma "PROD z:?A . N + ?B(z) type"
   14.30 +apply (rule form_rls)
   14.31 +apply (rule form_rls)
   14.32 +apply (rule form_rls)
   14.33 +apply (rule form_rls)
   14.34 +apply (rule form_rls)
   14.35 +done
   14.36 +
   14.37 +
   14.38 +subsection {* Multi-step proofs: Type inference *}
   14.39 +
   14.40 +lemma "PROD w:N. N + N type"
   14.41 +apply (tactic form_tac)
   14.42 +done
   14.43 +
   14.44 +lemma "<0, succ(0)> : ?A"
   14.45 +apply (tactic "intr_tac []")
   14.46 +done
   14.47 +
   14.48 +lemma "PROD w:N . Eq(?A,w,w) type"
   14.49 +apply (tactic "typechk_tac []")
   14.50 +done
   14.51 +
   14.52 +lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
   14.53 +apply (tactic "typechk_tac []")
   14.54 +done
   14.55 +
   14.56 +text "typechecking an application of fst"
   14.57 +lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
   14.58 +apply (tactic "typechk_tac []")
   14.59 +done
   14.60 +
   14.61 +text "typechecking the predecessor function"
   14.62 +lemma "lam n. rec(n, 0, %x y. x) : ?A"
   14.63 +apply (tactic "typechk_tac []")
   14.64 +done
   14.65 +
   14.66 +text "typechecking the addition function"
   14.67 +lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
   14.68 +apply (tactic "typechk_tac []")
   14.69 +done
   14.70 +
   14.71 +(*Proofs involving arbitrary types.
   14.72 +  For concreteness, every type variable left over is forced to be N*)
   14.73 +ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
   14.74 +
   14.75 +lemma "lam w. <w,w> : ?A"
   14.76 +apply (tactic "typechk_tac []")
   14.77 +apply (tactic N_tac)
   14.78 +done
   14.79 +
   14.80 +lemma "lam x. lam y. x : ?A"
   14.81 +apply (tactic "typechk_tac []")
   14.82 +apply (tactic N_tac)
   14.83 +done
   14.84 +
   14.85 +text "typechecking fst (as a function object)"
   14.86 +lemma "lam i. split(i, %j k. j) : ?A"
   14.87 +apply (tactic "typechk_tac []")
   14.88 +apply (tactic N_tac)
   14.89 +done
   14.90 +
   14.91 +end
    15.1 --- a/src/CTT/ex/elim.ML	Fri Jun 02 16:06:19 2006 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,182 +0,0 @@
    15.4 -(*  Title:      CTT/ex/elim
    15.5 -    ID:         $Id$
    15.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7 -    Copyright   1991  University of Cambridge
    15.8 -
    15.9 -Some examples taken from P. Martin-L\"of, Intuitionistic type theory
   15.10 -        (Bibliopolis, 1984).
   15.11 -
   15.12 -by (safe_tac prems 1);
   15.13 -by (step_tac prems 1);
   15.14 -by (pc_tac prems 1);
   15.15 -*)
   15.16 -
   15.17 -writeln"Examples with elimination rules";
   15.18 -
   15.19 -
   15.20 -writeln"This finds the functions fst and snd!"; 
   15.21 -Goal "A type ==> ?a : (A*A) --> A";
   15.22 -by (pc_tac [] 1  THEN  fold_tac basic_defs);   (*puts in fst and snd*)
   15.23 -result();
   15.24 -writeln"first solution is fst;  backtracking gives snd";
   15.25 -back(); 
   15.26 -back() handle ERROR _ => writeln"And there are indeed no others";  
   15.27 -
   15.28 -
   15.29 -writeln"Double negation of the Excluded Middle";
   15.30 -Goal "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
   15.31 -by (intr_tac []);
   15.32 -by (rtac ProdE 1);
   15.33 -by (assume_tac 1);
   15.34 -by (pc_tac [] 1);
   15.35 -result();
   15.36 -
   15.37 -Goal "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)";
   15.38 -by (pc_tac [] 1);
   15.39 -result();
   15.40 -(*The sequent version (ITT) could produce an interesting alternative
   15.41 -  by backtracking.  No longer.*)
   15.42 -
   15.43 -writeln"Binary sums and products";
   15.44 -Goal "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
   15.45 -by (pc_tac [] 1);
   15.46 -result();
   15.47 -
   15.48 -(*A distributive law*)
   15.49 -Goal "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)";
   15.50 -by (pc_tac [] 1);
   15.51 -result();
   15.52 -
   15.53 -(*more general version, same proof*)
   15.54 -val prems = Goal
   15.55 -   "[| A type;  !!x. x:A ==> B(x) type;  !!x. x:A ==> C(x) type|] ==> \
   15.56 -\      ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))";
   15.57 -by (pc_tac prems 1);
   15.58 -result();
   15.59 -
   15.60 -writeln"Construction of the currying functional";
   15.61 -Goal "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))";
   15.62 -by (pc_tac [] 1);
   15.63 -result();
   15.64 -
   15.65 -(*more general goal with same proof*)
   15.66 -val prems = Goal
   15.67 -    "[| A type; !!x. x:A ==> B(x) type;                         \
   15.68 -\               !!z. z: (SUM x:A. B(x)) ==> C(z) type           \
   15.69 -\    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).    \
   15.70 -\                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
   15.71 -by (pc_tac prems 1);
   15.72 -result();
   15.73 -
   15.74 -writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)";
   15.75 -Goal "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
   15.76 -by (pc_tac [] 1);
   15.77 -result();
   15.78 -
   15.79 -(*more general goal with same proof*)
   15.80 -val prems = Goal 
   15.81 - "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A . B(x)) ==> C(z) type|] \
   15.82 -\  ==> ?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) \
   15.83 -\       --> (PROD z : (SUM x:A . B(x)) . C(z))";
   15.84 -by (pc_tac prems 1);
   15.85 -result();
   15.86 -
   15.87 -writeln"Function application";
   15.88 -Goal "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B";
   15.89 -by (pc_tac [] 1);
   15.90 -result();
   15.91 -
   15.92 -writeln"Basic test of quantifier reasoning";
   15.93 -val prems = Goal  
   15.94 -    "[| A type;  B type;  !!x y.[| x:A;  y:B |] ==> C(x,y) type |] ==> \
   15.95 -\    ?a :     (SUM y:B . PROD x:A . C(x,y))  \
   15.96 -\         --> (PROD x:A . SUM y:B . C(x,y))";
   15.97 -by (pc_tac prems 1);
   15.98 -result();
   15.99 -
  15.100 -(*faulty proof attempt, stripping the quantifiers in wrong sequence
  15.101 -by (intr_tac[]);
  15.102 -by (pc_tac prems 1);        ...fails!!  *)
  15.103 -
  15.104 -writeln"Martin-Lof (1984) pages 36-7: the combinator S";
  15.105 -val prems = Goal  
  15.106 -    "[| A type;  !!x. x:A ==> B(x) type;  \
  15.107 -\       !!x y.[| x:A; y:B(x) |] ==> C(x,y) type |] \
  15.108 -\    ==> ?a :    (PROD x:A. PROD y:B(x). C(x,y)) \
  15.109 -\            --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
  15.110 -by (pc_tac prems 1);
  15.111 -result();
  15.112 -
  15.113 -writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination";
  15.114 -val prems = Goal
  15.115 -    "[| A type;  B type;  !!z. z: A+B ==> C(z) type|] ==> \
  15.116 -\    ?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))  \
  15.117 -\         --> (PROD z: A+B. C(z))";
  15.118 -by (pc_tac prems 1);
  15.119 -result();
  15.120 -
  15.121 -(*towards AXIOM OF CHOICE*)
  15.122 -Goal "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
  15.123 -by (pc_tac [] 1);
  15.124 -by (fold_tac basic_defs);   (*puts in fst and snd*)
  15.125 -result();
  15.126 -
  15.127 -(*Martin-Lof (1984) page 50*)
  15.128 -writeln"AXIOM OF CHOICE!  Delicate use of elimination rules";
  15.129 -val prems = Goal   
  15.130 -    "[| A type;  !!x. x:A ==> B(x) type;                        \
  15.131 -\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
  15.132 -\    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
  15.133 -\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
  15.134 -by (intr_tac prems);
  15.135 -by (add_mp_tac 2);
  15.136 -by (add_mp_tac 1);
  15.137 -by (etac SumE_fst 1);
  15.138 -by (rtac replace_type 1);
  15.139 -by (rtac subst_eqtyparg 1);
  15.140 -by (resolve_tac comp_rls 1);
  15.141 -by (rtac SumE_snd 4);
  15.142 -by (typechk_tac (SumE_fst::prems));
  15.143 -result();
  15.144 -
  15.145 -writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
  15.146 -val prems = Goal   
  15.147 -    "[| A type;  !!x. x:A ==> B(x) type;                         \
  15.148 -\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
  15.149 -\    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
  15.150 -\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
  15.151 -by (intr_tac prems);
  15.152 -(*Must not use add_mp_tac as subst_prodE hides the construction.*)
  15.153 -by (resolve_tac [ProdE RS SumE] 1  THEN  assume_tac 1);
  15.154 -by (TRYALL assume_tac);
  15.155 -by (rtac replace_type 1);
  15.156 -by (rtac subst_eqtyparg 1);
  15.157 -by (resolve_tac comp_rls 1);
  15.158 -by (etac (ProdE RS SumE) 4);
  15.159 -by (typechk_tac prems);
  15.160 -by (rtac replace_type 1);
  15.161 -by (rtac subst_eqtyparg 1);
  15.162 -by (resolve_tac comp_rls 1);
  15.163 -by (typechk_tac prems);
  15.164 -by (assume_tac 1);
  15.165 -by (fold_tac basic_defs);  (*puts in fst and snd*)
  15.166 -result();
  15.167 -
  15.168 -writeln"Example of sequent_style deduction"; 
  15.169 -(*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
  15.170 -    lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
  15.171 -val prems = Goal   
  15.172 -    "[| A type;  B type;  !!z. z:A*B ==> C(z) type |] ==>  \
  15.173 -\    ?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))";
  15.174 -by (resolve_tac intr_rls 1);
  15.175 -by (biresolve_tac safe_brls 2);
  15.176 -(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
  15.177 -by (res_inst_tac [ ("a","y") ] ProdE 2);
  15.178 -by (typechk_tac prems);
  15.179 -by (rtac SumE 1  THEN  assume_tac 1);
  15.180 -by (intr_tac[]);
  15.181 -by (TRYALL assume_tac);
  15.182 -by (typechk_tac prems);
  15.183 -result();
  15.184 -
  15.185 -writeln"Reached end of file.";
    16.1 --- a/src/CTT/ex/equal.ML	Fri Jun 02 16:06:19 2006 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,75 +0,0 @@
    16.4 -(*  Title:      CTT/ex/equal
    16.5 -    ID:         $Id$
    16.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.7 -    Copyright   1991  University of Cambridge
    16.8 -
    16.9 -Equality reasoning by rewriting.
   16.10 -*)
   16.11 -
   16.12 -Goal "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
   16.13 -by (rtac EqE 1);
   16.14 -by (resolve_tac elim_rls 1  THEN  assume_tac 1);
   16.15 -by (rew_tac []);
   16.16 -qed "split_eq";
   16.17 -
   16.18 -Goal "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B";
   16.19 -by (rtac EqE 1);
   16.20 -by (resolve_tac elim_rls 1  THEN  assume_tac 1);
   16.21 -by (rew_tac []);
   16.22 -by (ALLGOALS assume_tac);
   16.23 -qed "when_eq";
   16.24 -
   16.25 -
   16.26 -(*in the "rec" formulation of addition, 0+n=n *)
   16.27 -Goal "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
   16.28 -by (rtac EqE 1);
   16.29 -by (resolve_tac elim_rls 1  THEN  assume_tac 1);
   16.30 -by (rew_tac []);
   16.31 -result();
   16.32 -
   16.33 -
   16.34 -(*the harder version, n+0=n: recursive, uses induction hypothesis*)
   16.35 -Goal "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
   16.36 -by (rtac EqE 1);
   16.37 -by (resolve_tac elim_rls 1  THEN  assume_tac 1);
   16.38 -by (hyp_rew_tac []);
   16.39 -result();
   16.40 -
   16.41 -
   16.42 -(*Associativity of addition*)
   16.43 -Goal "[| a:N;  b:N;  c:N |] \
   16.44 -\     ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
   16.45 -\         rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
   16.46 -by (NE_tac "a" 1);
   16.47 -by (hyp_rew_tac []);
   16.48 -result();
   16.49 -
   16.50 -
   16.51 -(*Martin-Lof (1984) page 62: pairing is surjective*)
   16.52 -Goal "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
   16.53 -by (rtac EqE 1);
   16.54 -by (resolve_tac elim_rls 1  THEN  assume_tac 1);
   16.55 -by (DEPTH_SOLVE_1 (rew_tac []));   (*!!!!!!!*)
   16.56 -result();
   16.57 -
   16.58 -
   16.59 -Goal "[| a : A;  b : B |] ==> \
   16.60 -\    (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A";
   16.61 -by (rew_tac []);
   16.62 -result();
   16.63 -
   16.64 -
   16.65 -(*a contrived, complicated simplication, requires sum-elimination also*)
   16.66 -Goal "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =  \
   16.67 -\     lam x. x  :  PROD x:(SUM y:N. N). (SUM y:N. N)";
   16.68 -by (resolve_tac reduction_rls 1);
   16.69 -by (resolve_tac intrL_rls 3);
   16.70 -by (rtac EqE 4);
   16.71 -by (rtac SumE 4  THEN  assume_tac 4);
   16.72 -(*order of unifiers is essential here*)
   16.73 -by (rew_tac []);
   16.74 -result();
   16.75 -
   16.76 -writeln"Reached end of file.";
   16.77 -(*28 August 1988: loaded this file in 34 seconds*)
   16.78 -(*2 September 1988: loaded this file in 48 seconds*)
    17.1 --- a/src/CTT/ex/synth.ML	Fri Jun 02 16:06:19 2006 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,103 +0,0 @@
    17.4 -(*  Title:      CTT/ex/synth
    17.5 -    ID:         $Id$
    17.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.7 -    Copyright   1991  University of Cambridge
    17.8 -*)
    17.9 -
   17.10 -writeln"Synthesis examples, using a crude form of narrowing";
   17.11 -
   17.12 -context (theory "Arith");
   17.13 -
   17.14 -writeln"discovery of predecessor function";
   17.15 -Goal 
   17.16 - "?a : SUM pred:?A . Eq(N, pred`0, 0)   \
   17.17 -\                 *  (PROD n:N. Eq(N, pred ` succ(n), n))";
   17.18 -by (intr_tac[]);
   17.19 -by eqintr_tac;
   17.20 -by (resolve_tac reduction_rls 3);
   17.21 -by (resolve_tac comp_rls 5);
   17.22 -by (rew_tac[]);
   17.23 -result();
   17.24 -
   17.25 -writeln"the function fst as an element of a function type";
   17.26 -Goal "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)";
   17.27 -by (intr_tac []);
   17.28 -by eqintr_tac;
   17.29 -by (resolve_tac reduction_rls 2);
   17.30 -by (resolve_tac comp_rls 4);
   17.31 -by (typechk_tac []);
   17.32 -writeln"now put in A everywhere";
   17.33 -by (REPEAT (assume_tac 1));
   17.34 -by (fold_tac basic_defs);
   17.35 -result();
   17.36 -
   17.37 -writeln"An interesting use of the eliminator, when";
   17.38 -(*The early implementation of unification caused non-rigid path in occur check
   17.39 -  See following example.*)
   17.40 -Goal "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)  \
   17.41 -\                  * Eq(?A, ?b(inr(i)), <succ(0), i>)";
   17.42 -by (intr_tac[]);
   17.43 -by eqintr_tac;
   17.44 -by (resolve_tac comp_rls 1);
   17.45 -by (rew_tac[]);
   17.46 -uresult();
   17.47 -
   17.48 -(*Here we allow the type to depend on i.  
   17.49 - This prevents the cycle in the first unification (no longer needed).  
   17.50 - Requires flex-flex to preserve the dependence.
   17.51 - Simpler still: make ?A into a constant type N*N.*)
   17.52 -Goal "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)   \
   17.53 -\                 *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
   17.54 -
   17.55 -writeln"A tricky combination of when and split";
   17.56 -(*Now handled easily, but caused great problems once*)
   17.57 -Goal 
   17.58 -    "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)   \
   17.59 -\                          *  Eq(?A, ?b(inr(<i,j>)), j)";
   17.60 -by (intr_tac[]); 
   17.61 -by eqintr_tac;
   17.62 -by (resolve_tac [ PlusC_inl RS trans_elem ] 1);
   17.63 -by (resolve_tac comp_rls 4); 
   17.64 -by (resolve_tac reduction_rls 7);
   17.65 -by (resolve_tac comp_rls 10);
   17.66 -by (typechk_tac[]); (*2 secs*)
   17.67 -by (fold_tac basic_defs);
   17.68 -uresult();
   17.69 -
   17.70 -(*similar but allows the type to depend on i and j*)
   17.71 -Goal "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
   17.72 -\                         *   Eq(?A(i,j), ?b(inr(<i,j>)), j)";
   17.73 -
   17.74 -(*similar but specifying the type N simplifies the unification problems*)
   17.75 -Goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)  \
   17.76 -\                         *   Eq(N, ?b(inr(<i,j>)), j)";
   17.77 -
   17.78 -
   17.79 -writeln"Deriving the addition operator";
   17.80 -Goal "?c : PROD n:N. Eq(N, ?f(0,n), n)  \
   17.81 -\                 *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
   17.82 -by (intr_tac[]);
   17.83 -by eqintr_tac;
   17.84 -by (resolve_tac comp_rls 1);
   17.85 -by (rew_tac[]);
   17.86 -by (fold_tac arith_defs);
   17.87 -result();
   17.88 -
   17.89 -writeln"The addition function -- using explicit lambdas";
   17.90 -Goal
   17.91 -  "?c : SUM plus : ?A .  \
   17.92 -\        PROD x:N. Eq(N, plus`0`x, x)  \
   17.93 -\               *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";
   17.94 -by (intr_tac[]);
   17.95 -by eqintr_tac;
   17.96 -by (resolve_tac [TSimp.split_eqn] 3);
   17.97 -by (SELECT_GOAL (rew_tac[]) 4);
   17.98 -by (resolve_tac [TSimp.split_eqn] 3);
   17.99 -by (SELECT_GOAL (rew_tac[]) 4);
  17.100 -by (res_inst_tac [("p","y")] NC_succ 3);
  17.101 -  (**  by (resolve_tac comp_rls 3);  caused excessive branching  **)
  17.102 -by (rew_tac[]); 
  17.103 -by (fold_tac arith_defs);
  17.104 -result();
  17.105 -
  17.106 -writeln"Reached end of file.";
    18.1 --- a/src/CTT/ex/typechk.ML	Fri Jun 02 16:06:19 2006 +0200
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,82 +0,0 @@
    18.4 -(*  Title:      CTT/ex/typechk
    18.5 -    ID:         $Id$
    18.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.7 -    Copyright   1991  University of Cambridge
    18.8 -  
    18.9 -Easy examples: type checking and type deduction
   18.10 -*)
   18.11 -
   18.12 -writeln"Single-step proofs: verifying that a type is well-formed";
   18.13 -
   18.14 -Goal "?A type";
   18.15 -by (resolve_tac form_rls 1);
   18.16 -result(); 
   18.17 -writeln"getting a second solution";
   18.18 -back();
   18.19 -by (resolve_tac form_rls 1);
   18.20 -by (resolve_tac form_rls 1);
   18.21 -result(); 
   18.22 -
   18.23 -Goal "PROD z:?A . N + ?B(z) type";
   18.24 -by (resolve_tac form_rls 1);
   18.25 -by (resolve_tac form_rls 1);
   18.26 -by (resolve_tac form_rls 1);
   18.27 -by (resolve_tac form_rls 1);
   18.28 -by (resolve_tac form_rls 1);
   18.29 -uresult(); 
   18.30 -
   18.31 -
   18.32 -writeln"Multi-step proofs: Type inference";
   18.33 -
   18.34 -Goal "PROD w:N. N + N type";
   18.35 -by form_tac;
   18.36 -result(); 
   18.37 -
   18.38 -Goal "<0, succ(0)> : ?A";
   18.39 -by (intr_tac[]);
   18.40 -result(); 
   18.41 -
   18.42 -Goal "PROD w:N . Eq(?A,w,w) type";
   18.43 -by (typechk_tac[]);
   18.44 -result(); 
   18.45 -
   18.46 -Goal "PROD x:N . PROD y:N . Eq(?A,x,y) type";
   18.47 -by (typechk_tac[]);
   18.48 -result(); 
   18.49 -
   18.50 -writeln"typechecking an application of fst";
   18.51 -Goal "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
   18.52 -by (typechk_tac[]);
   18.53 -result(); 
   18.54 -
   18.55 -writeln"typechecking the predecessor function";
   18.56 -Goal "lam n. rec(n, 0, %x y. x) : ?A";
   18.57 -by (typechk_tac[]);
   18.58 -result(); 
   18.59 -
   18.60 -writeln"typechecking the addition function";
   18.61 -Goal "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
   18.62 -by (typechk_tac[]);
   18.63 -result(); 
   18.64 -
   18.65 -(*Proofs involving arbitrary types.
   18.66 -  For concreteness, every type variable left over is forced to be N*)
   18.67 -val N_tac = TRYALL (rtac NF);
   18.68 -
   18.69 -Goal "lam w. <w,w> : ?A";
   18.70 -by (typechk_tac[]);
   18.71 -by N_tac;
   18.72 -result(); 
   18.73 -
   18.74 -Goal "lam x. lam y. x : ?A";
   18.75 -by (typechk_tac[]);
   18.76 -by N_tac;
   18.77 -result(); 
   18.78 -
   18.79 -writeln"typechecking fst (as a function object) ";
   18.80 -Goal "lam i. split(i, %j k. j) : ?A";
   18.81 -by (typechk_tac[]);
   18.82 -by N_tac;
   18.83 -result(); 
   18.84 -
   18.85 -writeln"Reached end of file.";
    19.1 --- a/src/CTT/rew.ML	Fri Jun 02 16:06:19 2006 +0200
    19.2 +++ b/src/CTT/rew.ML	Fri Jun 02 18:15:38 2006 +0200
    19.3 @@ -1,15 +1,15 @@
    19.4 -(*  Title:      CTT/rew
    19.5 +(*  Title:      CTT/rew.ML
    19.6      ID:         $Id$
    19.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.8      Copyright   1991  University of Cambridge
    19.9  
   19.10 -Simplifier for CTT, using Typedsimp
   19.11 +Simplifier for CTT, using Typedsimp.
   19.12  *)
   19.13  
   19.14  (*Make list of ProdE RS ProdE ... RS ProdE RS EqE
   19.15    for using assumptions as rewrite rules*)
   19.16  fun peEs 0 = []
   19.17 -  | peEs n = EqE :: map (curry (op RS) ProdE) (peEs (n-1));
   19.18 +  | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
   19.19  
   19.20  (*Tactic used for proving conditions for the cond_rls*)
   19.21  val prove_cond_tac = eresolve_tac (peEs 5);
   19.22 @@ -17,19 +17,19 @@
   19.23  
   19.24  structure TSimp_data: TSIMP_DATA =
   19.25    struct
   19.26 -  val refl              = refl_elem
   19.27 -  val sym               = sym_elem
   19.28 -  val trans             = trans_elem
   19.29 -  val refl_red          = refl_red
   19.30 -  val trans_red         = trans_red
   19.31 -  val red_if_equal      = red_if_equal
   19.32 -  val default_rls       = comp_rls
   19.33 -  val routine_tac       = routine_tac routine_rls
   19.34 +  val refl              = thm "refl_elem"
   19.35 +  val sym               = thm "sym_elem"
   19.36 +  val trans             = thm "trans_elem"
   19.37 +  val refl_red          = thm "refl_red"
   19.38 +  val trans_red         = thm "trans_red"
   19.39 +  val red_if_equal      = thm "red_if_equal"
   19.40 +  val default_rls       = thms "comp_rls"
   19.41 +  val routine_tac       = routine_tac (thms "routine_rls")
   19.42    end;
   19.43  
   19.44  structure TSimp = TSimpFun (TSimp_data);
   19.45  
   19.46 -val standard_congr_rls = intrL2_rls @ elimL_rls;
   19.47 +val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
   19.48  
   19.49  (*Make a rewriting tactic from a normalization tactic*)
   19.50  fun make_rew_tac ntac =