theory Equivalence imports "../Nominal" XQuery begin (* Convergence *) inductive converges :: "ctx \ exp \ bool" ("_ \ _ \" [60,60] 60) where converges_intro : "\!! \ . \ : \ \ \ V. \ \ E \ V\ \ \ \ E \" lemma converges_elim: "\\ \ E \ ; \ : \\ \ \ V. \ \ E \ V" apply(erule converges.cases, auto) done lemma converges_weakening: "\\ \ E \; set \ \ set \'; valid \\ \ \' \ E \" apply(rule converges_intro) apply(frule valid_sub_restriction,assumption) apply(assumption) apply(clarsimp) apply(drule converges_elim) apply(assumption) apply(clarsimp) apply(rule_tac x="V" in exI) apply(erule eval_weakening) apply(simp_all add:ctx_wf_valid_sub) done (* Equivalence laws... *) inductive op_equiv :: "ctx \ exp \ exp \ bool" ("_ \ _ \ _" [60,60,60] 60) where op_equiv_intro: "\!!\ V. \ : \ \ \ \ E \ V \ \ \ E' \ V\ \ \ \ E \ E'" (* We can use the cons-nil presentation of the semantics to prove equivalence...*) lemma op_equiv2: "\!!\ V. \ : \ \ \ \2 E \ V \ \ \2 E' \ V\ \ \ \ E \ E'" apply(rule op_equiv_intro) apply(auto intro: eval_eval2 eval2_eval) done lemma op_equiv_elim: "\\ \ E \ E'; \ \ E \ V; \:\\ \ \ \ E' \ V" by (auto dest:op_equiv.cases) (* Equivalence is an equivalence relation... *) lemma op_equiv_refl: "\ \ E \ E" apply(auto intro:op_equiv_intro) done lemma op_equiv_symm: "\ \ E1 \ E2 \ \ \ E2 \ E1" apply(rule op_equiv_intro) apply(drule op_equiv.cases,auto) done lemma op_equiv_trans: "\\ \ E1 \ E2; \ \ E2 \ E3 \ \ \ \ E1 \ E3" apply(rule op_equiv_intro) apply(erule op_equiv.cases) apply(erule op_equiv.cases) apply(auto) done lemma seq_unit_l: "\ \ Seq Empty E \ E" apply(rule op_equiv_intro) apply(auto) apply(erule eval.cases,simp_all add:exp.inject,clarify) apply(erule eval.cases,simp_all) apply(subgoal_tac "\ \ Seq Empty E \ SeqV NilV V") apply(simp) apply(rule eval_seq) apply(rule eval_empty, erule ctx_wf_valid_sub,simp) done lemma seq_unit_r: "\ \ Seq E Empty \ E" apply(rule op_equiv_intro) apply(auto) apply(erule eval.cases,simp_all add:exp.inject,clarify) apply(erule_tac eval.cases)back apply(simp_all add: seqv_nil) apply(subgoal_tac "\ \ Seq E Empty \ SeqV V NilV") apply(simp add:seqv_nil) apply(erule eval_seq) apply(rule eval_empty, erule ctx_wf_valid_sub) done lemma seq_assoc: "\ \ Seq (Seq E1 E2) E3 \ Seq E1 (Seq E2 E3)" apply(rule op_equiv_intro) apply(auto) apply(erule eval.cases,simp_all add:exp.inject, clarify) apply(erule eval.cases,simp_all add:exp.inject, clarify) apply(subgoal_tac "\'' \ Seq E1 (Seq E2 E3) \ SeqV V1a (SeqV V2a V2)") prefer 2 apply(blast intro: eval_seq) apply(simp add: seqv_assoc) apply(erule eval.cases,simp_all add:exp.inject, clarify) apply(erule eval.cases,simp_all add:exp.inject, clarify) back apply(subgoal_tac "\'' \ Seq (Seq E1 E2) E3 \ SeqV (SeqV V1 V1a) V2a") prefer 2 apply(blast intro: eval_seq) apply(simp add:seqv_assoc) done lemma for_empty: "x \ \ \ \ \ For Empty x E \ Empty" apply(rule op_equiv_intro, auto) (* invert for derivation *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha) apply(clarsimp) apply(erule eval.cases, simp_all) apply(drule evals_nil_inv) apply(blast intro: eval_evals.intros) (* reverse direction *) apply(erule eval.cases, simp_all) apply(clarsimp) apply(rule eval_evals.intros) apply(rule eval_evals.intros,assumption) apply(rule eval_evals.intros,assumption) apply(simp add:fresh_prod) done lemma for_var: "\x \ (\,E); valid \\ \ \ \ For E x (Var x) \ E" apply(rule op_equiv_intro, auto) (* invert for derivation *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod) apply(clarsimp) apply(drule evals_var_id_inv,simp,simp) apply(erule eval_evals.intros) apply(rule evals_var_id,simp,simp) apply(simp add: ctx_wf_valid_valid_sub) apply(simp add:fresh_prod val_fresh) done lemma for_seq: "x \ (E1,E2,\) \ \ \ For (Seq E1 E2) x E \ Seq (For E1 x E) (For E2 x E)" apply(rule op_equiv_intro, auto) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod) apply(clarsimp) apply(erule eval.cases,simp_all add:exp.inject,clarify) apply(drule evals_seq_inv,clarify) apply(rule eval_evals.intros) apply(erule eval_evals.intros,simp, simp add:fresh_prod val_fresh) apply(erule eval_evals.intros,simp, simp add:fresh_prod val_fresh) (* reverse direction *) apply(erule eval.cases,simp_all add:exp.inject,clarify) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod) apply(clarsimp) apply(rule eval_evals.intros) apply(rule eval_evals.intros) apply(assumption) apply(assumption) apply(rule eval_evals.intros) apply(assumption) apply(assumption) apply(simp add:fresh_prod exp.fresh val_fresh) done lemma for_string: "x\ \ \ \ \ For (StringC s) x E \ Let (StringC s) x E" apply(rule op_equiv_intro, auto) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string) apply(clarify, erule eval_inv, simp add:exp.inject) apply(drule evals_sng_inv[simplified]) apply(rule eval_let, blast intro:eval_string) apply(simp, simp add:fresh_prod fresh_string val_fresh) (* reverse direction *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string) apply(clarify, erule eval_inv, simp add:exp.inject) apply(rule eval_for) apply(rule eval_string,assumption) apply(rule evals_sng) apply(simp) apply(simp_all add:fresh_prod val_fresh fresh_string) done lemma for_elem: "x\ (\,E') \ \ \ For (Elem l E') x E \ Let (Elem l E') x E" apply(rule op_equiv_intro, auto) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string) apply(clarify) apply(erule eval.cases, simp_all add: exp.inject,clarify) apply(drule evals_sng_inv[simplified]) apply(rule eval_let, blast intro:eval_elem) apply(simp, simp add:fresh_prod fresh_string val_fresh) (* reverse direction *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarify) apply(erule eval.cases, simp_all add:exp.inject, clarify) apply(rule eval_for) apply(erule eval_elem) apply(rule evals_sng) apply(simp) apply(simp_all add:fresh_prod val_fresh fresh_string) done lemma for_if: "\ x\ (\,E,E1,E2) \ \ \ \ For (Cond E E1 E2) x E3 \ Cond E (For E1 x E3) (For E2 x E3)" apply(rule op_equiv_intro, auto) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule eval.cases,simp_all add:exp.inject, clarify) apply(erule eval_cond1,simp) apply(erule eval_for,simp, simp add:fresh_prod val_fresh) apply(erule eval_cond2,simp) apply(erule eval_for,simp, simp add:fresh_prod val_fresh) (* reverse dir *) apply(erule eval.cases, simp_all add:exp.inject, clarify) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) back apply(rule eval_for) apply(erule eval_cond1,simp_all add:fresh_prod val_fresh) (* messy for some reason *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string exp.fresh) back apply(clarify, simp_all add:abs_fresh exp.inject) apply(clarify, simp add:exp.fresh abs_fresh exp.inject alpha) apply(clarify) apply(rule eval_for) apply(erule eval_cond2,simp_all add:fresh_prod val_fresh) done lemma for_let: "\ x1 \ (E1,E3,\); x2 \ (E1,E2,\); x1 \ x2\ \ \ \ For (Let E1 x1 E2) x2 E3 \ Let E1 x1 (For E2 x2 E3)" apply(rule op_equiv_intro, auto) apply(erule_tac x="x2" and xa="x2" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule_tac x="x1" and xa="x1" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule eval_evals.intros) apply(erule eval_evals.intros) apply(erule eval_weakening,simp_all add:fresh_prod fresh_list_cons val_fresh fresh_atm,fast) apply(rule valid_sub.intros) apply(drule ctx_wf_valid_sub,simp_all) (* \ *) apply(erule_tac x="x1" and xa="x1" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule_tac x="x2" and xa="x2" in eval.strong_cases, simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string fresh_list_cons fresh_atm, clarsimp) back apply(rule eval_evals.intros) apply(erule eval_evals.intros) apply(simp_all add:fresh_prod val_fresh abs_fresh) apply(erule eval_strengthening_cons, simp_all add:fresh_prod fresh_atm) done lemma for_for: "\ x1 \ (E1,E3,\); x2 \ (x1,E1,E2,\)\ \ \ \ For (For E1 x1 E2) x2 E3 \ For E1 x1 (For E2 x2 E3)" apply(rule op_equiv_intro, auto) (* \ *) apply(erule_tac x="x2" and xa="x2" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule_tac x="x1" and xa="x1" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule eval_for,simp_all add:fresh_prod val_fresh) apply(rule evals_for) apply(blast) apply( simp_all add: fresh_prod fresh_atm) (* \ *) apply(erule_tac x="x1" and xa="x1" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(drule evals_for_inv) apply(simp_all add:fresh_prod val_fresh abs_fresh fresh_atm) apply(clarify) apply(rule eval_for) apply(erule eval_for,assumption) apply(simp_all add:fresh_prod val_fresh abs_fresh fresh_atm) done (* This doesn't hold in both directions since we don't know that E1 evaluates to a value. We could make equivalence partial, so that if one side diverges on gamma then the expressions are trivially "equivalent" Since the language is terminating, this would be OK for now, but in general we don't want to allow rewrites that introduce nontermination. Alternatively we could consider directional equivalence of the form "if RHS terminates, then LHS terminates with the same value" - i.e. simulation. *) lemma let_fresh : "\\ \ E1 \ ; x \ (\,E1,E2)\ \ \ \ Let E1 x E2 \ E2" apply(rule op_equiv_intro) apply(auto) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod, clarsimp) apply (erule eval_strengthening_cons,simp add:fresh_prod) (* \ *) apply(drule converges_elim,simp,clarsimp) apply(erule eval_let) apply(erule eval_weakening) apply(auto , rule valid_sub.intros, erule ctx_wf_valid_sub,simp) apply(simp add:fresh_prod val_fresh) done (* TODO: Rules for hoisting "let" up to the toplevel *) lemma let_elem: "x \ (\,E1) \ \ \ Elem l (Let E1 x E2) \ Let E1 x (Elem l E2)" apply(rule op_equiv_intro) apply(auto) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval_evals.intros) apply(erule eval_evals.intros[simplified]) apply(simp add:fresh_prod fresh_string val_fresh) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) back apply(rule eval_evals.intros[simplified]) apply(erule eval_evals.intros) apply(simp_all add:fresh_prod val_fresh) done lemma let_seq1: "x \ (\,E,E2) \ \ \ Seq (Let E x E1) E2 \ Let E x (Seq E1 E2)" apply(rule op_equiv_intro) apply(auto) (* \ *) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(rule eval_evals.intros,assumption) apply(erule eval_evals.intros) apply(erule eval_weakening) apply(auto intro: valid_sub.intros ctx_wf_valid_sub)+ apply(simp add:fresh_prod fresh_string val_fresh) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) back apply(rule eval_evals.intros[simplified]) apply(erule eval_evals.intros) apply(assumption) apply(simp_all add:fresh_prod val_fresh) apply(erule eval_strengthening_cons) apply(simp add:fresh_prod fresh_string val_fresh) done lemma let_seq2: "x \ (\,E,E1) \ \ \ Seq E1 (Let E x E2) \ Let E x (Seq E1 E2)" apply(rule op_equiv_intro) apply(auto) (* \ *) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) back apply(rule eval_evals.intros,assumption) apply(rule eval_evals.intros) apply(erule eval_weakening) apply(auto intro: valid_sub.intros ctx_wf_valid_sub)+ apply(simp add:fresh_prod fresh_string val_fresh) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) back apply(rule eval_evals.intros[simplified]) apply(erule eval_strengthening_cons) apply(simp_all add:fresh_prod val_fresh) apply(erule eval_evals.intros) apply(assumption) apply(simp add:fresh_prod fresh_string val_fresh) done lemma let_cond : "x \ (\,E,E1,E2) \ \ \ Cond (Let E x E0) E1 E2 \ Let E x (Cond E0 E1 E2)" apply(rule op_equiv_intro) apply(auto) (* \ *) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) (* Case 1 *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(rule eval_evals.intros,assumption) apply(erule eval_evals.intros,assumption) apply(erule eval_weakening) apply(auto intro: valid_sub.intros ctx_wf_valid_sub)+ apply(simp add:fresh_prod fresh_string val_fresh) (* Case 2 *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval_evals.intros) apply(erule eval_evals.intros,assumption) apply(erule eval_weakening) apply(auto intro: valid_sub.intros ctx_wf_valid_sub)+ apply(simp add:fresh_prod fresh_string val_fresh) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) back (* case 1 *) apply(rule eval_evals.intros) apply(erule eval_evals.intros) apply(assumption) apply(simp_all add:fresh_prod val_fresh) apply(erule eval_strengthening_cons) apply(simp_all add:fresh_prod val_fresh) (* case 2 *) apply(clarsimp) apply(rule eval_cond2) apply(erule eval_evals.intros) apply(assumption) apply(simp add:fresh_prod fresh_string val_fresh) apply(assumption) apply(erule eval_strengthening_cons) apply(simp_all add:fresh_prod val_fresh) (* case 2 *) done lemma let_let: "\x1 \ (E1,E3,\); x2 \ (E1,E2,x1,\)\ \ \ \ Let (Let E1 x1 E2) x2 E3 \ Let E1 x1 (Let E2 x2 E3)" apply(rule op_equiv_intro, auto) apply(erule_tac x="x2" and xa="x2" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule_tac x="x1" and xa="x1" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule eval_evals.intros) apply(erule eval_evals.intros) apply(erule eval_weakening,simp_all add:fresh_prod fresh_list_cons val_fresh fresh_atm,fast) apply(rule valid_sub.intros)+ apply(drule ctx_wf_valid_sub,simp_all add:fresh_prod fresh_list_cons val_fresh fresh_atm) (* \ *) apply(erule_tac x="x1" and xa="x1" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule_tac x="x2" and xa="x2" in eval.strong_cases, simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string fresh_list_cons fresh_atm, clarsimp) back apply(rule eval_evals.intros) apply(erule eval_evals.intros) apply(simp_all add:fresh_prod val_fresh abs_fresh) apply(subgoal_tac "[(x2,V1a)] @ \' \ E3 \ V2a") apply(simp) apply(rule eval_strengthening(1)) apply(simp) apply(simp add:fresh_list_cons fresh_prod val_fresh fresh_atm fresh_list_nil) done lemma let_elem_lift: "x \ (\,E) \ \ \ Elem l E \ Let E x (Elem l (Var x))" apply(rule op_equiv_intro, auto) (* \ *) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) apply(erule eval_let) apply(rule eval_elem[simplified]) apply(rule eval_var,simp_all add:valid_sub.intros ctx_wf_valid_sub fresh_prod ctx_ty_fresh fresh_string val_fresh) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) back apply(erule eval.cases, simp_all add:exp.inject,clarsimp) back apply(auto dest:val_ctx_fresh_not_in simp add:ctx_ty_fresh) apply(erule eval_elem[simplified]) done lemma let_seq_lift: "\x \ (\,E1,E2);y\(\,E1,E2,x)\ \ \ \ Seq E1 E2 \ Let E1 x (Let E2 y (Seq (Var x) (Var y)))" apply(rule op_equiv_intro, auto) (* \ *) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) apply(erule eval_let) apply(rule eval_let) apply(erule eval_weakening) apply(auto) apply(auto intro:valid_sub.intros simp add: ctx_wf_valid_sub ctx_ty_fresh fresh_prod fresh_list_cons exp.fresh val_fresh) apply(rule eval_seq, rule eval_var) apply(auto) apply(rule valid_sub.intros)+ apply(erule ctx_wf_valid_sub) apply(simp add: ctx_ty_fresh fresh_prod fresh_list_cons exp.fresh val_fresh fresh_atm)+ apply(rule eval_var) apply(auto) apply(rule valid_sub.intros)+ apply(erule ctx_wf_valid_sub) apply(simp add: ctx_ty_fresh fresh_prod fresh_list_cons exp.fresh val_fresh fresh_atm)+ (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule_tac x="y" and xa="y" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod fresh_list_cons fresh_atm,clarsimp) back apply(erule eval.cases, simp_all add:exp.inject,clarsimp) back back apply(erule eval.cases, simp_all add:exp.inject,clarsimp) back back apply(erule eval.cases, simp_all add:exp.inject,clarsimp) back back apply(auto dest:val_ctx_fresh_not_in simp add:ctx_ty_fresh) apply(erule eval_seq) apply(erule eval_strengthening_cons) apply(simp add:fresh_prod) done lemma let_cond_lift: "\x \ (\,E,E1,E2)\ \ \ \ Cond E E1 E2 \ Let E x (Cond (Var x) E1 E2)" apply(rule op_equiv_intro, auto) apply(erule eval.cases, simp_all add:exp.inject,clarify) apply(subgoal_tac "x \ \'") apply(subgoal_tac "valid_sub ((x, Va) # \')") apply(erule eval_let) apply(rule eval_cond1) apply(rule_tac v="Va" in eval_var) apply(simp_all add: ctx_ty_fresh fresh_prod val_fresh) apply(erule eval_weakening) apply(auto) apply(rule v2, erule ctx_wf_valid_sub,simp) apply(subgoal_tac "x \ \'") apply(subgoal_tac "valid_sub ((x, Va) # \')") apply(erule eval_let) apply(rule eval_cond2) apply(rule_tac v="Va" in eval_var) apply(simp_all add: ctx_ty_fresh fresh_prod val_fresh) apply(erule eval_weakening) apply(auto) apply(rule v2, erule ctx_wf_valid_sub,simp) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval.cases, simp_all add: exp.inject, clarify) back apply(erule eval.cases, simp_all add:exp.inject, clarify) back apply(auto dest:val_ctx_fresh_not_in simp add:ctx_ty_fresh) apply(erule eval_cond1) apply(simp_all) apply(erule eval_strengthening_cons, simp add:fresh_prod) apply(erule eval.cases, simp_all add:exp.inject, clarify) back apply(auto dest:val_ctx_fresh_not_in simp add:ctx_ty_fresh) apply(erule eval_cond2) apply(simp_all) apply(erule eval_strengthening_cons, simp add:fresh_prod) done lemma let_for_lift: "\x \ (\,E1,E2);y \ (\,x,E1)\ \ \ \ For E1 y E2 \ Let E1 x (For (Var x) y E2)" apply(rule op_equiv_intro, auto) (* \ *) apply(erule_tac x="y" and xa="y" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(subgoal_tac "x \ \'") prefer 2 apply(simp add:ctx_ty_fresh fresh_prod val_fresh) apply(subgoal_tac "valid_sub ((x,V1)#\')") prefer 2 apply(rule v2, erule ctx_wf_valid_sub,simp) apply(erule eval_let, simp_all add: fresh_prod val_fresh) apply(rule eval_for, simp_all add: fresh_prod val_fresh fresh_list_cons) apply(rule_tac v="V1" in eval_var,simp_all) apply(erule eval_weakening, simp_all add: fresh_prod val_fresh fresh_list_cons) apply(fast) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string,clarsimp) apply(erule_tac x="y" and xa="y" in eval.strong_cases, simp_all add:abs_fresh val_fresh ctx_ty_fresh exp.inject alpha fresh_prod fresh_string fresh_list_cons fresh_atm, clarsimp) back apply(erule eval.cases, simp_all add: exp.inject, clarify) back apply(auto dest:val_ctx_fresh_not_in simp add:ctx_ty_fresh) apply(erule eval_for, simp_all add: fresh_prod val_fresh fresh_list_cons) apply(erule eval_strengthening_cons, simp add:fresh_prod fresh_atm) done lemma cond_empty: "\ \ Cond Empty E1 E2 \ E2" apply(rule op_equiv_intro) apply(auto) apply(erule eval.cases,simp_all add:exp.inject,clarsimp) apply(erule eval.cases,simp_all add:exp.inject,clarsimp) apply(subgoal_tac "emptyp NilV",simp, rule emptyp_empty) (* \ *) apply(blast intro: eval_evals.intros emptyp.intros eval_valid) done lemma cond_elem: "\ \ E \ \ \ \ Cond (Elem l E) E1 E2 \ E1" apply(rule op_equiv_intro) apply(auto) (* \ *) apply(erule eval.cases,simp_all add:exp.inject,clarsimp) apply(erule eval.cases,simp_all add:exp.inject,clarsimp) apply(drule nonempty_cons,simp) (* \ *) apply(drule converges_elim,assumption,clarify) apply(rule eval_evals.intros)+ apply(auto intro:nonempty_cons) done lemma cond_string: "\ \ Cond (StringC c) E1 E2 \ E1" apply(rule op_equiv_intro) apply(auto) apply(erule eval.cases,simp_all add:exp.inject,clarsimp) apply(erule eval.cases,simp_all add:exp.inject,clarsimp) apply(drule nonempty_cons,simp) (* \ *) apply(rule eval_evals.intros)+ apply(auto intro:nonempty_cons eval_valid) done lemma cond_seq: "\ \ E2 \ \ \ \ Cond (Seq E1 E2) E1' E2' \ Cond E1 E1' (Cond E2 E1' E2')" apply(rule op_equiv_intro) apply(auto) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) apply(erule eval.cases, simp_all add:exp.inject,clarsimp) apply(case_tac "V1a = NilV",clarsimp) apply(case_tac "V2 = NilV", clarsimp) apply(subgoal_tac "emptyp NilV", simp, rule emptyp_empty) apply(erule eval_cond2, rule emptyp_empty) apply(erule eval_cond1,assumption, assumption) apply(erule eval_cond1) apply(drule nonemptyp_append,clarsimp) apply(erule emptyp.cases,simp) apply(simp) apply(clarsimp) apply(erule eval.cases, simp_all add:exp.inject, clarsimp) apply(erule emptyp.cases,simp) apply(erule eval_cond2) apply(rule emptyp_empty) apply(erule eval_cond2, rule emptyp_empty, assumption) (* \ *) apply(erule eval.cases, simp_all add:exp.inject, clarsimp) (* Not quite true because E2 might diverge! *) apply(drule converges_elim,blast,clarsimp) apply(rule eval_cond1) apply(erule eval_seq,assumption) apply(erule nonemptyp_append1) apply(simp) apply(clarsimp) apply(erule eval.cases, simp_all add:exp.inject, clarsimp) back apply(rule eval_cond1) apply(erule eval_seq,assumption) apply(erule nonemptyp_append2) apply(simp) apply(clarsimp) apply(rule eval_cond2) apply(erule eval_seq,assumption) apply(erule emptyp.cases)+ apply(clarsimp, rule emptyp_empty) apply(assumption) done (* Congruence rules *) lemma elem_congr: "\ \ E1 \ E2 \ \ \ Elem l E1 \ Elem l E2" apply(rule op_equiv_intro) apply(erule op_equiv.cases) apply(auto) (* \ *) apply(erule eval.cases,simp_all add:exp.inject, clarsimp) apply(erule eval_evals.intros[simplified]) apply(erule eval.cases,simp_all add:exp.inject, clarsimp) apply(rule eval_evals.intros[simplified],clarsimp) done lemma seq_congr: "\\ \ E1 \ E1'; \ \ E2 \ E2'\ \ \ \ Seq E1 E2 \ Seq E1' E2'" apply(rule op_equiv_intro) apply(erule op_equiv.cases) apply(erule op_equiv.cases) apply(auto) (* \ *) apply(erule eval.cases,simp_all add:exp.inject, clarsimp) apply(erule eval_evals.intros[simplified],assumption) (* \ *) apply(erule eval.cases,simp_all add:exp.inject, clarsimp) apply(rule eval_evals.intros[simplified],clarsimp,blast) done lemma cond_congr: "\\ \ E \ E'; \ \ E1 \ E1'; \ \ E2 \ E2'\ \ \ \ Cond E E1 E2 \ Cond E' E1' E2'" apply(rule op_equiv_intro) apply(erule op_equiv.cases) apply(erule op_equiv.cases) apply(erule op_equiv.cases) apply(auto) (* \ *) apply(erule eval.cases,simp_all add:exp.inject, clarsimp) apply(blast intro: eval_cond1) apply(erule eval_cond2,assumption,assumption) (* \ *) apply(erule eval.cases,simp_all add:exp.inject, clarsimp) apply(blast intro: eval_cond1) apply(rule eval_cond2,blast,blast,blast) done lemma let_congr: "\\ \ E1 \ E1'; (x,StarTy (AtomTy AnyTy))#\ \ E2 \ E2'; x \ (\,E1,E1')\ \ \ \ Let E1 x E2 \ Let E1' x E2'" apply(rule op_equiv_intro) apply(erule op_equiv.cases) apply(erule op_equiv.cases) apply(auto) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval_let) apply(subgoal_tac "(x,V1) #\' : (x,StarTy(AtomTy(AnyTy)))#\") apply(blast) apply(auto simp add:fresh_prod val_fresh) apply(rule ctx_ty.intros,assumption) apply(rule any_tylist) apply(simp add:ctx_ty_fresh) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(rule eval_let) apply(simp) apply(subgoal_tac "(x,V1) #\' : (x,StarTy(AtomTy(AnyTy)))#\") apply(blast) apply(auto simp add:fresh_prod val_fresh) apply(rule ctx_ty.intros,assumption) apply(rule any_tylist) apply(simp add:ctx_ty_fresh) done lemma for_star_congr: "\(x,StarTy (AtomTy AnyTy))#\ \ E \ E'; \ : \; x \ \\ \ \,x\Vs \ E \* Vs' = \,x \ Vs \ E' \* Vs'" (* todo by induction on Vs *) apply(nominal_induct Vs arbitrary: Vs' \ rule: val_val_list.strong_inducts(2)) apply(simp) apply(auto) (* nil *) apply(frule evals_nil_inv, simp, rule evals_empty, erule eval_valid)+ (* cons \ *) apply(drule evals_cons_inv,clarsimp) apply(rule evals_cons,simp) apply(erule op_equiv_elim,simp) apply(blast intro: ctx_ty.intros intro: any_tylist) apply(assumption, simp add: ctx_ty_fresh) (* \ *) apply(drule evals_cons_inv,clarsimp) apply(rule evals_cons,simp) apply(drule op_equiv_symm) apply(erule op_equiv_elim,simp) apply(blast intro: ctx_ty.intros intro: any_tylist) apply(blast) apply(simp add: ctx_ty_fresh) done lemma for_congr: "\\ \ E1 \ E1'; (x,StarTy (AtomTy AnyTy))#\ \ E2 \ E2'; x \( \,E1,E1')\ \ \ \ For E1 x E2 \ For E1' x E2'" apply(rule op_equiv_intro) apply(erule op_equiv.cases) apply(erule op_equiv.cases) apply(auto) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval_for) apply(subgoal_tac "\',x\V1 \ E2 \* V2 = \',x\V1 \ E2' \* V2",simp) apply(rule for_star_congr) apply(erule op_equiv_intro) apply(assumption, simp_all add:ctx_ty_fresh fresh_prod val_fresh) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(rule eval_for) apply(simp) apply(subgoal_tac "\',x\V1 \ E2 \* V2 = \',x\V1 \ E2' \* V2",simp) apply(rule for_star_congr) apply(erule op_equiv_intro) apply(assumption, simp_all add:ctx_ty_fresh fresh_prod val_fresh) done (* Axis steps *) lemma self_id: "\ \ Step x Self NodeTest \ Var x" apply(rule op_equiv_intro) apply(auto) (* \ *) apply(erule eval.cases,simp_all add:exp.inject, clarsimp) apply(rule eval_var) apply(simp add:self_axis_id nodetest_id) apply(assumption) (* \ *) apply(erule eval.cases,simp_all add:exp.inject, clarsimp) apply(drule_tac ax="Self" and tst="NodeTest" in eval_step,assumption) apply(simp add:self_axis_id nodetest_id) done (* Let and substitution: soundness of inlining/CSE *) lemma let_var_id: "x \ (\,E) \ \ \ exp.Let E x (Var x) \ E" apply(rule op_equiv_intro) apply(auto) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval_inv, simp add:exp.inject) apply(auto dest:val_ctx_fresh_not_in simp add:ctx_ty_fresh) (*\ *) apply(erule eval_let) apply(rule eval_var) apply(simp_all add:fresh_prod val_fresh ctx_wf_valid_sub v2) done lemma let_over_cond: "x \ (E,\) \ \ \ Let E x (Cond E0 E1 E2) \ Cond (Let E x E0) (Let E x E1) (Let E x E2)" apply(rule op_equiv_intro) apply(auto) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval.cases, simp_all add:exp.inject, clarsimp) back apply(rule eval_cond1) apply(erule eval_let,simp_all add:fresh_prod val_fresh)+ apply(rule eval_cond2) apply(erule eval_let,simp_all add:fresh_prod val_fresh)+ (* \ *) apply(erule eval.cases, simp_all add:exp.inject, clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(subgoal_tac "V1a = V1b") prefer 2 apply(erule eval_det,assumption) apply(erule eval_valid) apply(clarsimp) apply(erule eval_let,simp_all add:fresh_prod val_fresh) apply(erule eval_cond1, simp_all) apply(clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod, clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(subgoal_tac "V1 = V1a") prefer 2 apply(erule eval_det,assumption) apply(erule eval_valid) apply(clarsimp) apply(erule eval_let,simp_all add:fresh_prod val_fresh) apply(erule eval_cond2, simp_all) done lemma let_over_seq: "x \ (E,\) \ \ \ Let E x (Seq E1 E2) \ Seq (Let E x E1) (Let E x E2)" apply(rule op_equiv_intro) apply(auto) (* \ *) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule eval.cases, simp_all add:exp.inject, clarsimp) back apply(rule eval_seq) apply(erule eval_let,assumption,simp_all add:fresh_prod val_fresh)+ (* \ *) apply(erule eval.cases, simp_all add:exp.inject, clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(subgoal_tac "V1 = V1a") prefer 2 apply(erule eval_det,assumption) apply(erule eval_valid) apply(erule eval_let,simp_all add:fresh_prod val_fresh) apply(erule eval_seq,assumption) done lemma let_over_let: "\x \ (E,\); y\(x,E1,E,\)\ \ \ \ Let E x (Let E1 y E2) \ Let (Let E x E1) y (Let E x E2)" apply(rule op_equiv_intro) apply(auto) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule_tac x="y" and xa="y" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod fresh_list_cons,clarsimp) back apply(rule eval_let) apply(rule eval_let) apply(assumption) apply(simp_all add:fresh_prod val_fresh) apply(rule eval_let) apply(rule eval_weakening,assumption) apply(clarsimp) apply(rule valid_sub.intros, erule eval_valid) apply(simp_all add:fresh_prod fresh_list_cons val_fresh fresh_atm abs_fresh) apply(erule eval_exchange) (* \ *) apply(erule_tac x="y" and xa="y" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod fresh_list_cons ,clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod fresh_list_cons ,clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod fresh_list_cons fresh_atm,clarsimp) apply(subgoal_tac "(y, V2a) # \ \ E \ V1a") prefer 2 apply(rule eval_weakening,assumption) apply(clarsimp) apply(rule valid_sub.intros, erule eval_valid,assumption) apply(subgoal_tac "V1 = V1a") prefer 2 apply(erule eval_det,assumption) apply(erule eval_valid) apply(clarsimp) apply(erule eval_let) apply(erule eval_let) apply(erule eval_exchange) apply(simp_all add:fresh_prod fresh_list_cons val_fresh fresh_atm) done lemma let_over_for: "\x \ (E,\); y\(x,E1,E,\)\ \ \ \ Let E x (For E1 y E2) \ For (Let E x E1) y (Let E x E2)" apply(rule op_equiv_intro) apply(auto) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod,clarsimp) apply(erule_tac x="y" and xa="y" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod fresh_list_cons,clarsimp) back apply(rule eval_for) apply(rule eval_let) apply(assumption) apply(assumption) apply(simp_all add:fresh_prod val_fresh abs_fresh) apply(erule evals_let,assumption) apply(simp add:fresh_prod)+ (* \ *) apply(erule_tac x="y" and xa="y" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod fresh_list_cons ,clarsimp) apply(erule_tac x="x" and xa="x" in eval.strong_cases,simp_all add: abs_fresh exp.inject alpha val_fresh ctx_ty_fresh fresh_prod fresh_list_cons fresh_atm ,clarsimp) apply(drule evals_let_inv,assumption) apply(simp add:fresh_prod fresh_atm)+ apply(erule eval_let) apply(erule eval_for) apply(assumption) apply(simp_all add:fresh_prod fresh_list_cons val_fresh fresh_atm) done lemma let_subst: "\\ \ E1 \ ; x \ (\,E1); valid \\ \ \ \ Let E1 x E2 \ E2[x::=E1]" apply(nominal_induct E2 avoiding: \ E1 E2 x rule:exp.strong_inducts) apply(auto) (* Var *) apply(erule let_var_id) apply(erule let_fresh, simp add:fresh_prod fresh_atm) (* String *) apply(erule let_fresh, simp add:fresh_prod fresh_atm fresh_string) (* Let *) apply(rule op_equiv_trans, rule let_over_let) apply(simp_all add:fresh_prod) apply(rule let_congr) apply(blast) apply(subgoal_tac "valid ((var,StarTy(AtomTy AnyTy))#\)") prefer 2 apply(erule valid.intros,assumption) apply(subgoal_tac "x \ ((var,StarTy(AtomTy AnyTy)) # \,E1)") prefer 2 apply(simp add:fresh_prod fresh_list_cons fresh_atm) apply(subgoal_tac "(var,StarTy(AtomTy AnyTy)) # \ \ E1 \") prefer 2 apply(erule converges_weakening,clarsimp,assumption) apply(clarsimp) apply(simp add:fresh_prod fresh_list_cons fresh_atm abs_fresh subst_fresh) (* Cond *) apply(rule op_equiv_trans, rule let_over_cond) apply(simp add:fresh_prod) apply(rule cond_congr) apply(blast+) (* Empty *) apply(erule let_fresh, simp add:fresh_prod fresh_atm fresh_string) (* Elem *) apply(rule op_equiv_trans, rule op_equiv_symm, rule let_elem) apply(simp add: fresh_prod) apply(rule elem_congr,blast) (* Seq *) apply(rule op_equiv_trans, rule let_over_seq) apply(simp add:fresh_prod) apply(rule seq_congr) apply(blast, blast) (* For *) apply(rule op_equiv_trans, rule let_over_for) apply(simp add:fresh_prod)+ apply(rule for_congr) apply(blast) apply(subgoal_tac "valid ((var,StarTy(AtomTy AnyTy))#\)") prefer 2 apply(erule valid.intros,assumption) apply(subgoal_tac "x \ ((var,StarTy(AtomTy AnyTy)) # \,E1)") prefer 2 apply(simp add:fresh_prod fresh_list_cons fresh_atm) apply(subgoal_tac "(var,StarTy(AtomTy AnyTy)) # \ \ E1 \") prefer 2 apply(erule converges_weakening,clarsimp,assumption) apply(clarsimp) apply(simp add:fresh_prod fresh_list_cons fresh_atm abs_fresh subst_fresh) (* Step case 1 *) apply(rule op_equiv_refl) (* Step case 2 *) apply(erule let_fresh, simp_all add:fresh_prod fresh_atm fresh_string axis_fresh test_fresh) done end