equal
deleted
inserted
replaced
399 ultimately have "supp x = A" |
399 ultimately have "supp x = A" |
400 by blast |
400 by blast |
401 } |
401 } |
402 ultimately show "supp x = A" by blast |
402 ultimately show "supp x = A" by blast |
403 qed |
403 qed |
404 |
|
405 |
404 |
406 lemma |
405 lemma |
407 "(supp x) ssupp x" |
406 "(supp x) ssupp x" |
408 unfolding ssupp_def |
407 unfolding ssupp_def |
409 apply(auto) |
408 apply(auto) |
413 apply(simp add: fresh_perm) |
412 apply(simp add: fresh_perm) |
414 apply(simp add: fresh_perm[symmetric]) |
413 apply(simp add: fresh_perm[symmetric]) |
415 (*Tzevelekos 2008, section 2.1.2 property 2.5*) |
414 (*Tzevelekos 2008, section 2.1.2 property 2.5*) |
416 oops |
415 oops |
417 |
416 |
|
417 (* The above is not true. Take p=(a\<leftrightarrow>b) and x={a,b}, then the goal is provably false *) |
|
418 lemma |
|
419 "b \<noteq> a \<Longrightarrow> \<not>(supp {a :: name,b}) ssupp {a,b}" |
|
420 unfolding ssupp_def |
|
421 apply (auto) |
|
422 apply (intro exI[of _ "(a\<leftrightarrow>b) :: perm"]) |
|
423 apply (subgoal_tac "(a \<leftrightarrow> b) \<bullet> {a, b} = {a, b}") |
|
424 apply simp |
|
425 apply (subgoal_tac "supp {a, b} = {atom a, atom b}") |
|
426 apply (simp add: flip_def) |
|
427 apply (simp add: supp_of_finite_insert supp_at_base supp_set_empty) |
|
428 apply blast |
|
429 by (smt empty_eqvt flip_at_simps(1) flip_at_simps(2) insert_commute insert_eqvt) |
418 |
430 |
419 function |
431 function |
420 qsubst :: "qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" ("_ [_ ::qq= _]" [90, 90, 90] 90) |
432 qsubst :: "qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" ("_ [_ ::qq= _]" [90, 90, 90] 90) |
421 where |
433 where |
422 "(QVar x)[y ::qq= s] = (if x = y then s else (QVar x))" |
434 "(QVar x)[y ::qq= s] = (if x = y then s else (QVar x))" |