diff -r d1293d30c657 -r aa999d263b10 Nominal/Manual/Term5n.thy --- a/Nominal/Manual/Term5n.thy Fri Mar 26 17:22:17 2010 +0100 +++ b/Nominal/Manual/Term5n.thy Fri Mar 26 22:22:41 2010 +0100 @@ -1,5 +1,5 @@ theory Term5 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp" begin atom_decl name @@ -23,7 +23,7 @@ print_theorems local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") - [[[], [], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} + [[[], [], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [(0,NONE), (2,SOME @{term rbv5})]])] *} print_theorems notation @@ -31,7 +31,7 @@ alpha_rlts ("_ \<approx>l _" [100, 100] 100) thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_rel_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} thm alpha5_inj lemma rbv5_eqvt[eqvt]: @@ -65,13 +65,45 @@ "(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)" -sorry +apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) +apply (simp_all add: alpha5_inj) +apply (erule conjE)+ +apply (erule exE) +apply (rule_tac x="-pi" in exI) +apply (rule alpha_gen_sym) +apply (simp add: alphas) +apply (simp add: alpha5_eqvt) +apply (simp add: alphas) +apply clarify +apply simp +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))" -sorry +apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) +apply (rule_tac [!] allI) +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 {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (erule conjE)+ +apply (erule exE)+ +apply (rule_tac x="pi + pia" in exI) +apply (rule alpha_gen_trans) +prefer 6 +apply assumption +apply (simp_all add: alphas alpha5_eqvt) +apply (clarify) +apply simp +done lemma alpha5_equivp: "equivp alpha_rtrm5"