nominal2: comparison Quot/Nominal/Terms.thy

equal deleted inserted replaced

-:8441b4b2469d
+:a69ec3f3f535
 shows   "P a rtrma"
 sorry
 section {*** lets with single assignments ***}
-datatype trm2 =
+datatype rtrm2 =
-Vr2 "name"
+rVr2 "name"
-| Ap2 "trm2" "trm2"
+| rAp2 "rtrm2" "rtrm2"
-| Lm2 "name" "trm2"
+| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"
-| Lt2 "assign" "trm2"
+| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"
-and assign =
+and rassign =
-As "name" "trm2"
+rAs "name" "rtrm2"
 (* to be given by the user *)
 primrec
-bv2
+rbv2
 where
-"bv2 (As x t) = {atom x}"
+"rbv2 (rAs x t) = {atom x}"
 (* needs to be calculated by the package *)
 primrec
-fv_trm2 and fv_assign
+fv_rtrm2 and fv_rassign
 where
-"fv_trm2 (Vr2 x) = {atom x}"
+"fv_rtrm2 (rVr2 x) = {atom x}"
-| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"
+| "fv_rtrm2 (rAp2 t1 t2) = (fv_rtrm2 t1) \<union> (fv_rtrm2 t2)"
-| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {atom x}"
+| "fv_rtrm2 (rLm2 x t) = (fv_rtrm2 t) - {atom x}"
-| "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"
+| "fv_rtrm2 (rLt2 as t) = (fv_rtrm2 t - rbv2 as) \<union> (fv_rassign as)"
-| "fv_assign (As x t) = (fv_trm2 t)"
+| "fv_rassign (rAs x t) = fv_rtrm2 t"
 (* needs to be stated by the package *)
 instantiation
-trm2 and assign :: pt
+rtrm2 and rassign :: pt
 begin
 primrec
-permute_trm2 and permute_assign
+permute_rtrm2 and permute_rassign
 where
-"permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
+"permute_rtrm2 pi (rVr2 a) = rVr2 (pi \<bullet> a)"
-| "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)"
+| "permute_rtrm2 pi (rAp2 t1 t2) = rAp2 (permute_rtrm2 pi t1) (permute_rtrm2 pi t2)"
-| "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)"
+| "permute_rtrm2 pi (rLm2 a t) = rLm2 (pi \<bullet> a) (permute_rtrm2 pi t)"
-| "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)"
+| "permute_rtrm2 pi (rLt2 as t) = rLt2 (permute_rassign pi as) (permute_rtrm2 pi t)"
-| "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)"
+| "permute_rassign pi (rAs a t) = rAs (pi \<bullet> a) (permute_rtrm2 pi t)"
-lemma pt_trm2_assign_zero:
+lemma pt_rtrm2_rassign_zero:
-fixes t::trm2
+fixes t::rtrm2
-and   b::assign
+and   b::rassign
 shows "0 \<bullet> t = t"
 and   "0 \<bullet> b = b"
-apply(induct t and b rule: trm2_assign.inducts)
+apply(induct t and b rule: rtrm2_rassign.inducts)
 apply(simp_all)
 done
-lemma pt_trm2_assign_plus:
+lemma pt_rtrm2_rassign_plus:
-fixes t::trm2
+fixes t::rtrm2
-and   b::assign
+and   b::rassign
 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
 and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
-apply(induct t and b rule: trm2_assign.inducts)
+apply(induct t and b rule: rtrm2_rassign.inducts)
 apply(simp_all)
 done
 instance
 apply default
-apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus)
+apply(simp_all add: pt_rtrm2_rassign_zero pt_rtrm2_rassign_plus)
 done
 end
 inductive
-alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
-where
+and
-a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"
+alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)
-| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"
+where
-| a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and>
+a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"
-(fv_trm2 t - {atom a})\<sharp>* pi \<and>
+| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"
-(pi \<bullet> t) \<approx>2 s \<and>
+| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"
-(pi \<bullet> a) = b)
+| a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s));
-\<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"
+\<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk>
-| a4: "\<exists>pi. (
+\<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
-fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>
+| a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *)
-(fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and>
-pi \<bullet> t1 = t2       (* \<and> (pi \<bullet> b1 = b2) *)
+lemma alpha2_equivp:
-) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2"
+"equivp alpha2"
+"equivp alpha2a"
-lemma alpha2_equivp: "equivp alpha2"
 sorry
-quotient_type qtrm2 = trm2 / alpha2
+quotient_type
-by (rule alpha2_equivp)
+trm2 = rtrm2 / alpha2
+and
+assign = rassign / alpha2a
+by (auto intro: alpha2_equivp)
 section {*** lets with many assignments ***}
 datatype trm3 =
 Vr3 "name"
 | Ap3 "trm3" "trm3"
-| Lm3 "name" "trm3"
+| Lm3 "name" "trm3" --"bind (name) in (trm3)"
-| Lt3 "assigns" "trm3"
+| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"
 and assigns =
 ANil
 | ACons "name" "trm3" "assigns"
 (* to be given by the user *)
 end
 inductive
 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
+and
+alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100)
 where
 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
