<commit_before>(*  Title:      HOL/UNITY/Rename.thy
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge
*)

header{*Renaming of State Sets*}

theory Rename = Extend:

constdefs
  
  rename :: "['a => 'b, 'a program] => 'b program"
    "rename h == extend (%(x,u::unit). h x)"

declare image_inv_f_f [simp] image_surj_f_inv_f [simp]

declare Extend.intro [simp,intro]

lemma good_map_bij [simp,intro]: "bij h ==> good_map (%(x,u). h x)"
apply (rule good_mapI)
apply (unfold bij_def inj_on_def surj_def, auto)
done

lemma fst_o_inv_eq_inv: "bij h ==> fst (inv (%(x,u). h x) s) = inv h s"
apply (unfold bij_def split_def, clarify)
apply (subgoal_tac "surj (%p. h (fst p))")
 prefer 2 apply (simp add: surj_def)
apply (erule injD)
apply (simp (no_asm_simp) add: surj_f_inv_f)
apply (erule surj_f_inv_f)
done

lemma mem_rename_set_iff: "bij h ==> z \<in> h`A = (inv h z \<in> A)"
by (force simp add: bij_is_inj bij_is_surj [THEN surj_f_inv_f])


lemma extend_set_eq_image [simp]: "extend_set (%(x,u). h x) A = h`A"
by (force simp add: extend_set_def)

lemma Init_rename [simp]: "Init (rename h F) = h`(Init F)"
by (simp add: rename_def)


subsection{*inverse properties*}

lemma extend_set_inv: 
     "bij h  
      ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)"
apply (unfold bij_def)
apply (rule ext)
apply (force simp add: extend_set_def project_set_def surj_f_inv_f)
done

(** for "rename" (programs) **)

lemma bij_extend_act_eq_project_act: "bij h  
      ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)"
apply (rule ext)
apply (force simp add: extend_act_def project_act_def bij_def surj_f_inv_f)
done

lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))"
apply (rule bijI)
apply (rule Extend.inj_extend_act)
apply (auto simp add: bij_extend_act_eq_project_act)
apply (rule surjI)
apply (rule Extend.extend_act_inverse)
apply (blast intro: bij_imp_bij_inv good_map_bij)
done

lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))"
apply (frule bij_imp_bij_inv [THEN bij_extend_act])
apply (simp add: bij_extend_act_eq_project_act bij_imp_bij_inv inv_inv_eq)
done

lemma bij_inv_project_act_eq: "bij h ==> inv (project_act (%(x,u::'c). inv h x)) =  
                project_act (%(x,u::'c). h x)"
apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric])
apply (rule surj_imp_inv_eq)
apply (blast intro: bij_extend_act bij_is_surj)
apply (simp (no_asm_simp) add: Extend.extend_act_inverse)
done

lemma extend_inv: "bij h   
      ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV"
apply (frule bij_imp_bij_inv)
apply (rule ext)
apply (rule program_equalityI)
  apply (simp (no_asm_simp) add: extend_set_inv)
 apply (simp add: Extend.project_act_Id Extend.Acts_extend 
          insert_Id_image_Acts bij_extend_act_eq_project_act inv_inv_eq) 
apply (simp add: Extend.AllowedActs_extend Extend.AllowedActs_project 
             bij_project_act bij_vimage_eq_inv_image bij_inv_project_act_eq)
done

lemma rename_inv_rename [simp]: "bij h ==> rename (inv h) (rename h F) = F"
by (simp add: rename_def extend_inv Extend.extend_inverse)

lemma rename_rename_inv [simp]: "bij h ==> rename h (rename (inv h) F) = F"
apply (frule bij_imp_bij_inv)
apply (erule inv_inv_eq [THEN subst], erule rename_inv_rename)
done

lemma rename_inv_eq: "bij h ==> rename (inv h) = inv (rename h)"
by (rule inv_equality [symmetric], auto)

(** (rename h) is bijective <=> h is bijective **)

lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))"
apply (rule bijI)
apply (blast intro: Extend.inj_extend)
apply (rule_tac f = "extend (% (x,u) . inv h x) " in surjI) 
apply (simplesubst inv_inv_eq [of h, symmetric], assumption) 
apply (subst extend_inv, simp add: bij_imp_bij_inv) 
apply (simp add: inv_inv_eq) 
apply (rule Extend.extend_inverse) 
apply (simp add: bij_imp_bij_inv) 
done

