# HG changeset patch # User urbanc # Date 1209760994 -7200 # Node ID ba8b1a8a12a7919972e5b732e0072cd663d72717 # Parent 9174c7afd8b8797ec527fde6c8930c8934954646 added more infrastructure for fresh_star diff -r 9174c7afd8b8 -r ba8b1a8a12a7 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Fri May 02 18:42:17 2008 +0200 +++ b/src/HOL/Nominal/Nominal.thy Fri May 02 22:43:14 2008 +0200 @@ -1327,14 +1327,13 @@ shows "(pi\x)\X" using a by (simp add: pt_set_bij1[OF pt, OF at]) +(* FIXME: is this lemma needed anywhere? *) lemma pt_set_bij3: fixes pi :: "'x prm" and x :: "'a" and X :: "'a set" shows "pi\(x\X) = (x\X)" -apply(case_tac "x\X = True") -apply(auto) -done +by (simp add: perm_bool) lemma pt_subseteq_eqvt: fixes pi :: "'x prm" @@ -1529,6 +1528,35 @@ 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\a)\*(pi\x) = a\*x" + and "(pi\b)\*(pi\x) = b\*x" +apply(unfold fresh_star_def) +apply(auto) +apply(drule_tac x="pi\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)\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\xa" in bspec) +apply(simp add: pt_set_bij1[OF ptb, OF at]) +apply(simp add: set_eqvt 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)\xa" in bspec) +apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt) +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" @@ -1577,6 +1605,31 @@ 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\a)\*(pi\x) = a\*x" + and "(pi\b)\*(pi\x) = b\*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_bij1: fixes pi :: "'x prm" and x :: "'a" @@ -1745,6 +1798,30 @@ thus ?thesis using eq3 by simp qed +lemma pt_pi_fresh_fresh: + fixes x :: "'a" + and pi :: "'x prm" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE ('x)" + and a: "\(a,b)\set pi. a\x \ b\x" + shows "pi\x=x" +using a +proof (induct pi) + case Nil + show "([]::'x prm)\x = x" by (rule pt1[OF pt]) +next + case (Cons ab pi) + have a: "\(a,b)\set (ab#pi). a\x \ b\x" by fact + have ih: "(\(a,b)\set pi. a\x \ b\x) \ pi\x=x" by fact + obtain a b where e: "ab=(a,b)" by (cases ab) (auto) + from a have a': "a\x" "b\x" using e by auto + have "(ab#pi)\x = ([(a,b)]@pi)\x" using e by simp + also have "\ = [(a,b)]\(pi\x)" by (simp only: pt2[OF pt]) + also have "\ = [(a,b)]\x" using ih a by simp + also have "\ = x" using a' by (simp add: pt_fresh_fresh[OF pt, OF at]) + finally show "(ab#pi)\x = x" by simp +qed + lemma pt_perm_compose: fixes pi1 :: "'x prm" and pi2 :: "'x prm" diff -r 9174c7afd8b8 -r ba8b1a8a12a7 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Fri May 02 18:42:17 2008 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Fri May 02 22:43:14 2008 +0200 @@ -746,6 +746,8 @@ val fresh_right = @{thm "Nominal.pt_fresh_right"}; val fresh_bij_ineq = @{thm "Nominal.pt_fresh_bij_ineq"}; val fresh_bij = @{thm "Nominal.pt_fresh_bij"}; + val fresh_star_bij_ineq = @{thms "Nominal.pt_fresh_star_bij_ineq"}; + val fresh_star_bij = @{thms "Nominal.pt_fresh_star_bij"}; val fresh_eqvt = @{thm "Nominal.pt_fresh_eqvt"}; val fresh_eqvt_ineq = @{thm "Nominal.pt_fresh_eqvt_ineq"}; val set_diff_eqvt = @{thm "Nominal.pt_set_diff_eqvt"}; @@ -775,6 +777,10 @@ (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) fun instR thm thms = map (fn ti => ti RS thm) thms; + (* takes a theorem thm and a list of theorems [(t1,m1),..,(tn,mn)] *) + (* produces a list of theorems of the form [[t1,m1] MRS thm,..,[tn,mn] MRS thm] *) + fun instRR thm thms = map (fn (ti,mi) => [ti,mi] MRS thm) thms; + (* takes two theorem lists (hopefully of the same length ;o) *) (* produces a list of theorems of the form *) (* [t1 RS m1,..,tn RS mn] where [t1,..,tn] is thms1 and [m1,..,mn] is thms2 *) @@ -817,7 +823,7 @@ fun inst_at thms = maps (fn ti => instR ti ats) thms; fun inst_fs thms = maps (fn ti => instR ti fss) thms; fun inst_cp thms cps = flat (inst_mult thms cps); - fun inst_pt_at thms = inst_zip ats (inst_pt thms); + fun inst_pt_at thms = maps (fn ti => instRR ti (pts ~~ ats)) thms; fun inst_dj thms = maps (fn ti => instR ti djs) thms; fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps; fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms)); @@ -897,6 +903,10 @@ and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq] in [(("fresh_bij", thms1 @ thms2),[])] end ||>> PureThy.add_thmss + let val thms1 = inst_pt_at fresh_star_bij + and thms2 = flat (map (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq); + in [(("fresh_star_bij", thms1 @ thms2),[])] end + ||>> PureThy.add_thmss let val thms1 = inst_pt_at [fresh_eqvt] and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq] in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end