# HG changeset patch # User Cezary Kaliszyk # Date 1271838048 -7200 # Node ID 72cdd2af7eb4419c4ba676f80f77eec9a357b957 # Parent c50601bc617e2ae61aa73e01cfbd48d9817d6fc1# Parent 39951d71bfceb3640b8908f74d8887ffa3f73bd1 merge diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/Abs.thy --- a/Nominal/Abs.thy Wed Apr 21 10:13:17 2010 +0200 +++ b/Nominal/Abs.thy Wed Apr 21 10:20:48 2010 +0200 @@ -423,15 +423,50 @@ apply(simp) done - +lemma + fixes t1 s1::"'a::fs" + and t2 s2::"'b::fs" + shows "Abs as (t1, t2) = Abs bs (s1, s2) \ (Abs as t1 = Abs bs s1 \ Abs as t2 = Abs bs s2)" +apply(subst abs_eq_iff) +apply(subst alphas_abs) +apply(subst alphas) +apply(rule impI) +apply(erule exE) +apply(simp add: supp_Pair) +apply(simp add: Un_Diff) +apply(simp add: fresh_star_union) +apply(erule conjE)+ +apply(rule conjI) +apply(rule trans) +apply(rule sym) +apply(rule_tac p="p" in supp_perm_eq) +apply(simp add: supp_abs) +apply(simp) +apply(rule trans) +apply(rule sym) +apply(rule_tac p="p" in supp_perm_eq) +apply(simp add: supp_abs) +apply(simp) +done -(* support of concrete atom sets *) +lemma fresh_star_eq: + assumes a: "as \* p" + shows "\a \ as. p \ a = a" +using a by (simp add: fresh_star_def fresh_def supp_perm) + +lemma fresh_star_set_eq: + assumes a: "as \* p" + shows "p \ as = as" +using a +apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq) +apply(auto) +by (metis permute_atom_def) lemma fixes t1 s1::"'a::fs" and t2 s2::"'b::fs" assumes asm: "finite as" - shows "(Abs as t1 = Abs as s1 \ Abs as t2 = Abs as s2) \ Abs as (t1, t2) = Abs as (s1, s2)" + shows "(Abs as t1 = Abs bs s1 \ Abs as t2 = Abs bs s2) \ Abs as (t1, t2) = Abs bs (s1, s2)" apply(subst abs_eq_iff) apply(subst abs_eq_iff) apply(subst alphas_abs) diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/Ex/Ex1.thy --- a/Nominal/Ex/Ex1.thy Wed Apr 21 10:13:17 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ -theory Ex1 -imports "../Parser" -begin - -text {* example 1, equivalent to example 2 from Terms *} - -atom_decl name - -ML {* val _ = recursive := false *} -nominal_datatype lam = - VAR "name" -| APP "lam" "lam" -| LAM x::"name" t::"lam" bind x in t -| LET bp::"bp" t::"lam" bind "bi bp" in t -and bp = - BP "name" "lam" -binder - bi::"bp \ atom set" -where - "bi (BP x t) = {atom x}" - -thm lam_bp.fv -thm lam_bp.supp -thm lam_bp.eq_iff -thm lam_bp.bn -thm lam_bp.perm -thm lam_bp.induct -thm lam_bp.inducts -thm lam_bp.distinct -ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} -thm lam_bp.fv[simplified lam_bp.supp] - -end - - - diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/Ex/SingleLet.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/SingleLet.thy Wed Apr 21 10:20:48 2010 +0200 @@ -0,0 +1,38 @@ +theory SingleLet +imports "../Parser" +begin + +atom_decl name + +ML {* val _ = recursive := false *} + +nominal_datatype trm = + Var "name" +| App "trm" "trm" +| Lam x::"name" t::"trm" bind x in t +| Let a::"assg" t::"trm" bind "bn a" in t +and assg = + As "name" "trm" +binder + bn::"assg \ atom set" +where + "bn (As x t) = {atom x}" + +print_theorems +thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] + +thm trm_assg.fv +thm trm_assg.supp +thm trm_assg.eq_iff[simplified alphas_abs[symmetric]] +thm trm_assg.bn +thm trm_assg.perm +thm trm_assg.induct +thm trm_assg.inducts +thm trm_assg.distinct +ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} +thm trm_assg.fv[simplified trm_assg.supp] + +end + + + diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/FSet.thy --- a/Nominal/FSet.thy Wed Apr 21 10:13:17 2010 +0200 +++ b/Nominal/FSet.thy Wed Apr 21 10:20:48 2010 +0200 @@ -614,7 +614,7 @@ have "fcard_raw l = 0" by fact then have "\x. \ memb x l" using memb_card_not_0[of _ l] by auto then have z: "l = []" using no_memb_nil by auto - then have "r = []" sorry + then have "r = []" using `l \ r` by simp then show ?case using z list_eq2_refl by simp next case (Suc m) diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/Fv.thy --- a/Nominal/Fv.thy Wed Apr 21 10:13:17 2010 +0200 +++ b/Nominal/Fv.thy Wed Apr 21 10:20:48 2010 +0200 @@ -137,7 +137,7 @@ *) ML {* -datatype alpha_type = AlphaGen | AlphaRes | AlphaLst; +datatype alpha_mode = AlphaGen | AlphaRes | AlphaLst; *} ML {* diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/Parser.thy --- a/Nominal/Parser.thy Wed Apr 21 10:13:17 2010 +0200 +++ b/Nominal/Parser.thy Wed Apr 21 10:20:48 2010 +0200 @@ -296,14 +296,19 @@ Parser.thy/raw_nominal_decls 1) define the raw datatype - 2) define the raw binding functions + 2) define the raw binding functions + Perm.thy/define_raw_perms - 3) define permutations of the raw datatype and show that raw type is in the pt typeclass + 3) define permutations of the raw datatype and show that the raw type is + in the pt typeclass + Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha 4) define fv and fv_bn 5) define alpha and alpha_bn + Perm.thy/distinct_rel 6) prove alpha_distincts (C1 x \ C2 y ...) (Proof by cases; simp) + Tacs.thy/build_rel_inj 6) prove alpha_eq_iff (C1 x = C2 y \ P x y ...) (left-to-right by intro rule, right-to-left by cases; simp) diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/Perm.thy --- a/Nominal/Perm.thy Wed Apr 21 10:13:17 2010 +0200 +++ b/Nominal/Perm.thy Wed Apr 21 10:20:48 2010 +0200 @@ -2,56 +2,11 @@ imports "../Nominal-General/Nominal2_Atoms" begin +(* definitions of the permute function for raw nominal datatypes *) ML {* -fun prove_perm_zero lthy induct perm_def perm_frees = -let - val perm_types = map fastype_of perm_frees; - val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); - fun glc ((perm, T), x) = - HOLogic.mk_eq (perm $ @{term "0::perm"} $ Free (x, T), Free (x, T)) - val gl = - HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))); - fun tac _ = - EVERY [ - Datatype_Aux.indtac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) - ]; -in - Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) -end; -*} - -ML {* -fun prove_perm_plus lthy induct perm_def perm_frees = -let - val pi1 = Free ("pi1", @{typ perm}); - val pi2 = Free ("pi2", @{typ perm}); - val perm_types = map fastype_of perm_frees - val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); - fun glc ((perm, T), x) = - HOLogic.mk_eq ( - perm $ (mk_plus pi1 pi2) $ Free (x, T), - perm $ pi1 $ (perm $ pi2 $ Free (x, T))) - val goal = - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) - fun tac _ = - EVERY [ - Datatype_Aux.indtac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) - ] -in - Datatype_Aux.split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] goal tac) -end; -*} - - -(* definitions of the permute function for a raw nominal datatype *) - -ML {* +(* returns the type of the nth datatype *) fun nth_dtyp dt_descr sorts i = Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); *} @@ -93,8 +48,59 @@ *} ML {* +fun prove_permute_zero lthy induct perm_defs perm_fns = +let + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = Datatype_Prop.make_tnames perm_types + + fun single_goal ((perm_fn, T), x) = + HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) + + val goals = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) + + val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) + + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 +in + Goal.prove lthy perm_indnames [] goals (K tac) + |> Datatype_Aux.split_conj_thm +end +*} + +ML {* +fun prove_permute_plus lthy induct perm_defs perm_fns = +let + val pi1 = Free ("p", @{typ perm}) + val pi2 = Free ("q", @{typ perm}) + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = Datatype_Prop.make_tnames perm_types + + fun single_goal ((perm, T), x) = HOLogic.mk_eq + (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T))) + + val goals = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) + + val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) + + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 +in + Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) + |> Datatype_Aux.split_conj_thm +end +*} + +ML {* (* defines the permutation functions for raw datatypes and proves that they are instances of pt + + dt_nos refers to the number of "un-unfolded" datatypes + given by the user *) fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy = let @@ -117,12 +123,12 @@ val lthy = Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; - val ((perm_frees, perm_ldef), lthy') = + val ((perm_fns, perm_ldef), lthy') = Primrec.add_primrec (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; - val perm_zero_thms = prove_perm_zero lthy' induct perm_ldef perm_frees - val perm_plus_thms = prove_perm_plus lthy' induct perm_ldef perm_frees + val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns + val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns val perm_zero_thms' = List.take (perm_zero_thms, dt_nos); val perm_plus_thms' = List.take (perm_plus_thms, dt_nos) val perms_name = space_implode "_" perm_fn_names @@ -130,42 +136,20 @@ val perms_plus_bind = Binding.name (perms_name ^ "_plus") fun tac _ (_, simps, _) = - (Class.intro_classes_tac []) THEN ALLGOALS (resolve_tac simps); + Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) fun morphism phi (dfs, simps, fvs) = (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); - in - lthy' - |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) - |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) - |> Class_Target.prove_instantiation_exit_result morphism tac - (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_frees) - end -*} - -(* Test *) -(*atom_decl name - -datatype trm = - Var "name" -| App "trm" "trm list" -| Lam "name" "trm" -| Let "bp" "trm" "trm" -and bp = - BUnit -| BVar "name" -| BPair "bp" "bp" - -setup {* fn thy => -let - val info = Datatype.the_info thy "Perm.trm" in - define_raw_perms info 2 thy |> snd + lthy' + |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) + |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) + |> Class_Target.prove_instantiation_exit_result morphism tac + (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns) end *} -print_theorems -*) +(* permutations for quotient types *) ML {* fun quotient_lift_consts_export qtys spec ctxt = @@ -228,11 +212,12 @@ (* Test *) -(*atom_decl name +(* +atom_decl name datatype trm = Var "name" -| App "trm" "trm list" +| App "trm" "(trm list) list" | Lam "name" "trm" | Let "bp" "trm" "trm" and bp = @@ -242,9 +227,9 @@ setup {* fn thy => let - val inf = Datatype.the_info thy "Perm.trm" + val info = Datatype.the_info thy "Perm.trm" in - define_raw_perms inf 2 thy |> snd + define_raw_perms info 2 thy |> snd end *} diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Wed Apr 21 10:13:17 2010 +0200 +++ b/Nominal/ROOT.ML Wed Apr 21 10:20:48 2010 +0200 @@ -3,7 +3,7 @@ no_document use_thys ["Ex/Lambda", "Ex/ExLF", - "Ex/Ex1", + "Ex/SingleLet", "Ex/Ex1rec", "Ex/Ex2", "Ex/Ex3",