# HG changeset patch # User Cezary Kaliszyk # Date 1266832659 -3600 # Node ID 9c968284553cda80cf563b8eae0c0df72b0c82b2 # Parent acbf50e8eac2900b3e91be9e0de82a1520ef835c Renaming. diff -r acbf50e8eac2 -r 9c968284553c Quot/Nominal/Fv.thy --- a/Quot/Nominal/Fv.thy Mon Feb 22 10:39:05 2010 +0100 +++ b/Quot/Nominal/Fv.thy Mon Feb 22 10:57:39 2010 +0100 @@ -90,6 +90,8 @@ *} +(* TODO: Notice datatypes without bindings and replace alpha with equality *) + ML {* (* Currently needs just one full_tname to access Datatype *) fun define_fv_alpha full_tname bindsall lthy = diff -r acbf50e8eac2 -r 9c968284553c Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Mon Feb 22 10:39:05 2010 +0100 +++ b/Quot/Nominal/Terms.thy Mon Feb 22 10:57:39 2010 +0100 @@ -342,86 +342,85 @@ section {*** lets with many assignments ***} -datatype trm3 = - Vr3 "name" -| Ap3 "trm3" "trm3" -| Lm3 "name" "trm3" --"bind (name) in (trm3)" -| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)" -and assigns = - ANil -| ACons "name" "trm3" "assigns" +datatype rtrm3 = + rVr3 "name" +| rAp3 "rtrm3" "rtrm3" +| rLm3 "name" "rtrm3" --"bind (name) in (trm3)" +| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)" +and rassigns = + rANil +| rACons "name" "rtrm3" "rassigns" (* to be given by the user *) primrec bv3 where - "bv3 ANil = {}" -| "bv3 (ACons x t as) = {atom x} \ (bv3 as)" + "bv3 rANil = {}" +| "bv3 (rACons x t as) = {atom x} \ (bv3 as)" -setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} +setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *} -local_setup {* snd o define_fv_alpha "Terms.trm3" +local_setup {* snd o define_fv_alpha "Terms.rtrm3" [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], [[], [[], [], []]]] *} print_theorems notation - alpha_trm3 ("_ \3 _" [100, 100] 100) and - alpha_assigns ("_ \3a _" [100, 100] 100) -thm alpha_trm3_alpha_assigns.intros + alpha_rtrm3 ("_ \3 _" [100, 100] 100) and + alpha_rassigns ("_ \3a _" [100, 100] 100) +thm alpha_rtrm3_alpha_rassigns.intros lemma alpha3_equivp: - "equivp alpha_trm3" - "equivp alpha_assigns" + "equivp alpha_rtrm3" + "equivp alpha_rassigns" sorry quotient_type - qtrm3 = trm3 / alpha_trm3 + trm3 = rtrm3 / alpha_rtrm3 and - qassigns = assigns / alpha_assigns + assigns = rassigns / alpha_rassigns by (auto intro: alpha3_equivp) section {*** lam with indirect list recursion ***} -datatype trm4 = - Vr4 "name" -| Ap4 "trm4" "trm4 list" -| Lm4 "name" "trm4" --"bind (name) in (trm)" -print_theorems +datatype rtrm4 = + rVr4 "name" +| rAp4 "rtrm4" "rtrm4 list" +| rLm4 "name" "rtrm4" --"bind (name) in (trm)" -thm trm4.recs +thm rtrm4.recs (* there cannot be a clause for lists, as *) (* permutations are already defined in Nominal (also functions, options, and so on) *) -setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *} +setup {* snd o define_raw_perms ["rtrm4"] ["Terms.rtrm4"] *} (* "repairing" of the permute function *) lemma repaired: - fixes ts::"trm4 list" - shows "permute_trm4_list p ts = p \ ts" + fixes ts::"rtrm4 list" + shows "permute_rtrm4_list p ts = p \ ts" apply(induct ts) apply(simp_all) done -thm permute_trm4_permute_trm4_list.simps -thm permute_trm4_permute_trm4_list.simps[simplified repaired] +thm permute_rtrm4_permute_rtrm4_list.simps +thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] -local_setup {* snd o define_fv_alpha "Terms.trm4" [ +local_setup {* snd o define_fv_alpha "Terms.rtrm4" [ [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} print_theorems notation - alpha_trm4 ("_ \4 _" [100, 100] 100) and - alpha_trm4_list ("_ \4l _" [100, 100] 100) -thm alpha_trm4_alpha_trm4_list.intros + alpha_rtrm4 ("_ \4 _" [100, 100] 100) and + alpha_rtrm4_list ("_ \4l _" [100, 100] 100) +thm alpha_rtrm4_alpha_rtrm4_list.intros -lemma alpha4_equivp: "equivp alpha_trm4" sorry -lemma alpha4list_equivp: "equivp alpha_trm4_list" sorry +lemma alpha4_equivp: "equivp alpha_rtrm4" sorry +lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry quotient_type - qtrm4 = trm4 / alpha_trm4 and - qtrm4list = "trm4 list" / alpha_trm4_list + qrtrm4 = rtrm4 / alpha_rtrm4 and + qrtrm4list = "rtrm4 list" / alpha_rtrm4_list by (simp_all add: alpha4_equivp alpha4list_equivp)