equal
deleted
inserted
replaced
69 |
69 |
70 lemma VAR_APP_Abs_eqvt[eqvt]: |
70 lemma VAR_APP_Abs_eqvt[eqvt]: |
71 "p \<bullet> VAR = VAR" "p \<bullet> APP = APP" "p \<bullet> Abs = Abs" |
71 "p \<bullet> VAR = VAR" "p \<bullet> APP = APP" "p \<bullet> Abs = Abs" |
72 by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def) |
72 by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def) |
73 |
73 |
74 nominal_primrec |
74 nominal_function |
75 Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000) |
75 Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000) |
76 where |
76 where |
77 "\<lbrace>Var x\<rbrace> = VAR \<cdot> (Var x)" |
77 "\<lbrace>Var x\<rbrace> = VAR \<cdot> (Var x)" |
78 | Ap: "\<lbrace>M \<cdot> N\<rbrace> = APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>" |
78 | Ap: "\<lbrace>M \<cdot> N\<rbrace> = APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>" |
79 | "\<lbrace>\<integral>x. M\<rbrace> = Abs \<cdot> (\<integral>x. \<lbrace>M\<rbrace>)" |
79 | "\<lbrace>\<integral>x. M\<rbrace> = Abs \<cdot> (\<integral>x. \<lbrace>M\<rbrace>)" |
126 by (induct M N rule: list_induct2') simp_all |
126 by (induct M N rule: list_induct2') simp_all |
127 |
127 |
128 lemma app_lst_rev_eq_iff: "app_lst n (rev M) = app_lst n (rev N) \<Longrightarrow> M = N" |
128 lemma app_lst_rev_eq_iff: "app_lst n (rev M) = app_lst n (rev N) \<Longrightarrow> M = N" |
129 by (drule app_lst_eq_iff) simp |
129 by (drule app_lst_eq_iff) simp |
130 |
130 |
131 nominal_primrec |
131 nominal_function |
132 Ltgt :: "lam list \<Rightarrow> lam" ("\<guillemotleft>_\<guillemotright>" 1000) |
132 Ltgt :: "lam list \<Rightarrow> lam" ("\<guillemotleft>_\<guillemotright>" 1000) |
133 where |
133 where |
134 [simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))" |
134 [simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))" |
135 unfolding eqvt_def Ltgt_graph_def |
135 unfolding eqvt_def Ltgt_graph_def |
136 apply (rule, perm_simp, rule, rule) |
136 apply (rule, perm_simp, rule, rule) |