-| a3: "\<exists>pi. (fv_trm3 t - {atom a} = fv_trm3 s - {atom b} \<and>
+| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
-(fv_trm3 t - {atom a})\<sharp>* pi \<and>
+| a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s));
-(pi \<bullet> t) \<approx>3 s \<and>
+\<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk>
-(pi \<bullet> a) = b)
+\<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s"
-\<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
+| a5: "ANil \<approx>3a ANil"
-| a4: "\<exists>pi. (
+| a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st"
-fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and>
-(fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and>
+lemma alpha3_equivp:
-pi \<bullet> t1 = t2      (* \<and> (pi \<bullet> b1 = b2)  *)
+"equivp alpha3"
-) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2"
+"equivp alpha3a"
-lemma alpha3_equivp: "equivp alpha3"
 sorry
-quotient_type qtrm3 = trm3 / alpha3
+quotient_type
-by (rule alpha3_equivp)
+qtrm3 = trm3 / alpha3
+and
+qassigns = assigns / alpha3a
+by (auto intro: alpha3_equivp)
 section {*** lam with indirect list recursion ***}
 datatype trm4 =
 Vr4 "name"
 | Ap4 "trm4" "trm4 list"
-| Lm4 "name" "trm4"
+| Lm4 "name" "trm4"  --"bind (name) in (trm)"
 thm trm4.recs
 primrec
 fv_trm4 and fv_trm4_list
 | "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
 (* needs to be stated by the package *)
 (* there cannot be a clause for lists, as *)
-(* permuteutations are  already defined in Nominal (also functions, options, and so on) *)
+(* permutations are  already defined in Nominal (also functions, options, and so on) *)
 instantiation
 trm4 :: pt
 begin
 (* does not work yet *)
 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)
 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100)
 where
 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"
 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
-| a4: "\<exists>pi. (fv_trm4 t - {atom a} = fv_trm4 s - {atom b} \<and>
+| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
-(fv_trm4 t - {atom a})\<sharp>* pi \<and>
-(pi \<bullet> t) \<approx>4 s \<and>
-(pi \<bullet> a) = b)
-\<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
 | a5: "[] \<approx>4list []"
 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"
 lemma alpha4_equivp: "equivp alpha4" sorry
 lemma alpha4list_equivp: "equivp alpha4list" sorry
 datatype rtrm5 =
 rVr5 "name"
 | rAp5 "rtrm5" "rtrm5"
-| rLt5 "rlts" "rtrm5"
+| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
 and rlts =
 rLnil
 | rLcons "name" "rtrm5" "rlts"
 primrec
 quotient_definition
 "bv5 :: lts \<Rightarrow> atom set"
 as
 "rbv5"
+lemma rbv5_eqvt:
+"pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
+sorry
+lemma rfv_trm5_eqvt:
+"pi \<bullet> (rfv_trm5 x) = rfv_trm5 (pi \<bullet> x)"
+sorry
+lemma rfv_lts_eqvt:
+"pi \<bullet> (rfv_lts x) = rfv_lts (pi \<bullet> x)"
+sorry
+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: alpha5_alphalts.inducts)
+apply (simp_all add: alpha5_inj)
+apply (erule exE)+
+apply(unfold alpha_gen)
+apply (erule conjE)+
+apply (rule conjI)
+apply (rule_tac x="x \<bullet> pi" in exI)
+apply (rule conjI)
+apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
+apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt)
+apply(rule conjI)
+apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
+apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt)
+apply (subst permute_eqvt[symmetric])
+apply (simp)
+apply (rule_tac x="x \<bullet> pia" in exI)
+apply (rule conjI)
+apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
+apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt)
+apply(rule conjI)
+apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
+apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt)
+apply (subst permute_eqvt[symmetric])
+apply (simp)
+done
 lemma alpha5_rfv:
 "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
 "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
 apply(induct rule: alpha5_alphalts.inducts)
 apply(simp_all add: alpha_gen)
 done
-lemma [quot_respect]:
-"(op = ===> alpha5 ===> alpha5) permute permute"
-"(op = ===> alphalts ===> alphalts) permute permute"
-"(op = ===> alpha5) rVr5 rVr5"
-"(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
-"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
-"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
-"(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
-"(alpha5 ===> op =) rfv_trm5 rfv_trm5"
-"(alphalts ===> op =) rfv_lts rfv_lts"
-"(alphalts ===> op =) rbv5 rbv5"
-sorry
 lemma bv_list_rsp:
 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
 apply(induct rule: alpha5_alphalts.inducts(2))
 apply(simp_all)
 done
+lemma [quot_respect]:
-lemma
+"(alphalts ===> op =) rfv_lts rfv_lts"
+"(alpha5 ===> op =) rfv_trm5 rfv_trm5"
+"(alphalts ===> op =) rbv5 rbv5"
+"(op = ===> alpha5) rVr5 rVr5"
+"(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
+"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+"(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
+"(op = ===> alpha5 ===> alpha5) permute permute"
+"(op = ===> alphalts ===> alphalts) permute permute"
+apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
+apply (auto)
+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)
+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 "(alphalts ===> op =) rbv5 rbv5"
 by (simp add: bv_list_rsp)
 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]

changeset 1096	a69ec3f3f535
parent 1093	139b257e10d2
child 1103	7e691b3c2414