author urbanc Sun, 27 Nov 2005 05:00:43 +0100 changeset 18264 3b808e24667b parent 18263 7f75925498da child 18265 f3f81becc1f1
added the version of nominal.thy that contains all properties about support of finite sets
```--- a/src/HOL/Nominal/Nominal.thy	Sun Nov 27 04:59:20 2005 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Sun Nov 27 05:00:43 2005 +0100
@@ -5,7 +5,7 @@
uses
("nominal_atoms.ML")
("nominal_package.ML")
-(*  ("nominal_induct.ML") *)
+  ("nominal_induct.ML")
("nominal_permeq.ML")
begin

@@ -26,6 +26,10 @@
perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"

+lemma perm_union:
+  shows "pi \<bullet> (X \<union> Y) = (pi \<bullet> X) \<union> (pi \<bullet> Y)"
+  by (auto simp add: perm_set_def)
+
(* permutation on units and products *)
primrec (perm_unit)
"pi\<bullet>()    = ()"
@@ -68,6 +72,10 @@
perm_true_def:  "pi\<bullet>True  = True"
perm_false_def: "pi\<bullet>False = False"

+lemma perm_bool:
+  shows "pi\<bullet>(b::bool) = b"
+  by (cases "b", auto)
+
(* permutation on options *)
primrec (perm_option)
perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
@@ -121,6 +129,14 @@
shows "supp () = {}"

+lemma supp_set_empty:
+  shows "supp {} = {}"
+  by (force simp add: supp_def perm_set_def)
+
+lemma supp_singleton:
+  shows "supp {x} = supp x"
+  by (force simp add: supp_def perm_set_def)
+
lemma supp_prod:
fixes x :: "'a"
and   y :: "'b"
@@ -175,6 +191,10 @@
done

+lemma fresh_set_empty:
+  shows "a\<sharp>{}"
+  by (simp add: fresh_def supp_set_empty)
+
lemma fresh_prod:
fixes a :: "'x"
and   x :: "'a"
@@ -184,7 +204,7 @@

lemma fresh_list_nil:
fixes a :: "'x"
-  shows "a\<sharp>([]::'a list)"
+  shows "a\<sharp>[]"

lemma fresh_list_cons:
@@ -220,6 +240,7 @@
done

+
section {* Abstract Properties for Permutations and  Atoms *}
(*=========================================================*)

@@ -911,6 +932,16 @@
shows "(pi\<bullet>x)\<in>(pi\<bullet>X)"
using a by (simp add: pt_set_bij[OF pt, OF at])

+lemma pt_set_bij2a:
+  fixes pi :: "'x prm"
+  and   x  :: "'a"
+  and   X  :: "'a set"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     a:  "x\<in>((rev pi)\<bullet>X)"
+  shows "(pi\<bullet>x)\<in>X"
+  using a by (simp add: pt_set_bij1[OF pt, OF at])
+
lemma pt_set_bij3:
fixes pi :: "'x prm"
and   x  :: "'a"
@@ -943,13 +974,6 @@
thus "x\<in>(pi\<bullet>Y)" by (force simp add: pt_set_bij1a[OF pt, OF at])
qed

-lemma pt_list_set_pi:
-  fixes pi :: "'x prm"
-  and   xs :: "'a list"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs, auto simp add: perm_set_def pt1[OF pt])
-
-- "some helper lemmas for the pt_perm_supp_ineq lemma"
lemma Collect_permI:
fixes pi :: "'x prm"
@@ -1296,18 +1320,6 @@
using a b
by (force simp add: "op supports_def")

-lemma supp_supports:
-  fixes x :: "'a"
-  assumes  pt: "pt TYPE('a) TYPE('x)"
-  and      at: "at TYPE ('x)"
-  shows "((supp x)::'x set) supports x"
-proof (unfold "op supports_def", intro strip)
-  fix a b
-  assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
-  hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
-  thus "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pt, OF at])
-qed
-
lemma supp_is_subset:
fixes S :: "'x set"
and   x :: "'a"
@@ -1325,6 +1337,18 @@
with b1 show False by simp
qed

+lemma supp_supports:
+  fixes x :: "'a"
+  assumes  pt: "pt TYPE('a) TYPE('x)"
+  and      at: "at TYPE ('x)"
+  shows "((supp x)::'x set) supports x"
+proof (unfold "op supports_def", intro strip)
+  fix a b
+  assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
+  hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
+  thus "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pt, OF at])
+qed
+
lemma supports_finite:
fixes S :: "'x set"
and   x :: "'a"
@@ -1516,7 +1540,7 @@
have "x#xs = [x]@xs" by simp
hence "(x#xs)\<bullet>y = ([x]@xs)\<bullet>y" by simp
hence "(x#xs)\<bullet>y = [x]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt])
-    thus ?case using a i p by (force)
+    thus ?case using a i p by force
qed

lemma pt_swap_eq:
@@ -1633,6 +1657,231 @@
from a1 a2 a3 show False by (force dest: finite_subset)
qed

+section {* Facts about the support of finite sets of finitely supported things *}
+(*=============================================================================*)
+
+constdefs
+  X_to_Un_supp :: "('a set) \<Rightarrow> 'x set"
+  "X_to_Un_supp X \<equiv> \<Union>x\<in>X. ((supp x)::'x set)"
+
+lemma UNION_f_eqvt:
+  fixes X::"('a set)"
+  and   f::"'a \<Rightarrow> 'x set"
+  and   pi::"'x prm"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows "pi\<bullet>(\<Union>x\<in>X. f x) = (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
+proof -
+  have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
+  show ?thesis
+    apply(rule_tac x="pi\<bullet>xa" in exI)
+    apply(rule conjI)
+    apply(rule_tac x="xa" in exI)
+    apply(simp)
+    apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xa) = pi\<bullet>(f xa)")(*A*)
+    apply(simp)
+    apply(rule pt_set_bij2[OF pt_x, OF at])
+    apply(assumption)
+    apply(rule sym)
+    apply(rule pt_fun_app_eq[OF pt, OF at])
+    apply(rule_tac x="(rev pi)\<bullet>x" in exI)
+    apply(rule conjI)
+    apply(rule sym)
+    apply(rule pt_pi_rev[OF pt_x, OF at])
+    apply(rule_tac x="a" in bexI)
+    apply(simp add: pt_set_bij1[OF pt_x, OF at])
+    apply(simp add: pt_fun_app_eq[OF pt, OF at])
+    apply(assumption)
+    done
+qed
+
+lemma X_to_Un_supp_eqvt:
+  fixes X::"('a set)"
+  and   pi::"'x prm"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
+  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def)
+  apply(simp add: pt_perm_supp[OF pt, OF at])
+  apply(simp add: pt_pi_rev[OF pt, OF at])
+  done
+
+lemma Union_supports_set:
+  fixes X::"('a set)"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows "(\<Union>x\<in>X. ((supp x)::'x set)) supports X"
+  apply(simp add: "op supports_def" fresh_def[symmetric])
+  apply(rule allI)+
+  apply(rule impI)
+  apply(erule conjE)
+  apply(auto)
+  apply(subgoal_tac "[(a,b)]\<bullet>aa = aa")(*A*)
+  apply(simp)
+  apply(rule pt_fresh_fresh[OF pt, OF at])
+  apply(force)
+  apply(force)
+  apply(rule_tac x="x" in exI)
+  apply(simp)
+  apply(rule sym)
+  apply(rule pt_fresh_fresh[OF pt, OF at])
+  apply(force)+
+  done
+
+lemma Union_of_fin_supp_sets:
+  fixes X::"('a set)"
+  assumes fs: "fs TYPE('a) TYPE('x)"
+  and     fi: "finite X"
+  shows "finite (\<Union>x\<in>X. ((supp x)::'x set))"
+using fi by (induct, auto simp add: fs1[OF fs])
+
+lemma Union_included_in_supp:
+  fixes X::"('a set)"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     fs: "fs TYPE('a) TYPE('x)"
+  and     fi: "finite X"
+  shows "(\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> supp X"
+proof -
+  have "supp ((X_to_Un_supp X)::'x set) \<subseteq> ((supp X)::'x set)"
+    apply(rule pt_empty_supp_fun_subset)
+    apply(force intro: pt_set_inst at_pt_inst pt at)+
+    apply(rule pt_eqvt_fun2b)
+    apply(force intro: pt_set_inst at_pt_inst pt at)+
+    apply(rule allI)
+    apply(rule allI)
+    apply(rule X_to_Un_supp_eqvt[OF pt, OF at])
+    done
+  hence "supp (\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> ((supp X)::'x set)" by (simp add: X_to_Un_supp_def)
+  moreover
+  have "supp (\<Union>x\<in>X. ((supp x)::'x set)) = (\<Union>x\<in>X. ((supp x)::'x set))"
+    apply(rule at_fin_set_supp[OF at])
+    apply(rule Union_of_fin_supp_sets[OF fs, OF fi])
+    done
+  ultimately show ?thesis by force
+qed
+
+lemma supp_of_fin_sets:
+  fixes X::"('a set)"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     fs: "fs TYPE('a) TYPE('x)"
+  and     fi: "finite X"
+  shows "(supp X) = (\<Union>x\<in>X. ((supp x)::'x set))"
+apply(rule subset_antisym)
+apply(rule supp_is_subset)
+apply(rule Union_supports_set[OF pt, OF at])
+apply(rule Union_of_fin_supp_sets[OF fs, OF fi])
+apply(rule Union_included_in_supp[OF pt, OF at, OF fs, OF fi])
+done
+
+lemma supp_fin_union:
+  fixes X::"('a set)"
+  and   Y::"('a set)"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     fs: "fs TYPE('a) TYPE('x)"
+  and     f1: "finite X"
+  and     f2: "finite Y"
+  shows "(supp (X\<union>Y)) = (supp X)\<union>((supp Y)::'x set)"
+using f1 f2 by (force simp add: supp_of_fin_sets[OF pt, OF at, OF fs])
+
+lemma supp_fin_insert:
+  fixes X::"('a set)"
+  and   x::"'a"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     fs: "fs TYPE('a) TYPE('x)"
+  and     f:  "finite X"
+  shows "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)"
+proof -
+  have "(supp (insert x X)) = ((supp ({x}\<union>(X::'a set)))::'x set)" by simp
+  also have "\<dots> = (supp {x})\<union>(supp X)"
+    by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f)
+  finally show "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)"
+qed
+
+lemma fresh_fin_union:
+  fixes X::"('a set)"
+  and   Y::"('a set)"
+  and   a::"'x"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     fs: "fs TYPE('a) TYPE('x)"
+  and     f1: "finite X"
+  and     f2: "finite Y"
+  shows "a\<sharp>(X\<union>Y) = (a\<sharp>X \<and> a\<sharp>Y)"
+apply(simp add: supp_fin_union[OF pt, OF at, OF fs, OF f1, OF f2])
+done
+
+lemma fresh_fin_insert:
+  fixes X::"('a set)"
+  and   x::"'a"
+  and   a::"'x"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     fs: "fs TYPE('a) TYPE('x)"
+  and     f:  "finite X"
+  shows "a\<sharp>(insert x X) = (a\<sharp>x \<and> a\<sharp>X)"
+apply(simp add: supp_fin_insert[OF pt, OF at, OF fs, OF f])
+done
+
+lemma fresh_fin_insert1:
+  fixes X::"('a set)"
+  and   x::"'a"
+  and   a::"'x"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     fs: "fs TYPE('a) TYPE('x)"
+  and     f:  "finite X"
+  and     a1:  "a\<sharp>x"
+  and     a2:  "a\<sharp>X"
+  shows "a\<sharp>(insert x X)"
+using a1 a2
+apply(simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
+done
+
+lemma pt_list_set_pi:
+  fixes pi :: "'x prm"
+  and   xs :: "'a list"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
+by (induct xs, auto simp add: perm_set_def pt1[OF pt])
+
+lemma pt_list_set_supp:
+  fixes xs :: "'a list"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     fs: "fs TYPE('a) TYPE('x)"
+  shows "supp (set xs) = ((supp xs)::'x set)"
+proof -
+  have "supp (set xs) = (\<Union>x\<in>(set xs). ((supp x)::'x set))"
+    by (rule supp_of_fin_sets[OF pt, OF at, OF fs], rule finite_set)
+  also have "(\<Union>x\<in>(set xs). ((supp x)::'x set)) = (supp xs)"
+  proof(induct xs)
+    case Nil show ?case by (simp add: supp_list_nil)
+  next
+    case (Cons h t) thus ?case by (simp add: supp_list_cons)
+  qed
+  finally show ?thesis by simp
+qed
+
+lemma pt_list_set_fresh:
+  fixes a :: "'x"
+  and   xs :: "'a list"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     fs: "fs TYPE('a) TYPE('x)"
+  and     a: "a\<sharp>xs"
+  shows "a\<sharp>(set xs) = a\<sharp>xs"
+by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
+
section {* Andy's freshness lemma *}
(*================================*)

@@ -2283,12 +2532,10 @@

(*****************************************)
(* setup for induction principles method *)
-(*
use "nominal_induct.ML";
method_setup nominal_induct =
{* nominal_induct_method *}
{* nominal induction *}
-*)

(*******************************)
(* permutation equality tactic *)```