# HG changeset patch # User Cezary Kaliszyk # Date 1266411391 -3600 # Node ID 62632eec979c6fae723eb5b70f1d6a1f8091a3a5 # Parent a7b4160ef463e75f93114de2184aa17c42b95d94 Tested the Perm code; works everywhere in Terms. diff -r a7b4160ef463 -r 62632eec979c Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Wed Feb 17 13:54:35 2010 +0100 +++ b/Quot/Nominal/Terms.thy Wed Feb 17 13:56:31 2010 +0100 @@ -1,5 +1,5 @@ theory Terms -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" begin atom_decl name @@ -39,46 +39,7 @@ | "rfv_bp (BVr x) = {atom x}" | "rfv_bp (BPr b1 b2) = (rfv_bp b1) \ (rfv_bp b2)" -(* needs to be stated by the package *) -instantiation - rtrm1 and bp :: pt -begin - -primrec - permute_rtrm1 and permute_bp -where - "permute_rtrm1 pi (rVr1 a) = rVr1 (pi \ a)" -| "permute_rtrm1 pi (rAp1 t1 t2) = rAp1 (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)" -| "permute_rtrm1 pi (rLm1 a t) = rLm1 (pi \ a) (permute_rtrm1 pi t)" -| "permute_rtrm1 pi (rLt1 bp t1 t2) = rLt1 (permute_bp pi bp) (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)" -| "permute_bp pi (BUnit) = BUnit" -| "permute_bp pi (BVr a) = BVr (pi \ a)" -| "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)" - -lemma pt_rtrm1_bp_zero: - fixes t::rtrm1 - and b::bp - shows "0 \ t = t" - and "0 \ b = b" -apply(induct t and b rule: rtrm1_bp.inducts) -apply(simp_all) -done - -lemma pt_rtrm1_bp_plus: - fixes t::rtrm1 - and b::bp - shows "((p + q) \ t) = p \ (q \ t)" - and "((p + q) \ b) = p \ (q \ b)" -apply(induct t and b rule: rtrm1_bp.inducts) -apply(simp_all) -done - -instance -apply default -apply(simp_all add: pt_rtrm1_bp_zero pt_rtrm1_bp_plus) -done - -end +setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} inductive alpha1 :: "rtrm1 \ rtrm1 \ bool" ("_ \1 _" [100, 100] 100) @@ -340,45 +301,7 @@ | "fv_rtrm2 (rLt2 as t) = (fv_rtrm2 t - rbv2 as) \ (fv_rassign as)" | "fv_rassign (rAs x t) = fv_rtrm2 t" -(* needs to be stated by the package *) -instantiation - rtrm2 and rassign :: pt -begin - -primrec - permute_rtrm2 and permute_rassign -where - "permute_rtrm2 pi (rVr2 a) = rVr2 (pi \ a)" -| "permute_rtrm2 pi (rAp2 t1 t2) = rAp2 (permute_rtrm2 pi t1) (permute_rtrm2 pi t2)" -| "permute_rtrm2 pi (rLm2 a t) = rLm2 (pi \ a) (permute_rtrm2 pi t)" -| "permute_rtrm2 pi (rLt2 as t) = rLt2 (permute_rassign pi as) (permute_rtrm2 pi t)" -| "permute_rassign pi (rAs a t) = rAs (pi \ a) (permute_rtrm2 pi t)" - -lemma pt_rtrm2_rassign_zero: - fixes t::rtrm2 - and b::rassign - shows "0 \ t = t" - and "0 \ b = b" -apply(induct t and b rule: rtrm2_rassign.inducts) -apply(simp_all) -done - -lemma pt_rtrm2_rassign_plus: - fixes t::rtrm2 - and b::rassign - shows "((p + q) \ t) = p \ (q \ t)" - and "((p + q) \ b) = p \ (q \ b)" -apply(induct t and b rule: rtrm2_rassign.inducts) -apply(simp_all) -done - -instance -apply default -apply(simp_all add: pt_rtrm2_rassign_zero pt_rtrm2_rassign_plus) -done - - -end +setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} inductive alpha2 :: "rtrm2 \ rtrm2 \ bool" ("_ \2 _" [100, 100] 100) @@ -434,46 +357,7 @@ | "fv_assigns (ANil) = {}" | "fv_assigns (ACons x t as) = (fv_trm3 t) \ (fv_assigns as)" -(* needs to be stated by the package *) -instantiation - trm3 and assigns :: pt -begin - -primrec - permute_trm3 and permute_assigns -where - "permute_trm3 pi (Vr3 a) = Vr3 (pi \ a)" -| "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)" -| "permute_trm3 pi (Lm3 a t) = Lm3 (pi \ a) (permute_trm3 pi t)" -| "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)" -| "permute_assigns pi (ANil) = ANil" -| "permute_assigns pi (ACons a t as) = ACons (pi \ a) (permute_trm3 pi t) (permute_assigns pi as)" - -lemma pt_trm3_assigns_zero: - fixes t::trm3 - and b::assigns - shows "0 \ t = t" - and "0 \ b = b" -apply(induct t and b rule: trm3_assigns.inducts) -apply(simp_all) -done - -lemma pt_trm3_assigns_plus: - fixes t::trm3 - and b::assigns - shows "((p + q) \ t) = p \ (q \ t)" - and "((p + q) \ b) = p \ (q \ b)" -apply(induct t and b rule: trm3_assigns.inducts) -apply(simp_all) -done - -instance -apply default -apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus) -done - - -end +setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} inductive alpha3 :: "trm3 \ trm3 \ bool" ("_ \3 _" [100, 100] 100) @@ -519,49 +403,9 @@ | "fv_trm4_list ([]) = {}" | "fv_trm4_list (t#ts) = (fv_trm4 t) \ (fv_trm4_list ts)" - -(* needs to be stated by the package *) -(* there cannot be a clause for lists, as *) +(* there cannot be a clause for lists, as *) (* permutations are already defined in Nominal (also functions, options, and so on) *) -instantiation - trm4 :: pt -begin - -(* does not work yet *) -primrec - permute_trm4 and permute_trm4_list -where - "permute_trm4 pi (Vr4 a) = Vr4 (pi \ a)" -| "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute_trm4_list pi ts)" -| "permute_trm4 pi (Lm4 a t) = Lm4 (pi \ a) (permute_trm4 pi t)" -| "permute_trm4_list pi ([]) = []" -| "permute_trm4_list pi (t#ts) = (permute_trm4 pi t) # (permute_trm4_list pi ts)" - -lemma pt_trm4_list_zero: - fixes t::trm4 - and ts::"trm4 list" - shows "0 \ t = t" - and "permute_trm4_list 0 ts = ts" -apply(induct t and ts rule: trm4.inducts) -apply(simp_all) -done - -lemma pt_trm4_list_plus: - fixes t::trm4 - and ts::"trm4 list" - shows "((p + q) \ t) = p \ (q \ t)" - and "(permute_trm4_list (p + q) ts) = permute_trm4_list p (permute_trm4_list q ts)" -apply(induct t and ts rule: trm4.inducts) -apply(simp_all) -done - - -instance -apply(default) -apply(simp_all add: pt_trm4_list_zero pt_trm4_list_plus) -done - -end +setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *} (* "repairing" of the permute function *) lemma repaired: @@ -616,43 +460,8 @@ | "rfv_lts (rLnil) = {}" | "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \ (rfv_lts ltl)" -instantiation - rtrm5 and rlts :: pt -begin - -primrec - permute_rtrm5 and permute_rlts -where - "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \ a)" -| "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)" -| "permute_rtrm5 pi (rLt5 ls t) = rLt5 (permute_rlts pi ls) (permute_rtrm5 pi t)" -| "permute_rlts pi (rLnil) = rLnil" -| "permute_rlts pi (rLcons n t ls) = rLcons (pi \ n) (permute_rtrm5 pi t) (permute_rlts pi ls)" - -lemma pt_rtrm5_zero: - fixes t::rtrm5 - and l::rlts - shows "0 \ t = t" - and "0 \ l = l" -apply(induct t and l rule: rtrm5_rlts.inducts) -apply(simp_all) -done - -lemma pt_rtrm5_plus: - fixes t::rtrm5 - and l::rlts - shows "((p + q) \ t) = p \ (q \ t)" - and "((p + q) \ l) = p \ (q \ l)" -apply(induct t and l rule: rtrm5_rlts.inducts) -apply(simp_all) -done - -instance -apply default -apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus) -done - -end +setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} +print_theorems inductive alpha5 :: "rtrm5 \ rtrm5 \ bool" ("_ \5 _" [100, 100] 100) @@ -946,37 +755,8 @@ | "rfv_trm6 (rLm6 n t) = (rfv_trm6 t) - {atom n}" | "rfv_trm6 (rLt6 l r) = (rfv_trm6 r - rbv6 l) \ rfv_trm6 l" -instantiation - rtrm6 :: pt -begin - -primrec - permute_rtrm6 -where - "permute_rtrm6 pi (rVr6 a) = rVr6 (pi \ a)" -| "permute_rtrm6 pi (rLm6 n t) = rLm6 (pi \ n) (permute_rtrm6 pi t)" -| "permute_rtrm6 pi (rLt6 l r) = rLt6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)" - -lemma pt_rtrm6_zero: - fixes t::rtrm6 - shows "0 \ t = t" -apply(induct t) -apply(simp_all) -done - -lemma pt_rtrm6_plus: - fixes t::rtrm6 - shows "((p + q) \ t) = p \ (q \ t)" -apply(induct t) -apply(simp_all) -done - -instance -apply default -apply(simp_all add: pt_rtrm6_zero pt_rtrm6_plus) -done - -end +setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} +print_theorems inductive alpha6 :: "rtrm6 \ rtrm6 \ bool" ("_ \6 _" [100, 100] 100) @@ -1134,37 +914,8 @@ | "rfv_trm7 (rLm7 n t) = (rfv_trm7 t) - {atom n}" | "rfv_trm7 (rLt7 l r) = (rfv_trm7 l) \ (rfv_trm7 r - rbv7 l)" -instantiation - rtrm7 :: pt -begin - -primrec - permute_rtrm7 -where - "permute_rtrm7 pi (rVr7 a) = rVr7 (pi \ a)" -| "permute_rtrm7 pi (rLm7 a t) = rLm7 (pi \ a) (permute_rtrm7 pi t)" -| "permute_rtrm7 pi (rLt7 t1 t2) = rLt7 (permute_rtrm7 pi t1) (permute_rtrm7 pi t2)" - -lemma pt_rtrm7_zero: - fixes t::rtrm7 - shows "0 \ t = t" -apply(induct t) -apply(simp_all) -done - -lemma pt_rtrm7_plus: - fixes t::rtrm7 - shows "((p + q) \ t) = p \ (q \ t)" -apply(induct t) -apply(simp_all) -done - -instance -apply default -apply(simp_all add: pt_rtrm7_zero pt_rtrm7_plus) -done - -end +setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} +print_theorems inductive alpha7 :: "rtrm7 \ rtrm7 \ bool" ("_ \7 _" [100, 100] 100) @@ -1216,21 +967,8 @@ | "rfv_bar8 (Bar1 v x t) = {atom v} \ (rfv_bar8 t - {atom x})" print_theorems -instantiation - rfoo8 and rbar8 :: pt -begin - -primrec - permute_rfoo8 and permute_rbar8 -where - "permute_rfoo8 pi (Foo0 a) = Foo0 (pi \ a)" -| "permute_rfoo8 pi (Foo1 b t) = Foo1 (permute_rbar8 pi b) (permute_rfoo8 pi t)" -| "permute_rbar8 pi (Bar0 a) = Bar0 (pi \ a)" -| "permute_rbar8 pi (Bar1 v x t) = Bar1 (pi \ v) (pi \ x) (permute_rbar8 pi t)" - -instance sorry - -end +setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} +print_theorems inductive alpha8f :: "rfoo8 \ rfoo8 \ bool" ("_ \f _" [100, 100] 100) @@ -1286,20 +1024,8 @@ | "rfv_lam9 (Lam9 b t) = (rfv_lam9 t - {atom b})" | "rfv_bla9 (Bla9 l r) = (rfv_lam9 r - rbv9 l) \ rfv_lam9 l" -instantiation - rlam9 and rbla9 :: pt -begin - -primrec - permute_rlam9 and permute_rbla9 -where - "permute_rlam9 pi (Var9 a) = Var9 (pi \ a)" -| "permute_rlam9 pi (Lam9 b t) = Lam9 (pi \ b) (permute_rlam9 pi t)" -| "permute_rbla9 pi (Bla9 l r) = Bla9 (permute_rlam9 pi l) (permute_rlam9 pi r)" - -instance sorry - -end +setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} +print_theorems inductive alpha9l :: "rlam9 \ rlam9 \ bool" ("_ \9l _" [100, 100] 100) @@ -1380,70 +1106,14 @@ Var "name" | Fun "ty" "ty" -instantiation - ty :: pt -begin - -primrec - permute_ty -where - "permute_ty pi (Var a) = Var (pi \ a)" -| "permute_ty pi (Fun T1 T2) = Fun (permute_ty pi T1) (permute_ty pi T2)" - -lemma pt_ty_zero: - fixes T::ty - shows "0 \ T = T" -apply(induct T rule: ty.inducts) -apply(simp_all) -done - -lemma pt_ty_plus: - fixes T::ty - shows "((p + q) \ T) = p \ (q \ T)" -apply(induct T rule: ty.inducts) -apply(simp_all) -done - -instance -apply default -apply(simp_all add: pt_ty_zero pt_ty_plus) -done - -end +setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *} +print_theorems datatype tyS = All "name set" "ty" -instantiation - tyS :: pt -begin - -primrec - permute_tyS -where - "permute_tyS pi (All xs T) = All (pi \ xs) (pi \ T)" - -lemma pt_tyS_zero: - fixes T::tyS - shows "0 \ T = T" -apply(induct T rule: tyS.inducts) -apply(simp_all) -done - -lemma pt_tyS_plus: - fixes T::tyS - shows "((p + q) \ T) = p \ (q \ T)" -apply(induct T rule: tyS.inducts) -apply(simp_all) -done - -instance -apply default -apply(simp_all add: pt_tyS_zero pt_tyS_plus) -done - -end - +setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} +print_theorems abbreviation "atoms xs \ {atom x| x. x \ xs}"