paulson@8256: (*  Title:      HOL/UNITY/Rename.thy
paulson@8256:     ID:         $Id$
paulson@8256:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@8256:     Copyright   2000  University of Cambridge
paulson@8256: 
paulson@8256: Renaming of state sets
paulson@8256: *)
paulson@8256: 
paulson@13790: theory Rename = Extend:
paulson@8256: 
paulson@8256: constdefs
paulson@8256:   
paulson@8256:   rename :: "['a => 'b, 'a program] => 'b program"
paulson@8256:     "rename h == extend (%(x,u::unit). h x)"
paulson@8256: 
paulson@13790: declare image_inv_f_f [simp] image_surj_f_inv_f [simp]
paulson@13790: 
paulson@13790: declare Extend.intro [simp,intro]
paulson@13790: 
paulson@13790: lemma good_map_bij [simp,intro]: "bij h ==> good_map (%(x,u). h x)"
paulson@13790: apply (rule good_mapI)
paulson@13790: apply (unfold bij_def inj_on_def surj_def, auto)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma fst_o_inv_eq_inv: "bij h ==> fst (inv (%(x,u). h x) s) = inv h s"
paulson@13790: apply (unfold bij_def split_def, clarify)
paulson@13790: apply (subgoal_tac "surj (%p. h (fst p))")
paulson@13790:  prefer 2 apply (simp add: surj_def)
paulson@13790: apply (erule injD)
paulson@13790: apply (simp (no_asm_simp) add: surj_f_inv_f)
paulson@13790: apply (erule surj_f_inv_f)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma mem_rename_set_iff: "bij h ==> z : h`A = (inv h z : A)"
paulson@13790: by (force simp add: bij_is_inj bij_is_surj [THEN surj_f_inv_f])
paulson@13790: 
paulson@13790: 
paulson@13790: lemma extend_set_eq_image [simp]: "extend_set (%(x,u). h x) A = h`A"
paulson@13790: by (force simp add: extend_set_def)
paulson@13790: 
paulson@13790: lemma Init_rename [simp]: "Init (rename h F) = h`(Init F)"
paulson@13790: by (simp add: rename_def)
paulson@13790: 
paulson@13790: 
paulson@13790: (*** inverse properties ***)
paulson@13790: 
paulson@13790: lemma extend_set_inv: 
paulson@13790:      "bij h  
paulson@13790:       ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)"
paulson@13790: apply (unfold bij_def)
paulson@13790: apply (rule ext)
paulson@13790: apply (force simp add: extend_set_def project_set_def surj_f_inv_f)
paulson@13790: done
paulson@13790: 
paulson@13790: (** for "rename" (programs) **)
paulson@13790: 
paulson@13790: lemma bij_extend_act_eq_project_act: "bij h  
paulson@13790:       ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)"
paulson@13790: apply (rule ext)
paulson@13790: apply (force simp add: extend_act_def project_act_def bij_def surj_f_inv_f)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))"
paulson@13790: apply (rule bijI)
paulson@13790: apply (rule Extend.inj_extend_act)
paulson@13790: apply (auto simp add: bij_extend_act_eq_project_act)
paulson@13790: apply (rule surjI)
paulson@13790: apply (rule Extend.extend_act_inverse)
paulson@13790: apply (blast intro: bij_imp_bij_inv good_map_bij)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))"
paulson@13790: apply (frule bij_imp_bij_inv [THEN bij_extend_act])
paulson@13790: apply (simp add: bij_extend_act_eq_project_act bij_imp_bij_inv inv_inv_eq)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma bij_inv_project_act_eq: "bij h ==> inv (project_act (%(x,u::'c). inv h x)) =  
paulson@13790:                 project_act (%(x,u::'c). h x)"
paulson@13790: apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric])
paulson@13790: apply (rule surj_imp_inv_eq)
paulson@13790: apply (blast intro: bij_extend_act bij_is_surj)
paulson@13790: apply (simp (no_asm_simp) add: Extend.extend_act_inverse)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma extend_inv: "bij h   
paulson@13790:       ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV"
paulson@13790: apply (frule bij_imp_bij_inv)
paulson@13790: apply (rule ext)
paulson@13790: apply (rule program_equalityI)
paulson@13790:   apply (simp (no_asm_simp) add: extend_set_inv)
paulson@13790:  apply (simp add: Extend.project_act_Id Extend.Acts_extend 
paulson@13790:           insert_Id_image_Acts bij_extend_act_eq_project_act inv_inv_eq) 
paulson@13790: apply (simp add: Extend.AllowedActs_extend Extend.AllowedActs_project 
paulson@13790:              bij_project_act bij_vimage_eq_inv_image bij_inv_project_act_eq)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_inv_rename [simp]: "bij h ==> rename (inv h) (rename h F) = F"
paulson@13790: by (simp add: rename_def extend_inv Extend.extend_inverse)
paulson@13790: 
paulson@13790: lemma rename_rename_inv [simp]: "bij h ==> rename h (rename (inv h) F) = F"
paulson@13790: apply (frule bij_imp_bij_inv)
paulson@13790: apply (erule inv_inv_eq [THEN subst], erule rename_inv_rename)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_inv_eq: "bij h ==> rename (inv h) = inv (rename h)"
paulson@13790: by (rule inv_equality [symmetric], auto)
paulson@13790: 
paulson@13790: (** (rename h) is bijective <=> h is bijective **)
paulson@13790: 
paulson@13790: lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))"
paulson@13790: apply (rule bijI)
paulson@13790: apply (blast intro: Extend.inj_extend)
paulson@13790: apply (rule_tac f = "extend (% (x,u) . inv h x) " in surjI)
paulson@13790: apply (subst inv_inv_eq [of h, symmetric], assumption) 
paulson@13790: apply (subst extend_inv, simp add: bij_imp_bij_inv) 
paulson@13790: apply (simp add: inv_inv_eq) 
paulson@13790: apply (rule Extend.extend_inverse) 
paulson@13790: apply (simp add: bij_imp_bij_inv) 
paulson@13790: done
paulson@13790: 
paulson@13790: lemma bij_project: "bij h ==> bij (project (%(x,u::'c). h x) UNIV)"
paulson@13790: apply (subst extend_inv [symmetric])
paulson@13790: apply (auto simp add: bij_imp_bij_inv bij_extend)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma inv_project_eq:
paulson@13790:      "bij h   
paulson@13790:       ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)"
paulson@13790: apply (rule inj_imp_inv_eq)
paulson@13790: apply (erule bij_project [THEN bij_is_inj])
paulson@13790: apply (simp (no_asm_simp) add: Extend.extend_inverse)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma Allowed_rename [simp]:
paulson@13790:      "bij h ==> Allowed (rename h F) = rename h ` Allowed F"
paulson@13790: apply (simp (no_asm_simp) add: rename_def Extend.Allowed_extend)
paulson@13790: apply (subst bij_vimage_eq_inv_image)
paulson@13790: apply (rule bij_project, blast)
paulson@13790: apply (simp (no_asm_simp) add: inv_project_eq)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma bij_rename: "bij h ==> bij (rename h)"
paulson@13790: apply (simp (no_asm_simp) add: rename_def bij_extend)
paulson@13790: done
paulson@13790: lemmas surj_rename = bij_rename [THEN bij_is_surj, standard]
paulson@13790: 
paulson@13790: lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
paulson@13790: apply (unfold inj_on_def, auto)
paulson@13790: apply (drule_tac x = "mk_program ({x}, {}, {}) " in spec)
paulson@13790: apply (drule_tac x = "mk_program ({y}, {}, {}) " in spec)
paulson@13790: apply (auto simp add: program_equality_iff rename_def extend_def)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma surj_rename_imp_surj: "surj (rename h) ==> surj h"
paulson@13790: apply (unfold surj_def, auto)
paulson@13790: apply (drule_tac x = "mk_program ({y}, {}, {}) " in spec)
paulson@13790: apply (auto simp add: program_equality_iff rename_def extend_def)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma bij_rename_imp_bij: "bij (rename h) ==> bij h"
paulson@13790: apply (unfold bij_def)
paulson@13790: apply (simp (no_asm_simp) add: inj_rename_imp_inj surj_rename_imp_surj)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma bij_rename_iff [simp]: "bij (rename h) = bij h"
paulson@13790: by (blast intro: bij_rename bij_rename_imp_bij)
paulson@13790: 
paulson@13790: 
paulson@13790: (*** the lattice operations ***)
paulson@13790: 
paulson@13790: lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP"
paulson@13790: by (simp add: rename_def Extend.extend_SKIP)
paulson@13790: 
paulson@13790: lemma rename_Join [simp]: 
paulson@13790:      "bij h ==> rename h (F Join G) = rename h F Join rename h G"
paulson@13790: by (simp add: rename_def Extend.extend_Join)
paulson@13790: 
paulson@13790: lemma rename_JN [simp]:
paulson@13790:      "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))"
paulson@13790: by (simp add: rename_def Extend.extend_JN)
paulson@13790: 
paulson@13790: 
paulson@13790: (*** Strong Safety: co, stable ***)
paulson@13790: 
paulson@13790: lemma rename_constrains: 
paulson@13790:      "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)"
paulson@13790: apply (unfold rename_def)
paulson@13790: apply (subst extend_set_eq_image [symmetric])+
paulson@13790: apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_constrains])
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_stable: 
paulson@13790:      "bij h ==> (rename h F : stable (h`A)) = (F : stable A)"
paulson@13790: apply (simp add: stable_def rename_constrains)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_invariant:
paulson@13790:      "bij h ==> (rename h F : invariant (h`A)) = (F : invariant A)"
paulson@13790: apply (simp add: invariant_def rename_stable bij_is_inj [THEN inj_image_subset_iff])
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_increasing:
paulson@13790:      "bij h ==> (rename h F : increasing func) = (F : increasing (func o h))"
paulson@13790: apply (simp add: increasing_def rename_stable [symmetric] bij_image_Collect_eq bij_is_surj [THEN surj_f_inv_f])
paulson@13790: done
paulson@13790: 
paulson@13790: 
paulson@13790: (*** Weak Safety: Co, Stable ***)
paulson@13790: 
paulson@13790: lemma reachable_rename_eq: 
paulson@13790:      "bij h ==> reachable (rename h F) = h ` (reachable F)"
paulson@13790: apply (simp add: rename_def Extend.reachable_extend_eq)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_Constrains:
paulson@13790:      "bij h ==> (rename h F : (h`A) Co (h`B)) = (F : A Co B)"
paulson@13790: by (simp add: Constrains_def reachable_rename_eq rename_constrains
paulson@13790:                bij_is_inj image_Int [symmetric])
paulson@13790: 
paulson@13790: lemma rename_Stable: 
paulson@13790:      "bij h ==> (rename h F : Stable (h`A)) = (F : Stable A)"
paulson@13790: by (simp add: Stable_def rename_Constrains)
paulson@13790: 
paulson@13790: lemma rename_Always: "bij h ==> (rename h F : Always (h`A)) = (F : Always A)"
paulson@13790: by (simp add: Always_def rename_Stable bij_is_inj [THEN inj_image_subset_iff])
paulson@13790: 
paulson@13790: lemma rename_Increasing:
paulson@13790:      "bij h ==> (rename h F : Increasing func) = (F : Increasing (func o h))"
paulson@13790: by (simp add: Increasing_def rename_Stable [symmetric] bij_image_Collect_eq 
paulson@13790:               bij_is_surj [THEN surj_f_inv_f])
paulson@13790: 
paulson@13790: 
paulson@13790: (*** Progress: transient, ensures ***)
paulson@13790: 
paulson@13790: lemma rename_transient: 
paulson@13790:      "bij h ==> (rename h F : transient (h`A)) = (F : transient A)"
paulson@13790: apply (unfold rename_def)
paulson@13790: apply (subst extend_set_eq_image [symmetric])
paulson@13790: apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_transient])
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_ensures: 
paulson@13790:      "bij h ==> (rename h F : (h`A) ensures (h`B)) = (F : A ensures B)"
paulson@13790: apply (unfold rename_def)
paulson@13790: apply (subst extend_set_eq_image [symmetric])+
paulson@13790: apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_ensures])
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_leadsTo: 
paulson@13790:      "bij h ==> (rename h F : (h`A) leadsTo (h`B)) = (F : A leadsTo B)"
paulson@13790: apply (unfold rename_def)
paulson@13790: apply (subst extend_set_eq_image [symmetric])+
paulson@13790: apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_leadsTo])
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_LeadsTo: 
paulson@13790:      "bij h ==> (rename h F : (h`A) LeadsTo (h`B)) = (F : A LeadsTo B)"
paulson@13790: apply (unfold rename_def)
paulson@13790: apply (subst extend_set_eq_image [symmetric])+
paulson@13790: apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_LeadsTo])
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_rename_guarantees_eq: 
paulson@13790:      "bij h ==> (rename h F : (rename h ` X) guarantees  
paulson@13790:                               (rename h ` Y)) =  
paulson@13790:                 (F : X guarantees Y)"
paulson@13790: apply (unfold rename_def)
paulson@13790: apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_guarantees_eq [symmetric]], assumption)
paulson@13790: apply (simp (no_asm_simp) add: fst_o_inv_eq_inv o_def)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_guarantees_eq_rename_inv:
paulson@13790:      "bij h ==> (rename h F : X guarantees Y) =  
paulson@13790:                 (F : (rename (inv h) ` X) guarantees  
paulson@13790:                      (rename (inv h) ` Y))"
paulson@13790: apply (subst rename_rename_guarantees_eq [symmetric], assumption)
paulson@13790: apply (simp add: image_eq_UN o_def bij_is_surj [THEN surj_f_inv_f])
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_preserves:
paulson@13790:      "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))"
paulson@13790: apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_preserves [symmetric]], assumption)
paulson@13790: apply (simp add: o_def fst_o_inv_eq_inv rename_def bij_is_surj [THEN surj_f_inv_f])
paulson@13790: done
paulson@13790: 
paulson@13790: lemma ok_rename_iff [simp]: "bij h ==> (rename h F ok rename h G) = (F ok G)"
paulson@13790: by (simp add: Extend.ok_extend_iff rename_def)
paulson@13790: 
paulson@13790: lemma OK_rename_iff [simp]: "bij h ==> OK I (%i. rename h (F i)) = (OK I F)"
paulson@13790: by (simp add: Extend.OK_extend_iff rename_def)
paulson@13790: 
paulson@13790: 
paulson@13790: (*** "image" versions of the rules, for lifting "guarantees" properties ***)
paulson@13790: 
paulson@13790: (*All the proofs are similar.  Better would have been to prove one 
paulson@13790:   meta-theorem, but how can we handle the polymorphism?  E.g. in 
paulson@13790:   rename_constrains the two appearances of "co" have different types!*)
paulson@13790: lemmas bij_eq_rename = surj_rename [THEN surj_f_inv_f, symmetric]
paulson@13790: 
paulson@13790: lemma rename_image_constrains:
paulson@13790:      "bij h ==> rename h ` (A co B) = (h ` A) co (h`B)" 
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_constrains) 
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_image_stable: "bij h ==> rename h ` stable A = stable (h ` A)"
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_stable)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_image_increasing:
paulson@13790:      "bij h ==> rename h ` increasing func = increasing (func o inv h)"
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_increasing o_def bij_is_inj) 
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_image_invariant:
paulson@13790:      "bij h ==> rename h ` invariant A = invariant (h ` A)"
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_invariant) 
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_image_Constrains:
paulson@13790:      "bij h ==> rename h ` (A Co B) = (h ` A) Co (h`B)"
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_Constrains)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_image_preserves:
paulson@13790:      "bij h ==> rename h ` preserves v = preserves (v o inv h)"
paulson@13790: by (simp add: o_def rename_image_stable preserves_def bij_image_INT 
paulson@13790:               bij_image_Collect_eq)
paulson@13790: 
paulson@13790: lemma rename_image_Stable:
paulson@13790:      "bij h ==> rename h ` Stable A = Stable (h ` A)"
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_Stable) 
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_image_Increasing:
paulson@13790:      "bij h ==> rename h ` Increasing func = Increasing (func o inv h)"
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_Increasing o_def bij_is_inj)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_image_Always: "bij h ==> rename h ` Always A = Always (h ` A)"
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_Always)
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_image_leadsTo:
paulson@13790:      "bij h ==> rename h ` (A leadsTo B) = (h ` A) leadsTo (h`B)"
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_leadsTo) 
paulson@13790: done
paulson@13790: 
paulson@13790: lemma rename_image_LeadsTo:
paulson@13790:      "bij h ==> rename h ` (A LeadsTo B) = (h ` A) LeadsTo (h`B)"
paulson@13790: apply auto 
paulson@13790:  defer 1
paulson@13790:  apply (rename_tac F) 
paulson@13790:  apply (subgoal_tac "\<exists>G. F = rename h G") 
paulson@13790:  apply (auto intro!: bij_eq_rename simp add: rename_LeadsTo) 
paulson@13790: done
paulson@13790: 
paulson@8256: end