nominal2: comparison Quot/Nominal/Terms.thy

equal deleted inserted replaced

-:a94c04c4a720
+:6d2200603585
 "bv1 (BUnit) = {}"
 | "bv1 (BVr x) = {atom x}"
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
+thm permute_rtrm1_permute_bp.simps
 local_setup {*
 snd o define_fv_alpha "Terms.rtrm1"
 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
 [[], [[]], [[], []]]] *}
-print_theorems
 notation
 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
 alpha_bp ("_ \<approx>1b _" [100, 100] 100)
 thm alpha_rtrm1_alpha_bp.intros
 done
 lemma bv1_eqvt[eqvt]:
 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
 apply (induct x)
-apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts)
+apply (simp_all add: atom_eqvt eqvts)
 done
 lemma fv_rtrm1_eqvt[eqvt]:
 "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
 "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
 apply (induct t and b)
 print_theorems
 lemma alpha_rfv1:
 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
 apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1))
-apply(simp_all add: fv_rtrm1_fv_bp.simps alpha_gen.simps)
+apply(simp_all add: alpha_gen.simps)
 done
 lemma [quot_respect]:
 "(op = ===> alpha_rtrm1) rVr1 rVr1"
 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"
 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
 lemma trm5_lts_zero:
 "0 \<bullet> (x\<Colon>trm5) = x"
 "0 \<bullet> (y\<Colon>lts) = y"
 apply(induct x and y rule: trm5_lts_inducts)
 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
 done
 lemma trm5_lts_plus:
 "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
 "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
 apply(induct x and y rule: trm5_lts_inducts)
 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
 done
 instance
 apply default
 apply (simp_all add: trm5_lts_zero trm5_lts_plus)
 done
 end
-lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
+lemmas
+permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
-lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+and
+alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-lemmas bv5[simp] = rbv5.simps[quot_lifted]
+and
+bv5[simp] = rbv5.simps[quot_lifted]
-lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.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)
 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
 print_theorems
 local_setup {* snd o define_fv_alpha "Terms.rtrm6" [
 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *}
-notation alpha_rtrm6 ("_ \<approx>6a _" [100, 100] 100)
+notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)
 (* HERE THE RULES DIFFER *)
 thm alpha_rtrm6.intros
-inductive
+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)) *}
-alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
+thm alpha6_inj
-where
-a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)"
-| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha6 fv_rtrm6 pi ({atom b}, s))) \<Longrightarrow> rLm6 a t \<approx>6 rLm6 b s"
-| a3: "(\<exists>pi. (((rbv6 t1), s1) \<approx>gen alpha6 fv_rtrm6 pi ((rbv6 t2), s2))) \<Longrightarrow> rLt6 t1 s1 \<approx>6 rLt6 t2 s2"
 lemma alpha6_equivps:
 shows "equivp alpha6"
 sorry
 quotient_type
-trm6 = rtrm6 / alpha6
+trm6 = rtrm6 / alpha_rtrm6
 by (auto intro: alpha6_equivps)
 local_setup {*
 (fn ctxt => ctxt
 |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6}))
 |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6})))
 *}
 print_theorems
 lemma [quot_respect]:
-"(op = ===> alpha6 ===> alpha6) permute permute"
+"(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute"
 apply auto (* will work with eqvt *)
 sorry
 (* Definitely not true , see lemma below *)
-lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
+lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6"
 apply simp apply clarify
-apply (erule alpha6.induct)
+apply (erule alpha_rtrm6.induct)
 oops
-lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha6 ===> op =) rbv6 rbv6"
+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 (rule a2)
+apply (simp add: alpha6_inj)
 apply (rule_tac x="(a \<leftrightarrow> b)" in  exI)
 apply (simp add: alpha_gen fresh_star_def)