lemma bij_project: "bij h ==> bij (project (%(x,u::'c). h x) UNIV)"
apply (subst extend_inv [symmetric])
apply (auto simp add: bij_imp_bij_inv bij_extend)
done

lemma inv_project_eq:
     "bij h   
      ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)"
apply (rule inj_imp_inv_eq)
apply (erule bij_project [THEN bij_is_inj])
apply (simp (no_asm_simp) add: Extend.extend_inverse)
done

lemma Allowed_rename [simp]:
     "bij h ==> Allowed (rename h F) = rename h ` Allowed F"
apply (simp (no_asm_simp) add: rename_def Extend.Allowed_extend)
apply (subst bij_vimage_eq_inv_image)
apply (rule bij_project, blast)
apply (simp (no_asm_simp) add: inv_project_eq)
done

lemma bij_rename: "bij h ==> bij (rename h)"
apply (simp (no_asm_simp) add: rename_def bij_extend)
done
lemmas surj_rename = bij_rename [THEN bij_is_surj, standard]

lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
apply (unfold inj_on_def, auto)
apply (drule_tac x = "mk_program ({x}, {}, {}) " in spec)
apply (drule_tac x = "mk_program ({y}, {}, {}) " in spec)
apply (auto simp add: program_equality_iff rename_def extend_def)
done

lemma surj_rename_imp_surj: "surj (rename h) ==> surj h"
apply (unfold surj_def, auto)
apply (drule_tac x = "mk_program ({y}, {}, {}) " in spec)
apply (auto simp add: program_equality_iff rename_def extend_def)
done

lemma bij_rename_imp_bij: "bij (rename h) ==> bij h"
apply (unfold bij_def)
apply (simp (no_asm_simp) add: inj_rename_imp_inj surj_rename_imp_surj)
done

lemma bij_rename_iff [simp]: "bij (rename h) = bij h"
by (blast intro: bij_rename bij_rename_imp_bij)


subsection{*the lattice operations*}

lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP"
by (simp add: rename_def Extend.extend_SKIP)

lemma rename_Join [simp]: 
     "bij h ==> rename h (F Join G) = rename h F Join rename h G"
by (simp add: rename_def Extend.extend_Join)<commit_msg>streamlined proof using new subst method<commit_after>(*  Title:      HOL/UNITY/Rename.thy
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge
*)

header{*Renaming of State Sets*}

theory Rename = Extend:

constdefs
  
  rename :: "['a => 'b, 'a program] => 'b program"
    "rename h == extend (%(x,u::unit). h x)"

declare image_inv_f_f [simp] image_surj_f_inv_f [simp]

declare Extend.intro [simp,intro]

lemma good_map_bij [simp,intro]: "bij h ==> good_map (%(x,u). h x)"
apply (rule good_mapI)
apply (unfold bij_def inj_on_def surj_def, auto)
done

lemma fst_o_inv_eq_inv: "bij h ==> fst (inv (%(x,u). h x) s) = inv h s"
apply (unfold bij_def split_def, clarify)
apply (subgoal_tac "surj (%p. h (fst p))")
 prefer 2 apply (simp add: surj_def)
apply (erule injD)
apply (simp (no_asm_simp) add: surj_f_inv_f)
apply (erule surj_f_inv_f)
done

lemma mem_rename_set_iff: "bij h ==> z \<in> h`A = (inv h z \<in> A)"
by (force simp add: bij_is_inj bij_is_surj [THEN surj_f_inv_f])


lemma extend_set_eq_image [simp]: "extend_set (%(x,u). h x) A = h`A"
by (force simp add: extend_set_def)

lemma Init_rename [simp]: "Init (rename h F) = h`(Init F)"
by (simp add: rename_def)


subsection{*inverse properties*}

lemma extend_set_inv: 
     "bij h  
      ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)"
apply (unfold bij_def)
apply (rule ext)
apply (force simp add: extend_set_def project_set_def surj_f_inv_f)
done

(** for "rename" (programs) **)

lemma bij_extend_act_eq_project_act: "bij h  
      ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)"
apply (rule ext)
apply (force simp add: extend_act_def project_act_def bij_def surj_f_inv_f)
done

lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))"
apply (rule bijI)
apply (rule Extend.inj_extend_act)
apply (auto simp add: bij_extend_act_eq_project_act)
apply (rule surjI)
apply (rule Extend.extend_act_inverse)
apply (blast intro: bij_imp_bij_inv good_map_bij)
done

lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))"
apply (frule bij_imp_bij_inv [THEN bij_extend_act])
apply (simp add: bij_extend_act_eq_project_act bij_imp_bij_inv inv_inv_eq)
done

