# HG changeset patch # User Cezary Kaliszyk # Date 1267189063 -3600 # Node ID 6eacf60ce41d6759f9be097b73bb7bfdb0c8308a # Parent 3365fce80f0f379e499603943781e6f755e49615 Permutation and FV_Alpha interface change. diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Fv.thy --- a/Nominal/Fv.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Fv.thy Fri Feb 26 13:57:43 2010 +0100 @@ -92,12 +92,10 @@ (* 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 = +fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = let val thy = ProofContext.theory_of lthy; - val {descr, ...} = Datatype.the_info thy full_tname; - val sorts = []; (* TODO *) + val {descr, sorts, ...} = dt_info; fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => "fv_" ^ name_of_typ (nth_dtyp i)) descr); diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/LFex.thy --- a/Nominal/LFex.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/LFex.thy Fri Feb 26 13:57:43 2010 +0100 @@ -19,11 +19,11 @@ | Lam "rty" "name" "rtrm" -setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "LFex.rkind") 3 *} print_theorems local_setup {* - snd o define_fv_alpha "LFex.rkind" + snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind") [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Lift.thy --- a/Nominal/Lift.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Lift.thy Fri Feb 26 13:57:43 2010 +0100 @@ -7,7 +7,7 @@ datatype rtrm2 = rVr2 "name" -| rAp2 "rtrm2" "rtrm2" +| rAp2 "rtrm2" "rtrm2 list" | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)" and ras = rAs "name" "rtrm2" @@ -45,6 +45,10 @@ [[[], []]] (*, [[], [[], []]] *) ]; val bv_simps = @{thms rbv2.simps} val info = Datatype.the_info @{theory} ftname; +*} + +. +{* val descr = #descr info; val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; val full_tnames = List.take (all_full_tnames, length tnames); diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Perm.thy --- a/Nominal/Perm.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Perm.thy Fri Feb 26 13:57:43 2010 +0100 @@ -54,12 +54,11 @@ *} ML {* -(* TODO: full_name can be obtained from new_type_names with Datatype *) -fun define_raw_perms new_type_names full_tnames thy = +fun define_raw_perms (dt_info : info) number thy = let - val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames); - (* TODO: [] should be the sorts that we'll take from the specification *) - val sorts = []; + val {descr, induct, sorts, ...} = dt_info; + val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; + val full_tnames = List.take (all_full_tnames, number); fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => "permute_" ^ name_of_typ (nth_dtyp i)) descr); @@ -101,8 +100,8 @@ val ((perm_frees, perm_ldef), lthy') = Primrec.add_primrec (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; - val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); - val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) + val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number); + val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number) val perms_name = space_implode "_" perm_names' val perms_zero_bind = Binding.name (perms_name ^ "_zero") val perms_append_bind = Binding.name (perms_name ^ "_append") diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term1.thy --- a/Nominal/Term1.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Term1.thy Fri Feb 26 13:57:43 2010 +0100 @@ -27,11 +27,11 @@ | "bv1 (BVr x) = {atom x}" | "bv1 (BPr bp1 bp2) = (bv1 bp1) \ (bv1 bp2)" -setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Term1.rtrm1", "Term1.bp"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} thm permute_rtrm1_permute_bp.simps local_setup {* - snd o define_fv_alpha "Term1.rtrm1" + snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], [[], [[]], [[], []]]] *} diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term2.thy --- a/Nominal/Term2.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Term2.thy Fri Feb 26 13:57:43 2010 +0100 @@ -20,9 +20,9 @@ where "rbv2 (rAs x t) = {atom x}" -setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Term2.rtrm2", "Term2.rassign"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *} -local_setup {* snd o define_fv_alpha "Term2.rtrm2" +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2") [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], [[[], []]]] *} diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term3.thy --- a/Nominal/Term3.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Term3.thy Fri Feb 26 13:57:43 2010 +0100 @@ -22,9 +22,9 @@ "bv3 rANil = {}" | "bv3 (rACons x t as) = {atom x} \ (bv3 as)" -setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Term3.rtrm3", "Term3.rassigns"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term3.rtrm3") 2 *} -local_setup {* snd o define_fv_alpha "Term3.rtrm3" +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term3.rtrm3") [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], [[], [[], [], []]]] *} print_theorems diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term4.thy --- a/Nominal/Term4.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Term4.thy Fri Feb 26 13:57:43 2010 +0100 @@ -16,7 +16,7 @@ (* 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 ["rtrm4"] ["Term4.rtrm4"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *} (* "repairing" of the permute function *) lemma repaired: @@ -29,8 +29,8 @@ thm permute_rtrm4_permute_rtrm4_list.simps thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] -local_setup {* snd o define_fv_alpha "Term4.rtrm4" [ - [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") + [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} print_theorems notation diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term5.thy --- a/Nominal/Term5.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Term5.thy Fri Feb 26 13:57:43 2010 +0100 @@ -19,10 +19,10 @@ | "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" -setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Term5.rtrm5", "Term5.rlts"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} print_theorems -local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} print_theorems diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term6.thy --- a/Nominal/Term6.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Term6.thy Fri Feb 26 13:57:43 2010 +0100 @@ -18,10 +18,10 @@ | "rbv6 (rLm6 n t) = {atom n} \ rbv6 t" | "rbv6 (rLt6 l r) = rbv6 l \ rbv6 r" -setup {* snd o define_raw_perms ["rtrm6"] ["Term6.rtrm6"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term6.rtrm6") 1 *} print_theorems -local_setup {* snd o define_fv_alpha "Term6.rtrm6" [ +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [ [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} notation alpha_rtrm6 ("_ \6 _" [100, 100] 100) thm alpha_rtrm6.intros diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term7.thy --- a/Nominal/Term7.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Term7.thy Fri Feb 26 13:57:43 2010 +0100 @@ -18,10 +18,10 @@ | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" | "rbv7 (rLt7 l r) = rbv7 l \ rbv7 r" -setup {* snd o define_raw_perms ["rtrm7"] ["Term7.rtrm7"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term7.rtrm7") 1 *} thm permute_rtrm7.simps -local_setup {* snd o define_fv_alpha "Term7.rtrm7" [ +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term7.rtrm7") [ [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} print_theorems notation diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term8.thy --- a/Nominal/Term8.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Term8.thy Fri Feb 26 13:57:43 2010 +0100 @@ -17,10 +17,10 @@ "rbv8 (Bar0 x) = {}" | "rbv8 (Bar1 v x b) = {atom v}" -setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Term8.rfoo8", "Term8.rbar8"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *} print_theorems -local_setup {* snd o define_fv_alpha "Term8.rfoo8" [ +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [ [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} notation alpha_rfoo8 ("_ \f' _" [100, 100] 100) and diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term9.thy --- a/Nominal/Term9.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/Term9.thy Fri Feb 26 13:57:43 2010 +0100 @@ -16,10 +16,10 @@ "rbv9 (Var9 x) = {}" | "rbv9 (Lam9 x b) = {atom x}" -setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Term9.rlam9", "Term9.rbla9"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term9.rlam9") 2 *} print_theorems -local_setup {* snd o define_fv_alpha "Term9.rlam9" [ +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term9.rlam9") [ [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} notation alpha_rlam9 ("_ \9l' _" [100, 100] 100) and diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/TySch.thy --- a/Nominal/TySch.thy Fri Feb 26 10:34:04 2010 +0100 +++ b/Nominal/TySch.thy Fri Feb 26 13:57:43 2010 +0100 @@ -9,21 +9,22 @@ Var "name" | Fun "ty" "ty" -setup {* snd o define_raw_perms ["ty"] ["TySch.ty"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.ty") 1 *} print_theorems datatype tyS = All "name set" "ty" -setup {* snd o define_raw_perms ["tyS"] ["TySch.tyS"] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *} print_theorems -local_setup {* snd o define_fv_alpha "TySch.ty" [[[[]], [[], []]]] *} +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty") + [[[[]], [[], []]]] *} print_theorems (* Doesnot work yet since we do not refer to fv_ty -local_setup {* define_raw_fv "TySch.tyS" [[[[], []]]] *} +local_setup {* define_raw_fv (Datatype.the_info @{theory} "TySch.tyS") [[[[], []]]] *} print_theorems *)