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 arbitrary: x  rule: big_step_induct)(*was geht schief, wenn hier arbitrary x, s steht?*)
  case (Skip t) 
  then show ?case 
apply(blast)done
  (* Warum funktioniert hier nicht Sledgehammer, wie es bei der Induktion �über deps funktioniert?
     [| (SKIP, s) => t; s = s' on deps SKIP x; (SKIP, s') => t' |] ==> t x = t' x
     !!s. [| s = s' on deps SKIP x; (SKIP, s') => t' |] ==> s x = t' x  ( *<- s und t' vermischt, eigenartig... * )
     Vermutung s=s' und !! haben einen schlechten Einfluss.
  *)
next
  case (IfTrue b s c1 t c2)
  then show ?case
    apply auto
(*sledgehammer minimize [atp = remote_vampire] (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)*)
by (metis 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)
   (* 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*)
by (metis 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)
  
next
  case (Assign y a s)
  thus ?case apply(auto)
by (metis Assign_same aval_eq_if_eq_on_vars)  (*Dass das hier so einfach geht, h�ätte ich nicht erwartet, es ist ja prinzipiell eine der Kernaussagen.*)  
next
  case (WhileFalse b s c  )
  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 (Semi c1 s1 s2 c2 s3 x)
  thus ?case (*gerade diese Regel hab ich f�ür die einfachste gehalten*) 
    apply auto
    
    sorry
next
  case (WhileTrue b s c s' t X)
  thus ?case
     apply auto 
     sorry

qed