src/HOL/Induct/Acc.thy
changeset 9802 adda1dc18bb8
parent 9596 6d6bf351b2cc
child 9906 5c027cca6262
     1.1 --- a/src/HOL/Induct/Acc.thy	Sat Sep 02 21:47:50 2000 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Sat Sep 02 21:48:10 2000 +0200
     1.3 @@ -14,16 +14,65 @@
     1.4  theory Acc = Main:
     1.5  
     1.6  consts
     1.7 -  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *}
     1.8 +  acc  :: "('a \<times> 'a) set => 'a set"  -- {* accessible part *}
     1.9  
    1.10  inductive "acc r"
    1.11    intros
    1.12      accI [rulify_prems]:
    1.13 -      "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    1.14 +      "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
    1.15  
    1.16  syntax
    1.17 -  termi :: "('a * 'a)set => 'a set"
    1.18 +  termi :: "('a \<times> 'a) set => 'a set"
    1.19  translations
    1.20 -  "termi r" == "acc(r^-1)"
    1.21 +  "termi r" == "acc (r^-1)"
    1.22 +
    1.23 +
    1.24 +theorem acc_induct:
    1.25 +  "[| a \<in> acc r;
    1.26 +      !!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x
    1.27 +  |] ==> P a"
    1.28 +proof -
    1.29 +  assume major: "a \<in> acc r"
    1.30 +  assume hyp: "!!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x"
    1.31 +  show ?thesis
    1.32 +    apply (rule major [THEN acc.induct])
    1.33 +    apply (rule hyp)
    1.34 +     apply (rule accI)
    1.35 +     apply fast
    1.36 +    apply fast
    1.37 +    done
    1.38 +qed
    1.39 +
    1.40 +theorem acc_downward: "[| b \<in> acc r; (a, b) \<in> r |] ==> a \<in> acc r"
    1.41 +  apply (erule acc.elims)
    1.42 +  apply fast
    1.43 +  done
    1.44 +
    1.45 +lemma acc_downwards_aux: "(b, a) \<in> r^* ==> a \<in> acc r --> b \<in> acc r"
    1.46 +  apply (erule rtrancl_induct)
    1.47 +   apply blast
    1.48 +  apply (blast dest: acc_downward)
    1.49 +  done
    1.50 +
    1.51 +theorem acc_downwards: "[| a \<in> acc r; (b, a) \<in> r^* |] ==> b \<in> acc r"
    1.52 +  apply (blast dest: acc_downwards_aux)
    1.53 +  done
    1.54 +
    1.55 +theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    1.56 +  apply (rule wfUNIVI)
    1.57 +  apply (induct_tac P x rule: acc_induct)
    1.58 +   apply blast
    1.59 +  apply blast
    1.60 +  done
    1.61 +
    1.62 +theorem acc_wfD: "wf r ==> x \<in> acc r"
    1.63 +  apply (erule wf_induct)
    1.64 +  apply (rule accI)
    1.65 +  apply blast
    1.66 +  done
    1.67 +
    1.68 +theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    1.69 +  apply (blast intro: acc_wfI dest: acc_wfD)
    1.70 +  done
    1.71  
    1.72  end