src/HOL/WF.ML
changeset 3413 c1f63cc3a768
parent 3320 3a5e4930fb77
child 3439 54785105178c
--- a/src/HOL/WF.ML	Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/WF.ML	Thu Jun 05 14:39:22 1997 +0200
@@ -84,6 +84,66 @@
 by (blast_tac (!claset addSIs [lemma1, lemma2]) 1);
 qed "wf_eq_minimal";
 
+(*---------------------------------------------------------------------------
+ * 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];
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of `insert'
+ *---------------------------------------------------------------------------*)
+
+goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
+br iffI 1;
+ by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
+      [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
+by(asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
+by(safe_tac (!claset));
+by(EVERY1[rtac allE, atac, etac impE, Blast_tac]);
+be bexE 1;
+by(rename_tac "a" 1);
+by(case_tac "a = x" 1);
+ by(res_inst_tac [("x","a")]bexI 2);
+  ba 3;
+ by(Blast_tac 2);
+by(case_tac "y:Q" 1);
+ by(Blast_tac 2);
+by(res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
+ ba 1;
+by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
+qed "wf_insert";
+AddIffs [wf_insert];
+
+(*** acyclic ***)
+
+goalw WF.thy [acyclic_def]
+ "!!r. wf r ==> acyclic r";
+by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
+qed "wf_acyclic";
+
+goalw WF.thy [acyclic_def]
+  "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
+by(simp_tac (!simpset addsimps [trancl_insert]) 1);
+by(blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
+qed "acyclic_insert";
+AddIffs [acyclic_insert];
+
+goalw WF.thy [acyclic_def] "acyclic(converse r) = acyclic r";
+by(simp_tac (!simpset addsimps [trancl_converse]) 1);
+qed "acyclic_converse";
 
 (** cut **)
 
@@ -272,4 +332,3 @@
 by (assume_tac 1);
 by (assume_tac 1);
 qed "tfl_wfrec";
-