# HG changeset patch # User Cezary Kaliszyk # Date 1306814061 -32400 # Node ID 5d0875b7ed3e188ba32a1a1b88e694b676f7e5ee # Parent d2154b4217073aac70f7cec5d4aa34b8c25a8901 Simple eqvt proofs with perm_simps for clarity diff -r d2154b421707 -r 5d0875b7ed3e Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue May 31 00:36:16 2011 +0100 +++ b/Nominal/Ex/Lambda.thy Tue May 31 12:54:21 2011 +0900 @@ -75,37 +75,12 @@ "height (Var x) = 1" | "height (App t1 t2) = max (height t1) (height t2) + 1" | "height (Lam [x].t) = height t + 1" -defer + unfolding eqvt_def height_graph_def + apply (rule, perm_simp, rule) apply(rule_tac y="x" in lam.exhaust) apply(auto simp add: lam.distinct lam.eq_iff) apply (erule Abs1_eq_fdest) apply(simp_all add: fresh_def pure_supp eqvt_at_def) -apply(subgoal_tac "\p x r. height_graph x r \ height_graph (p \ x) (p \ r)") -unfolding eqvt_def -apply(rule allI) -apply(simp add: permute_fun_def) -apply(rule ext) -apply(rule ext) -apply(simp add: permute_bool_def) -apply(rule iffI) -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="- p \ x" in meta_spec) -apply(drule_tac x="- p \ xa" in meta_spec) -apply(simp) -apply(drule_tac x="-p" in meta_spec) -apply(drule_tac x="x" in meta_spec) -apply(drule_tac x="xa" in meta_spec) -apply(simp) -apply(erule height_graph.induct) -apply(perm_simp) -apply(rule height_graph.intros) -apply(perm_simp) -apply(rule height_graph.intros) -apply(assumption) -apply(assumption) -apply(perm_simp) -apply(rule height_graph.intros) -apply(assumption) done termination @@ -122,7 +97,8 @@ "frees_lst (Var x) = [atom x]" | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" -defer + unfolding eqvt_def frees_lst_graph_def + apply (rule, perm_simp, rule) apply(rule_tac y="x" in lam.exhaust) apply(simp_all)[3] apply(auto)[1] @@ -132,32 +108,6 @@ apply(drule supp_eqvt_at) apply(simp add: finite_supp) apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) -apply(subgoal_tac "\p x r. frees_lst_graph x r \ frees_lst_graph (p \ x) (p \ r)") -unfolding eqvt_def -apply(rule allI) -apply(simp add: permute_fun_def) -apply(rule ext) -apply(rule ext) -apply(simp add: permute_bool_def) -apply(rule iffI) -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="- p \ x" in meta_spec) -apply(drule_tac x="- p \ xa" in meta_spec) -apply(simp) -apply(drule_tac x="-p" in meta_spec) -apply(drule_tac x="x" in meta_spec) -apply(drule_tac x="xa" in meta_spec) -apply(simp) -apply(erule frees_lst_graph.induct) -apply(perm_simp) -apply(rule frees_lst_graph.intros) -apply(perm_simp) -apply(rule frees_lst_graph.intros) -apply(assumption) -apply(assumption) -apply(perm_simp) -apply(rule frees_lst_graph.intros) -apply(assumption) done termination @@ -180,7 +130,8 @@ "(Var x)[y ::= s] = (if x = y then s else (Var x))" | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" | "atom x \ (y, s) \ (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" -defer + unfolding eqvt_def subst_graph_def + apply (rule, perm_simp, rule) apply(auto simp add: lam.distinct lam.eq_iff) apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) apply(blast)+ @@ -193,33 +144,6 @@ apply(subgoal_tac "(atom x \ atom xa) \ ya = ya") apply(simp add: eqvt_at_def) apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ -apply(subgoal_tac "\p x r. subst_graph x r \ subst_graph (p \ x) (p \ r)") -unfolding eqvt_def -apply(rule allI) -apply(simp add: permute_fun_def) -apply(rule ext) -apply(rule ext) -apply(simp add: permute_bool_def) -apply(rule iffI) -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="- p \ x" in meta_spec) -apply(drule_tac x="- p \ xa" in meta_spec) -apply(simp) -apply(drule_tac x="-p" in meta_spec) -apply(drule_tac x="x" in meta_spec) -apply(drule_tac x="xa" in meta_spec) -apply(simp) -apply(erule subst_graph.induct) -apply(perm_simp) -apply(rule subst_graph.intros) -apply(perm_simp) -apply(rule subst_graph.intros) -apply(assumption) -apply(assumption) -apply(perm_simp) -apply(rule subst_graph.intros) -apply(simp add: fresh_Pair) -apply(assumption) done termination @@ -374,7 +298,8 @@ "trans (Var x) xs = lookup xs 0 x" | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" | "atom x \ xs \ trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" -defer + unfolding eqvt_def trans_graph_def + apply (rule, perm_simp, rule) apply(case_tac x) apply(simp) apply(rule_tac y="a" and c="b" in lam.strong_exhaust)