src/HOL/WF_Rel.ML

--- a/src/HOL/WF_Rel.ML	Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Thu Jun 05 14:39:22 1997 +0200
@@ -63,15 +63,10 @@
  * Wellfoundedness of lexicographic combinations
  *---------------------------------------------------------------------------*)
 
-goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)";
-by (rtac allI 1);
-by (rtac (surjective_pairing RS ssubst) 1);
-by (Blast_tac 1);
-qed "split_all_pair";
-
 val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
  "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
-by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
+by (EVERY1 [rtac allI,rtac impI]);
+by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
 by (rtac (wfa RS spec RS mp) 1);
 by (EVERY1 [rtac allI,rtac impI]);
 by (rtac (wfb RS spec RS mp) 1);
@@ -80,25 +75,6 @@
 AddSIs [wf_lex_prod];
 
 (*---------------------------------------------------------------------------
- * Wellfoundedness of subsets
- *---------------------------------------------------------------------------*)
-
-goal thy "!!r. [| wf(r);  p<=r |] ==> wf(p)";
-by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
-by (Fast_tac 1);
-qed "wf_subset";
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of the empty relation.
- *---------------------------------------------------------------------------*)
-
-goal thy "wf({})";
-by (simp_tac (!simpset addsimps [wf_def]) 1);
-qed "wf_empty";
-AddSIs [wf_empty];
-
-
-(*---------------------------------------------------------------------------
  * Transitivity of WF combinators.
  *---------------------------------------------------------------------------*)
 goalw thy [trans_def, lex_prod_def]
@@ -124,3 +100,58 @@
 by (Blast_tac 1);
 qed "trans_finite_psubset";
 
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of finite acyclic relations
+ * Cannot go into WF because it needs Finite
+ *---------------------------------------------------------------------------*)
+
+goal thy "!!r. finite r ==> acyclic r --> wf r";
+be finite_induct 1;
+ by(Blast_tac 1);
+by(split_all_tac 1);
+by(Asm_full_simp_tac 1);
+qed_spec_mp "finite_acyclic_wf";
+
+goal thy "!!r. finite r ==> wf r = acyclic r";
+by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
+qed "wf_iff_acyclic_if_finite";
+
+
+(*---------------------------------------------------------------------------
+ * A relation is wellfounded iff it has no infinite descending chain
+ *---------------------------------------------------------------------------*)
+
+goalw thy [wf_eq_minimal RS eq_reflection]
+  "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
+br iffI 1;
+ br notI 1;
+ be exE 1;
+ by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
+ by(Blast_tac 1);
+be swap 1;
+by(Asm_full_simp_tac 1);
+be exE 1;
+be swap 1;
+br impI 1;
+be swap 1;
+be exE 1;
+by(rename_tac "x" 1);
+by(subgoal_tac
+ "!i. nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i) : Q & \
+\     (nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i),\
+\      nat_rec x (%i y. @z. z:Q & (z,y):r) i): r" 1);
+ by(Blast_tac 1);
+br allI 1;
+by(induct_tac "i" 1);
+ by(Asm_simp_tac 1);
+ by(subgoal_tac "? y. y : Q & (y,x):r" 1);
+  by(Blast_tac 2);
+ be exE 1;
+ be selectI 1;
+by(subgoal_tac "? y.y:Q & (y,nat_rec x (%i y. @z. z:Q & (z,y):r)(Suc i)):r" 1);
+ by(Blast_tac 2);
+by(Asm_full_simp_tac 1);
+be exE 1;
+(* `be selectI 1' takes a long time; hence the instantiation: *)
+by (eres_inst_tac[("P","%u.u:Q & (u,?v):r")]selectI 1);
+qed "wf_iff_no_infinite_down_chain";