src/HOL/UNITY/Lift_prog.thy
changeset 61943 7fba644ed827
parent 60773 d09c66a0ea10
child 62390 842917225d56
     1.1 --- a/src/HOL/UNITY/Lift_prog.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -270,13 +270,13 @@
     1.4       "[| delete_map j g = delete_map j g';  i\<noteq>j |] ==> g i = g' i"
     1.5  by force
     1.6  
     1.7 -(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
     1.8 +(*A set of the form (A \<times> UNIV) ignores the second (dummy) state component*)
     1.9  
    1.10 -lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) <*> UNIV"
    1.11 +lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) \<times> UNIV"
    1.12  by auto
    1.13  
    1.14  lemma vimage_sub_eq_lift_set [simp]:
    1.15 -     "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"
    1.16 +     "(sub i -`A) \<times> UNIV = lift_set i (A \<times> UNIV)"
    1.17  by auto
    1.18  
    1.19  lemma mem_lift_act_iff [iff]: 
    1.20 @@ -288,7 +288,7 @@
    1.21  
    1.22  lemma preserves_snd_lift_stable:
    1.23       "[| F \<in> preserves snd;  i\<noteq>j |]  
    1.24 -      ==> lift j F \<in> stable (lift_set i (A <*> UNIV))"
    1.25 +      ==> lift j F \<in> stable (lift_set i (A \<times> UNIV))"
    1.26  apply (auto simp add: lift_def lift_set_def stable_def constrains_def 
    1.27                        rename_def extend_def mem_rename_set_iff)
    1.28  apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
    1.29 @@ -298,9 +298,9 @@
    1.30  (*If i\<noteq>j then lift j F  does nothing to lift_set i, and the 
    1.31    premise ensures A \<subseteq> B.*)
    1.32  lemma constrains_imp_lift_constrains:
    1.33 -    "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
    1.34 +    "[| F i \<in> (A \<times> UNIV) co (B \<times> UNIV);   
    1.35          F j \<in> preserves snd |]   
    1.36 -     ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
    1.37 +     ==> lift j (F j) \<in> (lift_set i (A \<times> UNIV)) co (lift_set i (B \<times> UNIV))"
    1.38  apply (cases "i=j")
    1.39  apply (simp add: lift_def lift_set_def rename_constrains)
    1.40  apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
    1.41 @@ -310,8 +310,8 @@
    1.42  
    1.43  (*USELESS??*)
    1.44  lemma lift_map_image_Times:
    1.45 -     "lift_map i ` (A <*> UNIV) =  
    1.46 -      (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
    1.47 +     "lift_map i ` (A \<times> UNIV) =  
    1.48 +      (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) \<times> UNIV"
    1.49  apply (auto intro!: bexI image_eqI simp add: lift_map_def)
    1.50  apply (rule split_conv [symmetric])
    1.51  done