diff -r 304dfe6cc83a -r a9f3600c9ae6 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Thu Jun 23 22:21:43 2011 +0100 +++ b/Nominal/Ex/Classical.thy Fri Jun 24 10:12:47 2011 +0900 @@ -46,6 +46,9 @@ thm trm.supp thm trm.supp[simplified] +lemma swap_at_base_sort: "sort_of (atom a) \ sort_of (atom x) \ sort_of (atom b) \ sort_of (atom x) \ (atom a \ atom b) \ x = x" + by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1)) + nominal_primrec (* (invariant "\(_, e, d) y. atom e \ y \ atom d \ y") *) crename :: "trm \ coname \ coname \ trm" ("_[_\c>_]" [100,100,100] 100) where @@ -74,45 +77,20 @@ -- "covered all cases" apply(case_tac x) apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) - apply(simp) - apply(blast) - apply(simp add: fresh_star_def) - apply(blast) - apply(simp add: fresh_star_def) - apply(blast) - apply(simp add: fresh_star_def) - apply(blast) - apply(simp add: fresh_star_def) - apply(blast) - apply(simp add: fresh_star_def) - apply(blast) - apply(simp add: fresh_star_def) - apply(blast) - apply(simp add: fresh_star_def) - apply(blast) - apply(simp add: fresh_star_def) - apply(blast) - apply(simp add: fresh_star_def) - apply(metis) - apply(simp add: fresh_star_def) - apply(metis) - apply(simp add: fresh_star_def) - apply(metis) + apply (simp_all add: fresh_star_def)[12] + apply(metis)+ -- "compatibility" apply(simp_all) apply(rule conjI) - apply(erule conjE)+ + apply(elim conjE) apply(erule Abs_lst1_fcb) apply(simp add: Abs_fresh_iff) apply(simp add: Abs_fresh_iff) apply(erule fresh_eqvt_at) apply(simp add: finite_supp) apply(simp add: fresh_Pair fresh_at_base(1)) - apply(drule sym) - apply(drule sym) - apply(drule sym) - apply(drule sym) - apply(simp add: eqvt_at_def swap_fresh_fresh) + apply(simp add: eqvt_at_def swap_at_base_sort) + apply simp oops end