--- a/src/HOL/Library/Formal_Power_Series.thy Sun Apr 26 20:23:41 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Apr 27 08:22:37 2009 +0200
@@ -963,7 +963,7 @@
(* {a_{n+k}}_0^infty Corresponds to (f - setsum (\<lambda>i. a_i * x^i))/x^h, for h>0*)
lemma fps_power_mult_eq_shift:
- "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. k}" (is "?lhs = ?rhs")
+ "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: comm_ring_1) * X^i) {0 .. k}" (is "?lhs = ?rhs")
proof-
{fix n:: nat
have "?lhs $ n = (if n < Suc k then 0 else a n)"
@@ -974,7 +974,7 @@
next
case (Suc k)
note th = Suc.hyps[symmetric]
- have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. Suc k})$n = (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: ring_simps)
+ have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: ring_simps)
also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n"
using th
unfolding fps_sub_nth by simp
@@ -1012,8 +1012,9 @@
lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" by (simp add: fps_eq_iff)
+
lemma fps_mult_XD_shift:
- "(XD ^^ k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
+ "(XD ^^ k) (a:: ('a::{comm_ring_1, recpower}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
--- a/src/HOL/Nominal/Nominal.thy Sun Apr 26 20:23:41 2009 +0200
+++ b/src/HOL/Nominal/Nominal.thy Mon Apr 27 08:22:37 2009 +0200
@@ -18,7 +18,7 @@
types
'x prm = "('x \<times> 'x) list"
-(* polymorphic operations for permutation and swapping *)
+(* polymorphic constants for permutation and swapping *)
consts
perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80)
swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
@@ -34,7 +34,7 @@
constdefs
"perm_aux pi x \<equiv> pi\<bullet>x"
-(* permutation operations *)
+(* overloaded permutation operations *)
overloading
perm_fun \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)" (unchecked)
perm_bool \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool" (unchecked)
@@ -203,11 +203,12 @@
supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80)
"S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
+(* lemmas about supp *)
lemma supp_fresh_iff:
fixes x :: "'a"
shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
-apply(simp add: fresh_def)
-done
+ by (simp add: fresh_def)
+
lemma supp_unit:
shows "supp () = {}"
@@ -238,14 +239,13 @@
fixes x :: "'a"
and xs :: "'a list"
shows "supp (x#xs) = (supp x)\<union>(supp xs)"
-apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
-done
+ by (auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
lemma supp_list_append:
fixes xs :: "'a list"
and ys :: "'a list"
shows "supp (xs@ys) = (supp xs)\<union>(supp ys)"
- by (induct xs, auto simp add: supp_list_nil supp_list_cons)
+ by (induct xs) (auto simp add: supp_list_nil supp_list_cons)
lemma supp_list_rev:
fixes xs :: "'a list"
@@ -287,6 +287,7 @@
shows "(supp s) = {}"
by (simp add: supp_def perm_string)
+(* lemmas about freshness *)
lemma fresh_set_empty:
shows "a\<sharp>{}"
by (simp add: fresh_def supp_set_empty)
@@ -395,63 +396,6 @@
Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
*}
-section {* generalisation of freshness to lists and sets of atoms *}
-(*================================================================*)
-
-consts
- fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
-
-defs (overloaded)
- fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
-
-defs (overloaded)
- fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
-
-lemmas fresh_star_def = fresh_star_list fresh_star_set
-
-lemma fresh_star_prod_set:
- fixes xs::"'a set"
- shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
-by (auto simp add: fresh_star_def fresh_prod)
-
-lemma fresh_star_prod_list:
- fixes xs::"'a list"
- shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
- by (auto simp add: fresh_star_def fresh_prod)
-
-lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
-
-lemma fresh_star_set_eq: "set xs \<sharp>* c = xs \<sharp>* c"
- by (simp add: fresh_star_def)
-
-lemma fresh_star_Un_elim:
- "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
- apply rule
- apply (simp_all add: fresh_star_def)
- apply (erule meta_mp)
- apply blast
- done
-
-lemma fresh_star_insert_elim:
- "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
- by rule (simp_all add: fresh_star_def)
-
-lemma fresh_star_empty_elim:
- "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
- by (simp add: fresh_star_def)
-
-text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
-
-lemma fresh_star_unit_elim:
- shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
- and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
- by (simp_all add: fresh_star_def fresh_def supp_unit)
-
-lemma fresh_star_prod_elim:
- shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)"
- and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)"
- by (rule, simp_all add: fresh_star_prod)+
-
section {* Abstract Properties for Permutations and Atoms *}
(*=========================================================*)
@@ -511,7 +455,7 @@
shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
using a by (simp only: at_def)
-(* rules to calculate simple premutations *)
+(* rules to calculate simple permutations *)
lemmas at_calc = at2 at1 at3
lemma at_swap_simps:
@@ -706,7 +650,6 @@
shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
by (simp add: at_prm_rev_eq[OF at])
-
lemma at_ds1:
fixes a :: "'x"
assumes at: "at TYPE('x)"
@@ -862,15 +805,18 @@
by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def)
lemma at_finite_select:
- shows "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S"
- apply (drule Diff_infinite_finite)
- apply (simp add: at_def)
- apply blast
- apply (subgoal_tac "UNIV - S \<noteq> {}")
- apply (simp only: ex_in_conv [symmetric])
- apply blast
- apply (rule notI)
- apply simp
+ fixes S::"'a set"
+ assumes a: "at TYPE('a)"
+ and b: "finite S"
+ shows "\<exists>x. x \<notin> S"
+ using a b
+ apply(drule_tac S="UNIV::'a set" in Diff_infinite_finite)
+ apply(simp add: at_def)
+ apply(subgoal_tac "UNIV - S \<noteq> {}")
+ apply(simp only: ex_in_conv [symmetric])
+ apply(blast)
+ apply(rule notI)
+ apply(simp)
done
lemma at_different:
@@ -1246,8 +1192,8 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "pi\<bullet>(x=y) = (pi\<bullet>x = pi\<bullet>y)"
-using assms
-by (auto simp add: pt_bij perm_bool)
+ using pt at
+ by (auto simp add: pt_bij perm_bool)
lemma pt_bij3:
fixes pi :: "'x prm"
@@ -1255,7 +1201,7 @@
and y :: "'a"
assumes a: "x=y"
shows "(pi\<bullet>x = pi\<bullet>y)"
-using a by simp
+ using a by simp
lemma pt_bij4:
fixes pi :: "'x prm"
@@ -1265,7 +1211,7 @@
and at: "at TYPE('x)"
and a: "pi\<bullet>x = pi\<bullet>y"
shows "x = y"
-using a by (simp add: pt_bij[OF pt, OF at])
+ using a by (simp add: pt_bij[OF pt, OF at])
lemma pt_swap_bij:
fixes a :: "'x"
@@ -1598,35 +1544,6 @@
apply(simp add: pt_rev_pi[OF ptb, OF at])
done
-lemma pt_fresh_star_bij_ineq:
- fixes pi :: "'x prm"
- and x :: "'a"
- and a :: "'y set"
- and b :: "'y list"
- assumes pta: "pt TYPE('a) TYPE('x)"
- and ptb: "pt TYPE('y) TYPE('x)"
- and at: "at TYPE('x)"
- and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
- shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
- and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
-apply(unfold fresh_star_def)
-apply(auto)
-apply(drule_tac x="pi\<bullet>xa" in bspec)
-apply(rule pt_set_bij2[OF ptb, OF at])
-apply(assumption)
-apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
-apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
-apply(drule_tac x="pi\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
-apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
-apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
-apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
-done
-
lemma pt_fresh_left:
fixes pi :: "'x prm"
and x :: "'a"
@@ -1675,56 +1592,6 @@
apply(rule at)
done
-lemma pt_fresh_star_bij:
- fixes pi :: "'x prm"
- and x :: "'a"
- and a :: "'x set"
- and b :: "'x list"
- assumes pt: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE('x)"
- shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
- and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
-apply(rule pt_fresh_star_bij_ineq(1))
-apply(rule pt)
-apply(rule at_pt_inst)
-apply(rule at)+
-apply(rule cp_pt_inst)
-apply(rule pt)
-apply(rule at)
-apply(rule pt_fresh_star_bij_ineq(2))
-apply(rule pt)
-apply(rule at_pt_inst)
-apply(rule at)+
-apply(rule cp_pt_inst)
-apply(rule pt)
-apply(rule at)
-done
-
-lemma pt_fresh_star_eqvt:
- fixes pi :: "'x prm"
- and x :: "'a"
- and a :: "'x set"
- and b :: "'x list"
- assumes pt: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE('x)"
- shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
- and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
- by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at])
-
-lemma pt_fresh_star_eqvt_ineq:
- fixes pi::"'x prm"
- and a::"'y set"
- and b::"'y list"
- and x::"'a"
- assumes pta: "pt TYPE('a) TYPE('x)"
- and ptb: "pt TYPE('y) TYPE('x)"
- and at: "at TYPE('x)"
- and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
- and dj: "disjoint TYPE('y) TYPE('x)"
- shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
- and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
- by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
-
lemma pt_fresh_bij1:
fixes pi :: "'x prm"
and x :: "'a"
@@ -1777,7 +1644,6 @@
(* the next two lemmas are needed in the proof *)
(* of the structural induction principle *)
-
lemma pt_fresh_aux:
fixes a::"'x"
and b::"'x"
@@ -1881,27 +1747,6 @@
thus ?thesis using eq3 by simp
qed
-lemma pt_freshs_freshs:
- assumes pt: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE ('x)"
- and pi: "set (pi::'x prm) \<subseteq> Xs \<times> Ys"
- and Xs: "Xs \<sharp>* (x::'a)"
- and Ys: "Ys \<sharp>* x"
- shows "pi \<bullet> x = x"
- using pi
-proof (induct pi)
- case Nil
- show ?case by (simp add: pt1 [OF pt])
-next
- case (Cons p pi)
- obtain a b where p: "p = (a, b)" by (cases p)
- with Cons Xs Ys have "a \<sharp> x" "b \<sharp> x"
- by (simp_all add: fresh_star_def)
- with Cons p show ?case
- by (simp add: pt_fresh_fresh [OF pt at]
- pt2 [OF pt, of "[(a, b)]" pi, simplified])
-qed
-
lemma pt_pi_fresh_fresh:
fixes x :: "'a"
and pi :: "'x prm"
@@ -1967,8 +1812,7 @@
thus ?thesis by (simp add: pt2[OF pt])
qed
-section {* equivaraince for some connectives *}
-
+section {* equivariance for some connectives *}
lemma pt_all_eqvt:
fixes pi :: "'x prm"
and x :: "'a"
@@ -2014,8 +1858,6 @@
apply(rule theI'[OF unique])
done
-
-
section {* facts about supports *}
(*==============================*)
@@ -2184,6 +2026,7 @@
shows "(x \<sharp> X) = (x \<notin> X)"
by (simp add: at_fin_set_supp fresh_def at fs)
+
section {* Permutations acting on Functions *}
(*==========================================*)
@@ -2564,9 +2407,8 @@
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
+ using a1 a2
+ by (simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
lemma pt_list_set_supp:
fixes xs :: "'a list"
@@ -2595,14 +2437,191 @@
shows "a\<sharp>(set xs) = a\<sharp>xs"
by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
+
+section {* generalisation of freshness to lists and sets of atoms *}
+(*================================================================*)
+
+consts
+ fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
+
+defs (overloaded)
+ fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
+
+defs (overloaded)
+ fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
+
+lemmas fresh_star_def = fresh_star_list fresh_star_set
+
+lemma fresh_star_prod_set:
+ fixes xs::"'a set"
+ shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
+by (auto simp add: fresh_star_def fresh_prod)
+
+lemma fresh_star_prod_list:
+ fixes xs::"'a list"
+ shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
+ by (auto simp add: fresh_star_def fresh_prod)
+
+lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
+
+lemma fresh_star_set_eq: "set xs \<sharp>* c = xs \<sharp>* c"
+ by (simp add: fresh_star_def)
+
+lemma fresh_star_Un_elim:
+ "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
+ apply rule
+ apply (simp_all add: fresh_star_def)
+ apply (erule meta_mp)
+ apply blast
+ done
+
+lemma fresh_star_insert_elim:
+ "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
+ by rule (simp_all add: fresh_star_def)
+
+lemma fresh_star_empty_elim:
+ "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
+ by (simp add: fresh_star_def)
+
+text {* Normalization of freshness results; see \ @{text nominal_induct} *}
+
+lemma fresh_star_unit_elim:
+ shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
+ and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
+ by (simp_all add: fresh_star_def fresh_def supp_unit)
+
+lemma fresh_star_prod_elim:
+ shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)"
+ and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)"
+ by (rule, simp_all add: fresh_star_prod)+
+
+
+lemma pt_fresh_star_bij_ineq:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'y set"
+ and b :: "'y list"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
+ and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
+apply(unfold fresh_star_def)
+apply(auto)
+apply(drule_tac x="pi\<bullet>xa" in bspec)
+apply(erule pt_set_bij2[OF ptb, OF at])
+apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="pi\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+done
+
+lemma pt_fresh_star_bij:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'x set"
+ and b :: "'x list"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
+ and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
+apply(rule pt_fresh_star_bij_ineq(1))
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+apply(rule pt_fresh_star_bij_ineq(2))
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
+
+lemma pt_fresh_star_eqvt:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'x set"
+ and b :: "'x list"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
+ and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
+ by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at])
+
+lemma pt_fresh_star_eqvt_ineq:
+ fixes pi::"'x prm"
+ and a::"'y set"
+ and b::"'y list"
+ and x::"'a"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ and dj: "disjoint TYPE('y) TYPE('x)"
+ shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
+ and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
+ by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
+
+lemma pt_freshs_freshs:
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE ('x)"
+ and pi: "set (pi::'x prm) \<subseteq> Xs \<times> Ys"
+ and Xs: "Xs \<sharp>* (x::'a)"
+ and Ys: "Ys \<sharp>* x"
+ shows "pi\<bullet>x = x"
+ using pi
+proof (induct pi)
+ case Nil
+ show ?case by (simp add: pt1 [OF pt])
+next
+ case (Cons p pi)
+ obtain a b where p: "p = (a, b)" by (cases p)
+ with Cons Xs Ys have "a \<sharp> x" "b \<sharp> x"
+ by (simp_all add: fresh_star_def)
+ with Cons p show ?case
+ by (simp add: pt_fresh_fresh [OF pt at]
+ pt2 [OF pt, of "[(a, b)]" pi, simplified])
+qed
+
+lemma pt_fresh_star_pi:
+ fixes x::"'a"
+ and pi::"'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and a: "((supp x)::'x set)\<sharp>* pi"
+ shows "pi\<bullet>x = x"
+using a
+apply(induct pi)
+apply(auto simp add: fresh_star_def fresh_list_cons fresh_prod pt1[OF pt])
+apply(subgoal_tac "((a,b)#pi)\<bullet>x = ([(a,b)]@pi)\<bullet>x")
+apply(simp only: pt2[OF pt])
+apply(rule pt_fresh_fresh[OF pt at])
+apply(simp add: fresh_def at_supp[OF at])
+apply(blast)
+apply(simp add: fresh_def at_supp[OF at])
+apply(blast)
+apply(simp add: pt2[OF pt])
+done
+
section {* Infrastructure lemmas for strong rule inductions *}
(*==========================================================*)
-
text {*
For every set of atoms, there is another set of atoms
avoiding a finitely supported c and there is a permutation
- which make 'translates' between both sets.
+ which 'translates' between both sets.
*}
lemma at_set_avoiding_aux:
fixes Xs::"'a set"
@@ -3389,7 +3408,6 @@
syntax ABS :: "type \<Rightarrow> type \<Rightarrow> type" ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000)
-
section {* lemmas for deciding permutation equations *}
(*===================================================*)
@@ -3550,8 +3568,8 @@
shows "pi\<bullet>(x div y) = (pi\<bullet>x) div (pi\<bullet>y)"
by (simp add:perm_int_def)
-(*******************************************************************)
-(* Setup of the theorem attributes eqvt, eqvt_force, fresh and bij *)
+(*******************************************************)
+(* Setup of the theorem attributes eqvt and eqvt_force *)
use "nominal_thmdecls.ML"
setup "NominalThmDecls.setup"
--- a/src/HOL/Nominal/nominal_thmdecls.ML Sun Apr 26 20:23:41 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon Apr 27 08:22:37 2009 +0200
@@ -3,10 +3,10 @@
This file introduces the infrastructure for the lemma
collection "eqvts".
- By attaching [eqvt], [eqvt_force] to a lemma, the lemma gets
+ By attaching [eqvt] or [eqvt_force] to a lemma, it will get
stored in a data-slot in the context. Possible modifiers
- are [... add] and [... del] for adding and deleting, respectively
- the lemma from the data-slot.
+ are [... add] and [... del] for adding and deleting,
+ respectively, the lemma from the data-slot.
*)
signature NOMINAL_THMDECLS =
@@ -43,9 +43,6 @@
(* equality-lemma can be derived. *)
exception EQVT_FORM of string
-(* FIXME: should be a function in a library *)
-fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T))
-
val NOMINAL_EQVT_DEBUG = ref false
fun tactic (msg, tac) =
@@ -53,14 +50,14 @@
then tac THEN' (K (print_tac ("after " ^ msg)))
else tac
-fun tactic_eqvt ctx orig_thm pi pi' =
+fun prove_eqvt_tac ctxt orig_thm pi pi' =
let
- val mypi = Thm.cterm_of ctx pi
+ val mypi = Thm.cterm_of ctxt pi
val T = fastype_of pi'
- val mypifree = Thm.cterm_of ctx (Const (@{const_name "List.rev"}, T --> T) $ pi')
- val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
+ val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi')
+ val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp"
in
- EVERY1 [tactic ("iffI applied",rtac @{thm iffI}),
+ EVERY1 [tactic ("iffI applied", rtac @{thm iffI}),
tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
tactic ("solve with orig_thm", etac orig_thm),
tactic ("applies orig_thm instantiated with rev pi",
@@ -74,36 +71,38 @@
let
val thy = ProofContext.theory_of ctxt;
val pi' = Var (pi, typi);
- val lhs = Const (@{const_name "Nominal.perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
+ val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
val ([goal_term, pi''], ctxt') = Variable.import_terms false
[HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
val _ = Display.print_cterm (cterm_of thy goal_term)
in
Goal.prove ctxt' [] [] goal_term
- (fn _ => tactic_eqvt thy orig_thm pi' pi'') |>
+ (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
singleton (ProofContext.export ctxt' ctxt)
end
-(* replaces every variable x in t with pi o x *)
+(* replaces in t every variable, say x, with pi o x *)
fun apply_pi trm (pi, typi) =
let
- fun only_vars t =
- (case t of
- Var (n, ty) =>
- (Const (@{const_name "Nominal.perm"}, typi --> ty --> ty)
- $ (Var (pi, typi)) $ (Var (n, ty)))
- | _ => t)
+ fun replace n ty =
+ let
+ val c = Const (@{const_name "perm"}, typi --> ty --> ty)
+ val v1 = Var (pi, typi)
+ val v2 = Var (n, ty)
+ in
+ c $ v1 $ v2
+ end
in
- map_aterms only_vars trm
-end;
+ map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
+end
(* returns *the* pi which is in front of all variables, provided there *)
(* exists such a pi; otherwise raises EQVT_FORM *)
fun get_pi t thy =
let fun get_pi_aux s =
(case s of
- (Const (@{const_name "Nominal.perm"} ,typrm) $
- (Var (pi,typi as Type("List.list", [Type ("*", [Type (tyatm,[]),_])]))) $
+ (Const (@{const_name "perm"} ,typrm) $
+ (Var (pi,typi as Type(@{type_name "list"}, [Type ("*", [Type (tyatm,[]),_])]))) $
(Var (n,ty))) =>
let
(* FIXME: this should be an operation the library *)
@@ -148,7 +147,7 @@
end
(* case: eqvt-lemma is of the equational form *)
| (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
- (Const (@{const_name "Nominal.perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
+ (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
(if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
else raise EQVT_FORM "Type Equality")
@@ -161,13 +160,11 @@
" does not comply with the form of an equivariance lemma (" ^ s ^").")
-fun eqvt_map f (r:Data.T) = f r;
+val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
+val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));
-val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.add_thm));
-val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.del_thm));
-
-val eqvt_force_add = Thm.declaration_attribute (Data.map o eqvt_map o Thm.add_thm);
-val eqvt_force_del = Thm.declaration_attribute (Data.map o eqvt_map o Thm.del_thm);
+val eqvt_force_add = Thm.declaration_attribute (Data.map o Thm.add_thm);
+val eqvt_force_del = Thm.declaration_attribute (Data.map o Thm.del_thm);
val get_eqvt_thms = Context.Proof #> Data.get;