-apply (rule a1)
+apply (simp add: alpha6_inj)
-apply (rule refl)
+done
-done
+lemma fv6_rsp: "x \<approx>6 y \<Longrightarrow> fv_rtrm6 x = fv_rtrm6 y"
-lemma [quot_respect]:"(alpha6 ===> op =) fv_rtrm6 fv_rtrm6"
+apply (induct_tac x y rule: alpha_rtrm6.induct)
-apply simp apply clarify
-apply (induct_tac x y rule: alpha6.induct)
 apply simp_all
 apply (erule exE)
 apply (simp_all add: alpha_gen)
-apply (erule conjE)+
+done
-apply (erule exE)
-apply (erule conjE)+
+lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6"
-apply (simp)
+by (simp add: fv6_rsp)
-oops
-lemma [quot_respect]: "(op = ===> alpha6) rVr6 rVr6"
-by (simp_all add: a1)
 lemma [quot_respect]:
-"(op = ===> alpha6 ===> alpha6) rLm6 rLm6"
+"(op = ===> alpha_rtrm6) rVr6 rVr6"
-"(alpha6 ===> alpha6 ===> alpha6) rLt6 rLt6"
+"(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6"
-apply simp_all apply (clarify)
+apply auto
-apply (rule a2)
+apply (simp_all add: alpha6_inj)
 apply (rule_tac x="0::perm" in exI)
-apply (simp add: alpha_gen)
+apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm)
-(* needs rfv6_rsp *) defer
+done
-apply clarify
-apply (rule a3)
+lemma [quot_respect]:
-apply (rule_tac x="0::perm" in exI)
+"(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6"
-apply (simp add: alpha_gen)
+apply auto
+apply (simp_all add: alpha6_inj)
+apply (rule conjI)
+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
 apply default
 sorry
 end
 lemma lifted_induct:
-"\<lbrakk>x1 = x2; \<And>a b. a = b \<Longrightarrow> P (Vr6 a) (Vr6 b);
+"\<lbrakk>x1 = x2; \<And>name namea. name = namea \<Longrightarrow> P (Vr6 name) (Vr6 namea);
-\<And>a t b s.
+\<And>name rtrm6 namea rtrm6a.
-\<exists>pi. fv_trm6 t - {atom a} = fv_trm6 s - {atom b} \<and>
+\<lbrakk>True;
-(fv_trm6 t - {atom a}) \<sharp>* pi \<and> pi \<bullet> t = s \<and> P (pi \<bullet> t) s \<Longrightarrow>
+\<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and>
-P (Lm6 a t) (Lm6 b s);
+(fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk>
-\<And>t1 s1 t2 s2.
+\<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a);
-\<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
+\<And>rtrm61 rtrm61a rtrm62 rtrm62a.
-(fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<and> P (pi \<bullet> s1) s2 \<Longrightarrow>
+\<lbrakk>\<exists>pi. fv_trm6 rtrm61 - bv6 rtrm61 = fv_trm6 rtrm61a - bv6 rtrm61a \<and>
-P (Lt6 t1 s1) (Lt6 t2 s2)\<rbrakk>
+(fv_trm6 rtrm61 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm61 = rtrm61a \<and> P (pi \<bullet> rtrm61) rtrm61a;
-\<Longrightarrow> P x1 x2"
+\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
-unfolding alpha_gen
+(fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk>
-apply (lifting alpha6.induct[unfolded alpha_gen])
+\<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: (alpha6 ===> op =) rbv6 rbv6 *)
+(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)
 oops
 lemma lifted_inject_a3:
-"\<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
+"(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) =
-(fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<Longrightarrow> Lt6 t1 s1 = Lt6 t2 s2"
+((\<exists>pi. fv_trm6 rtrm61 - bv6 rtrm61 = fv_trm6 rtrm61a - bv6 rtrm61a \<and>
-apply(lifting a3[unfolded alpha_gen])
+(fv_trm6 rtrm61 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> 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: (alpha6 ===> op =) rbv6 rbv6 *)
+(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)
 oops
 "rbv7 (rVr7 n) = {atom n}"
 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
-print_theorems
+thm permute_rtrm7.simps
 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [
 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *}
 print_theorems
 notation

changeset 1201	6d2200603585
parent 1200	a94c04c4a720
child 1202	ab942ba2d243