amdI -> admI2
authornipkow
Thu Jun 26 10:43:15 1997 +0200 (1997-06-26)
changeset 34617bf1e7c40a0c
parent 3460 5d71eed16fbe
child 3462 3472fa00b1d4
amdI -> admI2
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/ex/Stream.ML
     1.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Jun 26 10:42:50 1997 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Jun 26 10:43:15 1997 +0200
     1.3 @@ -7,20 +7,6 @@
     1.4  
     1.5  *)
     1.6  
     1.7 -(* FIX: Put into Fix.ML to adm_lemmas !!! *)
     1.8 -
     1.9 -goal thy "!! P. [| adm (%x. P x --> Q x); adm (%x.Q x --> P x) |] \
    1.10 -\           ==> adm (%x. P x = Q x)";
    1.11 -by (res_inst_tac [("P2","(%x.(P x --> Q x) & (Q x --> P x))")] (adm_cong RS iffD1) 1);
    1.12 -by (Fast_tac 1);
    1.13 -by (etac adm_conj 1);
    1.14 -by (assume_tac 1);
    1.15 -qed"adm_iff";
    1.16 -
    1.17 -Addsimps [adm_iff];
    1.18 -
    1.19 -
    1.20 -
    1.21  Addsimps [andalso_and,andalso_or];
    1.22  
    1.23  (* ----------------------------------------------------------------------------------- *)
    1.24 @@ -486,7 +472,7 @@
    1.25  section "admissibility";
    1.26  
    1.27  (* Finite x is proven to be adm: Finite_flat shows that there are only chains of length one.
    1.28 -   Then the assumption that an _infinite_ chain exists (from admI) is set to a contradiction 
    1.29 +   Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction 
    1.30     to Finite_flat *)
    1.31  
    1.32  goal thy "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y";
    1.33 @@ -502,7 +488,7 @@
    1.34  
    1.35  
    1.36  goal thy "adm(%(x:: 'a Seq).Finite x)";
    1.37 -by (rtac admI 1);
    1.38 +by (rtac admI2 1);
    1.39  by (eres_inst_tac [("x","0")] allE 1);
    1.40  back();
    1.41  by (etac exE 1);
     2.1 --- a/src/HOLCF/ex/Stream.ML	Thu Jun 26 10:42:50 1997 +0200
     2.2 +++ b/src/HOLCF/ex/Stream.ML	Thu Jun 26 10:43:15 1997 +0200
     2.3 @@ -363,7 +363,7 @@
     2.4  	fast_tac (HOL_cs addSIs [stream_finite_UU, stream_finite_lemma1]) 1]);
     2.5  
     2.6  qed_goal "adm_not_stream_finite" thy "adm (%x. ~  stream_finite x)" (fn _ => [
     2.7 -	rtac admI 1,
     2.8 +	rtac admI2 1,
     2.9  	dtac spec 1,
    2.10  	etac contrapos 1,
    2.11  	dtac stream_finite_less 1,