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 
  thus ?case by blast
next
  case (Assign y a s)
  thus ?case apply(auto)
by (metis Assign_same aval_eq_if_eq_on_vars) 
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 s s2 c2 t)
  from Semi(6) obtain s2' where s2':"(c1, s') => s2' & (c2, s2') => t'" by fastsimp
  { fix w
    assume "w \<in> deps c2 x"
    hence "deps c1 w \<subseteq> deps (c1;c2) x" by fastsimp
    with Semi(5) s2' Semi(2)[of w s' s2'] have "s2 w = s2' w" by fastsimp
  }
  hence "s2 = s2' on deps c2 x" by fastsimp
  with Semi(4)[of x s2' t'] s2' show "t x = t' x" by fastsimp
next
  case (IfTrue b s c1 t c2)
  show ?case
  proof (cases "assigned c1 x \<or> assigned c2 x")
    case True
    with IfTrue(4) have "s = s' on vars b" by fastsimp
    hence "bval b s = bval b s'" by (simp add: bval_eq_if_eq_on_vars)
    with IfTrue(1,5) have "(c1, s')=> t'" by blast
    thus "t x = t' x" using IfTrue(3-4) by blast
  next
    case False
    hence "s x = s' x" using deps_unassigned_keep IfTrue(4) by fastsimp
    moreover
    from unassigned_implies_equal IfTrue(2) False have "s x = t x" by fastsimp
    moreover
    from unassigned_implies_equal IfTrue(5) False have "s' x = t' x" by fastsimp
    ultimately
    show "t x = t' x" by simp
  qed
next
  case (IfFalse b s c2 t c1)
  show ?case
  proof (cases "assigned c1 x \<or> assigned c2 x")
    case True
    with IfFalse(4) have "s = s' on vars b" by fastsimp
    hence "bval b s = bval b s'" by (simp add: bval_eq_if_eq_on_vars)
    with IfFalse(1,5) have "(c2, s') => t'" by blast
    thus "t x = t' x" using IfFalse(3-4) by blast
  next
    case False
    hence "s x = s' x" using deps_unassigned_keep IfFalse(4) by fastsimp
    moreover
    from unassigned_implies_equal IfFalse(2) False have "s x = t x" by fastsimp
    moreover
    from unassigned_implies_equal IfFalse(5) False have "s' x = t' x" by fastsimp
    ultimately
    show "t x = t' x" by simp
  qed
next
  case (WhileTrue b s c s2 t)
  thus ?case
  proof (cases "assigned c x")
    case True
    with WhileTrue(6) have "s = s' on vars b" by blast
    hence "bval b s = bval b s'" by (simp add: bval_eq_if_eq_on_vars)
    with WhileTrue(1,7) obtain s2' 
      where s2': "(c, s') => s2' \<and> (WHILE b DO c, s2') => t'" by blast
    { fix w
      assume "w \<in> deps (WHILE b DO c) x"
      hence "deps c w \<subseteq> deps (WHILE b DO c) x" using While2 by fastsimp 
      with WhileTrue(6) have "s = s' on deps c w" by fastsimp
      hence "s2 w = s2' w" using s2' WhileTrue(3)[of w s' s2'] by simp
    }
    hence "s2 = s2' on deps (WHILE b DO c) x" by simp
    with s2' WhileTrue(5)[of x s2' t'] show "t x = t' x" by simp
  next
    case False
    hence "s x = s' x" using deps_unassigned_keep WhileTrue(6) by simp
    moreover
    from WhileTrue(1,2,4) have "(WHILE b DO c, s) => t" by blast (*Frage nach Benutzung von WhileTrue(1,2,4)*)
    hence "s x = t x" using unassigned_implies_equal False by simp
    moreover 
    have "s' x = t' x" using unassigned_implies_equal False WhileTrue(7) by simp
    ultimately show "t x = t' x" by simp
  qed
qed




lemma deps_sound:
  "[| (c, s) => t; s = s' on deps c x; (c, s')=> t' |]==> t x = t' x"
proof (induct arbitrary: x s' t'  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 (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 (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)*)
apply (metis If1)
sorry


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)*)
  sorry
  

     


next 
  case (Semi c1 s1 s2 c2 s3 x)
  thus ?case (*gerade diese Regel hab ich f�ür die einfachste gehalten*) 
    apply auto
(*by (metis Seq) *)
    
    sorry
next
  case (WhileTrue b s c s' t X)
  thus ?case (*rekursion!!*)

     sorry

qed






lemma deps_sound:
  "[| (c, s) => t; s = s' on deps c x; (c, s') => t'  |]
   ==> t x = t' x"
apply (induct)(*Indutkion �über  influences w�äre verlockend, funktioniert �über deps + auto*)
apply (metis Collect_def assigned.simps(1) deps_unassigned_keep skipE)(*deps SKIP geht automatisch*)
apply(blast)


apply(auto)(*deps->influence*)
apply(auto)(*2. subgoal*)
apply (metis Assign_same aval_eq_if_eq_on_vars)




apply (auto)