products/sources/formale Sprachen/Coq/theories/Bool/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: set_of_functions.pvs   Sprache: Isabelle

Untersuchung Isabelle©
(*  Title:      ZF/Coind/ECR.thy
    Author:     Jacob Frost, Cambridge University Computer Laboratory
    Copyright   1995  University of Cambridge
*)

theory ECR imports Static Dynamic begin

(* The extended correspondence relation *)

consts
  HasTyRel :: i
coinductive
  domains "HasTyRel" \<subseteq> "Val * Ty"
  intros
    htr_constI [intro!]:
      "[| c \ Const; t \ Ty; isof(c,t) |] ==> \ HasTyRel"
    htr_closI [intro]:
      "[| x \ ExVar; e \ Exp; t \ Ty; ve \ ValEnv; te \ TyEnv;
          <te,e_fn(x,e),t> \<in> ElabRel;  
          ve_dom(ve) = te_dom(te);   
          {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in> Pow(HasTyRel) |] 
       ==> <v_clos(x,e,ve),t> \<in> HasTyRel" 
  monos  Pow_mono
  type_intros Val_ValEnv.intros
  
(* Pointwise extension to environments *)
 
definition
  hastyenv :: "[i,i] => o"  where
    "hastyenv(ve,te) ==
         ve_dom(ve) = te_dom(te) &          
         (\<forall>x \<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)> \<in> HasTyRel)"

(* Specialised co-induction rule *)

lemma htr_closCI [intro]:
     "[| x \ ExVar; e \ Exp; t \ Ty; ve \ ValEnv; te \ TyEnv;
         <te, e_fn(x, e), t> \<in> ElabRel; ve_dom(ve) = te_dom(te);  
         {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in>
           Pow({<v_clos(x,e,ve),t>} \<union> HasTyRel) |]     
      ==> <v_clos(x, e, ve),t> \<in> HasTyRel"
apply (rule singletonI [THEN HasTyRel.coinduct], auto)
done

(* Specialised elimination rules *)

inductive_cases
    htr_constE [elim!]: " \ HasTyRel"
  and htr_closE [elim]: " \ HasTyRel"


(* Properties of the pointwise extension to environments *)

lemmas HasTyRel_non_zero =
       HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE]

lemma hastyenv_owr: 
  "[| ve \ ValEnv; te \ TyEnv; hastyenv(ve,te); \ HasTyRel |]
   ==> hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"
by (auto simp add: hastyenv_def ve_app_owr HasTyRel_non_zero)

lemma basic_consistency_lem: 
  "[| ve \ ValEnv; te \ TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)"
apply (unfold isofenv_def hastyenv_def)
apply (force intro: te_appI ve_domI) 
done


(* ############################################################ *)
(* The Consistency theorem                                      *)
(* ############################################################ *)

lemma consistency_const:
     "[| c \ Const; hastyenv(ve,te); \ ElabRel |]
      ==> <v_const(c), t> \<in> HasTyRel"
by blast


lemma consistency_var: 
  "[| x \ ve_dom(ve); hastyenv(ve,te); \ ElabRel |] ==>
   <ve_app(ve,x),t> \<in> HasTyRel"
by (unfold hastyenv_def, blast)

lemma consistency_fn: 
  "[| ve \ ValEnv; x \ ExVar; e \ Exp; hastyenv(ve,te);
           <te,e_fn(x,e),t> \<in> ElabRel   
        |] ==> <v_clos(x, e, ve), t> \<in> HasTyRel"
by (unfold hastyenv_def, blast)

declare ElabRel.dom_subset [THEN subsetD, dest]

declare Ty.intros [simp, intro!]
declare TyEnv.intros [simp, intro!]
declare Val_ValEnv.intros [simp, intro!]

lemma consistency_fix: 
  "[| ve \ ValEnv; x \ ExVar; e \ Exp; f \ ExVar; cl \ Val;
      v_clos(x,e,ve_owr(ve,f,cl)) = cl;                           
      hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel |] ==>        
   <cl,t> \<in> HasTyRel"
apply (unfold hastyenv_def)
apply (erule elab_fixE, safe)
apply hypsubst_thin
apply (rule subst, assumption) 
apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
apply simp_all
apply (blast intro: ve_owrI) 
apply (rule ElabRel.fnI)
apply (simp_all add: ValNEE, force)
done


lemma consistency_app1:
 "[| ve \ ValEnv; e1 \ Exp; e2 \ Exp; c1 \ Const; c2 \ Const;
     <ve,e1,v_const(c1)> \<in> EvalRel;                       
     \<forall>t te.                                          
       hastyenv(ve,te) \<longrightarrow> <te,e1,t> \<in> ElabRel \<longrightarrow> <v_const(c1),t> \<in> HasTyRel;
     <ve, e2, v_const(c2)> \<in> EvalRel;                   
     \<forall>t te.                                          
       hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v_const(c2),t> \<in> HasTyRel;
     hastyenv(ve, te);                                  
     <te,e_app(e1,e2),t> \<in> ElabRel |] 
  ==> <v_const(c_app(c1, c2)),t> \<in> HasTyRel"
by (blast intro!: c_appI intro: isof_app)

lemma consistency_app2:
 "[| ve \ ValEnv; vem \ ValEnv; e1 \ Exp; e2 \ Exp; em \ Exp; xm \ ExVar;
     v \<in> Val;   
     <ve,e1,v_clos(xm,em,vem)> \<in> EvalRel;        
     \<forall>t te. hastyenv(ve,te) \<longrightarrow>                     
            <te,e1,t> \<in> ElabRel \<longrightarrow> <v_clos(xm,em,vem),t> \<in> HasTyRel;         
     <ve,e2,v2> \<in> EvalRel;                       
     \<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v2,t> \<in> HasTyRel;
     <ve_owr(vem,xm,v2),em,v> \<in> EvalRel;         
     \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) \<longrightarrow>      
            <te,em,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel;
     hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel |] 
   ==> <v,t> \<in> HasTyRel"
apply (erule elab_appE)
apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
apply (erule htr_closE)
apply (erule elab_fnE, simp)
apply clarify
apply (drule spec [THEN spec, THEN mp, THEN mp])
prefer 2 apply assumption+
apply (rule hastyenv_owr, assumption)
apply assumption 
apply (simp add: hastyenv_def, blast+)
done

lemma consistency [rule_format]:
   " \ EvalRel
    ==> (\<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel)"
apply (erule EvalRel.induct)
apply (simp_all add: consistency_const consistency_var consistency_fn 
                     consistency_fix consistency_app1)
apply (blast intro: consistency_app2)
done

lemma basic_consistency:
     "[| ve \ ValEnv; te \ TyEnv; isofenv(ve,te);
         <ve,e,v_const(c)> \<in> EvalRel; <te,e,t> \<in> ElabRel |] 
      ==> isof(c,t)"
by (blast dest: consistency intro!: basic_consistency_lem)

end

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.4Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff