more tidying. also generalized some tactics to prove "Type A" and
"a = b : A" judgements
--- a/src/CTT/Arith.ML Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/Arith.ML Wed Jul 05 18:27:55 2000 +0200
@@ -1,10 +1,8 @@
-(* Title: CTT/arith
+(* Title: CTT/Arith
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Theorems for arith.thy (Arithmetic operators)
-
Proofs about elementary arithmetic: addition, multiplication, etc.
Tests definitions and simplifier.
*)
@@ -16,27 +14,23 @@
(*typing of add: short and long versions*)
-val prems= goalw Arith.thy arith_defs
- "[| a:N; b:N |] ==> a #+ b : N";
-by (typechk_tac prems) ;
+Goalw arith_defs "[| a:N; b:N |] ==> a #+ b : N";
+by (typechk_tac []) ;
qed "add_typing";
-val prems= goalw Arith.thy arith_defs
- "[| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N";
-by (equal_tac prems) ;
+Goalw arith_defs "[| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N";
+by (equal_tac []) ;
qed "add_typingL";
(*computation for add: 0 and successor cases*)
-val prems= goalw Arith.thy arith_defs
- "b:N ==> 0 #+ b = b : N";
-by (rew_tac prems) ;
+Goalw arith_defs "b:N ==> 0 #+ b = b : N";
+by (rew_tac []) ;
qed "addC0";
-val prems= goalw Arith.thy arith_defs
- "[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
-by (rew_tac prems) ;
+Goalw arith_defs "[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
+by (rew_tac []) ;
qed "addC_succ";
@@ -44,26 +38,22 @@
(*typing of mult: short and long versions*)
-val prems= goalw Arith.thy arith_defs
- "[| a:N; b:N |] ==> a #* b : N";
-by (typechk_tac([add_typing]@prems)) ;
+Goalw arith_defs "[| a:N; b:N |] ==> a #* b : N";
+by (typechk_tac [add_typing]) ;
qed "mult_typing";
-val prems= goalw Arith.thy arith_defs
- "[| a=c:N; b=d:N |] ==> a #* b = c #* d : N";
-by (equal_tac (prems@[add_typingL])) ;
+Goalw arith_defs "[| a=c:N; b=d:N |] ==> a #* b = c #* d : N";
+by (equal_tac [add_typingL]) ;
qed "mult_typingL";
(*computation for mult: 0 and successor cases*)
-val prems= goalw Arith.thy arith_defs
- "b:N ==> 0 #* b = 0 : N";
-by (rew_tac prems) ;
+Goalw arith_defs "b:N ==> 0 #* b = 0 : N";
+by (rew_tac []) ;
qed "multC0";
-val prems= goalw Arith.thy arith_defs
- "[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
-by (rew_tac prems) ;
+Goalw arith_defs "[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
+by (rew_tac []) ;
qed "multC_succ";
@@ -71,41 +61,36 @@
(*typing of difference*)
-val prems= goalw Arith.thy arith_defs
- "[| a:N; b:N |] ==> a - b : N";
-by (typechk_tac prems) ;
+Goalw arith_defs "[| a:N; b:N |] ==> a - b : N";
+by (typechk_tac []) ;
qed "diff_typing";
-val prems= goalw Arith.thy arith_defs
- "[| a=c:N; b=d:N |] ==> a - b = c - d : N";
-by (equal_tac prems) ;
+Goalw arith_defs "[| a=c:N; b=d:N |] ==> a - b = c - d : N";
+by (equal_tac []) ;
qed "diff_typingL";
(*computation for difference: 0 and successor cases*)
-val prems= goalw Arith.thy arith_defs
- "a:N ==> a - 0 = a : N";
-by (rew_tac prems) ;
+Goalw arith_defs "a:N ==> a - 0 = a : N";
+by (rew_tac []) ;
qed "diffC0";
(*Note: rec(a, 0, %z w.z) is pred(a). *)
-val prems= goalw Arith.thy arith_defs
- "b:N ==> 0 - b = 0 : N";
+Goalw arith_defs "b:N ==> 0 - b = 0 : N";
by (NE_tac "b" 1);
-by (hyp_rew_tac prems) ;
+by (hyp_rew_tac []) ;
qed "diff_0_eq_0";
(*Essential to simplify FIRST!! (Else we get a critical pair)
succ(a) - succ(b) rewrites to pred(succ(a) - b) *)
-val prems= goalw Arith.thy arith_defs
- "[| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N";
-by (hyp_rew_tac prems);
+Goalw arith_defs "[| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N";
+by (hyp_rew_tac []);
by (NE_tac "b" 1);
-by (hyp_rew_tac prems) ;
+by (hyp_rew_tac []) ;
qed "diff_succ_succ";
@@ -152,23 +137,21 @@
**********)
(*Associative law for addition*)
-val prems= goal Arith.thy
- "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
+Goal "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
qed "add_assoc";
(*Commutative law for addition. Can be proved using three inductions.
Must simplify after first induction! Orientation of rewrites is delicate*)
-val prems= goal Arith.thy
- "[| a:N; b:N |] ==> a #+ b = b #+ a : N";
+Goal "[| a:N; b:N |] ==> a #+ b = b #+ a : N";
by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems);
+by (hyp_arith_rew_tac []);
by (NE_tac "b" 2);
by (rtac sym_elem 1);
by (NE_tac "b" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
qed "add_commute";
@@ -177,52 +160,48 @@
****************)
(*Commutative law for multiplication
-val prems= goal Arith.thy
- "[| a:N; b:N |] ==> a #* b = b #* a : N";
+Goal "[| a:N; b:N |] ==> a #* b = b #* a : N";
by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems);
+by (hyp_arith_rew_tac []);
by (NE_tac "b" 2);
by (rtac sym_elem 1);
by (NE_tac "b" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
qed "mult_commute"; NEEDS COMMUTATIVE MATCHING
***************)
(*right annihilation in product*)
-val prems= goal Arith.thy
- "a:N ==> a #* 0 = 0 : N";
+Goal "a:N ==> a #* 0 = 0 : N";
by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
qed "mult_0_right";
(*right successor law for multiplication*)
-val prems= goal Arith.thy
- "[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
+Goal "[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
by (NE_tac "a" 1);
-by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem]));
-by (REPEAT (assume_tac 1 ORELSE resolve_tac (prems@[add_commute,mult_typingL,add_typingL]@ intrL_rls@[refl_elem]) 1)) ;
+by (hyp_arith_rew_tac [add_assoc RS sym_elem]);
+by (REPEAT (assume_tac 1
+ ORELSE resolve_tac ([add_commute,mult_typingL,add_typingL]@ intrL_rls@
+ [refl_elem]) 1)) ;
qed "mult_succ_right";
(*Commutative law for multiplication*)
-val prems= goal Arith.thy
- "[| a:N; b:N |] ==> a #* b = b #* a : N";
+Goal "[| a:N; b:N |] ==> a #* b = b #* a : N";
by (NE_tac "a" 1);
-by (hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ;
+by (hyp_arith_rew_tac [mult_0_right, mult_succ_right]) ;
qed "mult_commute";
(*addition distributes over multiplication*)
-val prems= goal Arith.thy
- "[| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N";
+Goal "[| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N";
by (NE_tac "a" 1);
-by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ;
+by (hyp_arith_rew_tac [add_assoc RS sym_elem]) ;
qed "add_mult_distrib";
(*Associative law for multiplication*)
-val prems= goal Arith.thy
- "[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
+Goal "[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
by (NE_tac "a" 1);
-by (hyp_arith_rew_tac (prems @ [add_mult_distrib])) ;
+by (hyp_arith_rew_tac [add_mult_distrib]) ;
qed "mult_assoc";
@@ -233,10 +212,9 @@
Difference on natural numbers, without negative numbers
a - b = 0 iff a<=b a - b = succ(c) iff a>b *)
-val prems= goal Arith.thy
- "a:N ==> a - a = 0 : N";
+Goal "a:N ==> a - a = 0 : N";
by (NE_tac "a" 1);
-by (hyp_arith_rew_tac prems) ;
+by (hyp_arith_rew_tac []) ;
qed "diff_self_eq_0";
@@ -246,9 +224,7 @@
(*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
An example of induction over a quantified formula (a product).
Uses rewriting with a quantified, implicative inductive hypothesis.*)
-val prems =
-goal Arith.thy
- "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
+Goal "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
by (NE_tac "b" 1);
(*strip one "universal quantifier" but not the "implication"*)
by (resolve_tac intr_rls 3);
@@ -258,11 +234,11 @@
(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
by (rtac replace_type 5);
by (rtac replace_type 4);
-by (arith_rew_tac prems);
+by (arith_rew_tac []);
(*Solves first 0 goal, simplifies others. Two sugbgoals remain.
Both follow by rewriting, (2) using quantified induction hyp*)
by (intr_tac[]); (*strips remaining PRODs*)
-by (hyp_arith_rew_tac (prems@[add_0_right]));
+by (hyp_arith_rew_tac [add_0_right]);
by (assume_tac 1);
qed "add_diff_inverse_lemma";
@@ -271,11 +247,10 @@
Using ProdE does not work -- for ?B(?a) is ambiguous.
Instead, add_diff_inverse_lemma states the desired induction scheme;
the use of RS below instantiates Vars in ProdE automatically. *)
-val prems =
-goal Arith.thy "[| a:N; b:N; b-a = 0 : N |] ==> b #+ (a-b) = a : N";
+Goal "[| a:N; b:N; b-a = 0 : N |] ==> b #+ (a-b) = a : N";
by (rtac EqE 1);
by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
-by (REPEAT (resolve_tac (prems@[EqI]) 1));
+by (REPEAT (ares_tac [EqI] 1));
qed "add_diff_inverse";
@@ -285,63 +260,55 @@
(*typing of absolute difference: short and long versions*)
-val prems= goalw Arith.thy arith_defs
- "[| a:N; b:N |] ==> a |-| b : N";
-by (typechk_tac prems) ;
+Goalw arith_defs "[| a:N; b:N |] ==> a |-| b : N";
+by (typechk_tac []) ;
qed "absdiff_typing";
-val prems= goalw Arith.thy arith_defs
- "[| a=c:N; b=d:N |] ==> a |-| b = c |-| d : N";
-by (equal_tac prems) ;
+Goalw arith_defs "[| a=c:N; b=d:N |] ==> a |-| b = c |-| d : N";
+by (equal_tac []) ;
qed "absdiff_typingL";
-Goalw [absdiff_def]
- "a:N ==> a |-| a = 0 : N";
-by (arith_rew_tac (prems@[diff_self_eq_0])) ;
+Goalw [absdiff_def] "a:N ==> a |-| a = 0 : N";
+by (arith_rew_tac [diff_self_eq_0]) ;
qed "absdiff_self_eq_0";
-Goalw [absdiff_def]
- "a:N ==> 0 |-| a = a : N";
+Goalw [absdiff_def] "a:N ==> 0 |-| a = a : N";
by (hyp_arith_rew_tac []);
qed "absdiffC0";
-Goalw [absdiff_def]
- "[| a:N; b:N |] ==> succ(a) |-| succ(b) = a |-| b : N";
+Goalw [absdiff_def] "[| a:N; b:N |] ==> succ(a) |-| succ(b) = a |-| b : N";
by (hyp_arith_rew_tac []) ;
qed "absdiff_succ_succ";
(*Note how easy using commutative laws can be? ...not always... *)
-val prems = goalw Arith.thy [absdiff_def]
- "[| a:N; b:N |] ==> a |-| b = b |-| a : N";
+Goalw [absdiff_def] "[| a:N; b:N |] ==> a |-| b = b |-| a : N";
by (rtac add_commute 1);
-by (typechk_tac ([diff_typing]@prems));
+by (typechk_tac [diff_typing]);
qed "absdiff_commute";
(*If a+b=0 then a=0. Surprisingly tedious*)
-val prems =
-goal Arith.thy "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)";
+Goal "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)";
by (NE_tac "a" 1);
by (rtac replace_type 3);
-by (arith_rew_tac prems);
+by (arith_rew_tac []);
by (intr_tac[]); (*strips remaining PRODs*)
by (resolve_tac [ zero_ne_succ RS FE ] 2);
by (etac (EqE RS sym_elem) 3);
-by (typechk_tac ([add_typing] @prems));
+by (typechk_tac [add_typing]);
qed "add_eq0_lemma";
(*Version of above with the premise a+b=0.
Again, resolution instantiates variables in ProdE *)
-val prems =
-goal Arith.thy "[| a:N; b:N; a #+ b = 0 : N |] ==> a = 0 : N";
+Goal "[| a:N; b:N; a #+ b = 0 : N |] ==> a = 0 : N";
by (rtac EqE 1);
by (resolve_tac [add_eq0_lemma RS ProdE] 1);
by (rtac EqI 3);
-by (ALLGOALS (resolve_tac prems));
+by (typechk_tac []) ;
qed "add_eq0";
(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
-val prems = goalw Arith.thy [absdiff_def]
+Goalw [absdiff_def]
"[| a:N; b:N; a |-| b = 0 : N |] ==> \
\ ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)";
by (intr_tac[]);
@@ -349,20 +316,19 @@
by (rtac add_eq0 2);
by (rtac add_eq0 1);
by (resolve_tac [add_commute RS trans_elem] 6);
-by (typechk_tac (diff_typing::prems));
+by (typechk_tac [diff_typing]);
qed "absdiff_eq0_lem";
(*if a |-| b = 0 then a = b
proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
-val prems =
-goal Arith.thy "[| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N";
+Goal "[| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N";
by (rtac EqE 1);
by (resolve_tac [absdiff_eq0_lem RS SumE] 1);
-by (TRYALL (resolve_tac prems));
+by (TRYALL assume_tac);
by eqintr_tac;
by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
by (rtac EqE 3 THEN assume_tac 3);
-by (hyp_arith_rew_tac (prems@[add_0_right]));
+by (hyp_arith_rew_tac [add_0_right]);
qed "absdiff_eq0";
(***********************
@@ -371,40 +337,35 @@
(*typing of remainder: short and long versions*)
-Goalw [mod_def]
- "[| a:N; b:N |] ==> a mod b : N";
-by (typechk_tac (absdiff_typing::prems)) ;
+Goalw [mod_def] "[| a:N; b:N |] ==> a mod b : N";
+by (typechk_tac [absdiff_typing]) ;
qed "mod_typing";
-Goalw [mod_def]
- "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N";
+Goalw [mod_def] "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N";
by (equal_tac [absdiff_typingL]) ;
-by (ALLGOALS assume_tac);
qed "mod_typingL";
(*computation for mod : 0 and successor cases*)
Goalw [mod_def] "b:N ==> 0 mod b = 0 : N";
-by (rew_tac(absdiff_typing::prems)) ;
+by (rew_tac [absdiff_typing]) ;
qed "modC0";
Goalw [mod_def]
"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N";
-by (rew_tac(absdiff_typing::prems)) ;
+by (rew_tac [absdiff_typing]) ;
qed "modC_succ";
(*typing of quotient: short and long versions*)
Goalw [div_def] "[| a:N; b:N |] ==> a div b : N";
-by (typechk_tac ([absdiff_typing,mod_typing]@prems)) ;
+by (typechk_tac [absdiff_typing,mod_typing]) ;
qed "div_typing";
-Goalw [div_def]
- "[| a=c:N; b=d:N |] ==> a div b = c div d : N";
+Goalw [div_def] "[| a=c:N; b=d:N |] ==> a div b = c div d : N";
by (equal_tac [absdiff_typingL, mod_typingL]);
-by (ALLGOALS assume_tac);
qed "div_typingL";
val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
@@ -413,54 +374,51 @@
(*computation for quotient: 0 and successor cases*)
Goalw [div_def] "b:N ==> 0 div b = 0 : N";
-by (rew_tac([mod_typing, absdiff_typing] @ prems)) ;
+by (rew_tac [mod_typing, absdiff_typing]) ;
qed "divC0";
Goalw [div_def]
"[| a:N; b:N |] ==> succ(a) div b = \
\ rec(succ(a) mod b, succ(a div b), %x y. a div b) : N";
-by (rew_tac([mod_typing]@prems)) ;
+by (rew_tac [mod_typing]) ;
qed "divC_succ";
(*Version of above with same condition as the mod one*)
-val prems= goal Arith.thy
- "[| a:N; b:N |] ==> \
+Goal "[| a:N; b:N |] ==> \
\ succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N";
by (resolve_tac [ divC_succ RS trans_elem ] 1);
-by (rew_tac(div_typing_rls @ prems @ [modC_succ]));
+by (rew_tac(div_typing_rls @ [modC_succ]));
by (NE_tac "succ(a mod b)|-|b" 1);
-by (rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ;
+by (rew_tac [mod_typing, div_typing, absdiff_typing]);
qed "divC_succ2";
(*for case analysis on whether a number is 0 or a successor*)
-val prems= goal Arith.thy
- "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
+Goal "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
\ Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))";
by (NE_tac "a" 1);
by (rtac PlusI_inr 3);
by (rtac PlusI_inl 2);
by eqintr_tac;
-by (equal_tac prems) ;
+by (equal_tac []) ;
qed "iszero_decidable";
(*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *)
-val prems =
-goal Arith.thy "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N";
+Goal "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N";
by (NE_tac "a" 1);
-by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2]));
+by (arith_rew_tac (div_typing_rls@[modC0,modC_succ,divC0,divC_succ2]));
by (rtac EqE 1);
(*case analysis on succ(u mod b)|-|b *)
by (res_inst_tac [("a1", "succ(u mod b) |-| b")]
(iszero_decidable RS PlusE) 1);
by (etac SumE 3);
-by (hyp_arith_rew_tac (prems @ div_typing_rls @
+by (hyp_arith_rew_tac (div_typing_rls @
[modC0,modC_succ, divC0, divC_succ2]));
(*Replace one occurence of b by succ(u mod b). Clumsy!*)
by (resolve_tac [ add_typingL RS trans_elem ] 1);
by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
by (rtac refl_elem 3);
-by (hyp_arith_rew_tac (prems @ div_typing_rls));
+by (hyp_arith_rew_tac (div_typing_rls));
qed "mod_div_equality";
writeln"Reached end of file.";
--- a/src/CTT/Bool.ML Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/Bool.ML Wed Jul 05 18:27:55 2000 +0200
@@ -1,9 +1,9 @@
-(* Title: CTT/bool
+(* Title: CTT/Bool
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Theorems for bool.thy (booleans and conditionals)
+The two-element type (booleans and conditionals)
*)
val bool_defs = [Bool_def,true_def,false_def,cond_def];
--- a/src/CTT/CTT.ML Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/CTT.ML Wed Jul 05 18:27:55 2000 +0200
@@ -1,9 +1,9 @@
-(* Title: CTT/ctt.ML
+(* Title: CTT/CTT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Tactics and lemmas for ctt.thy (Constructive Type Theory)
+Tactics and derived rules for Constructive Type Theory
*)
(*Formation rules*)
@@ -33,30 +33,30 @@
val basic_defs = [fst_def,snd_def];
(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
-val prems= goal CTT.thy
- "[| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
+Goal "[| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
by (rtac sym_elem 1);
by (rtac SumIL 1);
by (ALLGOALS (rtac sym_elem ));
-by (ALLGOALS (resolve_tac prems)) ;
+by (ALLGOALS assume_tac) ;
qed "SumIL2";
val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
(*Exploit p:Prod(A,B) to create the assumption z:B(a).
A more natural form of product elimination. *)
-val prems= goal CTT.thy
- "[| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) \
+val prems = Goal "[| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) \
\ |] ==> c(p`a): C(p`a)";
-by (REPEAT (resolve_tac (prems@[ProdE]) 1)) ;
+by (REPEAT (resolve_tac (ProdE::prems) 1)) ;
qed "subst_prodE";
(** Tactics for type checking **)
-fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not (is_Var (head_of a))
+fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
+ | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
+ | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
| is_rigid_elem _ = false;
-(*Try solving a:A by assumption provided a is rigid!*)
+(*Try solving a:A or a=b:A by assumption provided a is rigid!*)
val test_assume_tac = SUBGOAL(fn (prem,i) =>
if is_rigid_elem (Logic.strip_assums_concl prem)
then assume_tac i else no_tac);
@@ -72,7 +72,7 @@
(*Solve all subgoals "A type" using formation rules. *)
-val form_tac = REPEAT_FIRST (filt_resolve_tac(form_rls) 1);
+val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
@@ -98,16 +98,15 @@
(*** Simplification ***)
(*To simplify the type in a goal*)
-val prems= goal CTT.thy
- "[| B = A; a : A |] ==> a : B";
+Goal "[| B = A; a : A |] ==> a : B";
by (rtac equal_types 1);
by (rtac sym_type 2);
-by (ALLGOALS (resolve_tac prems)) ;
+by (ALLGOALS assume_tac) ;
qed "replace_type";
(*Simplify the parameter of a unary type operator.*)
-val prems= goal CTT.thy
- "a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)";
+val prems = Goal
+ "[| a=c : A; !!z. z:A ==> B(z) type |] ==> B(a)=B(c)";
by (rtac subst_typeL 1);
by (rtac refl_type 2);
by (ALLGOALS (resolve_tac prems));
@@ -175,14 +174,13 @@
(** The elimination rules for fst/snd **)
-val [major] = goalw CTT.thy basic_defs
- "p : Sum(A,B) ==> fst(p) : A";
-by (rtac (major RS SumE) 1);
-by (assume_tac 1) ;
+Goalw basic_defs "p : Sum(A,B) ==> fst(p) : A";
+by (etac SumE 1);
+by (assume_tac 1);
qed "SumE_fst";
(*The first premise must be p:Sum(A,B) !!*)
-val major::prems= goalw CTT.thy basic_defs
+val major::prems= Goalw basic_defs
"[| p: Sum(A,B); A type; !!x. x:A ==> B(x) type \
\ |] ==> snd(p) : B(fst(p))";
by (rtac (major RS SumE) 1);
--- a/src/CTT/ex/elim.ML Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/ex/elim.ML Wed Jul 05 18:27:55 2000 +0200
@@ -15,8 +15,8 @@
writeln"This finds the functions fst and snd!";
-val prems = goal CTT.thy "A type ==> ?a : (A*A) --> A";
-by (pc_tac prems 1 THEN fold_tac basic_defs); (*puts in fst and snd*)
+Goal "A type ==> ?a : (A*A) --> A";
+by (pc_tac [] 1 THEN fold_tac basic_defs); (*puts in fst and snd*)
result();
writeln"first solution is fst; backtracking gives snd";
back();
@@ -24,47 +24,43 @@
writeln"Double negation of the Excluded Middle";
-val prems = goal CTT.thy "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
-by (intr_tac prems);
+Goal "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
+by (intr_tac []);
by (rtac ProdE 1);
by (assume_tac 1);
-by (pc_tac prems 1);
+by (pc_tac [] 1);
result();
-val prems = goal CTT.thy
- "[| A type; B type |] ==> ?a : (A*B) --> (B*A)";
-by (pc_tac prems 1);
+Goal "[| A type; B type |] ==> ?a : (A*B) --> (B*A)";
+by (pc_tac [] 1);
result();
(*The sequent version (ITT) could produce an interesting alternative
by backtracking. No longer.*)
writeln"Binary sums and products";
-val prems = goal CTT.thy
- "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
-by (pc_tac prems 1);
+Goal "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
+by (pc_tac [] 1);
result();
(*A distributive law*)
-val prems = goal CTT.thy
- "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)";
-by (pc_tac prems 1);
+Goal "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)";
+by (pc_tac [] 1);
result();
(*more general version, same proof*)
-val prems = goal CTT.thy
- "[| A type; !!x. x:A ==> B(x) type; !!x. x:A ==> C(x) type|] ==> \
-\ ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))";
+val prems = Goal
+ "[| A type; !!x. x:A ==> B(x) type; !!x. x:A ==> C(x) type|] ==> \
+\ ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))";
by (pc_tac prems 1);
result();
writeln"Construction of the currying functional";
-val prems = goal CTT.thy
- "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))";
-by (pc_tac prems 1);
+Goal "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))";
+by (pc_tac [] 1);
result();
(*more general goal with same proof*)
-val prems = goal CTT.thy
+val prems = Goal
"[| A type; !!x. x:A ==> B(x) type; \
\ !!z. z: (SUM x:A. B(x)) ==> C(z) type \
\ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \
@@ -73,27 +69,25 @@
result();
writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)";
-val prems = goal CTT.thy
- "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
-by (pc_tac prems 1);
+Goal "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
+by (pc_tac [] 1);
result();
(*more general goal with same proof*)
-val prems = goal CTT.thy
- "[| A type; !!x. x:A ==> B(x) type; !!z. z : (SUM x:A . B(x)) ==> C(z) type|] \
+val prems = Goal
+ "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A . B(x)) ==> C(z) type|] \
\ ==> ?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) \
\ --> (PROD z : (SUM x:A . B(x)) . C(z))";
by (pc_tac prems 1);
result();
writeln"Function application";
-val prems = goal CTT.thy
- "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B";
-by (pc_tac prems 1);
+Goal "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B";
+by (pc_tac [] 1);
result();
writeln"Basic test of quantifier reasoning";
-val prems = goal CTT.thy
+val prems = Goal
"[| A type; B type; !!x y.[| x:A; y:B |] ==> C(x,y) type |] ==> \
\ ?a : (SUM y:B . PROD x:A . C(x,y)) \
\ --> (PROD x:A . SUM y:B . C(x,y))";
@@ -105,7 +99,7 @@
by (pc_tac prems 1); ...fails!! *)
writeln"Martin-Lof (1984) pages 36-7: the combinator S";
-val prems = goal CTT.thy
+val prems = Goal
"[| A type; !!x. x:A ==> B(x) type; \
\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type |] \
\ ==> ?a : (PROD x:A. PROD y:B(x). C(x,y)) \
@@ -114,7 +108,7 @@
result();
writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination";
-val prems = goal CTT.thy
+val prems = Goal
"[| A type; B type; !!z. z: A+B ==> C(z) type|] ==> \
\ ?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y))) \
\ --> (PROD z: A+B. C(z))";
@@ -122,15 +116,14 @@
result();
(*towards AXIOM OF CHOICE*)
-val prems = goal CTT.thy
- "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
-by (pc_tac prems 1);
+Goal "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
+by (pc_tac [] 1);
by (fold_tac basic_defs); (*puts in fst and snd*)
result();
(*Martin-Lof (1984) page 50*)
-writeln"AXIOM OF CHOICE!!! Delicate use of elimination rules";
-val prems = goal CTT.thy
+writeln"AXIOM OF CHOICE! Delicate use of elimination rules";
+val prems = Goal
"[| A type; !!x. x:A ==> B(x) type; \
\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \
@@ -147,7 +140,7 @@
result();
writeln"Axiom of choice. Proof without fst, snd. Harder still!";
-val prems = goal CTT.thy
+val prems = Goal
"[| A type; !!x. x:A ==> B(x) type; \
\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \
@@ -172,7 +165,7 @@
writeln"Example of sequent_style deduction";
(*When splitting z:A*B, the assumption C(z) is affected; ?a becomes
lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w) *)
-val prems = goal CTT.thy
+val prems = Goal
"[| A type; B type; !!z. z:A*B ==> C(z) type |] ==> \
\ ?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))";
by (resolve_tac intr_rls 1);
--- a/src/CTT/ex/equal.ML Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/ex/equal.ML Wed Jul 05 18:27:55 2000 +0200
@@ -6,78 +6,68 @@
Equality reasoning by rewriting.
*)
-val prems =
-goal CTT.thy "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
+Goal "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
by (rtac EqE 1);
-by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
-by (rew_tac prems);
+by (resolve_tac elim_rls 1 THEN assume_tac 1);
+by (rew_tac []);
qed "split_eq";
-val prems =
-goal CTT.thy
- "[| A type; B type; p : A+B |] ==> when(p,inl,inr) = p : A + B";
+Goal "[| A type; B type; p : A+B |] ==> when(p,inl,inr) = p : A + B";
by (rtac EqE 1);
-by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
-by (rew_tac prems);
+by (resolve_tac elim_rls 1 THEN assume_tac 1);
+by (rew_tac []);
+by (ALLGOALS assume_tac);
qed "when_eq";
(*in the "rec" formulation of addition, 0+n=n *)
-val prems =
-goal CTT.thy "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
+Goal "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
by (rtac EqE 1);
-by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
-by (rew_tac prems);
+by (resolve_tac elim_rls 1 THEN assume_tac 1);
+by (rew_tac []);
result();
(*the harder version, n+0=n: recursive, uses induction hypothesis*)
-val prems =
-goal CTT.thy "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
+Goal "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
by (rtac EqE 1);
-by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
-by (hyp_rew_tac prems);
+by (resolve_tac elim_rls 1 THEN assume_tac 1);
+by (hyp_rew_tac []);
result();
(*Associativity of addition*)
-val prems =
-goal CTT.thy
- "[| a:N; b:N; c:N |] ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
-\ rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
+Goal "[| a:N; b:N; c:N |] \
+\ ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
+\ rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
by (NE_tac "a" 1);
-by (hyp_rew_tac prems);
+by (hyp_rew_tac []);
result();
(*Martin-Lof (1984) page 62: pairing is surjective*)
-val prems =
-goal CTT.thy
- "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
+Goal "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
by (rtac EqE 1);
-by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
-by (DEPTH_SOLVE_1 (rew_tac prems)); (*!!!!!!!*)
+by (resolve_tac elim_rls 1 THEN assume_tac 1);
+by (DEPTH_SOLVE_1 (rew_tac [])); (*!!!!!!!*)
result();
-val prems =
-goal CTT.thy "[| a : A; b : B |] ==> \
+Goal "[| a : A; b : B |] ==> \
\ (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A";
-by (rew_tac prems);
+by (rew_tac []);
result();
(*a contrived, complicated simplication, requires sum-elimination also*)
-val prems =
-goal CTT.thy
- "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) = \
+Goal "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) = \
\ lam x. x : PROD x:(SUM y:N. N). (SUM y:N. N)";
by (resolve_tac reduction_rls 1);
by (resolve_tac intrL_rls 3);
by (rtac EqE 4);
by (rtac SumE 4 THEN assume_tac 4);
(*order of unifiers is essential here*)
-by (rew_tac prems);
+by (rew_tac []);
result();
writeln"Reached end of file.";
--- a/src/CTT/ex/synth.ML Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/ex/synth.ML Wed Jul 05 18:27:55 2000 +0200
@@ -6,9 +6,10 @@
writeln"Synthesis examples, using a crude form of narrowing";
+context Arith.thy;
writeln"discovery of predecessor function";
-goal CTT.thy
+Goal
"?a : SUM pred:?A . Eq(N, pred`0, 0) \
\ * (PROD n:N. Eq(N, pred ` succ(n), n))";
by (intr_tac[]);
@@ -19,24 +20,22 @@
result();
writeln"the function fst as an element of a function type";
-val prems = goal CTT.thy
- "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)";
-by (intr_tac prems);
+Goal "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)";
+by (intr_tac []);
by eqintr_tac;
by (resolve_tac reduction_rls 2);
by (resolve_tac comp_rls 4);
-by (typechk_tac prems);
+by (typechk_tac []);
writeln"now put in A everywhere";
-by (REPEAT (resolve_tac prems 1));
+by (REPEAT (assume_tac 1));
by (fold_tac basic_defs);
result();
writeln"An interesting use of the eliminator, when";
(*The early implementation of unification caused non-rigid path in occur check
See following example.*)
-goal CTT.thy
- "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) \
-\ * Eq(?A, ?b(inr(i)), <succ(0), i>)";
+Goal "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) \
+\ * Eq(?A, ?b(inr(i)), <succ(0), i>)";
by (intr_tac[]);
by eqintr_tac;
by (resolve_tac comp_rls 1);
@@ -47,13 +46,12 @@
This prevents the cycle in the first unification (no longer needed).
Requires flex-flex to preserve the dependence.
Simpler still: make ?A into a constant type N*N.*)
-goal CTT.thy
- "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>) \
-\ * Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
+Goal "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>) \
+\ * Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
writeln"A tricky combination of when and split";
(*Now handled easily, but caused great problems once*)
-goal CTT.thy
+Goal
"?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i) \
\ * Eq(?A, ?b(inr(<i,j>)), j)";
by (intr_tac[]);
@@ -67,20 +65,17 @@
uresult();
(*similar but allows the type to depend on i and j*)
-goal CTT.thy
- "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
+Goal "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
\ * Eq(?A(i,j), ?b(inr(<i,j>)), j)";
(*similar but specifying the type N simplifies the unification problems*)
-goal CTT.thy
- "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i) \
+Goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i) \
\ * Eq(N, ?b(inr(<i,j>)), j)";
writeln"Deriving the addition operator";
-goal Arith.thy
- "?c : PROD n:N. Eq(N, ?f(0,n), n) \
-\ * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
+Goal "?c : PROD n:N. Eq(N, ?f(0,n), n) \
+\ * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
by (intr_tac[]);
by eqintr_tac;
by (resolve_tac comp_rls 1);
@@ -89,7 +84,7 @@
result();
writeln"The addition function -- using explicit lambdas";
-goal Arith.thy
+Goal
"?c : SUM plus : ?A . \
\ PROD x:N. Eq(N, plus`0`x, x) \
\ * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";
--- a/src/CTT/ex/typechk.ML Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/ex/typechk.ML Wed Jul 05 18:27:55 2000 +0200
@@ -8,7 +8,7 @@
writeln"Single-step proofs: verifying that a type is well-formed";
-goal CTT.thy "?A type";
+Goal "?A type";
by (resolve_tac form_rls 1);
result();
writeln"getting a second solution";
@@ -17,7 +17,7 @@
by (resolve_tac form_rls 1);
result();
-goal CTT.thy "PROD z:?A . N + ?B(z) type";
+Goal "PROD z:?A . N + ?B(z) type";
by (resolve_tac form_rls 1);
by (resolve_tac form_rls 1);
by (resolve_tac form_rls 1);
@@ -28,34 +28,34 @@
writeln"Multi-step proofs: Type inference";
-goal CTT.thy "PROD w:N. N + N type";
+Goal "PROD w:N. N + N type";
by form_tac;
result();
-goal CTT.thy "<0, succ(0)> : ?A";
+Goal "<0, succ(0)> : ?A";
by (intr_tac[]);
result();
-goal CTT.thy "PROD w:N . Eq(?A,w,w) type";
+Goal "PROD w:N . Eq(?A,w,w) type";
by (typechk_tac[]);
result();
-goal CTT.thy "PROD x:N . PROD y:N . Eq(?A,x,y) type";
+Goal "PROD x:N . PROD y:N . Eq(?A,x,y) type";
by (typechk_tac[]);
result();
writeln"typechecking an application of fst";
-goal CTT.thy "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
+Goal "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
by (typechk_tac[]);
result();
writeln"typechecking the predecessor function";
-goal CTT.thy "lam n. rec(n, 0, %x y. x) : ?A";
+Goal "lam n. rec(n, 0, %x y. x) : ?A";
by (typechk_tac[]);
result();
writeln"typechecking the addition function";
-goal CTT.thy "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
+Goal "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
by (typechk_tac[]);
result();
@@ -63,18 +63,18 @@
For concreteness, every type variable left over is forced to be N*)
val N_tac = TRYALL (rtac NF);
-goal CTT.thy "lam w. <w,w> : ?A";
+Goal "lam w. <w,w> : ?A";
by (typechk_tac[]);
by N_tac;
result();
-goal CTT.thy "lam x. lam y. x : ?A";
+Goal "lam x. lam y. x : ?A";
by (typechk_tac[]);
by N_tac;
result();
writeln"typechecking fst (as a function object) ";
-goal CTT.thy "lam i. split(i, %j k. j) : ?A";
+Goal "lam i. split(i, %j k. j) : ?A";
by (typechk_tac[]);
by N_tac;
result();