equal
deleted
inserted
replaced
1405 apply (default) |
1405 apply (default) |
1406 apply (rule fset_finite_supp) |
1406 apply (rule fset_finite_supp) |
1407 done |
1407 done |
1408 |
1408 |
1409 |
1409 |
1410 section {* Fresh-Star *} |
1410 section {* Freshness and Fresh-Star *} |
1411 |
1411 |
|
1412 lemma fresh_Unit_elim: |
|
1413 shows "(a \<sharp> () \<Longrightarrow> PROP C) \<equiv> PROP C" |
|
1414 by (simp add: fresh_Unit) |
|
1415 |
|
1416 lemma fresh_Pair_elim: |
|
1417 shows "(a \<sharp> (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> a \<sharp> y \<Longrightarrow> PROP C)" |
|
1418 by rule (simp_all add: fresh_Pair) |
|
1419 |
|
1420 (* this rule needs to be added before the fresh_prodD is *) |
|
1421 (* added to the simplifier with mksimps *) |
|
1422 lemma [simp]: |
|
1423 shows "a \<sharp> x1 \<Longrightarrow> a \<sharp> x2 \<Longrightarrow> a \<sharp> (x1, x2)" |
|
1424 by (simp add: fresh_Pair) |
|
1425 |
|
1426 lemma fresh_PairD: |
|
1427 shows "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> x" |
|
1428 and "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> y" |
|
1429 by (simp_all add: fresh_Pair) |
|
1430 |
|
1431 ML {* |
|
1432 val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs; |
|
1433 *} |
|
1434 |
|
1435 declaration {* fn _ => |
|
1436 Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs)) |
|
1437 *} |
1412 |
1438 |
1413 text {* The fresh-star generalisation of fresh is used in strong |
1439 text {* The fresh-star generalisation of fresh is used in strong |
1414 induction principles. *} |
1440 induction principles. *} |
1415 |
1441 |
1416 definition |
1442 definition |
1471 |
1497 |
1472 lemma fresh_star_empty_elim: |
1498 lemma fresh_star_empty_elim: |
1473 "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C" |
1499 "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C" |
1474 by (simp add: fresh_star_def) |
1500 by (simp add: fresh_star_def) |
1475 |
1501 |
1476 lemma fresh_star_unit_elim: |
1502 lemma fresh_star_Unit_elim: |
1477 shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C" |
1503 shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C" |
1478 by (simp add: fresh_star_def fresh_Unit) |
1504 by (simp add: fresh_star_def fresh_Unit) |
1479 |
1505 |
1480 lemma fresh_star_Pair_elim: |
1506 lemma fresh_star_Pair_elim: |
1481 shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)" |
1507 shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)" |