converted;
authorwenzelm
Sat Sep 02 21:48:10 2000 +0200 (2000-09-02)
changeset 9802adda1dc18bb8
parent 9801 5e7c4a45d8bb
child 9803 bc883b390d91
converted;
src/HOL/Induct/Acc.ML
src/HOL/Induct/Acc.thy
     1.1 --- a/src/HOL/Induct/Acc.ML	Sat Sep 02 21:47:50 2000 +0200
     1.2 +++ b/src/HOL/Induct/Acc.ML	Sat Sep 02 21:48:10 2000 +0200
     1.3 @@ -1,53 +1,8 @@
     1.4 -(*  Title:      HOL/ex/Acc
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1994  University of Cambridge
     1.8 -
     1.9 -Inductive definition of acc(r)
    1.10 -
    1.11 -See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
    1.12 -Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    1.13 -*)
    1.14  
    1.15  val accI = thm "acc.accI";
    1.16 -
    1.17 -val [major,indhyp] = Goal
    1.18 -    "[| a : acc(r);                                             \
    1.19 -\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
    1.20 -\    |] ==> P(a)";
    1.21 -by (rtac (major RS thm "acc.induct") 1);
    1.22 -by (rtac indhyp 1);
    1.23 -by (rtac accI 1);
    1.24 -by (ALLGOALS Fast_tac);
    1.25 -qed "acc_induct";
    1.26 -
    1.27 -Goal "[| b: acc(r);  (a,b): r |] ==> a: acc(r)";
    1.28 -by (etac (thm "acc.elims") 1);
    1.29 -by (Fast_tac 1);
    1.30 -qed "acc_downward";
    1.31 -
    1.32 -Goal "(b,a) : r^* ==> a : acc r --> b : acc r";
    1.33 -by (etac rtrancl_induct 1);
    1.34 -by (Blast_tac 1);
    1.35 - by (blast_tac (claset() addDs [acc_downward]) 1);
    1.36 -no_qed();
    1.37 -val lemma = result();
    1.38 -
    1.39 -Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
    1.40 -by (blast_tac (claset() addDs [lemma]) 1);
    1.41 -qed "acc_downwards";
    1.42 -
    1.43 -Goal "!x. x : acc(r) ==> wf(r)";
    1.44 -by (rtac wfUNIVI 1);
    1.45 -by (deepen_tac (claset() addEs [acc_induct]) 1 1);
    1.46 -qed "acc_wfI";
    1.47 -
    1.48 -Goal "wf(r) ==> x : acc(r)";
    1.49 -by (etac wf_induct 1);
    1.50 -by (rtac accI 1);
    1.51 -by (Blast_tac 1);
    1.52 -qed "acc_wfD";
    1.53 -
    1.54 -Goal "wf(r)  =  (!x. x : acc(r))";
    1.55 -by (blast_tac (claset() addIs [acc_wfI] addDs [acc_wfD]) 1);
    1.56 -qed "wf_acc_iff";
    1.57 +val acc_induct = thm "acc_induct";
    1.58 +val acc_downward = thm "acc_downward";
    1.59 +val acc_downwards = thm "acc_downwards";
    1.60 +val acc_wfI = thm "acc_wfI";
    1.61 +val acc_wfD = thm "acc_wfD";
    1.62 +val wf_acc_iff = thm "wf_acc_iff";
     2.1 --- a/src/HOL/Induct/Acc.thy	Sat Sep 02 21:47:50 2000 +0200
     2.2 +++ b/src/HOL/Induct/Acc.thy	Sat Sep 02 21:48:10 2000 +0200
     2.3 @@ -14,16 +14,65 @@
     2.4  theory Acc = Main:
     2.5  
     2.6  consts
     2.7 -  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *}
     2.8 +  acc  :: "('a \<times> 'a) set => 'a set"  -- {* accessible part *}
     2.9  
    2.10  inductive "acc r"
    2.11    intros
    2.12      accI [rulify_prems]:
    2.13 -      "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    2.14 +      "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
    2.15  
    2.16  syntax
    2.17 -  termi :: "('a * 'a)set => 'a set"
    2.18 +  termi :: "('a \<times> 'a) set => 'a set"
    2.19  translations
    2.20 -  "termi r" == "acc(r^-1)"
    2.21 +  "termi r" == "acc (r^-1)"
    2.22 +
    2.23 +
    2.24 +theorem acc_induct:
    2.25 +  "[| a \<in> acc r;
    2.26 +      !!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x
    2.27 +  |] ==> P a"
    2.28 +proof -
    2.29 +  assume major: "a \<in> acc r"
    2.30 +  assume hyp: "!!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x"
    2.31 +  show ?thesis
    2.32 +    apply (rule major [THEN acc.induct])
    2.33 +    apply (rule hyp)
    2.34 +     apply (rule accI)
    2.35 +     apply fast
    2.36 +    apply fast
    2.37 +    done
    2.38 +qed
    2.39 +
    2.40 +theorem acc_downward: "[| b \<in> acc r; (a, b) \<in> r |] ==> a \<in> acc r"
    2.41 +  apply (erule acc.elims)
    2.42 +  apply fast
    2.43 +  done
    2.44 +
    2.45 +lemma acc_downwards_aux: "(b, a) \<in> r^* ==> a \<in> acc r --> b \<in> acc r"
    2.46 +  apply (erule rtrancl_induct)
    2.47 +   apply blast
    2.48 +  apply (blast dest: acc_downward)
    2.49 +  done
    2.50 +
    2.51 +theorem acc_downwards: "[| a \<in> acc r; (b, a) \<in> r^* |] ==> b \<in> acc r"
    2.52 +  apply (blast dest: acc_downwards_aux)
    2.53 +  done
    2.54 +
    2.55 +theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    2.56 +  apply (rule wfUNIVI)
    2.57 +  apply (induct_tac P x rule: acc_induct)
    2.58 +   apply blast
    2.59 +  apply blast
    2.60 +  done
    2.61 +
    2.62 +theorem acc_wfD: "wf r ==> x \<in> acc r"
    2.63 +  apply (erule wf_induct)
    2.64 +  apply (rule accI)
    2.65 +  apply blast
    2.66 +  done
    2.67 +
    2.68 +theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    2.69 +  apply (blast intro: acc_wfI dest: acc_wfD)
    2.70 +  done
    2.71  
    2.72  end