diff -r 6542026b95cd -r c79d40b2128e Nominal/Term5.thy --- a/Nominal/Term5.thy Tue Mar 23 08:11:11 2010 +0100 +++ b/Nominal/Term5.thy Tue Mar 23 08:11:39 2010 +0100 @@ -71,22 +71,121 @@ "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" +apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *}) +done + +lemma alpha5_symp1: +"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> +(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> +(alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) -apply (simp only: alpha5_inj) -apply (simp add: alpha5_inj) +apply (simp_all add: alpha5_inj) apply (erule exE) -apply (simp only: alpha5_inj) apply (rule_tac x="- pi" in exI) -apply (erule alpha_gen_compose_sym2) -apply (simp_all add: alpha5_inj eqvts alpha5_eqvt) +apply (simp add: alpha_gen) + apply(simp add: fresh_star_def fresh_minus_perm) +apply clarify +apply (rule conjI) +apply (rotate_tac 3) +apply (frule_tac p="- pi" in alpha5_eqvt(2)) +apply simp +apply (rule conjI) +apply (rotate_tac 5) +apply (frule_tac p="- pi" in alpha5_eqvt(1)) +apply simp +apply (rotate_tac 6) +apply simp +apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) +apply (simp) +done + +thm alpha_gen_sym[no_vars] +thm alpha_gen_compose_sym[no_vars] + +lemma tt: + "\<lbrakk>R (- p \<bullet> x) y \<Longrightarrow> R (p \<bullet> y) x; (bs, x) \<approx>gen R f (- p) (cs, y)\<rbrakk> \<Longrightarrow> (cs, y) \<approx>gen R f p (bs, x)" + unfolding alphas + unfolding fresh_star_def + by (auto simp add: fresh_minus_perm) + +lemma alpha5_symp2: + shows "a \<approx>5 b \<Longrightarrow> b \<approx>5 a" + and "x \<approx>l y \<Longrightarrow> y \<approx>l x" + and "alpha_rbv5 x y \<Longrightarrow> alpha_rbv5 y x" +apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* binding case *) +apply(simp add: alpha5_inj) +apply(erule exE) +apply(rule_tac x="- pi" in exI) +apply(rule tt) +apply(simp add: alphas) +apply(erule conjE)+ +apply(drule_tac p="- pi" in alpha5_eqvt(2)) +apply(drule_tac p="- pi" in alpha5_eqvt(2)) +apply(drule_tac p="- pi" in alpha5_eqvt(1)) +apply(drule_tac p="- pi" in alpha5_eqvt(1)) +apply(simp) +apply(simp add: alphas) +apply(erule conjE)+ +apply metis +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) done lemma alpha5_transp: "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))" -apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *}) +(*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*) +apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) +apply (rule_tac [!] allI) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +defer +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) +(* HERE *) +(* +apply(rule alpha_gen_trans) +thm alpha_gen_trans +defer +apply (simp add: alpha_gen) +apply clarify +apply(simp add: fresh_star_plus) +apply (rule conjI) +apply (erule_tac x="- pi \<bullet> rltsaa" in allE) +apply (rotate_tac 5) +apply (drule_tac p="- pi" in alpha5_eqvt(2)) +apply simp +apply (drule_tac p="pi" in alpha5_eqvt(2)) +apply simp +apply (erule_tac x="- pi \<bullet> rtrm5aa" in allE) +apply (rotate_tac 7) +apply (drule_tac p="- pi" in alpha5_eqvt(1)) +apply simp +apply (rotate_tac 3) +apply (drule_tac p="pi" in alpha5_eqvt(1)) +apply simp done +*) +sorry lemma alpha5_equivp: "equivp alpha_rtrm5"