# HG changeset patch # User Christian Urban # Date 1268056886 -3600 # Node ID 226693549aa0a8214655ff9606ed7a744452458f # Parent f00761b5957ed5b7d1f33e8819004305385992c6# Parent e72d9d9eada309bf4a12eb73c586d2fb8bf7a465 merged diff -r f00761b5957e -r 226693549aa0 Nominal/Fv.thy --- a/Nominal/Fv.thy Mon Mar 08 15:01:01 2010 +0100 +++ b/Nominal/Fv.thy Mon Mar 08 15:01:26 2010 +0100 @@ -2,14 +2,15 @@ imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" begin -(* Bindings are given as a list which has a length being equal - to the length of the number of constructors. +(* Bindings are a list of lists of lists of triples. - Each element is a list whose length is equal to the number - of arguents. + The first list represents the datatypes defined. + The second list represents the constructors. + The internal list is a list of all the bndings that + concern the constructor. - Every element specifies bindings of this argument given as - a tuple: function, bound argument. + Every triple consists of a function, the binding and + the body. Eg: nominal_datatype @@ -21,12 +22,12 @@ yields: [ [], - [[], [], [(NONE, 0)]], - [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] + [(NONE, 0, 2)], + [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]] -A SOME binding has to have a function returning an atom set, -and a NONE binding has to be on an argument that is an atom -or an atom set. +A SOME binding has to have a function which takes an appropriate +argument and returns an atom set. A NONE binding has to be on an +argument that is an atom or an atom set. How the procedure works: For each of the defined datatypes, @@ -52,15 +53,50 @@ (* TODO: This one is not implemented *) For other arguments it should be an appropriate fv function stored in the database. + + For every argument that is a binding, we add a the same binding in its + body. *) ML {* +fun is_atom thy typ = + Sign.of_sort thy (typ, @{sort at}) +*} + + +(* Like map2, only if the second list is empty passes empty lists insted of error *) +ML {* fun map2i _ [] [] = [] | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys | map2i f (x :: xs) [] = f x [] :: map2i f xs [] | map2i _ _ _ = raise UnequalLengths; *} +(* Finds bindings with the same function and binding, and gathers all + bodys for such pairs *) +ML {* +fun gather_binds binds = +let + fun gather_binds_cons binds = + let + val common = map (fn (f, bi, _) => (f, bi)) binds + val nodups = distinct (op =) common + fun find_bodys (sf, sbi) = + filter (fn (f, bi, _) => f = sf andalso bi = sbi) binds + val bodys = map ((map (fn (_, _, bo) => bo)) o find_bodys) nodups + in + nodups ~~ bodys + end +in + map (map gather_binds_cons) binds +end +*} + +ML {* +fun un_gather_binds_cons binds = + flat (map (fn (((f, bi), bos), pi) => map (fn bo => ((f, bi, bo), pi)) bos) binds) +*} + ML {* open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); (* TODO: It is the same as one in 'nominal_atoms' *) @@ -110,7 +146,6 @@ ML {* fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = let - val thy = ProofContext.theory_of lthy; 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, _) => @@ -128,7 +163,9 @@ val pi_strs_same = replicate bindslen "pi" val pi_strs = Name.variant_list [] pi_strs_same; val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; - val bind_pis = bindcs ~~ pis; + val bind_pis_gath = bindcs ~~ pis; + val bind_pis = un_gather_binds_cons bind_pis_gath; + val bindcs = map fst bind_pis; val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); val args = map Free (names ~~ Ts); val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); @@ -178,14 +215,14 @@ val rhs = mk_pair (rhs_binds, arg2); val alpha = nth alpha_frees (body_index dt); val fv = nth fv_frees (body_index dt); - val pi = foldr1 add_perm rpis; + val pi = foldr1 add_perm (distinct (op =) rpis); val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; val alpha_gen = Syntax.check_term lthy alpha_gen_pre - val pi_supps = map ((curry op $) @{term "supp :: perm \ atom set"}) rpis; - val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) +(* val pi_supps = map ((curry op $) @{term "supp :: perm \ atom set"}) rpis; + val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) in - (*if length pi_supps > 1 then - HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen + (*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) + alpha_gen (* TODO Add some test that is makes sense *) end else @{term "True"} end @@ -198,7 +235,7 @@ (fv_eq, alpha_eq) end; fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; - val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall)) + val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr (gather_binds bindsall))) val add_binds = map (fn x => (Attrib.empty_binding, x)) val (fvs, lthy') = (Primrec.add_primrec (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) @@ -236,7 +273,7 @@ (* to be given by the user *) -primrec +primrec bv1 where "bv1 (BUnit) = {}" diff -r f00761b5957e -r 226693549aa0 Nominal/LFex.thy --- a/Nominal/LFex.thy Mon Mar 08 15:01:01 2010 +0100 +++ b/Nominal/LFex.thy Mon Mar 08 15:01:26 2010 +0100 @@ -5,7 +5,7 @@ atom_decl name atom_decl ident -ML {* restricted_nominal := false *} +ML {* restricted_nominal := 2 *} nominal_datatype kind = Type diff -r f00761b5957e -r 226693549aa0 Nominal/Parser.thy --- a/Nominal/Parser.thy Mon Mar 08 15:01:01 2010 +0100 +++ b/Nominal/Parser.thy Mon Mar 08 15:01:26 2010 +0100 @@ -223,7 +223,7 @@ end *} -ML {* val restricted_nominal=ref true *} +ML {* val restricted_nominal=ref 0 *} ML {* fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = @@ -269,7 +269,7 @@ val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc in -if !restricted_nominal then +if !restricted_nominal = 0 then ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) else let @@ -299,6 +299,11 @@ typ_of_dtyp descr sorts (DtRec i))) l) descr); val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; val (consts, const_defs) = split_list consts_defs; +in +if !restricted_nominal = 1 then + ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8) +else +let val (bns_rsp_pre, lthy9) = fold_map ( fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; @@ -341,6 +346,7 @@ ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20) end end +end *} ML {* diff -r f00761b5957e -r 226693549aa0 Nominal/Term1.thy --- a/Nominal/Term1.thy Mon Mar 08 15:01:01 2010 +0100 +++ b/Nominal/Term1.thy Mon Mar 08 15:01:26 2010 +0100 @@ -232,6 +232,7 @@ apply(simp only: Un_commute) apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) apply(simp only: Collect_disj_eq[symmetric] inf_or) +apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric]) sorry lemma supp_fv: diff -r f00761b5957e -r 226693549aa0 Nominal/Term5a.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term5a.thy Mon Mar 08 15:01:26 2010 +0100 @@ -0,0 +1,38 @@ +theory Term5 +imports "Parser" +begin + +atom_decl name + +ML {* restricted_nominal := 2 *} + +nominal_datatype trm5 = + Vr5 "name" +| Ap5 "trm5" "trm5" +| Lt5 l::"lts" t::"trm5" bind "bv5 l" in t +and lts = + Lnil +| Lcons "name" "trm5" "lts" +binder + bv5 +where + "bv5 Lnil = {}" +| "bv5 (Lcons n t ltl) = {atom n} \ (bv5 ltl)" + +lemma lets_ok: + "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" +apply (simp add: trm5_lts_inject) +apply (rule_tac x="(x \ y)" in exI) +apply (simp_all add: alpha_gen) +apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn) +done + +lemma lets_nok: + "x \ y \ (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \ (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))" +apply (simp only: trm5_lts_inject not_ex) +apply (rule allI) +apply (simp add: alpha_gen) +apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject) +done + +end diff -r f00761b5957e -r 226693549aa0 Nominal/Test.thy --- a/Nominal/Test.thy Mon Mar 08 15:01:01 2010 +0100 +++ b/Nominal/Test.thy Mon Mar 08 15:01:26 2010 +0100 @@ -499,8 +499,8 @@ "bp (PVar x) = {atom x}" | "bp (PUnit) = {}" | "bp (PPair p1 p2) = bp p1 \ bp p2" +thm alpha_exp_raw_alpha_pat_raw.intros -thm quot_respect (* example 6 from Peter Sewell's bestiary *) nominal_datatype exp6 = EVar name @@ -516,6 +516,7 @@ "bp6 (PVar' x) = {atom x}" | "bp6 (PUnit') = {}" | "bp6 (PPair' p1 p2) = bp6 p1 \ bp6 p2" +thm alpha_exp6_raw_alpha_pat6_raw.intros (* example 7 from Peter Sewell's bestiary *) nominal_datatype exp7 = @@ -535,6 +536,7 @@ "b7 (Assign x e) = {atom x}" | "b7s (Single a) = b7 a" | "b7s (More a as) = (b7 a) \ (b7s as)" +thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros (* example 8 from Peter Sewell's bestiary *) nominal_datatype exp8 = @@ -572,6 +574,7 @@ | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" | "b_fnclause (K x pat exp8) = {atom x}" +thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros