--- a/src/HOL/Arith.ML Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Arith.ML Mon Feb 05 21:27:16 1996 +0100
@@ -197,26 +197,36 @@
by (rtac refl 1);
qed "less_eq";
+goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \
+ \ (%f j. if j<n then j else f (j-n))";
+by (simp_tac (HOL_ss addsimps [mod_def]) 1);
+val mod_def1 = result() RS eq_reflection;
+
goal Arith.thy "!!m. m<n ==> m mod n = m";
-by (rtac (mod_def RS wf_less_trans) 1);
+by (rtac (mod_def1 RS wf_less_trans) 1);
by(Asm_simp_tac 1);
qed "mod_less";
goal Arith.thy "!!m. [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n";
-by (rtac (mod_def RS wf_less_trans) 1);
+by (rtac (mod_def1 RS wf_less_trans) 1);
by(asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
qed "mod_geq";
(*** Quotient ***)
+goal Arith.thy "(%m. m div n) = wfrec (trancl pred_nat) \
+ \ (%f j. if j<n then 0 else Suc (f (j-n)))";
+by (simp_tac (HOL_ss addsimps [div_def]) 1);
+val div_def1 = result() RS eq_reflection;
+
goal Arith.thy "!!m. m<n ==> m div n = 0";
-by (rtac (div_def RS wf_less_trans) 1);
+by (rtac (div_def1 RS wf_less_trans) 1);
by(Asm_simp_tac 1);
qed "div_less";
goal Arith.thy "!!M. [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)";
-by (rtac (div_def RS wf_less_trans) 1);
+by (rtac (div_def1 RS wf_less_trans) 1);
by(asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
qed "div_geq";
@@ -322,20 +332,20 @@
bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
-by (etac rev_mp 1);
+be rev_mp 1;
by(nat_ind_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
qed "add_lessD1";
goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
-by (etac le_trans 1);
-by (rtac le_add1 1);
+by (eresolve_tac [le_trans] 1);
+by (resolve_tac [le_add1] 1);
qed "le_imp_add_le";
goal Arith.thy "!!k::nat. m < n ==> m < n+k";
-by (etac less_le_trans 1);
-by (rtac le_add1 1);
+by (eresolve_tac [less_le_trans] 1);
+by (resolve_tac [le_add1] 1);
qed "less_imp_add_less";
goal Arith.thy "m+k<=n --> m<=(n::nat)";
@@ -350,7 +360,7 @@
by (asm_full_simp_tac
(!simpset delsimps [add_Suc_right]
addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
-by (etac subst 1);
+by (eresolve_tac [subst] 1);
by (simp_tac (!simpset addsimps [less_add_Suc1]) 1);
qed "less_add_eq_less";
@@ -386,7 +396,7 @@
(*non-strict, in 1st argument*)
goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k";
by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1);
-by (etac add_less_mono1 1);
+by (eresolve_tac [add_less_mono1] 1);
by (assume_tac 1);
qed "add_le_mono1";
@@ -395,5 +405,5 @@
by (etac (add_le_mono1 RS le_trans) 1);
by (simp_tac (!simpset addsimps [add_commute]) 1);
(*j moves to the end because it is free while k, l are bound*)
-by (etac add_le_mono1 1);
+by (eresolve_tac [add_le_mono1] 1);
qed "add_le_mono";
--- a/src/HOL/Arith.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Arith.thy Mon Feb 05 21:27:16 1996 +0100
@@ -20,8 +20,10 @@
add_def "m+n == nat_rec m n (%u v. Suc(v))"
diff_def "m-n == nat_rec n m (%u v. pred(v))"
mult_def "m*n == nat_rec m 0 (%u v. n + v)"
- mod_def "m mod n == wfrec (trancl pred_nat) m (%j f.if j<n then j else f (j-n))"
- div_def "m div n == wfrec (trancl pred_nat) m (%j f.if j<n then 0 else Suc (f (j-n)))"
+mod_def "m mod n == wfrec (trancl pred_nat)
+ (%f j. if j<n then j else f (j-n)) m"
+div_def "m div n == wfrec (trancl pred_nat)
+ (%f j. if j<n then 0 else Suc (f (j-n))) m"
end
(*"Difference" is subtraction of natural numbers.
--- a/src/HOL/Finite.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Finite.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Finite.thy
+(* Title: HOL/Finite.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Finite powerset operator
--- a/src/HOL/Fun.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Fun.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Fun.thy
+(* Title: HOL/Fun.thy
ID: $Id$
- Author: Tobias Nipkow, Cambridge University Computer Laboratory
+ Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Lemmas about functions.
--- a/src/HOL/Gfp.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Gfp.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/gfp.thy
+(* Title: HOL/gfp.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Greatest fixed points (requires Lfp too!)
--- a/src/HOL/Lfp.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Lfp.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Lfp.thy
+(* Title: HOL/Lfp.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
The Knaster-Tarski Theorem
--- a/src/HOL/List.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/List.thy Mon Feb 05 21:27:16 1996 +0100
@@ -13,7 +13,7 @@
consts
- "@" :: ['a list, 'a list] => 'a list (infixr 65)
+ "@" :: ['a list, 'a list] => 'a list (infixr 65)
drop :: [nat, 'a list] => 'a list
filter :: ['a => bool, 'a list] => 'a list
flat :: 'a list list => 'a list
@@ -22,7 +22,7 @@
length :: 'a list => nat
list_all :: ('a => bool) => ('a list => bool)
map :: ('a=>'b) => ('a list => 'b list)
- mem :: ['a, 'a list] => bool (infixl 55)
+ mem :: ['a, 'a list] => bool (infixl 55)
nth :: [nat, 'a list] => 'a
take :: [nat, 'a list] => 'a list
tl,ttl :: 'a list => 'a list
@@ -33,15 +33,15 @@
"@list" :: args => 'a list ("[(_)]")
(* Special syntax for list_all and filter *)
- "@Alls" :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
- "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
+ "@Alls" :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
+ "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
- "[x:xs . P]" == "filter (%x.P) xs"
- "Alls x:xs.P" == "list_all (%x.P) xs"
+ "[x:xs . P]" == "filter (%x.P) xs"
+ "Alls x:xs.P" == "list_all (%x.P) xs"
primrec hd list
hd_Nil "hd([]) = (@x.False)"
--- a/src/HOL/Nat.ML Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Nat.ML Mon Feb 05 21:27:16 1996 +0100
@@ -160,7 +160,17 @@
(*** nat_rec -- by wf recursion on pred_nat ***)
-bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec)));
+(* The unrolling rule for nat_rec *)
+goal Nat.thy
+ "(%n. nat_rec n c d) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
+ by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1);
+bind_thm("nat_rec_unfold", wf_pred_nat RS
+ ((result() RS eq_reflection) RS def_wfrec));
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec)));
+ *---------------------------------------------------------------------------*)
(** conversion rules **)
--- a/src/HOL/Nat.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Nat.thy Mon Feb 05 21:27:16 1996 +0100
@@ -33,7 +33,7 @@
(* type definition *)
-subtype (Nat)
+typedef (Nat)
nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" (lfp_def)
instance
@@ -65,6 +65,5 @@
le_def "m<=(n::nat) == ~(n<m)"
- nat_rec_def "nat_rec n c d == wfrec pred_nat n
- (nat_case (%g.c) (%m g.(d m (g m))))"
+nat_rec_def"nat_rec n c d == wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
end
--- a/src/HOL/Prod.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Prod.thy Mon Feb 05 21:27:16 1996 +0100
@@ -19,7 +19,7 @@
defs
Pair_Rep_def "Pair_Rep == (%a b. %x y. x=a & y=b)"
-subtype (Prod)
+typedef (Prod)
('a, 'b) "*" (infixr 20)
= "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
@@ -61,7 +61,7 @@
(** Unit **)
-subtype (Unit)
+typedef (Unit)
unit = "{p. p = True}"
consts
--- a/src/HOL/Relation.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Relation.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,24 +1,24 @@
-(* Title: Relation.thy
+(* Title: Relation.thy
ID: $Id$
- Author: Riccardo Mattolini, Dip. Sistemi e Informatica
- and Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Riccardo Mattolini, Dip. Sistemi e Informatica
+ and Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 Universita' di Firenze
Copyright 1993 University of Cambridge
*)
Relation = Prod +
consts
- id :: "('a * 'a)set" (*the identity relation*)
- O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
- trans :: "('a * 'a)set => bool" (*transitivity predicate*)
+ id :: "('a * 'a)set" (*the identity relation*)
+ O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
+ trans :: "('a * 'a)set => bool" (*transitivity predicate*)
converse :: "('a * 'b)set => ('b * 'a)set"
"^^" :: "[('a * 'b) set, 'a set] => 'b set" (infixl 90)
Domain :: "('a * 'b) set => 'a set"
Range :: "('a * 'b) set => 'b set"
defs
- id_def "id == {p. ? x. p = (x,x)}"
- comp_def "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
- trans_def "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
+ id_def "id == {p. ? x. p = (x,x)}"
+ comp_def "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
+ trans_def "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
converse_def "converse(r) == {(y,x). (x,y):r}"
Domain_def "Domain(r) == {x. ? y. (x,y):r}"
Range_def "Range(r) == Domain(converse(r))"
--- a/src/HOL/Sexp.ML Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Sexp.ML Mon Feb 05 21:27:16 1996 +0100
@@ -17,17 +17,17 @@
Scons_neq_Leaf, Scons_neq_Numb];
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
-by (rtac select_equality 1);
+by (resolve_tac [select_equality] 1);
by (ALLGOALS (fast_tac sexp_free_cs));
qed "sexp_case_Leaf";
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
-by (rtac select_equality 1);
+by (resolve_tac [select_equality] 1);
by (ALLGOALS (fast_tac sexp_free_cs));
qed "sexp_case_Numb";
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
-by (rtac select_equality 1);
+by (resolve_tac [select_equality] 1);
by (ALLGOALS (fast_tac sexp_free_cs));
qed "sexp_case_Scons";
@@ -109,9 +109,18 @@
(*** sexp_rec -- by wf recursion on pred_sexp ***)
+goal Sexp.thy
+ "(%M. sexp_rec M c d e) = wfrec pred_sexp \
+ \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
+by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
+bind_thm("sexp_rec_unfold", wf_pred_sexp RS
+ ((result() RS eq_reflection) RS def_wfrec));
(** conversion rules **)
-val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
+(*---------------------------------------------------------------------------
+ * Old:
+ * val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
+ *---------------------------------------------------------------------------*)
goal Sexp.thy "sexp_rec (Leaf a) c d h = c(a)";
--- a/src/HOL/Sexp.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Sexp.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Sexp
+(* Title: HOL/Sexp
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
S-expressions, general binary trees for defining recursive data structures
@@ -13,7 +13,7 @@
sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b,
'a item] => 'b"
- sexp_rec :: "['a item, 'a=>'b, nat=>'b,
+ sexp_rec :: "['a item, 'a=>'b, nat=>'b,
['a item, 'a item, 'b, 'b]=>'b] => 'b"
pred_sexp :: "('a item * 'a item)set"
@@ -26,7 +26,7 @@
defs
- sexp_case_def
+ sexp_case_def
"sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x))
| (? k. M=Numb(k) & z=d(k))
| (? N1 N2. M = N1 $ N2 & z=e N1 N2)"
@@ -35,6 +35,6 @@
"pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
sexp_rec_def
- "sexp_rec M c d e == wfrec pred_sexp M
- (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
+ "sexp_rec M c d e == wfrec pred_sexp
+ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
end
--- a/src/HOL/Sum.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Sum.thy Mon Feb 05 21:27:16 1996 +0100
@@ -18,7 +18,7 @@
Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)"
Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)"
-subtype (Sum)
+typedef (Sum)
('a, 'b) "+" (infixr 10)
= "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}"
--- a/src/HOL/Trancl.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Trancl.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Trancl.thy
+(* Title: HOL/Trancl.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Relfexive and Transitive closure of a relation
@@ -12,13 +12,13 @@
Trancl = Lfp + Relation +
consts
- rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100)
- trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100)
+ rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100)
+ trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100)
syntax
reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [100] 100)
defs
- rtrancl_def "r^* == lfp(%s. id Un (r O s))"
- trancl_def "r^+ == r O rtrancl(r)"
+ rtrancl_def "r^* == lfp(%s. id Un (r O s))"
+ trancl_def "r^+ == r O rtrancl(r)"
translations
"r^=" == "r Un id"
end
--- a/src/HOL/Univ.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Univ.thy Mon Feb 05 21:27:16 1996 +0100
@@ -15,7 +15,7 @@
(** lists, trees will be sets of nodes **)
-subtype (Node)
+typedef (Node)
'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
types
--- a/src/HOL/WF.ML Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/WF.ML Mon Feb 05 21:27:16 1996 +0100
@@ -1,9 +1,9 @@
-(* Title: HOL/WF.ML
+(* Title: HOL/wf.ML
ID: $Id$
- Author: Tobias Nipkow
- Copyright 1992 University of Cambridge
+ Author: Tobias Nipkow, with minor changes by Konrad Slind
+ Copyright 1992 University of Cambridge/1995 TU Munich
-For WF.thy. Well-founded Recursion
+For WF.thy. Wellfoundedness, induction, and recursion
*)
open WF;
@@ -48,7 +48,7 @@
by (REPEAT (resolve_tac prems 1));
qed "wf_anti_refl";
-(*transitive closure of a WF relation is WF!*)
+(*transitive closure of a wf relation is wf! *)
val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
by (rewtac wf_def);
by (strip_tac 1);
@@ -69,41 +69,32 @@
H_cong to expose the equality*)
goalw WF.thy [cut_def]
"(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
-by(simp_tac (!simpset addsimps [expand_fun_eq]
- setloop (split_tac [expand_if])) 1);
-qed "cut_cut_eq";
+by(simp_tac (HOL_ss addsimps [expand_fun_eq]
+ setloop (split_tac [expand_if])) 1);
+qed "cuts_eq";
goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
-by(Asm_simp_tac 1);
+by(asm_simp_tac HOL_ss 1);
qed "cut_apply";
-
(*** is_recfun ***)
goalw WF.thy [is_recfun_def,cut_def]
- "!!f. [| is_recfun r a H f; ~(b,a):r |] ==> f(b) = (@z.True)";
+ "!!f. [| is_recfun r H a f; ~(b,a):r |] ==> f(b) = (@z.True)";
by (etac ssubst 1);
-by(Asm_simp_tac 1);
+by(asm_simp_tac HOL_ss 1);
qed "is_recfun_undef";
-(*eresolve_tac transD solves (a,b):r using transitivity AT MOST ONCE
- mp amd allE instantiate induction hypotheses*)
-fun indhyp_tac hyps =
- ares_tac (TrueI::hyps) ORELSE'
- (cut_facts_tac hyps THEN'
- DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
- eresolve_tac [transD, mp, allE]));
-
(*** NOTE! some simplifications need a different finish_tac!! ***)
fun indhyp_tac hyps =
resolve_tac (TrueI::refl::hyps) ORELSE'
(cut_facts_tac hyps THEN'
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
eresolve_tac [transD, mp, allE]));
-val wf_super_ss = !simpset setsolver indhyp_tac;
+val wf_super_ss = HOL_ss setsolver indhyp_tac;
val prems = goalw WF.thy [is_recfun_def,cut_def]
- "[| wf(r); trans(r); is_recfun r a H f; is_recfun r b H g |] ==> \
+ "[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \
\ (x,a):r --> (x,b):r --> f(x)=g(x)";
by (cut_facts_tac prems 1);
by (etac wf_induct 1);
@@ -115,7 +106,7 @@
val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
"[| wf(r); trans(r); \
-\ is_recfun r a H f; is_recfun r b H g; (b,a):r |] ==> \
+\ is_recfun r H a f; is_recfun r H b g; (b,a):r |] ==> \
\ cut f r b = g";
val gundef = recgb RS is_recfun_undef
and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
@@ -128,70 +119,112 @@
(*** Main Existence Lemma -- Basic Properties of the_recfun ***)
val prems = goalw WF.thy [the_recfun_def]
- "is_recfun r a H f ==> is_recfun r a H (the_recfun r a H)";
-by (res_inst_tac [("P", "is_recfun r a H")] selectI 1);
+ "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
+by (res_inst_tac [("P", "is_recfun r H a")] selectI 1);
by (resolve_tac prems 1);
qed "is_the_recfun";
val prems = goal WF.thy
- "[| wf(r); trans(r) |] ==> is_recfun r a H (the_recfun r a H)";
-by (cut_facts_tac prems 1);
-by (wf_ind_tac "a" prems 1);
-by (res_inst_tac [("f", "cut (%y. wftrec r y H) r a1")] is_the_recfun 1);
-by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
-by (rtac (cut_cut_eq RS ssubst) 1);
-(*Applying the substitution: must keep the quantified assumption!!*)
-by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac,
- etac (mp RS ssubst), atac]);
-by (fold_tac [is_recfun_def]);
-by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cut_cut_eq]) 1);
+ "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
+ by (cut_facts_tac prems 1);
+ by (wf_ind_tac "a" prems 1);
+ by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
+ is_the_recfun 1);
+ by (rewrite_goals_tac [is_recfun_def]);
+ by (rtac (cuts_eq RS ssubst) 1);
+ by (rtac allI 1);
+ by (rtac impI 1);
+ by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1);
+ by (subgoal_tac
+ "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1);
+ by (etac allE 2);
+ by (dtac impE 2);
+ by (atac 2);
+ by (atac 3);
+ by (atac 2);
+ by (etac ssubst 1);
+ by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
+ by (rtac allI 1);
+ by (rtac impI 1);
+ by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
+ by (res_inst_tac [("f1","H"),("x","ya")](arg_cong RS fun_cong) 1);
+ by (fold_tac [is_recfun_def]);
+ by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
qed "unfold_the_recfun";
-
-(*Beware incompleteness of unification!*)
-val prems = goal WF.thy
- "[| wf(r); trans(r); (c,a):r; (c,b):r |] \
-\ ==> the_recfun r a H c = the_recfun r b H c";
-by (DEPTH_SOLVE (ares_tac (prems@[is_recfun_equal,unfold_the_recfun]) 1));
-qed "the_recfun_equal";
-
-val prems = goal WF.thy
- "[| wf(r); trans(r); (b,a):r |] \
-\ ==> cut (the_recfun r a H) r b = the_recfun r b H";
-by (REPEAT (ares_tac (prems@[is_recfun_cut,unfold_the_recfun]) 1));
-qed "the_recfun_cut";
-
-(*** Unfolding wftrec ***)
+val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun;
-goalw WF.thy [wftrec_def]
- "!!r. [| wf(r); trans(r) |] ==> \
-\ wftrec r a H = H a (cut (%x.wftrec r x H) r a)";
-by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun),
- REPEAT o atac, rtac H_cong1]);
-by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1);
-qed "wftrec";
-
-(*Unused but perhaps interesting*)
+(*--------------Old proof-----------------------------------------------------
val prems = goal WF.thy
- "[| wf(r); trans(r); !!f x. H x (cut f r x) = H x f |] ==> \
-\ wftrec r a H = H a (%x.wftrec r x H)";
-by (rtac (wftrec RS trans) 1);
-by (REPEAT (resolve_tac prems 1));
-qed "wftrec2";
+ "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
+by (cut_facts_tac prems 1);
+by (wf_ind_tac "a" prems 1);
+by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1);
+by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
+by (rtac (cuts_eq RS ssubst) 1);
+(*Applying the substitution: must keep the quantified assumption!!*)
+by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac,
+ etac (mp RS ssubst), atac]);
+by (fold_tac [is_recfun_def]);
+by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
+qed "unfold_the_recfun";
+---------------------------------------------------------------------------*)
(** Removal of the premise trans(r) **)
+val th = rewrite_rule[is_recfun_def]
+ (trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun)));
goalw WF.thy [wfrec_def]
- "!!r. wf(r) ==> wfrec r a H = H a (cut (%x.wfrec r x H) r a)";
+ "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
+by (rtac H_cong 1);
+by (rtac refl 2);
+by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
+by (rtac allI 1);
+by (rtac impI 1);
+by (simp_tac(HOL_ss addsimps [wfrec_def]) 1);
+by (res_inst_tac [("a1","a")] (th RS ssubst) 1);
+by (atac 1);
+by (forward_tac[wf_trancl] 1);
+by (forward_tac[r_into_trancl] 1);
+by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1);
+by (rtac H_cong 1); (*expose the equality of cuts*)
+by (rtac refl 2);
+by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
+by (strip_tac 1);
+by (res_inst_tac [("r2","r^+")] (is_recfun_equal_lemma RS mp RS mp) 1);
+by (atac 1);
+by (rtac trans_trancl 1);
+by (rtac unfold_the_recfun 1);
+by (atac 1);
+by (rtac trans_trancl 1);
+by (rtac unfold_the_recfun 1);
+by (atac 1);
+by (rtac trans_trancl 1);
+by (rtac transD 1);
+by (rtac trans_trancl 1);
+by (forw_inst_tac [("a","ya")] r_into_trancl 1);
+by (atac 1);
+by (atac 1);
+by (forw_inst_tac [("a","ya")] r_into_trancl 1);
+by (atac 1);
+qed "wfrec";
+
+(*--------------Old proof-----------------------------------------------------
+goalw WF.thy [wfrec_def]
+ "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
by (etac (wf_trancl RS wftrec RS ssubst) 1);
by (rtac trans_trancl 1);
by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*)
-by (simp_tac (!simpset addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1);
+by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
qed "wfrec";
+---------------------------------------------------------------------------*)
-(*This form avoids giant explosions in proofs. NOTE USE OF == *)
+(*---------------------------------------------------------------------------
+ * This form avoids giant explosions in proofs. NOTE USE OF ==
+ *---------------------------------------------------------------------------*)
val rew::prems = goal WF.thy
- "[| !!x. f(x)==wfrec r x H; wf(r) |] ==> f(a) = H a (cut (%x.f(x)) r a)";
+ "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a";
by (rewtac rew);
by (REPEAT (resolve_tac (prems@[wfrec]) 1));
qed "def_wfrec";
+
--- a/src/HOL/WF.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/WF.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/WF.thy
+(* Title: HOL/wf.ML
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1992 University of Cambridge
Well-founded Recursion
@@ -8,23 +8,22 @@
WF = Trancl +
consts
- wf :: "('a * 'a)set => bool"
- cut :: "['a => 'b, ('a * 'a)set, 'a] => 'a => 'b"
- wftrec,wfrec :: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'b"
- is_recfun :: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b, 'a=>'b] => bool"
- the_recfun :: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b"
+ wf :: "('a * 'a)set => bool"
+ cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
+ is_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
+ the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
+ wfrec :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
defs
wf_def "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
- cut_def "cut f r x == (%y. if (y,x):r then f y else @z.True)"
+ cut_def "cut f r x == (%y. if (y,x):r then f y else @z.True)"
- is_recfun_def "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
-
- the_recfun_def "the_recfun r a H == (@f.is_recfun r a H f)"
+ is_recfun_def "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
- wftrec_def "wftrec r a H == H a (the_recfun r a H)"
+ the_recfun_def "the_recfun r H a == (@f. is_recfun r H a f)"
- (*version not requiring transitivity*)
- wfrec_def "wfrec r a H == wftrec (trancl r) a (%x f.(H x (cut f r x)))"
+ wfrec_def
+ "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
+ r x) x)"
end
--- a/src/HOL/equalities.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/equalities.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/equalities
+(* Title: HOL/equalities
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Equalities involving union, intersection, inclusion, etc.
--- a/src/HOL/mono.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/mono.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/mono.thy
+(* Title: HOL/mono.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/HOL/subset.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/subset.thy Mon Feb 05 21:27:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/subset.thy
+(* Title: HOL/subset.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
--- a/src/HOL/thy_syntax.ML Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/thy_syntax.ML Mon Feb 05 21:27:16 1996 +0100
@@ -17,9 +17,9 @@
open ThyParse;
-(** subtype **)
+(** typedef **)
-fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
+fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
let
val name' = if_none opt_name t;
val name = strip_quotes name';
@@ -29,10 +29,10 @@
"Abs_" ^ name ^ "_inverse"])
end;
-val subtype_decl =
+val typedef_decl =
optional ("(" $$-- name --$$ ")" >> Some) None --
type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
- >> mk_subtype_decl;
+ >> mk_typedef_decl;
@@ -191,7 +191,7 @@
val user_keywords = ["intrs", "monos", "con_defs", "|"];
val user_sections =
- [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl,
+ [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
("inductive", inductive_decl ""),
("coinductive", inductive_decl "Co"),
("datatype", datatype_decl),
--- a/src/HOL/typedef.ML Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/typedef.ML Mon Feb 05 21:27:16 1996 +0100
@@ -1,20 +1,20 @@
-(* Title: HOL/subtype.ML
+(* Title: HOL/typedef.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-Internal interface for subtype definitions.
+Internal interface for typedef definitions.
*)
-signature SUBTYPE =
+signature TYPEDEF =
sig
val prove_nonempty: cterm -> thm list -> tactic option -> thm
- val add_subtype: string -> string * string list * mixfix ->
+ val add_typedef: string -> string * string list * mixfix ->
string -> string list -> thm list -> tactic option -> theory -> theory
- val add_subtype_i: string -> string * string list * mixfix ->
+ val add_typedef_i: string -> string * string list * mixfix ->
term -> string list -> thm list -> tactic option -> theory -> theory
end;
-structure Subtype: SUBTYPE =
+structure Typedef: TYPEDEF =
struct
open Syntax Logic HOLogic;
@@ -41,11 +41,11 @@
error ("Failed to prove non-emptyness of " ^ quote (string_of_cterm cset));
-(* ext_subtype *)
+(* ext_typedef *)
-fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
+fun ext_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
let
- val dummy = require_thy thy "Set" "subtype definitions";
+ val dummy = require_thy thy "Set" "typedef definitions";
val sign = sign_of thy;
(*rhs*)
@@ -122,7 +122,7 @@
(Abs_name ^ "_inverse", abs_type_inv)]
end
handle ERROR =>
- error ("The error(s) above occurred in subtype definition " ^ quote name);
+ error ("The error(s) above occurred in typedef definition " ^ quote name);
(* external interfaces *)
@@ -133,8 +133,8 @@
fun read_term sg str =
read_cterm sg (str, termTVar);
-val add_subtype = ext_subtype read_term;
-val add_subtype_i = ext_subtype cert_term;
+val add_typedef = ext_typedef read_term;
+val add_typedef_i = ext_typedef cert_term;
end;