theory Dependency
imports "../../Semantics/Big_Step" "../../Semantics/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
  Skip[intro]: "influences v SKIP v"
| Seq[intro]: 
  "[| influences x c1 y; influences y c2 z |]
   ==> influences x (c1 ; c2) z"
| Assign_same[intro]: 
  "x \<in> vars a ==> influences x (z ::= a) z"
| Assign_other[intro]: 
  "x ~= z ==> influences z (x ::= a) z"
| If1[intro]:
  "influences x c1 y
   ==> influences x (IF b THEN c1 ELSE c2) y"
| If2[intro]:
  "influences x c2 y
   ==> influences x (IF b THEN c1 ELSE c2) y"
| If_assigned[intro]:
  "[| assigned c1 y \<or> assigned c2 y; x \<in> vars b  |]
   ==> influences x (IF b THEN c1 ELSE c2) y"
| While1[intro]:
  "influences x (WHILE b DO c) x"
| While2:
  "[| influences x c y; influences y (WHILE b DO c) z |]
   ==> influences x (WHILE b DO c) z"
| While_assigned[intro]:
  "[| assigned c y; x \<in> vars b  |]
   ==> influences x (WHILE b DO c) y"


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


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

lemma deps_unassigned_keep[simp]: (*eine Folgerung von unassigned implies equal*)
  "~ assigned c x ==> x \<in> deps c x"
proof (induct arbitrary: x) (*<-todo: Hausarbeit 5 testen, f�ür das Ausw�ählen der Cases*)
case (SKIP x) show ?case apply (auto)done
next case ( Assign nat aexp) show ?case apply(simp)by (metis Assign.prems Assign_other assigned.simps(2)) 
next case ( Semi com1 com2) show ?case (*todo: Interessant, was macht apply(auto) hier kaputt, dass metis nicht mehr l�äuft*)
by (metis Collect_def Collect_mem_eq Semi.hyps(1) Semi.hyps(2) Semi.prems Seq assigned.simps(3) mem_def)
next case (If bexp com1 com2) show ?case
by (metis Collect_def Collect_mem_eq If.hyps(2) If.prems If2 assigned.simps(4) mem_def)    
next case (While bexp com) show ?case by( auto)
qed 
(* Wieso funktionieren geschachtelte Kommentare bei mir nicht?
Subgoals
goal (5 subgoals):
 1. ~ assigned SKIP x ==> x : deps SKIP x 
 2. !!nat aexp. ~ assigned (nat ::= aexp) x ==> x : deps (nat ::= aexp) x 
 3. !!com1 com2.
       [| ~ assigned com1 x ==> x : deps com1 x; ~ assigned com2 x ==> x : deps com2 x; ~ assigned (com1; com2) x |]
       ==> x : deps (com1; com2) x
 4. !!bexp com1 com2.
       [| ~ assigned com1 x ==> x : deps com1 x; ~ assigned com2 x ==> x : deps com2 x;
          ~ assigned (IF bexp THEN com1 ELSE com2) x |]
       ==> x : deps (IF bexp THEN com1 ELSE com2) x
 5. !!bexp com.
       [| ~ assigned com x ==> x : deps com x; ~ assigned (WHILE bexp DO com) x |] ==> x : deps (WHILE bexp DO com) x*)


text {* Main theorem *}

lemma deps_sound:
  "[| (c, s) => t; s = s' on deps c x; (c, s')=> t' |]==> t x = t' x"
