# HG changeset patch
# User berghofe
# Date 1170865781 -3600
# Node ID 990a638e6f69d3dacf4d884fa18f9d60f1f38986
# Parent  96ba62dff41378695ccc06cd616f1b5f5fd55f45
- Adapted to new inductive definition package
- Predicate version of wellfoundedness

diff -r 96ba62dff413 -r 990a638e6f69 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Wed Feb 07 17:28:09 2007 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Wed Feb 07 17:29:41 2007 +0100
@@ -9,18 +9,21 @@
 imports Transitive_Closure
 begin
 
-consts
-  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => ('a * 'b) set"
-
-inductive "wfrec_rel R F"
-intros
-  wfrecI: "ALL z. (z, x) : R --> (z, g z) : wfrec_rel R F ==>
-            (x, F g x) : wfrec_rel R F"
+inductive2
+  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
+  for R :: "('a * 'a) set"
+  and F :: "('a => 'b) => 'a => 'b"
+where
+  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
+            wfrec_rel R F x (F g x)"
 
 constdefs
   wf         :: "('a * 'a)set => bool"
   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
 
+  wfP :: "('a => 'a => bool) => bool"
+  "wfP r == wf (Collect2 r)"
+
   acyclic :: "('a*'a)set => bool"
   "acyclic r == !x. (x,x) ~: r^+"
 
@@ -32,16 +35,30 @@
      (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
 
   wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
-  "wfrec R F == %x. THE y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)"
+  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+
+abbreviation acyclicP :: "('a => 'a => bool) => bool" where
+  "acyclicP r == acyclic (Collect2 r)"
 
 axclass wellorder \<subseteq> linorder
   wf: "wf {(x,y::'a::ord). x<y}"
 
 
+lemma wfP_wf_eq [pred_set_conv]: "wfP (member2 r) = wf r"
+  by (simp add: wfP_def)
+
+lemma wf_implies_wfP: "wf r \<Longrightarrow> wfP (member2 r)"
+  by (simp add: wfP_def)
+
+lemma wfP_implies_wf: "wfP r \<Longrightarrow> wf (Collect2 r)"
+  by (simp add: wfP_def)
+
 lemma wfUNIVI: 
    "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"
 by (unfold wf_def, blast)
 
+lemmas wfPUNIVI = wfUNIVI [to_pred]
+
 text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is
     well-founded over their intersection, then @{term "wf r"}*}
 lemma wfI: 
@@ -56,8 +73,13 @@
      |]  ==>  P(a)"
 by (unfold wf_def, blast)
 
+lemmas wfP_induct = wf_induct [to_pred]
+
 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
 
+lemmas wfP_induct_rule =
+  wf_induct_rule [to_pred, consumes 1, case_names less, induct set: wfP]
+
 lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r"
 by (erule_tac a=a in wf_induct, blast)
 
@@ -80,6 +102,8 @@
 apply (blast elim: tranclE)
 done
 
+lemmas wfP_trancl = wf_trancl [to_pred]
+
 lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"
 apply (subst trancl_converse [symmetric])
 apply (erule wf_trancl)
@@ -102,16 +126,22 @@
   thus "wf r" by (unfold wf_def, force)
 qed
 
+lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
+
 text{*Well-foundedness of subsets*}
 lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
 apply (simp (no_asm_use) add: wf_eq_minimal)
 apply fast
 done
 
+lemmas wfP_subset = wf_subset [to_pred]
+
 text{*Well-foundedness of the empty relation*}
 lemma wf_empty [iff]: "wf({})"
 by (simp add: wf_def)
 
+lemmas wfP_empty [iff] = wf_empty [to_pred]
+
 lemma wf_Int1: "wf r ==> wf (r Int r')"
 by (erule wf_subset, rule Int_lower1)
 
@@ -166,6 +196,9 @@
 apply (blast elim!: allE)  
 done
 
+lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. Collect2 (r i)",
+  to_pred member2_SUP, simplified, standard]
+
 lemma wf_Union: 
  "[| ALL r:R. wf r;  
      ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
@@ -209,6 +242,8 @@
 apply (blast elim: wf_trancl [THEN wf_irrefl])
 done
 
+lemmas wfP_acyclicP = wf_acyclic [to_pred]
+
 lemma acyclic_insert [iff]:
      "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
 apply (simp add: acyclic_def trancl_insert)
@@ -218,6 +253,8 @@
 lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
 by (simp add: acyclic_def trancl_converse)
 
+lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
+
 lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
 apply (simp add: acyclic_def antisym_def)
 apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
@@ -249,11 +286,11 @@
 text{*Inductive characterization of wfrec combinator; for details see:  
 John Harrison, "Inductive definitions: automation and application"*}
 
-lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. (x, y) : wfrec_rel R F"
+lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
 apply (simp add: adm_wf_def)
 apply (erule_tac a=x in wf_induct) 
 apply (rule ex1I)
-apply (rule_tac g = "%x. THE y. (x, y) : wfrec_rel R F" in wfrec_rel.wfrecI)
+apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
 apply (fast dest!: theI')
 apply (erule wfrec_rel.cases, simp)
 apply (erule allE, erule allE, erule allE, erule mp)