src/HOLCF/Ssum3.ML

 (* ------------------------------------------------------------------------ *)
 (* first 5 ugly lemmas                                                      *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ssum_lemma9" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
+"[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (strip_tac 1),
         (res_inst_tac [("p","Y(i)")] IssumE 1),

         (etac is_ub_thelub 1)
         ]);
 
 
 qed_goal "ssum_lemma10" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
+"[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (strip_tac 1),
         (res_inst_tac [("p","Y(i)")] IssumE 1),

         (etac subst 1),
         (etac is_ub_thelub 1)
         ]);
 
 qed_goal "ssum_lemma11" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
+"[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (asm_simp_tac Ssum0_ss 1),

         (etac (inst_ssum_pcpo RS ssubst) 1),
         (asm_simp_tac Ssum0_ss 1)
         ]);
 
 qed_goal "ssum_lemma12" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
+"[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (asm_simp_tac Ssum0_ss 1),

         (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
         ]);
 
 
 qed_goal "ssum_lemma13" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
+"[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (asm_simp_tac Ssum0_ss 1),

         tac,
         (rtac less_ssum3d 1)
         ]);
 
 qed_goalw "ssum_chainE" Ssum3.thy [sinl_def,sinr_def] 
-        "is_chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"
+        "chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
         (etac ssum_lemma4 1)
         ]);
 
 
 qed_goalw "thelub_ssum2a" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
-"[| is_chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ 
+"[| chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ 
 \   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun 1),

         (rtac refl 1),
         (asm_simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1)
         ]);
 
 qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
-"[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
+"[| chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
 \   lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun 1),

         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
         cont_Iwhen3]) 1)
         ]);
 
 qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def] 
-        "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
+        "[| chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (asm_simp_tac (Ssum0_ss addsimps 
         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,

         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
         cont_Iwhen3]) 1)
         ]);
 
 qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def] 
-        "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
+        "[| chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (asm_simp_tac (Ssum0_ss addsimps 
         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,

         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
         cont_Iwhen3]) 1)
         ]);
 
 qed_goal "thelub_ssum3" Ssum3.thy  
-"is_chain(Y) ==>\ 
+"chain(Y) ==>\ 
 \   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))\
 \ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),