--- a/src/CTT/Arith.ML Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,422 +0,0 @@
-(* Title: CTT/Arith.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Proofs about elementary arithmetic: addition, multiplication, etc.
-Tests definitions and simplifier.
-*)
-
-val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def];
-
-
-(** Addition *)
-
-(*typing of add: short and long versions*)
-
-Goalw arith_defs "[| a:N; b:N |] ==> a #+ b : N";
-by (typechk_tac []) ;
-qed "add_typing";
-
-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*)
-
-Goalw arith_defs "b:N ==> 0 #+ b = b : N";
-by (rew_tac []) ;
-qed "addC0";
-
-Goalw arith_defs "[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
-by (rew_tac []) ;
-qed "addC_succ";
-
-
-(** Multiplication *)
-
-(*typing of mult: short and long versions*)
-
-Goalw arith_defs "[| a:N; b:N |] ==> a #* b : N";
-by (typechk_tac [add_typing]) ;
-qed "mult_typing";
-
-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*)
-
-Goalw arith_defs "b:N ==> 0 #* b = 0 : N";
-by (rew_tac []) ;
-qed "multC0";
-
-Goalw arith_defs "[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
-by (rew_tac []) ;
-qed "multC_succ";
-
-
-(** Difference *)
-
-(*typing of difference*)
-
-Goalw arith_defs "[| a:N; b:N |] ==> a - b : N";
-by (typechk_tac []) ;
-qed "diff_typing";
-
-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*)
-
-Goalw arith_defs "a:N ==> a - 0 = a : N";
-by (rew_tac []) ;
-qed "diffC0";
-
-(*Note: rec(a, 0, %z w.z) is pred(a). *)
-
-Goalw arith_defs "b:N ==> 0 - b = 0 : N";
-by (NE_tac "b" 1);
-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) *)
-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 []) ;
-qed "diff_succ_succ";
-
-
-
-(*** Simplification *)
-
-val arith_typing_rls =
- [add_typing, mult_typing, diff_typing];
-
-val arith_congr_rls =
- [add_typingL, mult_typingL, diff_typingL];
-
-val congr_rls = arith_congr_rls@standard_congr_rls;
-
-val arithC_rls =
- [addC0, addC_succ,
- multC0, multC_succ,
- diffC0, diff_0_eq_0, diff_succ_succ];
-
-
-structure Arith_simp_data: TSIMP_DATA =
- struct
- val refl = refl_elem
- val sym = sym_elem
- val trans = trans_elem
- val refl_red = refl_red
- val trans_red = trans_red
- val red_if_equal = red_if_equal
- val default_rls = arithC_rls @ comp_rls
- val routine_tac = routine_tac (arith_typing_rls @ routine_rls)
- end;
-
-structure Arith_simp = TSimpFun (Arith_simp_data);
-
-fun arith_rew_tac prems = make_rew_tac
- (Arith_simp.norm_tac(congr_rls, prems));
-
-fun hyp_arith_rew_tac prems = make_rew_tac
- (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems));
-
-
-(**********
- Addition
- **********)
-
-(*Associative law for addition*)
-Goal "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
-by (NE_tac "a" 1);
-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*)
-Goal "[| a:N; b:N |] ==> a #+ b = b #+ a : N";
-by (NE_tac "a" 1);
-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 []) ;
-qed "add_commute";
-
-
-(****************
- Multiplication
- ****************)
-
-(*Commutative law for multiplication
-Goal "[| a:N; b:N |] ==> a #* b = b #* a : N";
-by (NE_tac "a" 1);
-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 []) ;
-qed "mult_commute"; NEEDS COMMUTATIVE MATCHING
-***************)
-
-(*right annihilation in product*)
-Goal "a:N ==> a #* 0 = 0 : N";
-by (NE_tac "a" 1);
-by (hyp_arith_rew_tac []) ;
-qed "mult_0_right";
-
-(*right successor law for multiplication*)
-Goal "[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
-by (NE_tac "a" 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*)
-Goal "[| a:N; b:N |] ==> a #* b = b #* a : N";
-by (NE_tac "a" 1);
-by (hyp_arith_rew_tac [mult_0_right, mult_succ_right]) ;
-qed "mult_commute";
-
-(*addition distributes over multiplication*)
-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 [add_assoc RS sym_elem]) ;
-qed "add_mult_distrib";
-
-
-(*Associative law for multiplication*)
-Goal "[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
-by (NE_tac "a" 1);
-by (hyp_arith_rew_tac [add_mult_distrib]) ;
-qed "mult_assoc";
-
-
-(************
- Difference
- ************
-
-Difference on natural numbers, without negative numbers
- a - b = 0 iff a<=b a - b = succ(c) iff a>b *)
-
-Goal "a:N ==> a - a = 0 : N";
-by (NE_tac "a" 1);
-by (hyp_arith_rew_tac []) ;
-qed "diff_self_eq_0";
-
-
-(* [| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N *)
-val add_0_right = addC0 RSN (3, add_commute RS trans_elem);
-
-(*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.*)
-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);
-(*case analysis on x in
- (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
-by (NE_tac "x" 4 THEN assume_tac 4);
-(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
-by (rtac replace_type 5);
-by (rtac replace_type 4);
-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 [add_0_right]);
-by (assume_tac 1);
-qed "add_diff_inverse_lemma";
-
-
-(*Version of above with premise b-a=0 i.e. a >= b.
- 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. *)
-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 (ares_tac [EqI] 1));
-qed "add_diff_inverse";
-
-
-(********************
- Absolute difference
- ********************)
-
-(*typing of absolute difference: short and long versions*)
-
-Goalw arith_defs "[| a:N; b:N |] ==> a |-| b : N";
-by (typechk_tac []) ;
-qed "absdiff_typing";
-
-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 [diff_self_eq_0]) ;
-qed "absdiff_self_eq_0";
-
-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";
-by (hyp_arith_rew_tac []) ;
-qed "absdiff_succ_succ";
-
-(*Note how easy using commutative laws can be? ...not always... *)
-Goalw [absdiff_def] "[| a:N; b:N |] ==> a |-| b = b |-| a : N";
-by (rtac add_commute 1);
-by (typechk_tac [diff_typing]);
-qed "absdiff_commute";
-
-(*If a+b=0 then a=0. Surprisingly tedious*)
-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 []);
-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]);
-qed "add_eq0_lemma";
-
-(*Version of above with the premise a+b=0.
- Again, resolution instantiates variables in ProdE *)
-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 (typechk_tac []) ;
-qed "add_eq0";
-
-(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
-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[]);
-by eqintr_tac;
-by (rtac add_eq0 2);
-by (rtac add_eq0 1);
-by (resolve_tac [add_commute RS trans_elem] 6);
-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*)
-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 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 [add_0_right]);
-qed "absdiff_eq0";
-
-(***********************
- Remainder and Quotient
- ***********************)
-
-(*typing of remainder: short and long versions*)
-
-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";
-by (equal_tac [absdiff_typingL]) ;
-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]) ;
-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]) ;
-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]) ;
-qed "div_typing";
-
-Goalw [div_def] "[| a=c:N; b=d:N |] ==> a div b = c div d : N";
-by (equal_tac [absdiff_typingL, mod_typingL]);
-qed "div_typingL";
-
-val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
-
-
-(*computation for quotient: 0 and successor cases*)
-
-Goalw [div_def] "b:N ==> 0 div b = 0 : N";
-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]) ;
-qed "divC_succ";
-
-
-(*Version of above with same condition as the mod one*)
-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 @ [modC_succ]));
-by (NE_tac "succ(a mod b)|-|b" 1);
-by (rew_tac [mod_typing, div_typing, absdiff_typing]);
-qed "divC_succ2";
-
-(*for case analysis on whether a number is 0 or a successor*)
-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 []) ;
-qed "iszero_decidable";
-
-(*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *)
-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@[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 (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 (div_typing_rls));
-qed "mod_div_equality";
--- a/src/CTT/Arith.thy Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/Arith.thy Fri Jun 02 18:15:38 2006 +0200
@@ -4,16 +4,13 @@
Copyright 1991 University of Cambridge
*)
-header {* Arithmetic operators and their definitions *}
+header {* Elementary arithmetic *}
theory Arith
imports Bool
begin
-text {*
- Proves about elementary arithmetic: addition, multiplication, etc.
- Tests definitions and simplifier.
-*}
+subsection {* Arithmetic operators and their definitions *}
consts
"#+" :: "[i,i]=>i" (infixr 65)
@@ -37,6 +34,426 @@
mod_def: "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
div_def: "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
-ML {* use_legacy_bindings (the_context ()) *}
+lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
+
+
+subsection {* Proofs about elementary arithmetic: addition, multiplication, etc. *}
+
+(** Addition *)
+
+(*typing of add: short and long versions*)
+
+lemma add_typing: "[| a:N; b:N |] ==> a #+ b : N"
+apply (unfold arith_defs)
+apply (tactic "typechk_tac []")
+done
+
+lemma add_typingL: "[| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N"
+apply (unfold arith_defs)
+apply (tactic "equal_tac []")
+done
+
+
+(*computation for add: 0 and successor cases*)
+
+lemma addC0: "b:N ==> 0 #+ b = b : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+lemma addC_succ: "[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+
+(** Multiplication *)
+
+(*typing of mult: short and long versions*)
+
+lemma mult_typing: "[| a:N; b:N |] ==> a #* b : N"
+apply (unfold arith_defs)
+apply (tactic {* typechk_tac [thm "add_typing"] *})
+done
+
+lemma mult_typingL: "[| a=c:N; b=d:N |] ==> a #* b = c #* d : N"
+apply (unfold arith_defs)
+apply (tactic {* equal_tac [thm "add_typingL"] *})
+done
+
+(*computation for mult: 0 and successor cases*)
+
+lemma multC0: "b:N ==> 0 #* b = 0 : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+lemma multC_succ: "[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+
+(** Difference *)
+
+(*typing of difference*)
+
+lemma diff_typing: "[| a:N; b:N |] ==> a - b : N"
+apply (unfold arith_defs)
+apply (tactic "typechk_tac []")
+done
+
+lemma diff_typingL: "[| a=c:N; b=d:N |] ==> a - b = c - d : N"
+apply (unfold arith_defs)
+apply (tactic "equal_tac []")
+done
+
+
+(*computation for difference: 0 and successor cases*)
+
+lemma diffC0: "a:N ==> a - 0 = a : N"
+apply (unfold arith_defs)
+apply (tactic "rew_tac []")
+done
+
+(*Note: rec(a, 0, %z w.z) is pred(a). *)
+
+lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
+apply (unfold arith_defs)
+apply (tactic {* NE_tac "b" 1 *})
+apply (tactic "hyp_rew_tac []")
+done
+
+
+(*Essential to simplify FIRST!! (Else we get a critical pair)
+ succ(a) - succ(b) rewrites to pred(succ(a) - b) *)
+lemma diff_succ_succ: "[| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N"
+apply (unfold arith_defs)
+apply (tactic "hyp_rew_tac []")
+apply (tactic {* NE_tac "b" 1 *})
+apply (tactic "hyp_rew_tac []")
+done
+
+
+subsection {* Simplification *}
+
+lemmas arith_typing_rls = add_typing mult_typing diff_typing
+ and arith_congr_rls = add_typingL mult_typingL diff_typingL
+lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls
+
+lemmas arithC_rls =
+ addC0 addC_succ
+ multC0 multC_succ
+ diffC0 diff_0_eq_0 diff_succ_succ
+
+ML {*
+
+structure Arith_simp_data: TSIMP_DATA =
+ struct
+ val refl = thm "refl_elem"
+ val sym = thm "sym_elem"
+ val trans = thm "trans_elem"
+ val refl_red = thm "refl_red"
+ val trans_red = thm "trans_red"
+ val red_if_equal = thm "red_if_equal"
+ val default_rls = thms "arithC_rls" @ thms "comp_rls"
+ val routine_tac = routine_tac (thms "arith_typing_rls" @ thms "routine_rls")
+ end
+
+structure Arith_simp = TSimpFun (Arith_simp_data)
+
+local val congr_rls = thms "congr_rls" in
+
+fun arith_rew_tac prems = make_rew_tac
+ (Arith_simp.norm_tac(congr_rls, prems))
+
+fun hyp_arith_rew_tac prems = make_rew_tac
+ (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems))
end
+*}
+
+
+subsection {* Addition *}
+
+(*Associative law for addition*)
+lemma add_assoc: "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+
+(*Commutative law for addition. Can be proved using three inductions.
+ Must simplify after first induction! Orientation of rewrites is delicate*)
+lemma add_commute: "[| a:N; b:N |] ==> a #+ b = b #+ a : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+apply (tactic {* NE_tac "b" 2 *})
+apply (rule sym_elem)
+apply (tactic {* NE_tac "b" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+
+subsection {* Multiplication *}
+
+(*right annihilation in product*)
+lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+(*right successor law for multiplication*)
+lemma mult_succ_right: "[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
+apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
+done
+
+(*Commutative law for multiplication*)
+lemma mult_commute: "[| a:N; b:N |] ==> a #* b = b #* a : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [thm "mult_0_right", thm "mult_succ_right"] *})
+done
+
+(*addition distributes over multiplication*)
+lemma add_mult_distrib: "[| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
+done
+
+(*Associative law for multiplication*)
+lemma mult_assoc: "[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [thm "add_mult_distrib"] *})
+done
+
+
+subsection {* Difference *}
+
+text {*
+Difference on natural numbers, without negative numbers
+ a - b = 0 iff a<=b a - b = succ(c) iff a>b *}
+
+lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+
+lemma add_0_right: "[| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N"
+ by (rule addC0 [THEN [3] add_commute [THEN trans_elem]])
+
+(*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.*)
+lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
+apply (tactic {* NE_tac "b" 1 *})
+(*strip one "universal quantifier" but not the "implication"*)
+apply (rule_tac [3] intr_rls)
+(*case analysis on x in
+ (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
+apply (tactic {* NE_tac "x" 4 *}, tactic "assume_tac 4")
+(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
+apply (rule_tac [5] replace_type)
+apply (rule_tac [4] replace_type)
+apply (tactic "arith_rew_tac []")
+(*Solves first 0 goal, simplifies others. Two sugbgoals remain.
+ Both follow by rewriting, (2) using quantified induction hyp*)
+apply (tactic "intr_tac []") (*strips remaining PRODs*)
+apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
+apply assumption
+done
+
+
+(*Version of above with premise b-a=0 i.e. a >= b.
+ 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. *)
+lemma add_diff_inverse: "[| a:N; b:N; b-a = 0 : N |] ==> b #+ (a-b) = a : N"
+apply (rule EqE)
+apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE])
+apply (assumption | rule EqI)+
+done
+
+
+subsection {* Absolute difference *}
+
+(*typing of absolute difference: short and long versions*)
+
+lemma absdiff_typing: "[| a:N; b:N |] ==> a |-| b : N"
+apply (unfold arith_defs)
+apply (tactic "typechk_tac []")
+done
+
+lemma absdiff_typingL: "[| a=c:N; b=d:N |] ==> a |-| b = c |-| d : N"
+apply (unfold arith_defs)
+apply (tactic "equal_tac []")
+done
+
+lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
+apply (unfold absdiff_def)
+apply (tactic {* arith_rew_tac [thm "diff_self_eq_0"] *})
+done
+
+lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
+apply (unfold absdiff_def)
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+
+lemma absdiff_succ_succ: "[| a:N; b:N |] ==> succ(a) |-| succ(b) = a |-| b : N"
+apply (unfold absdiff_def)
+apply (tactic "hyp_arith_rew_tac []")
+done
+
+(*Note how easy using commutative laws can be? ...not always... *)
+lemma absdiff_commute: "[| a:N; b:N |] ==> a |-| b = b |-| a : N"
+apply (unfold absdiff_def)
+apply (rule add_commute)
+apply (tactic {* typechk_tac [thm "diff_typing"] *})
+done
+
+(*If a+b=0 then a=0. Surprisingly tedious*)
+lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"
+apply (tactic {* NE_tac "a" 1 *})
+apply (rule_tac [3] replace_type)
+apply (tactic "arith_rew_tac []")
+apply (tactic "intr_tac []") (*strips remaining PRODs*)
+apply (rule_tac [2] zero_ne_succ [THEN FE])
+apply (erule_tac [3] EqE [THEN sym_elem])
+apply (tactic {* typechk_tac [thm "add_typing"] *})
+done
+
+(*Version of above with the premise a+b=0.
+ Again, resolution instantiates variables in ProdE *)
+lemma add_eq0: "[| a:N; b:N; a #+ b = 0 : N |] ==> a = 0 : N"
+apply (rule EqE)
+apply (rule add_eq0_lemma [THEN ProdE])
+apply (rule_tac [3] EqI)
+apply (tactic "typechk_tac []")
+done
+
+(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
+lemma absdiff_eq0_lem:
+ "[| a:N; b:N; a |-| b = 0 : N |] ==>
+ ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
+apply (unfold absdiff_def)
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule_tac [2] add_eq0)
+apply (rule add_eq0)
+apply (rule_tac [6] add_commute [THEN trans_elem])
+apply (tactic {* typechk_tac [thm "diff_typing"] *})
+done
+
+(*if a |-| b = 0 then a = b
+ proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
+lemma absdiff_eq0: "[| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N"
+apply (rule EqE)
+apply (rule absdiff_eq0_lem [THEN SumE])
+apply (tactic "TRYALL assume_tac")
+apply (tactic eqintr_tac)
+apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
+apply (rule_tac [3] EqE, tactic "assume_tac 3")
+apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
+done
+
+
+subsection {* Remainder and Quotient *}
+
+(*typing of remainder: short and long versions*)
+
+lemma mod_typing: "[| a:N; b:N |] ==> a mod b : N"
+apply (unfold mod_def)
+apply (tactic {* typechk_tac [thm "absdiff_typing"] *})
+done
+
+lemma mod_typingL: "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N"
+apply (unfold mod_def)
+apply (tactic {* equal_tac [thm "absdiff_typingL"] *})
+done
+
+
+(*computation for mod : 0 and successor cases*)
+
+lemma modC0: "b:N ==> 0 mod b = 0 : N"
+apply (unfold mod_def)
+apply (tactic {* rew_tac [thm "absdiff_typing"] *})
+done
+
+lemma modC_succ:
+"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
+apply (unfold mod_def)
+apply (tactic {* rew_tac [thm "absdiff_typing"] *})
+done
+
+
+(*typing of quotient: short and long versions*)
+
+lemma div_typing: "[| a:N; b:N |] ==> a div b : N"
+apply (unfold div_def)
+apply (tactic {* typechk_tac [thm "absdiff_typing", thm "mod_typing"] *})
+done
+
+lemma div_typingL: "[| a=c:N; b=d:N |] ==> a div b = c div d : N"
+apply (unfold div_def)
+apply (tactic {* equal_tac [thm "absdiff_typingL", thm "mod_typingL"] *})
+done
+
+lemmas div_typing_rls = mod_typing div_typing absdiff_typing
+
+
+(*computation for quotient: 0 and successor cases*)
+
+lemma divC0: "b:N ==> 0 div b = 0 : N"
+apply (unfold div_def)
+apply (tactic {* rew_tac [thm "mod_typing", thm "absdiff_typing"] *})
+done
+
+lemma divC_succ:
+ "[| a:N; b:N |] ==> succ(a) div b =
+ rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
+apply (unfold div_def)
+apply (tactic {* rew_tac [thm "mod_typing"] *})
+done
+
+
+(*Version of above with same condition as the mod one*)
+lemma divC_succ2: "[| a:N; b:N |] ==>
+ succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
+apply (rule divC_succ [THEN trans_elem])
+apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *})
+apply (tactic {* NE_tac "succ (a mod b) |-|b" 1 *})
+apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
+done
+
+(*for case analysis on whether a number is 0 or a successor*)
+lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) :
+ Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
+apply (tactic {* NE_tac "a" 1 *})
+apply (rule_tac [3] PlusI_inr)
+apply (rule_tac [2] PlusI_inl)
+apply (tactic eqintr_tac)
+apply (tactic "equal_tac []")
+done
+
+(*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *)
+lemma mod_div_equality: "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
+ [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
+apply (rule EqE)
+(*case analysis on succ(u mod b)|-|b *)
+apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
+apply (erule_tac [3] SumE)
+apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls" @
+ [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
+(*Replace one occurence of b by succ(u mod b). Clumsy!*)
+apply (rule add_typingL [THEN trans_elem])
+apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
+apply (rule_tac [3] refl_elem)
+apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls") *})
+done
+
+end
--- a/src/CTT/Bool.ML Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* Title: CTT/Bool
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-*)
-
-val bool_defs = [Bool_def,true_def,false_def,cond_def];
-
-(*Derivation of rules for the type Bool*)
-
-(*formation rule*)
-Goalw bool_defs "Bool type";
-by (typechk_tac []) ;
-qed "boolF";
-
-
-(*introduction rules for true, false*)
-
-Goalw bool_defs "true : Bool";
-by (typechk_tac []) ;
-qed "boolI_true";
-
-Goalw bool_defs "false : Bool";
-by (typechk_tac []) ;
-qed "boolI_false";
-
-(*elimination rule: typing of cond*)
-Goalw bool_defs
- "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)";
-by (typechk_tac []);
-by (ALLGOALS (etac TE));
-by (typechk_tac []) ;
-qed "boolE";
-
-Goalw bool_defs
- "[| p = q : Bool; a = c : C(true); b = d : C(false) |] \
-\ ==> cond(p,a,b) = cond(q,c,d) : C(p)";
-by (rtac PlusEL 1);
-by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ;
-qed "boolEL";
-
-(*computation rules for true, false*)
-
-Goalw bool_defs
- "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)";
-by (resolve_tac comp_rls 1);
-by (typechk_tac []);
-by (ALLGOALS (etac TE));
-by (typechk_tac []) ;
-qed "boolC_true";
-
-Goalw bool_defs
- "[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)";
-by (resolve_tac comp_rls 1);
-by (typechk_tac []);
-by (ALLGOALS (etac TE));
-by (typechk_tac []) ;
-qed "boolC_false";
--- a/src/CTT/Bool.thy Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/Bool.thy Fri Jun 02 18:15:38 2006 +0200
@@ -8,20 +8,80 @@
theory Bool
imports CTT
-uses "~~/src/Provers/typedsimp.ML" "rew.ML"
begin
-consts
- Bool :: "t"
- true :: "i"
- false :: "i"
- cond :: "[i,i,i]=>i"
-defs
- Bool_def: "Bool == T+T"
- true_def: "true == inl(tt)"
- false_def: "false == inr(tt)"
- cond_def: "cond(a,b,c) == when(a, %u. b, %u. c)"
+constdefs
+ Bool :: "t"
+ "Bool == T+T"
+
+ true :: "i"
+ "true == inl(tt)"
+
+ false :: "i"
+ "false == inr(tt)"
+
+ cond :: "[i,i,i]=>i"
+ "cond(a,b,c) == when(a, %u. b, %u. c)"
+
+lemmas bool_defs = Bool_def true_def false_def cond_def
+
+
+subsection {* Derivation of rules for the type Bool *}
+
+(*formation rule*)
+lemma boolF: "Bool type"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+done
+
+
+(*introduction rules for true, false*)
+
+lemma boolI_true: "true : Bool"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+done
+
+lemma boolI_false: "false : Bool"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+done
-ML {* use_legacy_bindings (the_context ()) *}
+(*elimination rule: typing of cond*)
+lemma boolE:
+ "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)"
+apply (unfold bool_defs)
+apply (tactic "typechk_tac []")
+apply (erule_tac [!] TE)
+apply (tactic "typechk_tac []")
+done
+
+lemma boolEL:
+ "[| p = q : Bool; a = c : C(true); b = d : C(false) |]
+ ==> cond(p,a,b) = cond(q,c,d) : C(p)"
+apply (unfold bool_defs)
+apply (rule PlusEL)
+apply (erule asm_rl refl_elem [THEN TEL])+
+done
+
+(*computation rules for true, false*)
+
+lemma boolC_true:
+ "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)"
+apply (unfold bool_defs)
+apply (rule comp_rls)
+apply (tactic "typechk_tac []")
+apply (erule_tac [!] TE)
+apply (tactic "typechk_tac []")
+done
+
+lemma boolC_false:
+ "[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)"
+apply (unfold bool_defs)
+apply (rule comp_rls)
+apply (tactic "typechk_tac []")
+apply (erule_tac [!] TE)
+apply (tactic "typechk_tac []")
+done
end
--- a/src/CTT/CTT.ML Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,189 +0,0 @@
-(* Title: CTT/CTT.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Tactics and derived rules for Constructive Type Theory
-*)
-
-(*Formation rules*)
-val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
-and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
-
-
-(*Introduction rules
- OMITTED: EqI, because its premise is an eqelem, not an elem*)
-val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
-and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];
-
-
-(*Elimination rules
- OMITTED: EqE, because its conclusion is an eqelem, not an elem
- TE, because it does not involve a constructor *)
-val elim_rls = [NE, ProdE, SumE, PlusE, FE]
-and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];
-
-(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
-val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];
-
-(*rules with conclusion a:A, an elem judgement*)
-val element_rls = intr_rls @ elim_rls;
-
-(*Definitions are (meta)equality axioms*)
-val basic_defs = [fst_def,snd_def];
-
-(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
-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 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 "[| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) \
-\ |] ==> c(p`a): C(p`a)";
-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))
- | 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 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);
-
-fun ASSUME tf i = test_assume_tac i ORELSE tf i;
-
-
-(*For simplification: type formation and checking,
- but no equalities between terms*)
-val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;
-
-fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
-
-
-(*Solve all subgoals "A type" using formation rules. *)
-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. *)
-fun typechk_tac thms =
- let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
- in REPEAT_FIRST (ASSUME tac) end;
-
-
-(*Solve a:A (a flexible, A rigid) by introduction rules.
- Cannot use stringtrees (filt_resolve_tac) since
- goals like ?a:SUM(A,B) have a trivial head-string *)
-fun intr_tac thms =
- let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
- in REPEAT_FIRST (ASSUME tac) end;
-
-
-(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
-fun equal_tac thms =
- let val rls = thms @ form_rls @ element_rls @ intrL_rls @
- elimL_rls @ [refl_elem]
- in REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3)) end;
-
-(*** Simplification ***)
-
-(*To simplify the type in a goal*)
-Goal "[| B = A; a : A |] ==> a : B";
-by (rtac equal_types 1);
-by (rtac sym_type 2);
-by (ALLGOALS assume_tac) ;
-qed "replace_type";
-
-(*Simplify the parameter of a unary type operator.*)
-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));
-by (assume_tac 1) ;
-qed "subst_eqtyparg";
-
-(*Make a reduction rule for simplification.
- A goal a=c becomes b=c, by virtue of a=b *)
-fun resolve_trans rl = rl RS trans_elem;
-
-(*Simplification rules for Constructive Type Theory*)
-val reduction_rls = map resolve_trans comp_rls;
-
-(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
- Uses other intro rules to avoid changing flexible goals.*)
-val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));
-
-(** Tactics that instantiate CTT-rules.
- Vars in the given terms will be incremented!
- The (rtac EqE i) lets them apply to equality judgements. **)
-
-fun NE_tac (sp: string) i =
- TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;
-
-fun SumE_tac (sp: string) i =
- TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;
-
-fun PlusE_tac (sp: string) i =
- TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
-
-(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
-
-(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
-fun add_mp_tac i =
- rtac subst_prodE i THEN assume_tac i THEN assume_tac i;
-
-(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac i = etac subst_prodE i THEN assume_tac i;
-
-(*"safe" when regarded as predicate calculus rules*)
-val safe_brls = sort (make_ord lessb)
- [ (true,FE), (true,asm_rl),
- (false,ProdI), (true,SumE), (true,PlusE) ];
-
-val unsafe_brls =
- [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
- (true,subst_prodE) ];
-
-(*0 subgoals vs 1 or more*)
-val (safe0_brls, safep_brls) =
- List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
-
-fun safestep_tac thms i =
- form_tac ORELSE
- resolve_tac thms i ORELSE
- biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE
- DETERM (biresolve_tac safep_brls i);
-
-fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i);
-
-fun step_tac thms = safestep_tac thms ORELSE' biresolve_tac unsafe_brls;
-
-(*Fails unless it solves the goal!*)
-fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);
-
-(** The elimination rules for fst/snd **)
-
-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 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);
-by (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1);
-by (typechk_tac prems) ;
-qed "SumE_snd";
--- a/src/CTT/CTT.thy Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/CTT.thy Fri Jun 02 18:15:38 2006 +0200
@@ -8,6 +8,7 @@
theory CTT
imports Pure
+uses "~~/src/Provers/typedsimp.ML" ("rew.ML")
begin
typedecl i
@@ -57,36 +58,35 @@
pair :: "[i,i]=>i" ("(1<_,/_>)")
syntax
- "@PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
- "@SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10)
- "@-->" :: "[t,t]=>t" ("(_ -->/ _)" [31,30] 30)
- "@*" :: "[t,t]=>t" ("(_ */ _)" [51,50] 50)
-
+ "_PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
+ "_SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10)
translations
- "PROD x:A. B" => "Prod(A, %x. B)"
- "A --> B" => "Prod(A, %_. B)"
- "SUM x:A. B" => "Sum(A, %x. B)"
- "A * B" => "Sum(A, %_. B)"
+ "PROD x:A. B" == "Prod(A, %x. B)"
+ "SUM x:A. B" == "Sum(A, %x. B)"
+
+abbreviation
+ Arrow :: "[t,t]=>t" (infixr "-->" 30)
+ "A --> B == PROD _:A. B"
+ Times :: "[t,t]=>t" (infixr "*" 50)
+ "A * B == SUM _:A. B"
-print_translation {*
- [("Prod", dependent_tr' ("@PROD", "@-->")),
- ("Sum", dependent_tr' ("@SUM", "@*"))]
-*}
+const_syntax (xsymbols)
+ Elem ("(_ /\<in> _)" [10,10] 5)
+ Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
+ Arrow (infixr "\<longrightarrow>" 30)
+ Times (infixr "\<times>" 50)
+const_syntax (HTML output)
+ Elem ("(_ /\<in> _)" [10,10] 5)
+ Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
+ Times (infixr "\<times>" 50)
syntax (xsymbols)
- "@-->" :: "[t,t]=>t" ("(_ \<longrightarrow>/ _)" [31,30] 30)
- "@*" :: "[t,t]=>t" ("(_ \<times>/ _)" [51,50] 50)
- Elem :: "[i, t]=>prop" ("(_ /\<in> _)" [10,10] 5)
- Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
"@SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10)
"@PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10)
"lam " :: "[idts, i] => i" ("(3\<lambda>\<lambda>_./ _)" 10)
syntax (HTML output)
- "@*" :: "[t,t]=>t" ("(_ \<times>/ _)" [51,50] 50)
- Elem :: "[i, t]=>prop" ("(_ /\<in> _)" [10,10] 5)
- Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
"@SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10)
"@PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10)
"lam " :: "[idts, i] => i" ("(3\<lambda>\<lambda>_./ _)" 10)
@@ -273,6 +273,233 @@
TEL: "[| p = q : T; c = d : C(tt) |] ==> c = d : C(p)"
TC: "p : T ==> p = tt : T"
-ML {* use_legacy_bindings (the_context ()) *}
+
+subsection "Tactics and derived rules for Constructive Type Theory"
+
+(*Formation rules*)
+lemmas form_rls = NF ProdF SumF PlusF EqF FF TF
+ and formL_rls = ProdFL SumFL PlusFL EqFL
+
+(*Introduction rules
+ OMITTED: EqI, because its premise is an eqelem, not an elem*)
+lemmas intr_rls = NI0 NI_succ ProdI SumI PlusI_inl PlusI_inr TI
+ and intrL_rls = NI_succL ProdIL SumIL PlusI_inlL PlusI_inrL
+
+(*Elimination rules
+ OMITTED: EqE, because its conclusion is an eqelem, not an elem
+ TE, because it does not involve a constructor *)
+lemmas elim_rls = NE ProdE SumE PlusE FE
+ and elimL_rls = NEL ProdEL SumEL PlusEL FEL
+
+(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
+lemmas comp_rls = NC0 NC_succ ProdC SumC PlusC_inl PlusC_inr
+
+(*rules with conclusion a:A, an elem judgement*)
+lemmas element_rls = intr_rls elim_rls
+
+(*Definitions are (meta)equality axioms*)
+lemmas basic_defs = fst_def snd_def
+
+(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
+lemma SumIL2: "[| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
+apply (rule sym_elem)
+apply (rule SumIL)
+apply (rule_tac [!] sym_elem)
+apply assumption+
+done
+
+lemmas 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. *)
+lemma subst_prodE:
+ assumes "p: Prod(A,B)"
+ and "a: A"
+ and "!!z. z: B(a) ==> c(z): C(z)"
+ shows "c(p`a): C(p`a)"
+apply (rule prems ProdE)+
+done
+
+
+subsection {* Tactics for type checking *}
+
+ML {*
+
+local
+
+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
+
+in
+
+(*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)
+
+fun ASSUME tf i = test_assume_tac i ORELSE tf i
+
+end;
+
+*}
+
+(*For simplification: type formation and checking,
+ but no equalities between terms*)
+lemmas routine_rls = form_rls formL_rls refl_type element_rls
+
+ML {*
+local
+ val routine_rls = thms "routine_rls";
+ val form_rls = thms "form_rls";
+ val intr_rls = thms "intr_rls";
+ val element_rls = thms "element_rls";
+ val equal_rls = form_rls @ element_rls @ thms "intrL_rls" @
+ thms "elimL_rls" @ thms "refl_elem"
+in
+
+fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
+
+(*Solve all subgoals "A type" using formation rules. *)
+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. *)
+fun typechk_tac thms =
+ let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
+ in REPEAT_FIRST (ASSUME tac) end
+
+(*Solve a:A (a flexible, A rigid) by introduction rules.
+ Cannot use stringtrees (filt_resolve_tac) since
+ goals like ?a:SUM(A,B) have a trivial head-string *)
+fun intr_tac thms =
+ let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
+ in REPEAT_FIRST (ASSUME tac) end
+
+(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
+fun equal_tac thms =
+ REPEAT_FIRST (ASSUME (filt_resolve_tac (thms @ equal_rls) 3))
end
+
+*}
+
+
+subsection {* Simplification *}
+
+(*To simplify the type in a goal*)
+lemma replace_type: "[| B = A; a : A |] ==> a : B"
+apply (rule equal_types)
+apply (rule_tac [2] sym_type)
+apply assumption+
+done
+
+(*Simplify the parameter of a unary type operator.*)
+lemma subst_eqtyparg:
+ assumes "a=c : A"
+ and "!!z. z:A ==> B(z) type"
+ shows "B(a)=B(c)"
+apply (rule subst_typeL)
+apply (rule_tac [2] refl_type)
+apply (rule prems)
+apply assumption
+done
+
+(*Simplification rules for Constructive Type Theory*)
+lemmas reduction_rls = comp_rls [THEN trans_elem]
+
+ML {*
+local
+ val EqI = thm "EqI";
+ val EqE = thm "EqE";
+ val NE = thm "NE";
+ val FE = thm "FE";
+ val ProdI = thm "ProdI";
+ val SumI = thm "SumI";
+ val SumE = thm "SumE";
+ val PlusE = thm "PlusE";
+ val PlusI_inl = thm "PlusI_inl";
+ val PlusI_inr = thm "PlusI_inr";
+ val subst_prodE = thm "subst_prodE";
+ val intr_rls = thms "intr_rls";
+in
+
+(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
+ Uses other intro rules to avoid changing flexible goals.*)
+val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1))
+
+(** Tactics that instantiate CTT-rules.
+ Vars in the given terms will be incremented!
+ The (rtac EqE i) lets them apply to equality judgements. **)
+
+fun NE_tac (sp: string) i =
+ TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i
+
+fun SumE_tac (sp: string) i =
+ TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i
+
+fun PlusE_tac (sp: string) i =
+ TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i
+
+(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
+
+(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
+fun add_mp_tac i =
+ rtac subst_prodE i THEN assume_tac i THEN assume_tac i
+
+(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
+fun mp_tac i = etac subst_prodE i THEN assume_tac i
+
+(*"safe" when regarded as predicate calculus rules*)
+val safe_brls = sort (make_ord lessb)
+ [ (true,FE), (true,asm_rl),
+ (false,ProdI), (true,SumE), (true,PlusE) ]
+
+val unsafe_brls =
+ [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
+ (true,subst_prodE) ]
+
+(*0 subgoals vs 1 or more*)
+val (safe0_brls, safep_brls) =
+ List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls
+
+fun safestep_tac thms i =
+ form_tac ORELSE
+ resolve_tac thms i ORELSE
+ biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE
+ DETERM (biresolve_tac safep_brls i)
+
+fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i)
+
+fun step_tac thms = safestep_tac thms ORELSE' biresolve_tac unsafe_brls
+
+(*Fails unless it solves the goal!*)
+fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
+
+end
+*}
+
+use "rew.ML"
+
+
+subsection {* The elimination rules for fst/snd *}
+
+lemma SumE_fst: "p : Sum(A,B) ==> fst(p) : A"
+apply (unfold basic_defs)
+apply (erule SumE)
+apply assumption
+done
+
+(*The first premise must be p:Sum(A,B) !!*)
+lemma SumE_snd:
+ assumes major: "p: Sum(A,B)"
+ and "A type"
+ and "!!x. x:A ==> B(x) type"
+ shows "snd(p) : B(fst(p))"
+ apply (unfold basic_defs)
+ apply (rule major [THEN SumE])
+ apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
+ apply (tactic {* typechk_tac (thms "prems") *})
+ done
+
+end
--- a/src/CTT/IsaMakefile Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/IsaMakefile Fri Jun 02 18:15:38 2006 +0200
@@ -26,8 +26,8 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.ML Arith.thy \
- Bool.ML Bool.thy CTT.ML CTT.thy Main.thy ROOT.ML rew.ML
+$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \
+ Bool.thy CTT.thy Main.thy ROOT.ML rew.ML
@$(ISATOOL) usedir -b $(OUT)/Pure CTT
@@ -35,8 +35,8 @@
CTT-ex: CTT $(LOG)/CTT-ex.gz
-$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/elim.ML ex/equal.ML \
- ex/synth.ML ex/typechk.ML
+$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \
+ ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy
@$(ISATOOL) usedir $(OUT)/CTT ex
--- a/src/CTT/README.html Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/README.html Fri Jun 02 18:15:38 2006 +0200
@@ -13,10 +13,7 @@
<H2>CTT: Constructive Type Theory</H2>
-This directory contains the ML sources of the Isabelle system for
-Constructive Type Theory (extensional equality, no universes).<p>
-
-The <tt>ex</tt> subdirectory contains some examples.<p>
+This is a version of Constructive Type Theory (extensional equality, no universes).<p>
Useful references on Constructive Type Theory:
--- a/src/CTT/ROOT.ML Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/ROOT.ML Fri Jun 02 18:15:38 2006 +0200
@@ -1,15 +1,10 @@
-(* Title: CTT/ROOT
+(* Title: CTT/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-
-Adds Constructive Type Theory to a database containing pure Isabelle.
-Should be executed in the subdirectory CTT.
*)
val banner = "Constructive Type Theory";
writeln banner;
use_thy "Main";
-
-Goal "tt : T"; (*leave subgoal package empty*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ex/Elimination.thy Fri Jun 02 18:15:38 2006 +0200
@@ -0,0 +1,194 @@
+(* Title: CTT/ex/Elimination.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+
+Some examples taken from P. Martin-L\"of, Intuitionistic type theory
+ (Bibliopolis, 1984).
+*)
+
+header "Examples with elimination rules"
+
+theory Elimination
+imports CTT
+begin
+
+text "This finds the functions fst and snd!"
+
+lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
+apply (tactic {* pc_tac [] 1 *})
+done
+
+lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
+apply (tactic {* pc_tac [] 1 *})
+back
+done
+
+text "Double negation of the Excluded Middle"
+lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
+apply (tactic "intr_tac []")
+apply (rule ProdE)
+apply assumption
+apply (tactic "pc_tac [] 1")
+done
+
+lemma "[| A type; B type |] ==> ?a : (A*B) --> (B*A)"
+apply (tactic "pc_tac [] 1")
+done
+(*The sequent version (ITT) could produce an interesting alternative
+ by backtracking. No longer.*)
+
+text "Binary sums and products"
+lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
+apply (tactic "pc_tac [] 1")
+done
+
+(*A distributive law*)
+lemma "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)"
+apply (tactic "pc_tac [] 1")
+done
+
+(*more general version, same proof*)
+lemma
+ assumes "A type"
+ and "!!x. x:A ==> B(x) type"
+ and "!!x. x:A ==> C(x) type"
+ shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Construction of the currying functional"
+lemma "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
+apply (tactic "pc_tac [] 1")
+done
+
+(*more general goal with same proof*)
+lemma
+ assumes "A type"
+ and "!!x. x:A ==> B(x) type"
+ and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
+ shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
+ (PROD x:A . PROD y:B(x) . C(<x,y>))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
+lemma "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
+apply (tactic "pc_tac [] 1")
+done
+
+(*more general goal with same proof*)
+lemma
+ assumes "A type"
+ and "!!x. x:A ==> B(x) type"
+ and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
+ shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
+ --> (PROD z : (SUM x:A . B(x)) . C(z))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Function application"
+lemma "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B"
+apply (tactic "pc_tac [] 1")
+done
+
+text "Basic test of quantifier reasoning"
+lemma
+ assumes "A type"
+ and "B type"
+ and "!!x y.[| x:A; y:B |] ==> C(x,y) type"
+ shows
+ "?a : (SUM y:B . PROD x:A . C(x,y))
+ --> (PROD x:A . SUM y:B . C(x,y))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Martin-Lof (1984) pages 36-7: the combinator S"
+lemma
+ assumes "A type"
+ and "!!x. x:A ==> B(x) type"
+ and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
+ shows "?a : (PROD x:A. PROD y:B(x). C(x,y))
+ --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
+lemma
+ assumes "A type"
+ and "B type"
+ and "!!z. z: A+B ==> C(z) type"
+ shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
+ --> (PROD z: A+B. C(z))"
+apply (tactic {* pc_tac (thms "prems") 1 *})
+done
+
+(*towards AXIOM OF CHOICE*)
+lemma [folded basic_defs]:
+ "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
+apply (tactic "pc_tac [] 1")
+done
+
+
+(*Martin-Lof (1984) page 50*)
+text "AXIOM OF CHOICE! Delicate use of elimination rules"
+lemma
+ assumes "A type"
+ and "!!x. x:A ==> B(x) type"
+ and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
+ shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
+ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+apply (tactic {* intr_tac (thms "prems") *})
+apply (tactic "add_mp_tac 2")
+apply (tactic "add_mp_tac 1")
+apply (erule SumE_fst)
+apply (rule replace_type)
+apply (rule subst_eqtyparg)
+apply (rule comp_rls)
+apply (rule_tac [4] SumE_snd)
+apply (tactic {* typechk_tac (thm "SumE_fst" :: thms "prems") *})
+done
+
+text "Axiom of choice. Proof without fst, snd. Harder still!"
+lemma [folded basic_defs]:
+ assumes "A type"
+ and "!!x. x:A ==> B(x) type"
+ and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
+ shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
+ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+apply (tactic {* intr_tac (thms "prems") *})
+(*Must not use add_mp_tac as subst_prodE hides the construction.*)
+apply (rule ProdE [THEN SumE], assumption)
+apply (tactic "TRYALL assume_tac")
+apply (rule replace_type)
+apply (rule subst_eqtyparg)
+apply (rule comp_rls)
+apply (erule_tac [4] ProdE [THEN SumE])
+apply (tactic {* typechk_tac (thms "prems") *})
+apply (rule replace_type)
+apply (rule subst_eqtyparg)
+apply (rule comp_rls)
+apply (tactic {* typechk_tac (thms "prems") *})
+apply assumption
+done
+
+text "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) *)
+lemma
+ assumes "A type"
+ and "B type"
+ and "!!z. z:A*B ==> C(z) type"
+ shows "?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))"
+apply (rule intr_rls)
+apply (tactic {* biresolve_tac safe_brls 2 *})
+(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
+apply (rule_tac [2] a = "y" in ProdE)
+apply (tactic {* typechk_tac (thms "prems") *})
+apply (rule SumE, assumption)
+apply (tactic "intr_tac []")
+apply (tactic "TRYALL assume_tac")
+apply (tactic {* typechk_tac (thms "prems") *})
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ex/Equality.thy Fri Jun 02 18:15:38 2006 +0200
@@ -0,0 +1,70 @@
+(* Title: CTT/ex/Equality.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+*)
+
+header "Equality reasoning by rewriting"
+
+theory Equality
+imports CTT
+begin
+
+lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic "rew_tac []")
+done
+
+lemma when_eq: "[| A type; B type; p : A+B |] ==> when(p,inl,inr) = p : A + B"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic "rew_tac []")
+done
+
+(*in the "rec" formulation of addition, 0+n=n *)
+lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic "rew_tac []")
+done
+
+(*the harder version, n+0=n: recursive, uses induction hypothesis*)
+lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic "hyp_rew_tac []")
+done
+
+(*Associativity of addition*)
+lemma "[| 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"
+apply (tactic {* NE_tac "a" 1 *})
+apply (tactic "hyp_rew_tac []")
+done
+
+(*Martin-Lof (1984) page 62: pairing is surjective*)
+lemma "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)"
+apply (rule EqE)
+apply (rule elim_rls, assumption)
+apply (tactic {* DEPTH_SOLVE_1 (rew_tac []) *}) (*!!!!!!!*)
+done
+
+lemma "[| a : A; b : B |] ==>
+ (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
+apply (tactic "rew_tac []")
+done
+
+(*a contrived, complicated simplication, requires sum-elimination also*)
+lemma "(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)"
+apply (rule reduction_rls)
+apply (rule_tac [3] intrL_rls)
+apply (rule_tac [4] EqE)
+apply (rule_tac [4] SumE, tactic "assume_tac 4")
+(*order of unifiers is essential here*)
+apply (tactic "rew_tac []")
+done
+
+end
--- a/src/CTT/ex/ROOT.ML Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/ex/ROOT.ML Fri Jun 02 18:15:38 2006 +0200
@@ -3,12 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Executes all examples for Constructive Type Theory.
+Examples for Constructive Type Theory.
*)
-print_depth 2;
-
-time_use "typechk.ML";
-time_use "elim.ML";
-time_use "equal.ML";
-time_use "synth.ML";
+use_thy "Typechecking";
+use_thy "Elimination";
+use_thy "Equality";
+use_thy "Synthesis";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ex/Synthesis.thy Fri Jun 02 18:15:38 2006 +0200
@@ -0,0 +1,106 @@
+(* Title: CTT/ex/Synthesis.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+*)
+
+header "Synthesis examples, using a crude form of narrowing"
+
+theory Synthesis
+imports Arith
+begin
+
+text "discovery of predecessor function"
+lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
+ * (PROD n:N. Eq(N, pred ` succ(n), n))"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule_tac [3] reduction_rls)
+apply (rule_tac [5] comp_rls)
+apply (tactic "rew_tac []")
+done
+
+text "the function fst as an element of a function type"
+lemma [folded basic_defs]:
+ "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule_tac [2] reduction_rls)
+apply (rule_tac [4] comp_rls)
+apply (tactic "typechk_tac []")
+txt "now put in A everywhere"
+apply assumption+
+done
+
+text "An interesting use of the eliminator, when"
+(*The early implementation of unification caused non-rigid path in occur check
+ See following example.*)
+lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>)
+ * Eq(?A, ?b(inr(i)), <succ(0), i>)"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule comp_rls)
+apply (tactic "rew_tac []")
+oops
+
+(*Here we allow the type to depend on i.
+ 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.*)
+lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>)
+ * Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
+oops
+
+text "A tricky combination of when and split"
+(*Now handled easily, but caused great problems once*)
+lemma [folded basic_defs]:
+ "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
+ * Eq(?A, ?b(inr(<i,j>)), j)"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule PlusC_inl [THEN trans_elem])
+apply (rule_tac [4] comp_rls)
+apply (rule_tac [7] reduction_rls)
+apply (rule_tac [10] comp_rls)
+apply (tactic "typechk_tac []")
+oops
+
+(*similar but allows the type to depend on i and j*)
+lemma "?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)"
+oops
+
+(*similar but specifying the type N simplifies the unification problems*)
+lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
+ * Eq(N, ?b(inr(<i,j>)), j)"
+oops
+
+
+text "Deriving the addition operator"
+lemma [folded arith_defs]:
+ "?c : PROD n:N. Eq(N, ?f(0,n), n)
+ * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (rule comp_rls)
+apply (tactic "rew_tac []")
+oops
+
+text "The addition function -- using explicit lambdas"
+lemma [folded arith_defs]:
+ "?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)))"
+apply (tactic "intr_tac []")
+apply (tactic eqintr_tac)
+apply (tactic "resolve_tac [TSimp.split_eqn] 3")
+apply (tactic "SELECT_GOAL (rew_tac []) 4")
+apply (tactic "resolve_tac [TSimp.split_eqn] 3")
+apply (tactic "SELECT_GOAL (rew_tac []) 4")
+apply (rule_tac [3] p = "y" in NC_succ)
+ (** by (resolve_tac comp_rls 3); caused excessive branching **)
+apply (tactic "rew_tac []")
+done
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ex/Typechecking.thy Fri Jun 02 18:15:38 2006 +0200
@@ -0,0 +1,88 @@
+(* Title: CTT/ex/Typechecking.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+*)
+
+header "Easy examples: type checking and type deduction"
+
+theory Typechecking
+imports CTT
+begin
+
+subsection {* Single-step proofs: verifying that a type is well-formed *}
+
+lemma "?A type"
+apply (rule form_rls)
+done
+
+lemma "?A type"
+apply (rule form_rls)
+back
+apply (rule form_rls)
+apply (rule form_rls)
+done
+
+lemma "PROD z:?A . N + ?B(z) type"
+apply (rule form_rls)
+apply (rule form_rls)
+apply (rule form_rls)
+apply (rule form_rls)
+apply (rule form_rls)
+done
+
+
+subsection {* Multi-step proofs: Type inference *}
+
+lemma "PROD w:N. N + N type"
+apply (tactic form_tac)
+done
+
+lemma "<0, succ(0)> : ?A"
+apply (tactic "intr_tac []")
+done
+
+lemma "PROD w:N . Eq(?A,w,w) type"
+apply (tactic "typechk_tac []")
+done
+
+lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
+apply (tactic "typechk_tac []")
+done
+
+text "typechecking an application of fst"
+lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
+apply (tactic "typechk_tac []")
+done
+
+text "typechecking the predecessor function"
+lemma "lam n. rec(n, 0, %x y. x) : ?A"
+apply (tactic "typechk_tac []")
+done
+
+text "typechecking the addition function"
+lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
+apply (tactic "typechk_tac []")
+done
+
+(*Proofs involving arbitrary types.
+ For concreteness, every type variable left over is forced to be N*)
+ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
+
+lemma "lam w. <w,w> : ?A"
+apply (tactic "typechk_tac []")
+apply (tactic N_tac)
+done
+
+lemma "lam x. lam y. x : ?A"
+apply (tactic "typechk_tac []")
+apply (tactic N_tac)
+done
+
+text "typechecking fst (as a function object)"
+lemma "lam i. split(i, %j k. j) : ?A"
+apply (tactic "typechk_tac []")
+apply (tactic N_tac)
+done
+
+end
--- a/src/CTT/ex/elim.ML Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,182 +0,0 @@
-(* Title: CTT/ex/elim
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Some examples taken from P. Martin-L\"of, Intuitionistic type theory
- (Bibliopolis, 1984).
-
-by (safe_tac prems 1);
-by (step_tac prems 1);
-by (pc_tac prems 1);
-*)
-
-writeln"Examples with elimination rules";
-
-
-writeln"This finds the functions 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();
-back() handle ERROR _ => writeln"And there are indeed no others";
-
-
-writeln"Double negation of the Excluded Middle";
-Goal "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
-by (intr_tac []);
-by (rtac ProdE 1);
-by (assume_tac 1);
-by (pc_tac [] 1);
-result();
-
-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";
-Goal "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
-by (pc_tac [] 1);
-result();
-
-(*A distributive law*)
-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
- "[| 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";
-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
- "[| 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)). \
-\ (PROD x:A . PROD y:B(x) . C(<x,y>))";
-by (pc_tac prems 1);
-result();
-
-writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)";
-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
- "[| 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";
-Goal "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B";
-by (pc_tac [] 1);
-result();
-
-writeln"Basic test of quantifier reasoning";
-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))";
-by (pc_tac prems 1);
-result();
-
-(*faulty proof attempt, stripping the quantifiers in wrong sequence
-by (intr_tac[]);
-by (pc_tac prems 1); ...fails!! *)
-
-writeln"Martin-Lof (1984) pages 36-7: the combinator S";
-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)) \
-\ --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
-by (pc_tac prems 1);
-result();
-
-writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination";
-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))";
-by (pc_tac prems 1);
-result();
-
-(*towards AXIOM OF CHOICE*)
-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
- "[| 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)). \
-\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
-by (intr_tac prems);
-by (add_mp_tac 2);
-by (add_mp_tac 1);
-by (etac SumE_fst 1);
-by (rtac replace_type 1);
-by (rtac subst_eqtyparg 1);
-by (resolve_tac comp_rls 1);
-by (rtac SumE_snd 4);
-by (typechk_tac (SumE_fst::prems));
-result();
-
-writeln"Axiom of choice. Proof without fst, snd. Harder still!";
-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)). \
-\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
-by (intr_tac prems);
-(*Must not use add_mp_tac as subst_prodE hides the construction.*)
-by (resolve_tac [ProdE RS SumE] 1 THEN assume_tac 1);
-by (TRYALL assume_tac);
-by (rtac replace_type 1);
-by (rtac subst_eqtyparg 1);
-by (resolve_tac comp_rls 1);
-by (etac (ProdE RS SumE) 4);
-by (typechk_tac prems);
-by (rtac replace_type 1);
-by (rtac subst_eqtyparg 1);
-by (resolve_tac comp_rls 1);
-by (typechk_tac prems);
-by (assume_tac 1);
-by (fold_tac basic_defs); (*puts in fst and snd*)
-result();
-
-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
- "[| 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);
-by (biresolve_tac safe_brls 2);
-(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
-by (res_inst_tac [ ("a","y") ] ProdE 2);
-by (typechk_tac prems);
-by (rtac SumE 1 THEN assume_tac 1);
-by (intr_tac[]);
-by (TRYALL assume_tac);
-by (typechk_tac prems);
-result();
-
-writeln"Reached end of file.";
--- a/src/CTT/ex/equal.ML Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(* Title: CTT/ex/equal
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Equality reasoning by rewriting.
-*)
-
-Goal "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
-by (rtac EqE 1);
-by (resolve_tac elim_rls 1 THEN assume_tac 1);
-by (rew_tac []);
-qed "split_eq";
-
-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 assume_tac 1);
-by (rew_tac []);
-by (ALLGOALS assume_tac);
-qed "when_eq";
-
-
-(*in the "rec" formulation of addition, 0+n=n *)
-Goal "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
-by (rtac EqE 1);
-by (resolve_tac elim_rls 1 THEN assume_tac 1);
-by (rew_tac []);
-result();
-
-
-(*the harder version, n+0=n: recursive, uses induction hypothesis*)
-Goal "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
-by (rtac EqE 1);
-by (resolve_tac elim_rls 1 THEN assume_tac 1);
-by (hyp_rew_tac []);
-result();
-
-
-(*Associativity of addition*)
-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 []);
-result();
-
-
-(*Martin-Lof (1984) page 62: pairing is surjective*)
-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 assume_tac 1);
-by (DEPTH_SOLVE_1 (rew_tac [])); (*!!!!!!!*)
-result();
-
-
-Goal "[| a : A; b : B |] ==> \
-\ (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A";
-by (rew_tac []);
-result();
-
-
-(*a contrived, complicated simplication, requires sum-elimination also*)
-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 []);
-result();
-
-writeln"Reached end of file.";
-(*28 August 1988: loaded this file in 34 seconds*)
-(*2 September 1988: loaded this file in 48 seconds*)
--- a/src/CTT/ex/synth.ML Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,103 +0,0 @@
-(* Title: CTT/ex/synth
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-*)
-
-writeln"Synthesis examples, using a crude form of narrowing";
-
-context (theory "Arith");
-
-writeln"discovery of predecessor function";
-Goal
- "?a : SUM pred:?A . Eq(N, pred`0, 0) \
-\ * (PROD n:N. Eq(N, pred ` succ(n), n))";
-by (intr_tac[]);
-by eqintr_tac;
-by (resolve_tac reduction_rls 3);
-by (resolve_tac comp_rls 5);
-by (rew_tac[]);
-result();
-
-writeln"the function fst as an element of a function type";
-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 []);
-writeln"now put in A everywhere";
-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 "?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);
-by (rew_tac[]);
-uresult();
-
-(*Here we allow the type to depend on i.
- 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 "?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
- "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i) \
-\ * Eq(?A, ?b(inr(<i,j>)), j)";
-by (intr_tac[]);
-by eqintr_tac;
-by (resolve_tac [ PlusC_inl RS trans_elem ] 1);
-by (resolve_tac comp_rls 4);
-by (resolve_tac reduction_rls 7);
-by (resolve_tac comp_rls 10);
-by (typechk_tac[]); (*2 secs*)
-by (fold_tac basic_defs);
-uresult();
-
-(*similar but allows the type to depend on i and j*)
-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 "?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 "?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);
-by (rew_tac[]);
-by (fold_tac arith_defs);
-result();
-
-writeln"The addition function -- using explicit lambdas";
-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)))";
-by (intr_tac[]);
-by eqintr_tac;
-by (resolve_tac [TSimp.split_eqn] 3);
-by (SELECT_GOAL (rew_tac[]) 4);
-by (resolve_tac [TSimp.split_eqn] 3);
-by (SELECT_GOAL (rew_tac[]) 4);
-by (res_inst_tac [("p","y")] NC_succ 3);
- (** by (resolve_tac comp_rls 3); caused excessive branching **)
-by (rew_tac[]);
-by (fold_tac arith_defs);
-result();
-
-writeln"Reached end of file.";
--- a/src/CTT/ex/typechk.ML Fri Jun 02 16:06:19 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(* Title: CTT/ex/typechk
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Easy examples: type checking and type deduction
-*)
-
-writeln"Single-step proofs: verifying that a type is well-formed";
-
-Goal "?A type";
-by (resolve_tac form_rls 1);
-result();
-writeln"getting a second solution";
-back();
-by (resolve_tac form_rls 1);
-by (resolve_tac form_rls 1);
-result();
-
-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);
-by (resolve_tac form_rls 1);
-by (resolve_tac form_rls 1);
-uresult();
-
-
-writeln"Multi-step proofs: Type inference";
-
-Goal "PROD w:N. N + N type";
-by form_tac;
-result();
-
-Goal "<0, succ(0)> : ?A";
-by (intr_tac[]);
-result();
-
-Goal "PROD w:N . Eq(?A,w,w) type";
-by (typechk_tac[]);
-result();
-
-Goal "PROD x:N . PROD y:N . Eq(?A,x,y) type";
-by (typechk_tac[]);
-result();
-
-writeln"typechecking an application of fst";
-Goal "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
-by (typechk_tac[]);
-result();
-
-writeln"typechecking the predecessor function";
-Goal "lam n. rec(n, 0, %x y. x) : ?A";
-by (typechk_tac[]);
-result();
-
-writeln"typechecking the addition function";
-Goal "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
-by (typechk_tac[]);
-result();
-
-(*Proofs involving arbitrary types.
- For concreteness, every type variable left over is forced to be N*)
-val N_tac = TRYALL (rtac NF);
-
-Goal "lam w. <w,w> : ?A";
-by (typechk_tac[]);
-by N_tac;
-result();
-
-Goal "lam x. lam y. x : ?A";
-by (typechk_tac[]);
-by N_tac;
-result();
-
-writeln"typechecking fst (as a function object) ";
-Goal "lam i. split(i, %j k. j) : ?A";
-by (typechk_tac[]);
-by N_tac;
-result();
-
-writeln"Reached end of file.";
--- a/src/CTT/rew.ML Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/rew.ML Fri Jun 02 18:15:38 2006 +0200
@@ -1,15 +1,15 @@
-(* Title: CTT/rew
+(* Title: CTT/rew.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Simplifier for CTT, using Typedsimp
+Simplifier for CTT, using Typedsimp.
*)
(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
for using assumptions as rewrite rules*)
fun peEs 0 = []
- | peEs n = EqE :: map (curry (op RS) ProdE) (peEs (n-1));
+ | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
(*Tactic used for proving conditions for the cond_rls*)
val prove_cond_tac = eresolve_tac (peEs 5);
@@ -17,19 +17,19 @@
structure TSimp_data: TSIMP_DATA =
struct
- val refl = refl_elem
- val sym = sym_elem
- val trans = trans_elem
- val refl_red = refl_red
- val trans_red = trans_red
- val red_if_equal = red_if_equal
- val default_rls = comp_rls
- val routine_tac = routine_tac routine_rls
+ val refl = thm "refl_elem"
+ val sym = thm "sym_elem"
+ val trans = thm "trans_elem"
+ val refl_red = thm "refl_red"
+ val trans_red = thm "trans_red"
+ val red_if_equal = thm "red_if_equal"
+ val default_rls = thms "comp_rls"
+ val routine_tac = routine_tac (thms "routine_rls")
end;
structure TSimp = TSimpFun (TSimp_data);
-val standard_congr_rls = intrL2_rls @ elimL_rls;
+val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
(*Make a rewriting tactic from a normalization tactic*)
fun make_rew_tac ntac =