proof (induct c s t arbitrary: x s' t' rule: big_step_induct)
  case (Skip x_neu) 
  (*  x_neu = s' on deps SKIP x
  (SKIP, s') => t'*)
  thus ?case by blast
next
  case (Assign x_neu a s)
(*this:
  s = s' on deps (x_neu ::= a) x
  (x_neu ::= a, s') => t' *)
  thus ?case apply(auto) by (metis Assign_same aval_eq_if_eq_on_vars) 
next 
  case(WhileFalse b s c )
(*this:
  ~ bval b s
  s = s' on deps (WHILE b DO c) x
  (WHILE b DO c, s') => t'*)
  then show ?case
      apply auto  by (metis While1 WhileE WhileFalse.hyps WhileFalse.prems(2) While_assigned assigned.simps(5) bval_eq_if_eq_on_vars unassigned_implies_equal)
next

  case (IfTrue b s c1 t c2)
(*this:
1  bval b s
2  (c1, s) => t
3  [| s = ?s' on deps c1 ?x; (c1, ?s') => ?t' |] ==> t ?x = ?t' ?x
4  s = s' on deps (IF b THEN c1 ELSE c2) x
5  (IF b THEN c1 ELSE c2, s') => t'*)
 then show ?case
  apply auto
  apply (metis If1)
  by (metis Collect_def IfTrue.hyps(1) IfTrue.hyps(2) IfTrue.prems(1) If_assigned assigned.simps(4) bval_eq_if_eq_on_vars deps_unassigned_keep unassigned_implies_equal)
next
  case (IfFalse b s c1 t c2)
  then show ?case 
  apply auto (*Sledgehammer funktioniert nicht, manuelles Anpassen l�¡�äuft*)
 apply (metis Collect_def IfFalse.hyps(1) IfFalse.hyps(2) IfFalse.prems(1) If_assigned assigned.simps(4) bval_eq_if_eq_on_vars deps_unassigned_keep unassigned_implies_equal)
 by (metis If2)


next
  case (Semi c1 s s2 c2 t)thm Semi (*Was ist hier so besonders, dass metis nicht mehr terminiert. todo: Die Beweise der anderen F�älle anschauen und vergleichen. -> Diese Regeln sind die einzigen, die Abh�ängigkeiten von Befehl zu Befehl tragen. Deshalb muss man erst den existierenden Zwischenstand s2' finden. Damit es Sound ist dann noch Gleichheit zeigen (obtain nachschlagen). Danach schauen ob auto reicht.*)
(*this:
1 (c1, s) => s2
2 [| s = ?s' on deps c1 ?x; (c1, ?s') => ?t' |] ==> s2 ?x = ?t' ?x
3 (c2, s2) => t
4 [| s2 = ?s' on deps c2 ?x; (c2, ?s') => ?t' |] ==> t ?x = ?t' ?x
5 s = s' on deps (c1; c2) x
6 (c1; c2, s') => t'*)(*siehe Semi Nr 2*)
(*  then show ?case apply auto
by (metis Seq)<-terminiert nicht*)(* apply bestsimp <-terminiert nicht*)(*apply force<-terminiert auch nicht. Manueller Beweis n�ötig*) 
  from `(c1;c2,s')=>t'`  obtain s2' where "(c1, s') => s2' "" (c2, s2') => t'" by blast (*Folie 170*)
   
{ fix y
    assume "y : deps c2 x"
    from this have "deps c1 y <= deps (c1;c2) x" by auto 
    from `s = s' on deps (c1; c2) x`  `(c1, s') => s2' `` (c2, s2') => t'` `[| s = s' on deps c1 y; (c1, s') => s2' |] ==> s2 y = s2' y` this  have "s2 y= s2' y" by auto
  } 
  from this`[| s2 = s2' on deps c2 x; (c2, s2') => t' |] ==> t x = t' x`  `(c1, s') => s2' `` (c2, s2') => t'` show ?case  by auto

 

next
  case (WhileTrue b s c s2 t)(*Beweis per Hand, Metis hat Probleme mit dem Terminieren*)
(*this:
1  bval b s
2  (c, s) => s2
3  [| s = ?s' on deps c ?x; (c, ?s') => ?t' |] ==> s2 ?x = ?t' ?x
4  (WHILE b DO c, s2) => t
5  [| s2 = ?s' on deps (WHILE b DO c) ?x; (WHILE b DO c, ?s') => ?t' |] ==> t ?x = ?t' ?x
6  s = s' on deps (WHILE b DO c) x
7  (WHILE b DO c, s') => t'*)
then show ?case
proof (cases "assigned c x") (*Isabelle->Cases*)
 case False

     from `bval b s``(WHILE b DO c, s2) => t` `(c, s) => s2`  have "(WHILE b DO c, s) => t" by auto
(*1*)from unassigned_implies_equal `~assigned c x` `(WHILE b DO c, s ) => t `  have se1: "s x = t x"  by auto
(*2*)from unassigned_implies_equal `~assigned c x` `(WHILE b DO c, s') => t'`  have se2: "s' x = t' x" by auto
(*3*)from deps_unassigned_keep `s = s' on deps (WHILE b DO c) x` this have se3: "s x = s' x"  by auto 
     from se1 se2 se3 show "t x = t' x" by auto
next
 case True (*then  show "t x = t' x" using WhileTrue by auto*) 
  from `assigned c x`(**) `s = s' on deps (WHILE b DO c) x`  have "s = s' on vars b" by auto
  from this  have  "bval b s = bval b s'"  apply ( auto intro: bval_eq_if_eq_on_vars)apply (metis WhileTrue.hyps(1) bval_eq_if_eq_on_vars)by (metis WhileTrue.hyps(1) bval_eq_if_eq_on_vars)(*selbst wenn man das Lemma aus vars.thy benutzt, ist dieser sehr einfach erscheinende Zusammenhang �überraschend schwer, was verursacht diese Probleme? *)
  from this `bval b s` `(WHILE b DO c, s') => t'` obtain s2'  where  "(c, s') => s2'" "(WHILE b DO c, s2') => t'" by auto
   { fix y
     assume "y : deps (WHILE b DO c) x"
     from this While2 have "deps c y <= deps (WHILE b DO c) x" by auto 
     from this `s = s' on deps (WHILE b DO c) x`  have "s = s' on deps c y" by auto
     from this`(c, s') => s2'``(WHILE b DO c, s2') => t'` `[| s = s' on deps c y; (c, s') => s2' |] ==> s2 y = s2' y` have "s2 y = s2' y"  by auto
   }
  from this `(c, s') => s2' `` (WHILE b DO c, s2') => t'` ` [| s2 = s2' on deps (WHILE b DO c) x; (WHILE b DO c, s2') => t' |] ==> t x = t' x`  show "t x = t' x" by auto
qed
qed