Theory SafeDAss_P4

(*  Title:      Safe DAss P4
    Author:     Javier de Dios and Ricardo Peña
    Copyright:  June 2008, Universidad Complutense de Madrid
*)


header {* Derived Assertions. P4. fv e $\subseteq$ L *}

theory SafeDAss_P4 imports SafeDAssBasic
begin


text{*
Lemmas for LET
*}

lemma fvs_as_subseteq_L1:
  "∀a∈set as. atom a
   ==> fvs as ⊆ atom2var ` set as"
apply (induct as,simp_all)
apply (rule conjI)
 apply (case_tac a,simp_all)
by blast


lemma P4_LET: 
  "[|fv e1 ⊆ L1; fv e2 ⊆ L2|] 
  ==> fv (Let x1 = e1 In e2 a) ⊆ L1 ∪ (L2 - {x1})"
by (clarsimp,blast)



text{*
Lemmas for CASE
*}


lemma P4_CASE_aux [rule_format]:
  "x ∈ fvAlts alts 
  --> length alts > 0 
  --> (∃i < length alts. x ∈ fv (snd (alts ! i)) ∧
                         x ∉ set (snd (extractP (fst (alts ! i)))))"
apply (induct alts,simp)
apply (rule impI,simp)
apply (erule disjE)
 apply (case_tac a, simp_all)
 apply (elim conjE)
 apply (rule_tac x="0" in exI,simp)
apply (case_tac alts,simp_all)
apply (erule exE)
apply (case_tac i,simp_all)
apply (rule_tac x="Suc 0" in exI,simp)  
apply (rule_tac x="Suc (Suc nat)" in exI) 
by simp 

lemma P4_CASE:
  "[| ∀i < length alts. x ∈ fst (assert ! i) ∧ 
          x ∉ set (snd (extractP (fst (alts ! i))));
     ∀i < length alts. fv (snd (alts ! i)) ⊆ fst (assert ! i);
     length alts > 0  |] 
   ==> fv (Case VarE x a Of alts a') ⊆ 
       (\<Union>i< length alts. fst (assert ! i) -  set (snd (extractP (fst (alts ! i))))) ∪ {x}"
apply auto
apply (subgoal_tac "length alts > 0")
 prefer 2 apply simp
apply (frule P4_CASE_aux,assumption+)
apply (erule exE)
apply (erule_tac x="i" in allE,simp) 
apply (elim conjE)
apply (erule_tac x="i" in ballE,simp)
 apply blast
by simp





text{*
Lemmas for CASED
*}

lemma P4_CASED_aux [rule_format]:
  "x ∈ fvAlts' alts --> 
   length alts > 0 --> 
   (∃i < length alts. x ∈ fv (snd (alts ! i)) ∧
                      x ∉ set (snd (extractP (fst (alts ! i)))))"
apply (induct alts,simp)
apply (rule impI,simp)
apply (erule disjE)
apply (case_tac a)
 apply (simp,elim conjE)
 apply (rule_tac x="0" in exI,simp)
apply simp
apply (case_tac alts,simp)
apply (simp, erule exE)
apply (case_tac i,simp)
 apply (rule_tac x="Suc 0" in exI,simp)
by (rule_tac x="Suc (Suc nat)" in exI,simp)




lemma P4_CASED:
  "[| ∀i < length alts. fv (snd (alts ! i)) ⊆ fst (assert ! i);
     length alts > 0  |] 
   ==> fv (CaseD VarE x a Of alts a) ⊆ 
       insert x (\<Union>i < length alts fst (assert ! i) -  set (snd (extractP (fst (alts ! i)))))"
apply clarsimp
apply (subgoal_tac "length alts > 0")
 prefer 2 apply simp
apply (frule P4_CASED_aux,assumption+)
by blast


(**** P4_PRIMOP ***)

lemma P4_APP_PRIMOP:
 "[| atom a1; atom a2 |] 
  ==> fv (AppE f [a1, a2] rs' a) ⊆ {atom2var a1, atom2var a2}"
apply (simp,rule conjI)
 apply (case_tac a1,simp_all)
by (case_tac a2,simp_all)


end