theory hw8_template imports Big_Step Vars begin text {* Independence analysis *} instantiation com :: vars begin fun vars_com :: "com \ vname set" where "vars_com SKIP = {}" (* the other clauses for vars_com follow here *) instance .. end (* after this point, one can refer to the above function as vars *) lemma confinement: "(c,s) \ s' \ s = s' on (UNIV - vars c)" sorry lemma irrelevance: "\(c,s1) \ s1'; s1 = s2 on X; vars c \ X\ \ \ s2'. (c,s2) \ s2' \ s1' = s2' on X" (* proof (induction arbitrary: s2 rule: big_step_induct) *) sorry lemma independence_aux: assumes v: "vars c1 \ vars c2 = {}" and c12: "(c1 ; c2, s) \ s12" shows "(c2 ; c1, s) \ s12" sorry lemma independence: "vars c1 \ vars c2 = {} \ c1 ; c2 \ c2 ; c1" sorry (* extra credit development (if any) should come here *) text {* Fixed point reasoning *} lemma decomposition: "\ X. X = - (g ` (- (f ` X)))" sorry end