# HG changeset patch # User clasohm # Date 823552036 -3600 # Node ID 7f5a4cd082091d0efd0c89b955053c0f3372ff4a # Parent 3f7d67927fe2d18fbf9de27480a3117bfe7d6f19 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/Arith.ML --- 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 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 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 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 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 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"; diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/Arith.thy --- 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 '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)" diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/Nat.ML --- 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 **) diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/Nat.thy --- 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 ('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))" diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/Sexp.ML --- 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)"; diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/Sexp.thy --- 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 diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/Sum.thy --- 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))}" diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/Trancl.thy --- 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 diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/Univ.thy --- 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 diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/WF.ML --- 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"; + diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/WF.thy --- 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 diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/equalities.thy --- 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. diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/mono.thy --- 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 *) diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/subset.thy --- 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 *) diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/thy_syntax.ML --- 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), diff -r 3f7d67927fe2 -r 7f5a4cd08209 src/HOL/typedef.ML --- 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;