Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Abs.thy
changeset 1351 cffc5d78ab7f
parent 1350 5b31e49678fc
child 1403 4a10338c2535
equal deleted inserted replaced
1350:5b31e49678fc 1351:cffc5d78ab7f 
   423 
   423 
   424 fun
 
   424 fun
 
   425   add_perm 
   425   add_perm 
   426 where
 
   426 where
 
   427   "add_perm [] = 0"
 
   427   "add_perm [] = 0"
 
   428 | "add_perm ((a,b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
 
   428 | "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
 
       
   429 
       
   430 fun
 
       
   431   elem_perm
 
       
   432 where
 
       
   433   "elem_perm [] = {}"
 
       
   434 | "elem_perm ((a, b) # xs) = {a, b} \<union> elem_perm xs"
 
       
   435 
   429 
   436 
   430 lemma add_perm_apend:
 
   437 lemma add_perm_apend:
 
   431   shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
 
   438   shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
 
   432 apply(induct xs arbitrary: ys)
 
   439 apply(induct xs arbitrary: ys)
 
   433 apply(auto simp add: add_assoc)
 
   440 apply(auto simp add: add_assoc)
 
   434 done
 
   441 done
 
   435 
   442 
   436 lemma
 
   443 lemma perm_list_exists:
 
   437   fixes p::perm
 
   444   fixes p::perm
 
   438   shows "\<exists>xs. p = add_perm xs"
 
   445   shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"
 
   439 apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)
 
   446 apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)
 
   440 apply(rename_tac p)
 
   447 apply(rename_tac p)
 
   441 apply(case_tac "supp p = {}")
 
   448 apply(case_tac "supp p = {}")
 
   442 apply(simp)
 
   449 apply(simp)
 
   443 apply(simp add: supp_perm)
 
   450 apply(simp add: supp_perm)
 
   444 apply(drule perm_zero)
 
   451 apply(drule perm_zero)
 
   445 apply(simp)
 
   452 apply(simp)
 
   446 apply(rule_tac x="[]" in exI)
 
   453 apply(rule_tac x="[]" in exI)
 
   447 apply(simp)
 
   454 apply(simp add: supp_Nil)
 
   448 apply(subgoal_tac "\<exists>x. x \<in> supp p")
 
   455 apply(subgoal_tac "\<exists>x. x \<in> supp p")
 
   449 defer
 
   456 defer
 
   450 apply(auto)[1]
 
   457 apply(auto)[1]
 
   451 apply(erule exE)
 
   458 apply(erule exE)
 
   452 apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)
 
   459 apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)
 
   453 apply(drule mp)
 
   460 apply(drule mp)
 
   454 defer
 
   461 defer
 
   455 apply(erule exE)
 
   462 apply(erule exE)
 
   456 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)
 
   463 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)
 
   457 apply(simp add: add_perm_apend)
 
   464 apply(simp add: add_perm_apend)
 
       
   465 apply(erule conjE)
 
   458 apply(drule sym)
 
   466 apply(drule sym)
 
   459 apply(simp)
 
   467 apply(simp)
 
   460 apply(simp add: expand_perm_eq)
 
   468 apply(simp add: expand_perm_eq)
 
       
   469 apply(simp add: supp_append)
 
       
   470 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)
 
       
   471 apply(rule conjI)
 
       
   472 prefer 2
 
       
   473 apply(auto)[1]
 
       
   474 apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))
 
       
   475 defer
 
   461 apply(rule psubset_card_mono)
 
   476 apply(rule psubset_card_mono)
 
   462 apply(simp add: finite_supp)
 
   477 apply(simp add: finite_supp)
 
   463 apply(rule psubsetI)
 
   478 apply(rule psubsetI)
 
   464 defer
 
   479 defer
 
   465 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")
 
   480 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")
 
   466 apply(blast)
 
   481 apply(blast)
 
   467 apply(simp add: supp_perm)
 
   482 apply(simp add: supp_perm)
 
   468 apply(auto simp add: supp_perm)
 
   483 defer
 
       
   484 apply(auto simp add: supp_perm)[1]
 
   469 apply(case_tac "x = xa")
 
   485 apply(case_tac "x = xa")
 
   470 apply(simp)
 
   486 apply(simp)
 
   471 apply(case_tac "((- p) \<bullet> x) = xa")
 
   487 apply(case_tac "((- p) \<bullet> x) = xa")
 
   472 apply(simp)
 
   488 apply(simp)
 
   473 apply(case_tac "sort_of xa = sort_of x")
 
   489 apply(case_tac "sort_of xa = sort_of x")
 
   474 apply(simp)
 
   490 apply(simp)
 
   475 apply(auto)[1]
 
   491 apply(auto)[1]
 
   476 apply(simp)
 
   492 apply(simp)
 
   477 apply(simp)
 
   493 apply(simp)
 
       
   494 apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")
 
       
   495 apply(blast)
 
       
   496 apply(auto simp add: supp_perm)[1]
 
       
   497 apply(case_tac "x = xa")
 
       
   498 apply(simp)
 
       
   499 apply(case_tac "((- p) \<bullet> x) = xa")
 
       
   500 apply(simp)
 
       
   501 apply(case_tac "sort_of xa = sort_of x")
 
       
   502 apply(simp)
 
       
   503 apply(auto)[1]
 
       
   504 apply(simp)
 
       
   505 apply(simp)
 
       
   506 done
 
       
   507 
       
   508 lemma tt0:
 
       
   509   fixes p::perm
 
       
   510   shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x"
 
       
   511 apply(auto simp add: fresh_star_def supp_perm fresh_def)
 
       
   512 done
 
       
   513 
       
   514 lemma uu0:
 
       
   515   shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x"
 
       
   516 apply(induct xs rule: add_perm.induct)
 
       
   517 apply(simp)
 
       
   518 apply(simp add: swap_fresh_fresh)
 
       
   519 done
 
       
   520 
       
   521 lemma yy0:
 
       
   522   fixes xs::"(atom \<times> atom) list"
 
       
   523   shows "supp xs = elem_perm xs"
 
       
   524 apply(induct xs rule: elem_perm.induct)
 
       
   525 apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom)
 
   478 done
 
   526 done
 
   479 
   527 
   480 lemma tt1:
 
   528 lemma tt1:
 
   481   shows "(supp x) \<sharp>* add_perm xs \<Longrightarrow> (add_perm xs) \<bullet> x = x"
 
   529   shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
 
   482 apply(induct xs rule: add_perm.induct)
 
   530 apply(drule tt0)
 
   483 apply(simp)
 
   531 apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p")
 
   484 apply(simp)
 
   532 prefer 2
 
   485 apply(case_tac "a = b")
 
   533 apply(rule perm_list_exists)
 
   486 apply(simp)
 
   534 apply(erule exE)
 
   487 apply(drule meta_mp)
 
   535 apply(simp only: yy0)
 
   488 defer
 
   536 apply(rule uu0)
 
   489 apply(simp)
 
   537 apply(auto)
 
   490 apply(rule swap_fresh_fresh)
 
   538 done
 
   491 apply(simp add: fresh_def)
 
       
   492 apply(auto)[1]
 
       
   493 apply(simp add: fresh_star_def fresh_def supp_perm)
 
       
   494 apply(drule_tac x="a" in bspec)
 
       
   495 apply(simp)
 
       
   496 oops
 
       
   497 
   539 
   498 
   540 
   499 lemma perm_induct_test:
 
   541 lemma perm_induct_test:
 
   500   fixes P :: "perm => bool"
 
   542   fixes P :: "perm => bool"
 
   501   assumes fin: "finite (supp p)" 
   543   assumes fin: "finite (supp p)" 
   510 apply(simp add: zero)
 
   552 apply(simp add: zero)
 
   511 apply(rotate_tac 3)
 
   553 apply(rotate_tac 3)
 
   512 sorry
 
   554 sorry
 
   513 
   555 
   514 
   556 
   515 
   557 (*
 
   516 lemma tt:
 
   558 lemma tt:
 
   517   "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
 
   559   "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
 
   518 apply(induct p rule: perm_induct_test)
 
   560 apply(induct p rule: perm_induct_test)
 
   519 apply(simp)
 
   561 apply(simp)
 
   520 apply(rule swap_fresh_fresh)
 
   562 apply(rule swap_fresh_fresh)
 
   537 apply(simp add: fresh_star_def fresh_def)
 
   579 apply(simp add: fresh_star_def fresh_def)
 
   538 apply(drule meta_mp)
 
   580 apply(drule meta_mp)
 
   539 apply(simp add: fresh_star_def fresh_def)
 
   581 apply(simp add: fresh_star_def fresh_def)
 
   540 apply(simp)
 
   582 apply(simp)
 
   541 done
 
   583 done
 
   542 
   584 *)
 
   543 lemma yy:
 
   585 lemma yy:
 
   544   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
 
   586   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
 
   545   shows "S1 = S2"
 
   587   shows "S1 = S2"
 
   546 using assms
 
   588 using assms
 
   547 apply (metis insert_Diff_single insert_absorb)
 
   589 apply (metis insert_Diff_single insert_absorb)
 
   554 using a
 
   596 using a
 
   555 apply(case_tac "a = b")
 
   597 apply(case_tac "a = b")
 
   556 apply(simp)
 
   598 apply(simp)
 
   557 oops
 
   599 oops
 
   558 
   600 
   559 *)
 
       
   560 
   601 
   561 fun
 
   602 fun
 
   562   distinct_perms 
   603   distinct_perms 
   563 where
 
   604 where
 
   564   "distinct_perms [] = True"
 
   605   "distinct_perms [] = True"
nominal2