theory Dependency_Template
imports Big_Step Vars
begin


text {* From Homework 5 *}
primrec assigned :: "com => name => bool" where
  "assigned SKIP x <-> False"
| "assigned (x ::= a) y <-> (x = y)"
| "assigned (c1; c2) x <-> assigned c1 x \<or> assigned c2 x"
| "assigned (IF b THEN c1 ELSE c2) x <-> assigned c1 x \<or> assigned c2 x"
| "assigned (WHILE b DO c) x <-> assigned c x"

lemma unassigned_implies_equal:
  "[| (c, s) => t; ~ assigned c x  |] ==> s x = t x"
by (induct c s t rule: big_step_induct) auto


text {* The dependency relation *}

inductive influences :: "name => com => name => bool"
where
  "influences x SKIP x"(*Skip*)
| "[|b: (vars_aexp a)|]           ==> influences b (x::= a) x"(*assign:assigned      *)(*assigned const implizit enthalten, da dann keine Regel zutrifft-> nicht abh�ängig*)
| "[|~(b=x)|]                     ==> influences b (x::= a) b"(*assign:not influenced*)
| "[|influences v1 c1 v2;influences v2 c2 v3 |] ==>influences v1 (c1; c2) v3"  (*Semi*)
| "[|influences a c1 b|]==>influences a (IF be THEN c1 ELSE c2) b"(*if: false*)(*was w�ürde "influenced a c1 b" bedeuten?*)
| "[|influences a c2 b|]==>influences a (IF be THEN c1 ELSE c2) b"(*if: true*)
       (*Wenn eine Variable in einem oder beiden Zweigen nicht zugewiesen wird, h�ängt sie u.a. von sich selbst ab.*)

| "[|av:(vars_bexp be);assigned c1 c1v|]==>influences av (IF be THEN c1 ELSE c2) c1v"(*if:b influences true*) 
| "[|av:(vars_bexp be);assigned c2 c2v|]==>influences av (IF be THEN c1 ELSE c2) c2v"(*if:b influences false*)

| "influences a (WHILE be DO c) a"(*While false=Skip*)(*while: no influence(schon durch Skip abgedeckt)*)
| "[|av:(vars_bexp be); assigned c cv|]==>influences av (WHILE  be DO c) cv"(*WHILE: b influences*)
| "[|influences a c b|]==>influences a (WHILE  be DO c) b"(*WHILE:  influences (wie IF-true)*)  
| "[|influences a (WHILE be DO cm)  b; influences b (WHILE be DO cm) c|]==>influences a (WHILE be DO cm) c"(*WHILE: assign +*) 

(*Die folgenden 2 Fragestellungen k�önnen ignoriert werden. Todo: Herausfinden, wie man emacs ohne xwindows Umlaute dauerhaft beibringt.*)
(*todo: Was mache ich bei Zuweisungen an sich selbst? Eigentlich m�¯�¡�¡�üsste man bei c1 entspricht a::= a die Abh�¯�¡�¡�ängigkeit av auf a l�¯�¡�¡�öschen, da a nicht durch av beeinflusst wird. Anders ist das, wenn dieses nur eine mit IF eingef�¯�¡�¡�ührte M�¯�¡�¡�öglichkeit im SET ist*)
(*todo:Was mache ich, wenn die Zuweisung einer Variable in c1 und c2 identisch ist?
  L�¯�¡�¡�ösung: identische Zuweisungen verbieten und nur erlauben, wenn auch nicht identische Zuweisungen m�¯�¡�¡�öglich sind.*)
  (*| "[|av:(vars_bexp be);assigned c1 c1v; ~(influences c1v c1 c1v); influences c1v c1 c1v |]==>influences av (IF be THEN c1 ELSE c2) c1v"*)




text {* All dependencies of a variable *}
abbreviation deps :: "com => name => name set" where
"deps c x == {y. influences y c x}"

value "deps SKIP 0"

text {* A simple lemma that is useful later *}

lemma deps_unassigned_keep:
  "~ assigned c x ==> x \<in> deps c x"
oops

text {* Main theorem *}

lemma deps_sound:
  "[| (c, s) => t; s = s' on deps c x; (c, s') => t'  |]
   ==> t x = t' x"
oops


end