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/Terms.thy
changeset 1057 f81b506f62a7
parent 1056 a9135d300fbf
child 1058 afedef46d3ab
equal deleted inserted replaced
1056:a9135d300fbf 1057:f81b506f62a7 
   712 and
 
   712 and
 
   713   alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
 
   713   alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
 
   714 where
 
   714 where
 
   715   a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
 
   715   a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
 
   716 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
 
   716 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
 
   717 | a3: "\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
 
   717 | a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2)); 
   718              (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
 
   718         \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))\<rbrakk>
 
   719               (pi \<bullet> (rbv5 l1) = rbv5 l2))
 
       
   720         \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
 
   719         \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
 
   721 | a4: "rLnil \<approx>l rLnil"
 
   720 | a4: "rLnil \<approx>l rLnil"
 
   722 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
 
   721 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
 
   723 
   722 
   724 print_theorems
 
   723 print_theorems
 
   725 
   724 
   726 lemma alpha5_inj:
 
   725 lemma alpha5_inj:
 
   727   "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
 
   726   "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
 
   728   "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
 
   727   "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
 
   729   "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
 
   728   "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2))) \<and>
 
   730          (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
 
   729          (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))))"
 
   731          (pi \<bullet> (rbv5 l1) = rbv5 l2)))"
 
       
   732   "rLnil \<approx>l rLnil"
 
   730   "rLnil \<approx>l rLnil"
 
   733   "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)"
 
   731   "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
 
   734 apply -
 
   732 apply -
 
   735 apply (simp_all add: alpha5_alphalts.intros)
 
   733 apply (simp_all add: alpha5_alphalts.intros)
 
   736 apply rule
 
   734 apply rule
 
   737 apply (erule alpha5.cases)
 
   735 apply (erule alpha5.cases)
 
   738 apply (simp_all add: alpha5_alphalts.intros)
 
   736 apply (simp_all add: alpha5_alphalts.intros)
 
   801 lemma alpha5_rfv:
 
   799 lemma alpha5_rfv:
 
   802   "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
 
   800   "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
 
   803   "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
 
   801   "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
 
   804   apply(induct rule: alpha5_alphalts.inducts)
 
   802   apply(induct rule: alpha5_alphalts.inducts)
 
   805   apply(simp_all add: alpha_gen)
 
   803   apply(simp_all add: alpha_gen)
 
   806   apply(erule conjE)+
 
       
   807   apply(erule exE)
 
       
   808   apply(erule conjE)+
 
       
   809   apply simp
 
       
   810   done
 
   804   done
 
   811 
   805 
   812 lemma [quot_respect]:
 
   806 lemma [quot_respect]:
 
   813 "(op = ===> alpha5 ===> alpha5) permute permute"
 
   807 "(op = ===> alpha5 ===> alpha5) permute permute"
 
   814 "(op = ===> alphalts ===> alphalts) permute permute"
 
   808 "(op = ===> alphalts ===> alphalts) permute permute"
 
   826   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
 
   820   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
 
   827 apply(induct rule: alpha5_alphalts.inducts(2))
 
   821 apply(induct rule: alpha5_alphalts.inducts(2))
 
   828 apply(simp_all)
 
   822 apply(simp_all)
 
   829 done
 
   823 done
 
   830 
   824 
       
   825 
   831 lemma 
   826 lemma 
   832   shows "(alphalts ===> op =) rbv5 rbv5"
 
   827   shows "(alphalts ===> op =) rbv5 rbv5"
 
   833   by (simp add: bv_list_rsp)
 
   828   by (simp add: bv_list_rsp)
 
   834 
       
   835 
   829 
   836 instantiation trm5 and lts :: pt
 
   830 instantiation trm5 and lts :: pt
 
   837 begin
 
   831 begin
 
   838 
   832 
   839 quotient_definition
 
   833 quotient_definition
 
   873 
   867 
   874 lemma alpha5_INJ:
 
   868 lemma alpha5_INJ:
 
   875   "((Vr5 a) = (Vr5 b)) = (a = b)"
 
   869   "((Vr5 a) = (Vr5 b)) = (a = b)"
 
   876   "(Ap5 t1 s1 = Ap5 t2 s2) = (t1 = t2 \<and> s1 = s2)"
 
   870   "(Ap5 t1 s1 = Ap5 t2 s2) = (t1 = t2 \<and> s1 = s2)"
 
   877   "(Lt5 l1 t1 = Lt5 l2 t2) =
 
   871   "(Lt5 l1 t1 = Lt5 l2 t2) =
 
   878      (\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2) \<and>
 
   872      ((\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2))) \<and>
 
   879             (bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2) \<and>
 
   873       (\<exists>pi. ((bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2))))"
 
   880             (pi \<bullet> (bv5 l1) = bv5 l2)))"
 
       
   881   "Lnil = Lnil"
 
   874   "Lnil = Lnil"
 
   882   "(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (ls1 = ls2 \<and> t1 = t2 \<and> n1 = n2)"
 
   875   "(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (n1 = n2 \<and> ls1 = ls2 \<and> t1 = t2)"
 
   883 unfolding alpha_gen
 
   876 unfolding alpha_gen
 
   884 apply(lifting alpha5_inj[unfolded alpha_gen])
 
   877 apply(lifting alpha5_inj[unfolded alpha_gen])
 
   885 done
 
   878 done
 
   886 
   879 
   887 lemma bv5[simp]:
 
   880 lemma bv5[simp]:
 
   898 by (lifting rfv_trm5_rfv_lts.simps)
 
   891 by (lifting rfv_trm5_rfv_lts.simps)
 
   899 
   892 
   900 lemma lets_ok:
 
   893 lemma lets_ok:
 
   901   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
 
   894   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
 
   902 apply (subst alpha5_INJ)
 
   895 apply (subst alpha5_INJ)
 
       
   896 apply (rule conjI)
 
   903 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 
   897 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 
   904 apply (simp only: alpha_gen)
 
   898 apply (simp only: alpha_gen)
 
   905 apply (simp add: permute_trm5_lts fresh_star_def)
 
   899 apply (simp add: permute_trm5_lts fresh_star_def)
 
   906 apply (simp add: insert_eqvt eqvts atom_eqvt)
 
   900 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 
   907 done
 
   901 apply (simp only: alpha_gen)
 
   908 
   902 apply (simp add: permute_trm5_lts fresh_star_def)
 
   909 lemma lets_ok2:
 
   903 done
 
       
   904 
       
   905 lemma lets_not_ok1:
 
   910   "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
 
   906   "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
 
   911      (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 
   907              (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 
   912 apply (subst alpha5_INJ)
 
   908 apply (subst alpha5_INJ(3))
 
       
   909 apply(clarify)
 
   913 apply (simp add: alpha_gen)
 
   910 apply (simp add: alpha_gen)
 
   914 apply (simp add: permute_trm5_lts fresh_star_def)
 
   911 apply (simp add: permute_trm5_lts fresh_star_def)
 
   915 apply (rule allI)
 
   912 apply (simp add: alpha5_INJ(5))
 
   916 apply (subst alpha5_INJ)
 
   913 apply(clarify)
 
   917 apply (subst alpha5_INJ)
 
   914 apply (simp add: alpha5_INJ(2))
 
   918 apply (subst alpha5_INJ)
 
   915 apply (simp only: alpha5_INJ(1))
 
   919 apply (simp add: insert_eqvt eqvts atom_eqvt)
 
   916 done
 
   920 apply (subst alpha5_INJ(5))
 
   917 
   921 apply (subst alpha5_INJ)
 
   918 
   922 apply (subst alpha5_INJ(5))
 
   919 
   923 apply (subst alpha5_INJ)
 
   920 
   924 apply (rule impI)+
 
       
   925 apply (simp)
 
       
   926 done
 
       
   927 
   921 
   928 text {* type schemes *} 
   922 text {* type schemes *} 
   929 datatype ty = 
   923 datatype ty = 
   930   Var "name" 
   924   Var "name" 
   931 | Fun "ty" "ty"
 
   925 | Fun "ty" "ty"
nominal2