Modified and shortened adm_disj lemmas.
authornipkow
Fri Feb 14 11:40:53 1997 +0100 (1997-02-14)
changeset 26193fd774ee405a
parent 2618 15451c558a32
child 2620 54f21bf9522a
Modified and shortened adm_disj lemmas.
src/HOLCF/Fix.ML
     1.1 --- a/src/HOLCF/Fix.ML	Fri Feb 14 10:57:17 1997 +0100
     1.2 +++ b/src/HOLCF/Fix.ML	Fri Feb 14 11:40:53 1997 +0100
     1.3 @@ -1044,9 +1044,8 @@
     1.4  
     1.5  local
     1.6  
     1.7 -  val adm_disj_lemma1 = prove_goal Pcpo.thy 
     1.8 -  "[| is_chain Y; !n.P (Y n) | Q(Y n)|]\
     1.9 -  \ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))"
    1.10 +  val adm_disj_lemma1 = prove_goal HOL.thy 
    1.11 +  "!n.P(Y n)|Q(Y n) ==> (? i.!j.R i j --> Q(Y(j))) | (!i.? j.R i j & P(Y(j)))"
    1.12   (fn prems =>
    1.13          [
    1.14          (cut_facts_tac prems 1),
    1.15 @@ -1054,113 +1053,44 @@
    1.16          ]);
    1.17  
    1.18    val adm_disj_lemma2 = prove_goal Fix.thy  
    1.19 -  "[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
    1.20 +  "!!Q. [| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
    1.21    \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
    1.22 - (fn prems =>
    1.23 + (fn _ => [fast_tac (!claset addEs [adm_def2 RS iffD1 RS spec RS mp RS mp]
    1.24 +                             addss !simpset) 1]);
    1.25 +
    1.26 +  val adm_disj_lemma3 = prove_goalw Fix.thy [is_chain]
    1.27 +  "!!Q. is_chain(Y) ==> is_chain(%m. if m < Suc i then Y(Suc i) else Y m)"
    1.28 + (fn _ =>
    1.29          [
    1.30 -        (cut_facts_tac prems 1),
    1.31 -        (etac exE 1),
    1.32 -        (etac conjE 1),
    1.33 -        (etac conjE 1),
    1.34 -        (res_inst_tac [("s","lub(range(X))"),("t","lub(range(Y))")] ssubst 1),
    1.35 -        (atac 1),
    1.36 -        (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
    1.37 -        (atac 1),
    1.38 -        (atac 1),
    1.39 -        (atac 1)
    1.40 +        asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
    1.41 +        safe_tac HOL_cs,
    1.42 +        subgoal_tac "ia = i" 1,
    1.43 +        Asm_simp_tac 1,
    1.44 +        trans_tac 1
    1.45          ]);
    1.46  
    1.47 -  val adm_disj_lemma3 = prove_goal Fix.thy
    1.48 -  "[| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
    1.49 -  \         is_chain(%m. if m < Suc i then Y(Suc i) else Y m)"
    1.50 - (fn prems =>
    1.51 +  val adm_disj_lemma4 = prove_goal Nat.thy
    1.52 +  "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
    1.53 + (fn _ =>
    1.54          [
    1.55 -        (cut_facts_tac prems 1),
    1.56 -        (rtac is_chainI 1),
    1.57 -        (rtac allI 1),
    1.58 -        (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
    1.59 -        (res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1),
    1.60 -        (rtac iffI 1),
    1.61 -        (etac FalseE 2),
    1.62 -        (rtac notE 1),
    1.63 -        (rtac (not_less_eq RS iffD2) 1),
    1.64 -        (atac 1),
    1.65 -        (atac 1),
    1.66 -        (res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
    1.67 -        (Asm_simp_tac  1),
    1.68 -        (rtac iffI 1),
    1.69 -        (etac FalseE 2),
    1.70 -        (rtac notE 1),
    1.71 -        (etac less_not_sym 1),  
    1.72 -        (atac 1),
    1.73 -        (Asm_simp_tac 1),
    1.74 -        (etac (is_chainE RS spec) 1),
    1.75 -        (hyp_subst_tac 1),
    1.76 -        (Asm_simp_tac 1),
    1.77 -        (Asm_simp_tac 1),
    1.78 -        (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1)
    1.79 -        ]);
    1.80 -
    1.81 -  val adm_disj_lemma4 = prove_goal Fix.thy
    1.82 -  "[| ! j. i < j --> Q(Y(j)) |] ==>\
    1.83 -  \        ! n. Q( if n < Suc i then Y(Suc i) else Y n)"
    1.84 - (fn prems =>
    1.85 -        [
    1.86 -        (cut_facts_tac prems 1),
    1.87 -        (rtac allI 1),
    1.88 -        (res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1),
    1.89 -        (res_inst_tac[("s","Y(Suc(i))"),
    1.90 -                      ("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1),
    1.91 -        (Asm_simp_tac 1),
    1.92 -        (etac allE 1),
    1.93 -        (rtac mp 1),
    1.94 -        (atac 1),
    1.95 -        (Asm_simp_tac 1),
    1.96 -        (res_inst_tac[("s","Y(n)"),
    1.97 -                      ("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
    1.98 -        (Asm_simp_tac 1),
    1.99 -        (hyp_subst_tac 1),
   1.100 -        (dtac spec 1),
   1.101 -        (rtac mp 1),
   1.102 -        (atac 1),
   1.103 -        (Asm_simp_tac 1),
   1.104 -        (res_inst_tac [("s","Y(n)"),
   1.105 -                       ("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")]ssubst 1),
   1.106 -        (res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
   1.107 -        (rtac iffI 1),
   1.108 -        (etac FalseE 2),
   1.109 -        (rtac notE 1),
   1.110 -        (etac less_not_sym 1),  
   1.111 -        (atac 1),
   1.112 -        (Asm_simp_tac 1),
   1.113 -        (dtac spec 1),
   1.114 -        (rtac mp 1),
   1.115 -        (atac 1),
   1.116 -        (etac Suc_lessD 1)
   1.117 +        asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
   1.118 +        strip_tac 1,
   1.119 +        etac allE 1,
   1.120 +        etac mp 1,
   1.121 +        trans_tac 1
   1.122          ]);
   1.123  
   1.124    val adm_disj_lemma5 = prove_goal Fix.thy
   1.125 -  "[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\
   1.126 +  "!!Y::nat=>'a. [| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
   1.127    \       lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
   1.128   (fn prems =>
   1.129          [
   1.130 -        (cut_facts_tac prems 1),
   1.131 -        (rtac lub_equal2 1),
   1.132 -        (atac 2),
   1.133 -        (rtac adm_disj_lemma3 2),
   1.134 -        (atac 2),
   1.135 -        (atac 2),
   1.136 -        (res_inst_tac [("x","i")] exI 1),
   1.137 -        (strip_tac 1),
   1.138 -        (res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1),
   1.139 -        (rtac iffI 1),
   1.140 -        (etac FalseE 2),
   1.141 -        (rtac notE 1),
   1.142 -        (rtac (not_less_eq RS iffD2) 1),
   1.143 -        (atac 1),
   1.144 -        (atac 1),
   1.145 -        (stac if_False 1),
   1.146 -        (rtac refl 1)
   1.147 +        safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
   1.148 +        atac 2,
   1.149 +        asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
   1.150 +        res_inst_tac [("x","i")] exI 1,
   1.151 +        strip_tac 1,
   1.152 +        trans_tac 1
   1.153          ]);
   1.154  
   1.155    val adm_disj_lemma6 = prove_goal Fix.thy
   1.156 @@ -1174,7 +1104,6 @@
   1.157          (rtac conjI 1),
   1.158          (rtac adm_disj_lemma3 1),
   1.159          (atac 1),
   1.160 -        (atac 1),
   1.161          (rtac conjI 1),
   1.162          (rtac adm_disj_lemma4 1),
   1.163          (atac 1),
   1.164 @@ -1207,7 +1136,7 @@
   1.165          ]);
   1.166  
   1.167    val adm_disj_lemma8 = prove_goal Fix.thy 
   1.168 -  "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(Least(%j. m<j & P(Y(j)))))"
   1.169 +  "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))"
   1.170   (fn prems =>
   1.171          [
   1.172          (cut_facts_tac prems 1),
   1.173 @@ -1298,7 +1227,6 @@
   1.174          (strip_tac 1),
   1.175          (rtac (adm_disj_lemma1 RS disjE) 1),
   1.176          (atac 1),
   1.177 -        (atac 1),
   1.178          (rtac disjI2 1),
   1.179          (etac adm_disj_lemma12 1),
   1.180          (atac 1),