--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Term6.thy Thu Feb 25 14:14:08 2010 +0100
@@ -0,0 +1,155 @@
+theory Term6
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+begin
+
+atom_decl name
+
+(* example with a bn function defined over the type itself, NOT respectful. *)
+
+datatype rtrm6 =
+ rVr6 "name"
+| rLm6 "name" "rtrm6" --"bind name in rtrm6"
+| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
+
+primrec
+ rbv6
+where
+ "rbv6 (rVr6 n) = {}"
+| "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
+| "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
+
+setup {* snd o define_raw_perms ["rtrm6"] ["Term6.rtrm6"] *}
+print_theorems
+
+local_setup {* snd o define_fv_alpha "Term6.rtrm6" [
+ [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
+notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)
+thm alpha_rtrm6.intros
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *}
+thm alpha6_inj
+
+local_setup {*
+snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct})
+*}
+
+local_setup {*
+snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}
+*}
+
+local_setup {*
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []),
+ build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt))
+*}
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []),
+ (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *}
+thm alpha6_equivp
+
+quotient_type
+ trm6 = rtrm6 / alpha_rtrm6
+ by (auto intro: alpha6_equivp)
+
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6})))
+*}
+print_theorems
+
+lemma [quot_respect]:
+ "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute"
+by (auto simp add: alpha6_eqvt)
+
+(* Definitely not true , see lemma below *)
+lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6"
+apply simp apply clarify
+apply (erule alpha_rtrm6.induct)
+oops
+
+lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha_rtrm6 ===> op =) rbv6 rbv6"
+apply simp
+apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI)
+apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI)
+apply simp
+apply (simp add: alpha6_inj)
+apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
+apply (simp add: alpha_gen fresh_star_def)
+apply (simp add: alpha6_inj)
+done
+
+lemma fv6_rsp: "x \<approx>6 y \<Longrightarrow> fv_rtrm6 x = fv_rtrm6 y"
+apply (induct_tac x y rule: alpha_rtrm6.induct)
+apply simp_all
+apply (erule exE)
+apply (simp_all add: alpha_gen)
+done
+
+lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6"
+by (simp add: fv6_rsp)
+
+lemma [quot_respect]:
+ "(op = ===> alpha_rtrm6) rVr6 rVr6"
+ "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6"
+apply auto
+apply (simp_all add: alpha6_inj)
+apply (rule_tac x="0::perm" in exI)
+apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm)
+done
+
+lemma [quot_respect]:
+ "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6"
+apply auto
+apply (simp_all add: alpha6_inj)
+apply (rule_tac [!] x="0::perm" in exI)
+apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm)
+(* needs rbv6_rsp *)
+oops
+
+instantiation trm6 :: pt begin
+
+quotient_definition
+ "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"
+is
+ "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
+
+instance
+apply default
+sorry
+end
+
+lemma lifted_induct:
+"\<lbrakk>x1 = x2; \<And>name namea. name = namea \<Longrightarrow> P (Vr6 name) (Vr6 namea);
+ \<And>name rtrm6 namea rtrm6a.
+ \<lbrakk>True;
+ \<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and>
+ (fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk>
+ \<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a);
+ \<And>rtrm61 rtrm61a rtrm62 rtrm62a.
+ \<lbrakk>rtrm61 = rtrm61a; P rtrm61 rtrm61a;
+ \<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
+ (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk>
+ \<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk>
+\<Longrightarrow> P x1 x2"
+apply (lifting alpha_rtrm6.induct[unfolded alpha_gen])
+apply injection
+(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)
+oops
+
+lemma lifted_inject_a3:
+"(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) =
+(rtrm61 = rtrm61a \<and>
+ (\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
+ (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))"
+apply(lifting alpha6_inj(3)[unfolded alpha_gen])
+apply injection
+(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)
+oops
+
+
+
+
+end