equal
deleted
inserted
replaced
97 next |
97 next |
98 show "eqvt Numeral_graph" unfolding eqvt_def Numeral_graph_def |
98 show "eqvt Numeral_graph" unfolding eqvt_def Numeral_graph_def |
99 by (rule, perm_simp, rule) |
99 by (rule, perm_simp, rule) |
100 qed |
100 qed |
101 |
101 |
102 termination (eqvt) by lexicographic_order |
102 nominal_termination (eqvt) by lexicographic_order |
103 |
103 |
104 lemma supp_numeral[simp]: |
104 lemma supp_numeral[simp]: |
105 "supp \<lbrace>x\<rbrace> = supp x" |
105 "supp \<lbrace>x\<rbrace> = supp x" |
106 by (induct x rule: lam.induct) |
106 by (induct x rule: lam.induct) |
107 (simp_all add: lam.supp) |
107 (simp_all add: lam.supp) |
142 apply (subgoal_tac "eqvt app_lst") |
142 apply (subgoal_tac "eqvt app_lst") |
143 apply (erule fresh_fun_eqvt_app2) |
143 apply (erule fresh_fun_eqvt_app2) |
144 apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev) |
144 apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev) |
145 done |
145 done |
146 |
146 |
147 termination (eqvt) by lexicographic_order |
147 nominal_termination (eqvt) by lexicographic_order |
148 |
148 |
149 lemma ltgt_eq_iff[simp]: |
149 lemma ltgt_eq_iff[simp]: |
150 "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N" |
150 "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N" |
151 proof auto |
151 proof auto |
152 obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto |
152 obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto |