diff -r 6d140b2c751f -r f7aca5601279 Nominal/Term5.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Term5.thy	Thu Feb 25 14:20:40 2010 +0100
@@ -0,0 +1,203 @@
+theory Term5
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+begin
+
+atom_decl name
+
+datatype rtrm5 =
+  rVr5 "name"
+| rAp5 "rtrm5" "rtrm5"
+| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
+and rlts =
+  rLnil
+| rLcons "name" "rtrm5" "rlts"
+
+primrec
+  rbv5
+where
+  "rbv5 rLnil = {}"
+| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
+
+
+setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Term5.rtrm5", "Term5.rlts"] *}
+print_theorems
+
+local_setup {* snd o define_fv_alpha "Term5.rtrm5" [
+  [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}
+print_theorems
+
+(* Alternate version with additional binding of name in rlts in rLcons *)
+(*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [
+  [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]]  ] *}
+print_theorems*)
+
+notation
+  alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
+  alpha_rlts ("_ \<approx>l _" [100, 100] 100)
+thm alpha_rtrm5_alpha_rlts.intros
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}
+thm alpha5_inj
+
+lemma rbv5_eqvt[eqvt]:
+  "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
+  apply (induct x)
+  apply (simp_all add: eqvts atom_eqvt)
+  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)"
+  apply (induct x and l)
+  apply (simp_all add: eqvts atom_eqvt)
+  done
+
+lemma alpha5_eqvt:
+  "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
+  "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
+  apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)
+  apply (simp_all add: alpha5_inj)
+  apply (tactic {* 
+    ALLGOALS (
+      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt})
+    ) *})
+  apply (simp_all only: eqvts atom_eqvt)
+  done
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),
+  (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *}
+thm alpha5_equivp
+
+quotient_type
+  trm5 = rtrm5 / alpha_rtrm5
+and
+  lts = rlts / alpha_rlts
+  by (auto intro: alpha5_equivp)
+
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
+ |> 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 ("bv5", @{term 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)"
+  apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
+  apply(simp_all add: alpha_gen)
+  done
+
+lemma bv_list_rsp:
+  shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
+  apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2))
+  apply(simp_all)
+  done
+
+lemma [quot_respect]:
+  "(alpha_rlts ===> op =) fv_rlts fv_rlts"
+  "(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"
+  "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"
+  "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
+  "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
+  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
+  apply (clarify) apply (rule conjI)
+  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+  done
+
+lemma
+  shows "(alpha_rlts ===> op =) rbv5 rbv5"
+  by (simp add: bv_list_rsp)
+
+lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
+
+instantiation trm5 and lts :: pt
+begin
+
+quotient_definition
+  "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
+is
+  "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
+
+quotient_definition
+  "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
+is
+  "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
+
+instance by default
+  (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted])
+
+end
+
+lemmas
+    permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
+and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+and bv5[simp] = rbv5.simps[quot_lifted]
+and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
+
+lemma lets_ok:
+  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+apply (subst alpha5_INJ)
+apply (rule conjI)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp only: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp only: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
+done
+
+lemma lets_ok2:
+  "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+   (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (subst alpha5_INJ)
+apply (rule conjI)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp only: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
+apply (rule_tac x="0 :: perm" in exI)
+apply (simp only: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
+done
+
+
+lemma lets_not_ok1:
+  "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(3) alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1))
+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)
+done
+
+
+end