src/HOL/WF.ML
changeset 3413 c1f63cc3a768
parent 3320 3a5e4930fb77
child 3439 54785105178c
     1.1 --- a/src/HOL/WF.ML	Thu Jun 05 14:06:23 1997 +0200
     1.2 +++ b/src/HOL/WF.ML	Thu Jun 05 14:39:22 1997 +0200
     1.3 @@ -84,6 +84,66 @@
     1.4  by (blast_tac (!claset addSIs [lemma1, lemma2]) 1);
     1.5  qed "wf_eq_minimal";
     1.6  
     1.7 +(*---------------------------------------------------------------------------
     1.8 + * Wellfoundedness of subsets
     1.9 + *---------------------------------------------------------------------------*)
    1.10 +
    1.11 +goal thy "!!r. [| wf(r);  p<=r |] ==> wf(p)";
    1.12 +by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
    1.13 +by (Fast_tac 1);
    1.14 +qed "wf_subset";
    1.15 +
    1.16 +(*---------------------------------------------------------------------------
    1.17 + * Wellfoundedness of the empty relation.
    1.18 + *---------------------------------------------------------------------------*)
    1.19 +
    1.20 +goal thy "wf({})";
    1.21 +by (simp_tac (!simpset addsimps [wf_def]) 1);
    1.22 +qed "wf_empty";
    1.23 +AddSIs [wf_empty];
    1.24 +
    1.25 +(*---------------------------------------------------------------------------
    1.26 + * Wellfoundedness of `insert'
    1.27 + *---------------------------------------------------------------------------*)
    1.28 +
    1.29 +goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
    1.30 +br iffI 1;
    1.31 + by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
    1.32 +      [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
    1.33 +by(asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
    1.34 +by(safe_tac (!claset));
    1.35 +by(EVERY1[rtac allE, atac, etac impE, Blast_tac]);
    1.36 +be bexE 1;
    1.37 +by(rename_tac "a" 1);
    1.38 +by(case_tac "a = x" 1);
    1.39 + by(res_inst_tac [("x","a")]bexI 2);
    1.40 +  ba 3;
    1.41 + by(Blast_tac 2);
    1.42 +by(case_tac "y:Q" 1);
    1.43 + by(Blast_tac 2);
    1.44 +by(res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
    1.45 + ba 1;
    1.46 +by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
    1.47 +qed "wf_insert";
    1.48 +AddIffs [wf_insert];
    1.49 +
    1.50 +(*** acyclic ***)
    1.51 +
    1.52 +goalw WF.thy [acyclic_def]
    1.53 + "!!r. wf r ==> acyclic r";
    1.54 +by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
    1.55 +qed "wf_acyclic";
    1.56 +
    1.57 +goalw WF.thy [acyclic_def]
    1.58 +  "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
    1.59 +by(simp_tac (!simpset addsimps [trancl_insert]) 1);
    1.60 +by(blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
    1.61 +qed "acyclic_insert";
    1.62 +AddIffs [acyclic_insert];
    1.63 +
    1.64 +goalw WF.thy [acyclic_def] "acyclic(converse r) = acyclic r";
    1.65 +by(simp_tac (!simpset addsimps [trancl_converse]) 1);
    1.66 +qed "acyclic_converse";
    1.67  
    1.68  (** cut **)
    1.69  
    1.70 @@ -272,4 +332,3 @@
    1.71  by (assume_tac 1);
    1.72  by (assume_tac 1);
    1.73  qed "tfl_wfrec";
    1.74 -