lemma bij_inv_project_act_eq: "bij h ==> inv (project_act (%(x,u::'c). inv h x)) =  
                project_act (%(x,u::'c). h x)"
apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric])
apply (rule surj_imp_inv_eq)
apply (blast intro: bij_extend_act bij_is_surj)
apply (simp (no_asm_simp) add: Extend.extend_act_inverse)
done

lemma extend_inv: "bij h   
      ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV"
apply (frule bij_imp_bij_inv)
apply (rule ext)
apply (rule program_equalityI)
  apply (simp (no_asm_simp) add: extend_set_inv)
 apply (simp add: Extend.project_act_Id Extend.Acts_extend 
          insert_Id_image_Acts bij_extend_act_eq_project_act inv_inv_eq) 
apply (simp add: Extend.AllowedActs_extend Extend.AllowedActs_project 
             bij_project_act bij_vimage_eq_inv_image bij_inv_project_act_eq)
done

lemma rename_inv_rename [simp]: "bij h ==> rename (inv h) (rename h F) = F"
by (simp add: rename_def extend_inv Extend.extend_inverse)

lemma rename_rename_inv [simp]: "bij h ==> rename h (rename (inv h) F) = F"
apply (frule bij_imp_bij_inv)
apply (erule inv_inv_eq [THEN subst], erule rename_inv_rename)
done

lemma rename_inv_eq: "bij h ==> rename (inv h) = inv (rename h)"
by (rule inv_equality [symmetric], auto)

(** (rename h) is bijective <=> h is bijective **)

lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))"
apply (rule bijI)
apply (blast intro: Extend.inj_extend)
apply (rule_tac f = "extend (% (x,u) . inv h x)" in surjI) 
apply (subst (1 2) inv_inv_eq [of h, symmetric], assumption+)
apply (simp add: bij_imp_bij_inv extend_inv [of "inv h"]) 
apply (simp add: inv_inv_eq)
apply (rule Extend.extend_inverse) 
apply (simp add: bij_imp_bij_inv) 
done

lemma bij_project: "bij h ==> bij (project (%(x,u::'c). h x) UNIV)"
apply (subst extend_inv [symmetric])
apply (auto simp add: bij_imp_bij_inv bij_extend)
done

lemma inv_project_eq:
     "bij h   
      ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)"
apply (rule inj_imp_inv_eq)
apply (erule bij_project [THEN bij_is_inj])
apply (simp (no_asm_simp) add: Extend.extend_inverse)
done

lemma Allowed_rename [simp]:
     "bij h ==> Allowed (rename h F) = rename h ` Allowed F"
apply (simp (no_asm_simp) add: rename_def Extend.Allowed_extend)
apply (subst bij_vimage_eq_inv_image)
apply (rule bij_project, blast)
apply (simp (no_asm_simp) add: inv_project_eq)
done

lemma bij_rename: "bij h ==> bij (rename h)"
apply (simp (no_asm_simp) add: rename_def bij_extend)
done
lemmas surj_rename = bij_rename [THEN bij_is_surj, standard]

lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
apply (unfold inj_on_def, auto)
apply (drule_tac x = "mk_program ({x}, {}, {})" in spec)
apply (drule_tac x = "mk_program ({y}, {}, {})" in spec)
apply (auto simp add: program_equality_iff rename_def extend_def)
done

lemma surj_rename_imp_surj: "surj (rename h) ==> surj h"
apply (unfold surj_def, auto)
apply (drule_tac x = "mk_program ({y}, {}, {})" in spec)
apply (auto simp add: program_equality_iff rename_def extend_def)
done

lemma bij_rename_imp_bij: "bij (rename h) ==> bij h"
apply (unfold bij_def)
apply (simp (no_asm_simp) add: inj_rename_imp_inj surj_rename_imp_surj)
done

lemma bij_rename_iff [simp]: "bij (rename h) = bij h"
by (blast intro: bij_rename bij_rename_imp_bij)


subsection{*the lattice operations*}

lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP"
by (simp add: rename_def Extend.extend_SKIP)

lemma rename_Join [simp]: 
     "bij h ==> rename h (F Join G) = rename h F Join rename h G"
by (simp add: rename_def Extend.extend_Join)
{'fraction_non_alphanumeric': 0.13176309950503498, 'fraction_numerical': 0.0010240655401945725, 'mean_word_length': 4.960834181078332, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 59, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7187389', 'n_tokens_mistral': 4816, 'n_tokens_neox': 4797, 'n_words': 1380}