296 text {*

   297   tests by cu

   298 *}

   299 

   300 

   301 lemma test3:

   302   fixes c::"'a::fs"

   303   assumes a: "y = Let2 x1 x2 trm1 trm2"

   304   and b: "\<forall>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<longrightarrow> P"

   305   shows "P"

   306 using b[simplified a]

   307 apply -

   308 apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)")

   309 apply(erule exE)

   310 apply(drule_tac p="- q" in permute_boolI)

   311 apply(perm_simp)

   312 apply(simp only: foo.eq_iff)

   313 apply(drule_tac x="x1" in spec)

   314 apply(drule_tac x="x2" in spec)

   315 apply(simp)

   316 apply(drule mp)

   317 apply(rule conjI)

   318 defer

   319 apply(rule_tac p="q" in permute_boolE)

   320 apply(perm_simp add: permute_minus_cancel)

   321 apply(rule conjI)

   322 prefer 2

   323 apply(rule_tac x="(atom x2 \<rightleftharpoons> atom (q \<bullet> x2)) \<bullet> trm2" in exI)

   324 apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])

   325 apply(simp)

   326 apply(simp add: fresh_star_def)

   327 apply(simp add: fresh_def supp_Pair)

   328 apply(simp)

   329 apply(case_tac "x1=x2")

   330 apply(simp)

   331 apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])

   332 apply(simp)

   333 apply(simp add: fresh_star_def)

   334 apply(simp add: fresh_def supp_Pair)

   335 apply(simp)

   336 apply(rule exI)

   337 apply(rule refl)

   338 apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])

   339 apply(simp)

   340 apply(simp add: fresh_star_def)

   341 apply(simp add: fresh_def supp_Pair)

   342 apply(simp)

   343 apply(simp add: flip_def[symmetric] atom_eqvt)

   344 apply(subgoal_tac "q \<bullet> x2 \<noteq> x1")

   345 apply(simp)

   346 apply(subst Abs_swap2[where a="atom x1" and b="atom (q \<bullet> x1)"])

   347 apply(simp)

   348 apply(subgoal_tac " atom (q \<bullet> x1) \<notin> supp ((x2 \<leftrightarrow> q \<bullet> x2) \<bullet> trm1)")

   349 apply(simp add: fresh_star_def)

   350 apply(simp add: fresh_star_def)

   351 apply(simp add: fresh_def supp_Pair)

   352 apply(erule conjE)+

   353 apply(rule_tac p="(x2 \<leftrightarrow> q \<bullet> x2)" in permute_boolE)

   354 apply(simp add: mem_eqvt Not_eqvt atom_eqvt supp_eqvt)

   355 apply(subgoal_tac "q \<bullet> x2 \<noteq> q \<bullet> x1")

   356 apply(subgoal_tac "x2 \<noteq> q \<bullet> x1")

   357 apply(simp)

   358 apply(simp add: supp_at_base)

   359 apply(simp)

   360 apply(simp)

   361 apply(rule exI)

   362 apply(rule refl)

   363 apply(simp add: fresh_star_def)

   364 apply(simp add: fresh_def supp_Pair)

   365 apply(simp add: supp_at_base)

   366 apply(simp)

   367 defer

   368 apply(rule_tac p="q" in permute_boolE)

   369 apply(perm_simp add: permute_minus_cancel fresh_star_prod)

   370 apply(simp)

   371 apply(rule at_set_avoiding3[where x="()", simplified])

   372 apply(simp)

   373 apply(simp add: finite_supp)

   374 apply(simp add: finite_supp)

   375 apply(simp add: fresh_star_def fresh_Unit)

   376 done

   377 

   378 lemma test4:

   379   fixes c::"'a::fs"

   380   assumes a: "y = Let2 x1 x2 trm1 trm2"

   381   and b: "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"

   382   shows "P"

   383 apply(rule test3)

   384 apply(rule a)

   385 using b

   386 apply(auto)

   387 done

   388 

   389