nominal2: comparison Nominal/Term5.thy

equal deleted inserted replaced

-:1909be313353
+:1850361efb8f
 done
 lemma fv_rtrm5_rlts_eqvt[eqvt]:
 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
 "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
-"pi \<bullet> (fv_rbv5 l) = fv_rbv5 (pi \<bullet> l)"
 apply (induct x and l)
 apply (simp_all add: eqvts atom_eqvt)
 done
 (*lemma alpha5_eqvt:
 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
-|> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5}))
 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))
 |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))
 *}
 print_theorems
 lemma alpha5_rfv:
 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
-"(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))"
+"(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
-"(alpha_rbv5 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)"
+"(alpha_rbv5 b c \<Longrightarrow> True)"
 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
 apply(simp_all add: eqvts)
 apply(simp add: alpha_gen)
 apply(clarify)
 apply(simp)
-sorry
+done
 lemma bv_list_rsp:
 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
 apply(simp_all)
 apply(clarify)
 apply simp
 done
+local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
+print_theorems
+lemma alpha_rbv_rsp_pre:
+"x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z"
+apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+apply (simp_all add: alpha_dis alpha5_inj)
+apply clarify
+apply (case_tac [!] z)
+apply (simp_all add: alpha_dis alpha5_inj)
+apply clarify
+apply auto
+apply (meson alpha5_symp alpha5_transp)
+apply (meson alpha5_symp alpha5_transp)
+done
+lemma alpha_rbv_rsp_pre2:
+"x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y"
+apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+apply (simp_all add: alpha_dis alpha5_inj)
+apply clarify
+apply (case_tac [!] z)
+apply (simp_all add: alpha_dis alpha5_inj)
+apply clarify
+apply auto
+apply (meson alpha5_symp alpha5_transp)
+apply (meson alpha5_symp alpha5_transp)
+done
 lemma [quot_respect]:
 "(alpha_rlts ===> op =) fv_rlts fv_rlts"
-"(alpha_rlts ===> op =) fv_rbv5 fv_rbv5"
 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
 "(alpha_rlts ===> op =) rbv5 rbv5"
 "(op = ===> alpha_rtrm5) rVr5 rVr5"
 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"
 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
 apply (clarify)
 apply (rule_tac x="0" in exI)
 apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
 apply clarify
-apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+apply (simp add: alpha_rbv_rsp_pre2)
-apply simp_all
+apply (simp add: alpha_rbv_rsp_pre)
-apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+done
-apply simp_all
-defer defer (* Both sides false, so equal when we have distinct *)
-apply (erule conjE)+
-apply clarify
-apply (simp add: alpha5_inj)
-sorry (* may be true? *)
 lemma
 shows "(alpha_rlts ===> op =) rbv5 rbv5"
 by (simp add: bv_list_rsp)
 end
 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
 lemmas bv5[simp] = rbv5.simps[quot_lifted]
-lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted]
+lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
-lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted]
 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas alpha5_DIS = alpha_dis[quot_lifted]
 lemma lets_bla:
 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
 apply (simp only: alpha5_INJ)
 apply (simp only: bv5)
 thm alpha5_INJ
 apply (simp only: alpha5_INJ)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
-apply (metis flip_at_simps(1) supp_at_base supp_eqvt)
 done
 lemma lets_ok3:
 "x \<noteq> y \<Longrightarrow>
 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
 "x \<noteq> y \<Longrightarrow>
 (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 apply (simp add: alpha5_INJ alpha_gen)
 apply (simp add: permute_trm5_lts eqvts)
-apply (simp add: alpha5_INJ(5))
+apply (simp add: alpha5_INJ)
-apply (simp add: alpha5_INJ(1))
+done
-done
-lemma distinct_helper:
-shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
-apply auto
-apply (erule alpha_rtrm5.cases)
-apply (simp_all only: rtrm5.distinct)
-done
-lemma distinct_helper2:
-shows "(Vr5 x) \<noteq> (Ap5 y z)"
-by (lifting distinct_helper)
 lemma lets_nok:
 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
-apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts)
+apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts)
 done
 end

changeset 1464	1850361efb8f
parent 1462	7c59dd8e5435
child 1474	8a03753e0e02