Tuned inductive definition.
authorberghofe
Tue Oct 05 15:31:42 1999 +0200 (1999-10-05)
changeset 7721cb353d802ade
parent 7720 b92bbfda8de5
child 7722 8add8fdce3f1
Tuned inductive definition.
src/HOL/Induct/Acc.ML
src/HOL/Induct/Acc.thy
     1.1 --- a/src/HOL/Induct/Acc.ML	Tue Oct 05 15:31:39 1999 +0200
     1.2 +++ b/src/HOL/Induct/Acc.ML	Tue Oct 05 15:31:42 1999 +0200
     1.3 @@ -9,16 +9,20 @@
     1.4  Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
     1.5  *)
     1.6  
     1.7 -(*The intended introduction rule*)
     1.8 -val prems = goal Acc.thy
     1.9 -    "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
    1.10 -by (fast_tac (claset() addIs prems @ 
    1.11 -                             map (rewrite_rule [pred_def]) acc.intrs) 1);
    1.12 -qed "accI";
    1.13 +val accI = thm "acc.accI";
    1.14 +
    1.15 +val [major,indhyp] = Goal
    1.16 +    "[| a : acc(r);                                             \
    1.17 +\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
    1.18 +\    |] ==> P(a)";
    1.19 +by (rtac (major RS thm "acc.induct") 1);
    1.20 +by (rtac indhyp 1);
    1.21 +by (rtac accI 1);
    1.22 +by (ALLGOALS Fast_tac);
    1.23 +qed "acc_induct";
    1.24  
    1.25  Goal "[| b: acc(r);  (a,b): r |] ==> a: acc(r)";
    1.26 -by (etac acc.elim 1);
    1.27 -by (rewtac pred_def);
    1.28 +by (etac (thm "acc.elims") 1);
    1.29  by (Fast_tac 1);
    1.30  qed "acc_downward";
    1.31  
    1.32 @@ -33,18 +37,6 @@
    1.33  by (blast_tac (claset() addDs [lemma]) 1);
    1.34  qed "acc_downwards";
    1.35  
    1.36 -val [major,indhyp] = goal Acc.thy
    1.37 -    "[| a : acc(r);                                             \
    1.38 -\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
    1.39 -\    |] ==> P(a)";
    1.40 -by (rtac (major RS acc.induct) 1);
    1.41 -by (rtac indhyp 1);
    1.42 -by (resolve_tac acc.intrs 1);
    1.43 -by (rewtac pred_def);
    1.44 -by (Fast_tac 2);
    1.45 -by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
    1.46 -qed "acc_induct";
    1.47 -
    1.48  Goal "!x. x : acc(r) ==> wf(r)";
    1.49  by (rtac wfUNIVI 1);
    1.50  by (deepen_tac (claset() addEs [acc_induct]) 1 1);
     2.1 --- a/src/HOL/Induct/Acc.thy	Tue Oct 05 15:31:39 1999 +0200
     2.2 +++ b/src/HOL/Induct/Acc.thy	Tue Oct 05 15:31:42 1999 +0200
     2.3 @@ -9,19 +9,15 @@
     2.4  Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
     2.5  *)
     2.6  
     2.7 -Acc = WF + Inductive +
     2.8 -
     2.9 -constdefs
    2.10 -  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
    2.11 -  "pred x r == {y. (y,x):r}"
    2.12 +theory Acc = WF + Inductive:
    2.13  
    2.14  consts
    2.15    acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
    2.16  
    2.17 -inductive "acc(r)"
    2.18 +inductive "acc r"
    2.19    intrs
    2.20 -    pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
    2.21 -  monos     Pow_mono
    2.22 +    accI [rulify_prems]: "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    2.23 +
    2.24  
    2.25  syntax        termi :: "('a * 'a)set => 'a set"
    2.26  translations "termi r" == "acc(r^-1)"