equal
deleted
inserted
replaced
1 (* CR_Takahashi from Nominal1 ported to Nominal2 *) |
1 (* CR_Takahashi from Nominal1 ported to Nominal2 *) |
2 theory CR imports Nominal2 begin |
2 theory CR |
|
3 imports "../Nominal2" |
|
4 begin |
3 |
5 |
4 atom_decl name |
6 atom_decl name |
5 |
7 |
6 nominal_datatype lam = |
8 nominal_datatype lam = |
7 Var "name" |
9 Var "name" |
83 inductive |
85 inductive |
84 beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80) |
86 beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80) |
85 where |
87 where |
86 bs1[intro, simp]: "M \<longrightarrow>b* M" |
88 bs1[intro, simp]: "M \<longrightarrow>b* M" |
87 | bs2[intro]: "\<lbrakk>M1\<longrightarrow>b* M2; M2 \<longrightarrow>b M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>b* M3" |
89 | bs2[intro]: "\<lbrakk>M1\<longrightarrow>b* M2; M2 \<longrightarrow>b M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>b* M3" |
|
90 |
|
91 equivariance beta_star |
88 |
92 |
89 lemma bs3[intro, trans]: |
93 lemma bs3[intro, trans]: |
90 assumes "A \<longrightarrow>b* B" |
94 assumes "A \<longrightarrow>b* B" |
91 and "B \<longrightarrow>b* C" |
95 and "B \<longrightarrow>b* C" |
92 shows "A \<longrightarrow>b* C" |
96 shows "A \<longrightarrow>b* C" |