diff -r 5335c0ea743a -r 313e6f2cdd89 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Thu May 31 12:01:13 2012 +0100 +++ b/Nominal/Ex/Classical.thy Mon Jun 04 21:39:51 2012 +0100 @@ -83,21 +83,28 @@ apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) - apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) - apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) + apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq) + apply(clarify) + apply(simp add: eqvt_at_def) + apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq) apply(elim conjE) apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) - apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) - apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) + apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) + apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq) apply(elim conjE) apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -105,7 +112,9 @@ apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(rule conjI) apply(elim conjE) @@ -114,7 +123,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -124,7 +135,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -132,13 +145,17 @@ apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(elim conjE) apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(elim conjE) apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") @@ -146,7 +163,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -156,7 +175,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -167,7 +188,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -177,7 +200,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -189,7 +214,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -197,8 +224,11 @@ apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) + apply(simp add: eqvt_at_def) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -210,7 +240,9 @@ apply(simp add: Abs_fresh_star) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -254,19 +286,25 @@ apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(elim conjE) apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(elim conjE) apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(elim conjE) apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") @@ -274,7 +312,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -285,7 +325,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -294,7 +336,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -304,7 +348,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -314,7 +360,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -322,13 +370,17 @@ apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(elim conjE) apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(elim conjE) apply(rule conjI) @@ -337,7 +389,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -346,7 +400,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -355,7 +411,9 @@ apply(simp add: Abs_fresh_star) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(erule conjE)+ apply(rule conjI) @@ -364,7 +422,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast) @@ -373,7 +433,9 @@ apply(erule Abs_lst1_fcb2) apply(simp add: Abs_fresh_iff) apply(simp add: fresh_at_base fresh_star_def fresh_Pair) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) apply(blast) apply(blast)