# HG changeset patch # User Christian Urban # Date 1283011785 -28800 # Node ID b9d9c45402653c560aa0b8832c722580553b12de # Parent 76be909eaf048f2bed22ea7ca4651aab8cf2319e proved supports lemmas diff -r 76be909eaf04 -r b9d9c4540265 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Sat Aug 28 18:15:23 2010 +0800 +++ b/Nominal-General/nominal_library.ML Sun Aug 29 00:09:45 2010 +0800 @@ -33,6 +33,10 @@ val mk_supp_ty: typ -> term -> term val mk_supp: term -> term + val supports_const: typ -> term + val mk_supports_ty: typ -> term -> term -> term + val mk_supports: term -> term -> term + val mk_equiv: thm -> thm val safe_mk_equiv: thm -> thm @@ -43,6 +47,9 @@ val mk_conj: term * term -> term val fold_conj: term list -> term + (* fresh arguments for a term *) + val fresh_args: Proof.context -> term -> term list + (* datatype operations *) type cns_info = (term * typ * typ list * bool list) list @@ -114,6 +121,9 @@ fun mk_supp_ty ty t = supp_const ty $ t; fun mk_supp t = mk_supp_ty (fastype_of t) t; +fun supports_const ty = Const (@{const_name "supports"}, [@{typ "atom set"}, ty] ---> @{typ bool}); +fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; +fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; fun mk_equiv r = r RS @{thm eq_reflection}; fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; @@ -142,6 +152,18 @@ fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} + +(* produces fresh arguments for a term *) + +fun fresh_args ctxt f = + f |> fastype_of + |> binder_types + |> map (pair "z") + |> Variable.variant_frees ctxt [f] + |> map Free + + + (** datatypes **) (* constructor infos *) diff -r 76be909eaf04 -r b9d9c4540265 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sat Aug 28 18:15:23 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Sun Aug 29 00:09:45 2010 +0800 @@ -21,6 +21,8 @@ where "bn (As x y t) = {atom x}" +thm Ball_def Bex_def mem_def + thm single_let.distinct thm single_let.induct thm single_let.exhaust @@ -30,19 +32,88 @@ thm single_let.eq_iff thm single_let.fv_bn_eqvt thm single_let.size_eqvt - +thm single_let.supports -(* +lemma test: + "finite (supp (t::trm)) \ finite (supp (a::assg))" +apply(rule single_let.induct) +apply(rule supports_finite) +apply(rule single_let.supports) +apply(simp only: finite_supp supp_Pair finite_Un) +apply(rule supports_finite) +apply(rule single_let.supports) +apply(simp only: finite_supp supp_Pair finite_Un, simp) +apply(rule supports_finite) +apply(rule single_let.supports) +apply(simp only: finite_supp supp_Pair finite_Un, simp) +apply(rule supports_finite) +apply(rule single_let.supports) +apply(simp only: finite_supp supp_Pair finite_Un, simp) +apply(rule supports_finite) +apply(rule single_let.supports) +apply(simp only: finite_supp supp_Pair finite_Un, simp) +apply(rule supports_finite) +apply(rule single_let.supports) +apply(simp only: finite_supp supp_Pair finite_Un, simp) +apply(rule supports_finite) +apply(rule single_let.supports) +apply(simp only: finite_supp supp_Pair finite_Un, simp) +apply(rule supports_finite) +apply(rule single_let.supports) +apply(simp only: finite_supp supp_Pair finite_Un, simp) +done + +instantiation trm and assg :: fs +begin + +instance +apply(default) +apply(simp_all add: test) +done + +end + + +lemma test: + "(\p. (bs, x) \lst (op=) f p (cs, y)) \ (\p. (bs, x) \lst (op=) supp p (cs, y))" +oops + +lemma Abs_eq_iff: + shows "Abs bs x = Abs cs y \ (\p. (bs, x) \gen (op =) supp p (cs, y))" + and "Abs_res bs x = Abs_res cs y \ (\p. (bs, x) \res (op =) supp p (cs, y))" + and "Abs_lst bsl x = Abs_lst csl y \ (\p. (bsl, x) \lst (op =) supp p (csl, y))" + by (lifting alphas_abs) + +(* lemma supp_fv: - "supp t = fv_trm t" - "supp b = fv_bn b" -apply(induct t and b rule: i1) -apply(simp_all add: f1) -apply(simp_all add: supp_def) -apply(simp_all add: b1) + "supp t = fv_trm t \ supp b = fv_bn b" +apply(rule single_let.induct) +apply(simp_all only: single_let.fv_defs)[2] +apply(simp_all only: supp_def)[2] +apply(simp_all only: single_let.perm_simps)[2] +apply(simp_all only: single_let.eq_iff)[2] +apply(simp_all only: de_Morgan_conj)[2] +apply(simp_all only: Collect_disj_eq)[2] +apply(simp_all only: finite_Un)[2] +apply(simp_all only: de_Morgan_conj)[2] +apply(simp_all only: Collect_disj_eq)[2] +apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)") +apply(simp only: single_let.fv_defs) +apply(simp only: supp_abs) +apply(simp (no_asm) only: supp_def) +apply(simp only: single_let.perm_simps) +apply(simp only: single_let.eq_iff) +apply(subst test) +apply(simp only: Abs_eq_iff[symmetric]) +apply(simp only: alphas_abs[symmetric]) +apply(simp only: eqvts) +thm Abs_eq_iff +apply(simp only: alphas) sorry +*) +(* consts perm_bn_trm :: "perm \ trm \ trm" consts perm_bn_assg :: "perm \ assg \ assg" diff -r 76be909eaf04 -r b9d9c4540265 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sat Aug 28 18:15:23 2010 +0800 +++ b/Nominal/NewParser.thy Sun Aug 29 00:09:45 2010 +0800 @@ -9,6 +9,7 @@ ("nominal_dt_rawfuns.ML") ("nominal_dt_alpha.ML") ("nominal_dt_quot.ML") + ("nominal_dt_supp.ML") begin use "nominal_dt_rawperm.ML" @@ -23,13 +24,16 @@ use "nominal_dt_quot.ML" ML {* open Nominal_Dt_Quot *} +use "nominal_dt_supp.ML" +ML {* open Nominal_Dt_Supp *} section{* Interface for nominal_datatype *} ML {* (* attributes *) -val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) -val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add) +val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) +val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) +val simp_attr = Attrib.internal (K Simplifier.simp_add) *} @@ -300,7 +304,7 @@ else raise TEST lthy0 (* noting the raw permutations as eqvt theorems *) - val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a + val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a (* definition of raw fv_functions *) val _ = warning "Definition of raw fv-functions"; @@ -345,7 +349,7 @@ else raise TEST lthy4 (* noting the raw_bn_eqvt lemmas in a temprorary theory *) - val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_bn_eqvt) lthy4) + val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4) val raw_fv_eqvt = if get_STEPS lthy > 7 @@ -361,7 +365,7 @@ |> map (fn thm => thm RS @{thm sym}) else raise TEST lthy4 - val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_fv_eqvt) lthy_tmp) + val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) val (alpha_eqvt, lthy6) = if get_STEPS lthy > 9 @@ -440,7 +444,7 @@ (* noting the quot_respects lemmas *) val (_, lthy6a) = if get_STEPS lthy > 21 - then Local_Theory.note ((Binding.empty, [rsp_attrib]), + then Local_Theory.note ((Binding.empty, [rsp_attr]), raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 else raise TEST lthy6 @@ -503,7 +507,7 @@ then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 else raise TEST lthy9 - val qconstrs = map #qconst qconstrs_info + val qtrms = map #qconst qconstrs_info val qbns = map #qconst qbns_info val qfvs = map #qconst qfvs_info val qfv_bns = map #qconst qfv_bns_info @@ -536,6 +540,14 @@ ||>> lift_thms qtys [] raw_exhaust_thms else raise TEST lthyA + (* Supports lemmas *) + + val qsupports_thms = + if get_STEPS lthy > 28 + then prove_supports lthyB qperm_simps qtrms + else raise TEST lthyB + + (* noting the theorems *) (* generating the prefix for the theorem names *) @@ -548,11 +560,12 @@ ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) - ||>> Local_Theory.note ((thms_suffix "perm_simps", []), qperm_simps) + ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) + ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) in (0, lthy9') diff -r 76be909eaf04 -r b9d9c4540265 Nominal/nominal_dt_supp.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_supp.ML Sun Aug 29 00:09:45 2010 +0800 @@ -0,0 +1,57 @@ +(* Title: nominal_dt_alpha.ML + Author: Christian Urban + Author: Cezary Kaliszyk + + Deriving support propoerties for the quotient types. +*) + +signature NOMINAL_DT_SUPP = +sig + val prove_supports: Proof.context -> thm list -> term list -> thm list + +end + +structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = +struct + + +(* supports lemmas *) + +fun mk_supports_goal ctxt qtrm = +let + val vs = fresh_args ctxt qtrm + val rhs = list_comb (qtrm, vs) + val lhs = mk_supp (foldl1 HOLogic.mk_prod vs) +in + mk_supports lhs rhs + |> HOLogic.mk_Trueprop +end + +fun supports_tac ctxt perm_simps = +let + val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} + val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} +in + EVERY' [ simp_tac ss1, + Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], + simp_tac ss2 ] +end + +fun prove_supports_single ctxt perm_simps qtrm = +let + val goal = mk_supports_goal ctxt qtrm + val ctxt' = Variable.auto_fixes goal ctxt +in + Goal.prove ctxt' [] [] goal + (K (HEADGOAL (supports_tac ctxt perm_simps))) + |> singleton (ProofContext.export ctxt' ctxt) +end + +fun prove_supports ctxt perm_simps qtrms = + map (prove_supports_single ctxt perm_simps) qtrms + + + + +end (* structure *) +