Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Nominal/LamEx2.thy
changeset 1020 89ccda903f4a
parent 1019 d7b8c4243cd6
child 1021 bacf3584640e
equal deleted inserted replaced
1019:d7b8c4243cd6 1020:89ccda903f4a 
   233 apply(simp add: a1)
 
   233 apply(simp add: a1)
 
   234 apply(rotate_tac 4)
 
   234 apply(rotate_tac 4)
 
   235 apply(erule alpha.cases)
 
   235 apply(erule alpha.cases)
 
   236 apply(simp_all)
 
   236 apply(simp_all)
 
   237 apply(simp add: a2)
 
   237 apply(simp add: a2)
 
   238 apply(rotate_tac 1)
 
       
   239 apply(erule alpha.cases)
 
   238 apply(erule alpha.cases)
 
   240 apply(simp_all)
 
   239 apply(simp_all)
 
       
   240 apply(rule a3)
 
   241 apply(simp add: alpha_gen.simps)
 
   241 apply(simp add: alpha_gen.simps)
 
   242 apply(erule conjE)+
 
   242 apply(erule conjE)+
 
   243 apply(erule exE)+
 
   243 apply(erule exE)+
 
   244 apply(erule conjE)+
 
   244 apply(erule conjE)+
 
   245 apply(rule a3)
 
       
   246 apply(rule_tac x="pia + pi" in exI)
 
   245 apply(rule_tac x="pia + pi" in exI)
 
   247 apply(simp add: alpha_gen.simps)
 
       
   248 apply(simp add: fresh_star_plus)
 
   246 apply(simp add: fresh_star_plus)
 
   249 apply(drule_tac x="- pia \<bullet> sa" in spec)
 
   247 apply(drule_tac x="- pia \<bullet> sa" in spec)
 
   250 apply(drule mp)
 
   248 apply(drule mp)
 
   251 apply(rotate_tac 7)
 
   249 apply(rotate_tac 7)
 
   252 apply(drule_tac pi="- pia" in alpha_eqvt)
 
   250 apply(drule_tac pi="- pia" in alpha_eqvt)
 
   405 apply clarify
 
   403 apply clarify
 
   406 apply (rule alpha_gen_rsp_pre[of "alpha",OF alpha_eqvt])
 
   404 apply (rule alpha_gen_rsp_pre[of "alpha",OF alpha_eqvt])
 
   407 apply auto
 
   405 apply auto
 
   408 done
 
   406 done
 
   409 
   407 
       
   408 (*
 
   410 (* pi_abs would be also sufficient to prove the next lemma *)
 
   409 (* pi_abs would be also sufficient to prove the next lemma *)
 
   411 lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)"
 
   410 lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)"
 
   412 apply (unfold rep_lam_def)
 
   411 apply (unfold rep_lam_def)
 
   413 sorry
 
   412 sorry
 
   414 
   413 
   415 lemma [quot_preserve]: "(prod_fun id rep_lam --->
 
   414 lemma [quot_preserve]: "(prod_fun id rep_lam --->
 
   416            (abs_lam ---> abs_lam ---> id) ---> (abs_lam ---> id) ---> id ---> (prod_fun id rep_lam) ---> id)
 
   415            (abs_lam ---> abs_lam ---> id) ---> (abs_lam ---> id) ---> id ---> (prod_fun id rep_lam) ---> id)
 
   417            alpha_gen = alpha_gen"
 
   416            alpha_gen = alpha_gen"
 
   418 apply (simp add: expand_fun_eq)
 
   417 apply (simp add: expand_fun_eq alpha_gen.simps Quotient_abs_rep[OF Quotient_lam])
 
   419 apply (simp add: alpha_gen.simps)
 
       
   420 apply (simp add: replam_eqvt)
 
   418 apply (simp add: replam_eqvt)
 
   421 apply (simp only: Quotient_abs_rep[OF Quotient_lam])
 
   419 apply (simp only: Quotient_abs_rep[OF Quotient_lam])
 
   422 apply auto
 
   420 apply auto
 
   423 done
 
   421 done
 
       
   422 *)
 
   424 
   423 
   425 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)"
 
   424 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)"
 
   426 apply (simp add: expand_fun_eq)
 
   425 apply (simp add: expand_fun_eq)
 
   427 apply (simp add: Quotient_rel_rep[OF Quotient_lam])
 
   426 apply (simp add: Quotient_rel_rep[OF Quotient_lam])
 
   428 done
 
   427 done
 
   429 
   428 
   430 lemma a3:
 
   429 lemma a3:
 
   431   "\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s) \<Longrightarrow> Lam a t = Lam b s"
 
   430   "\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s) \<Longrightarrow> Lam a t = Lam b s"
 
   432   apply (lifting a3)
 
   431   apply (unfold alpha_gen)
 
       
   432   apply (lifting a3[unfolded alpha_gen])
 
   433   done
 
   433   done
 
   434 
   434 
   435 
   435 
   436 lemma a3_inv:
 
   436 lemma a3_inv:
 
   437   "Lam a t = Lam b s \<Longrightarrow> \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)"
 
   437   "Lam a t = Lam b s \<Longrightarrow> \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)"
 
   438 apply(lifting a3_inverse)
 
   438   apply (unfold alpha_gen)
 
   439 done
 
   439   apply (lifting a3_inverse[unfolded alpha_gen])
 
       
   440   done
 
   440 
   441 
   441 lemma alpha_cases: 
   442 lemma alpha_cases: 
   442   "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
 
   443   "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
 
   443     \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
 
   444     \<And>t1 t2 s1 s2. \<lbrakk>a1 = App t1 s1; a2 = App t2 s2; t1 = t2; s1 = s2\<rbrakk> \<Longrightarrow> P;
 
   444     \<And>a t b s. \<lbrakk>a1 = Lam a t; a2 = Lam b s; \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)\<rbrakk>
 
   445     \<And>a t b s. \<lbrakk>a1 = Lam a t; a2 = Lam b s; \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)\<rbrakk>
 
   445    \<Longrightarrow> P\<rbrakk>
 
   446    \<Longrightarrow> P\<rbrakk>
 
   446     \<Longrightarrow> P"
 
   447     \<Longrightarrow> P"
 
   447   by (lifting alpha.cases)
 
   448 unfolding alpha_gen
 
   448 
   449 apply (lifting alpha.cases[unfolded alpha_gen])
 
   449 thm alpha.induct
 
   450 done
 
   450 
   451 
   451 (* not sure whether needed *)
 
   452 (* not sure whether needed *)
 
   452 lemma alpha_induct: 
   453 lemma alpha_induct: 
   453   "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
 
   454   "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
 
   454     \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
 
   455     \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
 
   455  \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2 fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
 
   456  \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2 fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
 
   456     \<Longrightarrow> qxb qx qxa"
 
   457     \<Longrightarrow> qxb qx qxa"
 
   457   by (lifting alpha.induct)
 
   458 unfolding alpha_gen by (lifting alpha.induct[unfolded alpha_gen])
 
   458 
   459 
   459 (* should they lift automatically *)
 
   460 (* should they lift automatically *)
 
   460 lemma lam_inject [simp]: 
   461 lemma lam_inject [simp]: 
   461   shows "(Var a = Var b) = (a = b)"
 
   462   shows "(Var a = Var b) = (a = b)"
 
   462   and   "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
 
   463   and   "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
nominal2