# HG changeset patch # User Cezary Kaliszyk # Date 1269703239 -3600 # Node ID 721d92623c9d6c0896b4b7ef47a0159a16faa391 # Parent b9e4c812d2c60566d4637417b97eabfc4f4783ba Lets finally abstract lists. diff -r b9e4c812d2c6 -r 721d92623c9d Nominal/ExLet.thy --- a/Nominal/ExLet.thy Sat Mar 27 16:17:45 2010 +0100 +++ b/Nominal/ExLet.thy Sat Mar 27 16:20:39 2010 +0100 @@ -7,7 +7,7 @@ atom_decl name ML {* val _ = recursive := false *} - +ML {* val _ = alpha_type := AlphaLst *} nominal_datatype trm = Vr "name" | Ap "trm" "trm" @@ -19,8 +19,8 @@ binder bn where - "bn Lnil = {}" -| "bn (Lcons x t l) = {atom x} \ (bn l)" + "bn Lnil = []" +| "bn (Lcons x t l) = (atom x) # (bn l)" thm trm_lts.fv thm trm_lts.eq_iff @@ -29,7 +29,7 @@ thm trm_lts.induct[no_vars] thm trm_lts.inducts[no_vars] thm trm_lts.distinct -thm trm_lts.fv[simplified trm_lts.supp] +thm trm_lts.fv[simplified trm_lts.supp(1-2)] primrec permute_bn_raw @@ -80,7 +80,7 @@ done lemma Lt_subst: - "supp (Abs (bn lts) trm) \* q \ (Lt lts trm) = Lt (permute_bn q lts) (q \ trm)" + "supp (Abs_lst (bn lts) trm) \* q \ (Lt lts trm) = Lt (permute_bn q lts) (q \ trm)" apply (simp only: trm_lts.eq_iff) apply (rule_tac x="q" in exI) apply (simp add: alphas) @@ -98,7 +98,7 @@ lemma fin_bn: - "finite (bn l)" + "finite (set (bn l))" apply(induct l rule: trm_lts.inducts(2)) apply(simp_all add:permute_bn eqvts) done @@ -110,7 +110,7 @@ assumes a1: "\name c. P1 c (Vr name)" and a2: "\trm1 trm2 c. \\d. P1 d trm1; \d. P1 d trm2\ \ P1 c (Ap trm1 trm2)" and a3: "\name trm c. \atom name \ c; \d. P1 d trm\ \ P1 c (Lm name trm)" - and a4: "\lts trm c. \bn lts \* c; \d. P2 d lts; \d. P1 d trm\ \ P1 c (Lt lts trm)" + and a4: "\lts trm c. \set (bn lts) \* c; \d. P2 d lts; \d. P1 d trm\ \ P1 c (Lt lts trm)" and a5: "\c. P2 c Lnil" and a6: "\name trm lts c. \\d. P1 d trm; \d. P2 d lts\ \ P2 c (Lcons name trm lts)" shows "P1 c t" and "P2 c l" @@ -142,14 +142,14 @@ apply(simp add: fresh_def) apply(simp add: trm_lts.fv[simplified trm_lts.supp]) apply(simp) - apply(subgoal_tac "\q. (q \ bn (p \ lts)) \* c \ supp (Abs (bn (p \ lts)) (p \ trm)) \* q") + apply(subgoal_tac "\q. (q \ set (bn (p \ lts))) \* c \ supp (Abs_lst (bn (p \ lts)) (p \ trm)) \* q") apply(erule exE) apply(erule conjE) apply(subst Lt_subst) apply assumption apply(rule a4) - apply(simp add:perm_bn) - apply assumption + apply(simp add:perm_bn[symmetric]) + apply(simp add: eqvts) apply (simp add: fresh_star_def fresh_def) apply(rotate_tac 1) apply(drule_tac x="q + p" in meta_spec) @@ -157,8 +157,6 @@ apply(rule at_set_avoiding2) apply(rule fin_bn) apply(simp add: finite_supp) - apply(simp add: supp_abs) - apply(rule finite_Diff) apply(simp add: finite_supp) apply(simp add: fresh_star_def fresh_def supp_abs) apply(simp add: eqvts permute_bn) @@ -196,12 +194,10 @@ lemma lets_not_ok1: - "(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = + "x \ y \ + (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" - apply (simp add: alphas trm_lts.eq_iff) - apply (rule_tac x="0::perm" in exI) - apply (simp add: fresh_star_def eqvts) - apply blast + apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts) done lemma lets_nok: diff -r b9e4c812d2c6 -r 721d92623c9d Nominal/ExLetRec.thy --- a/Nominal/ExLetRec.thy Sat Mar 27 16:17:45 2010 +0100 +++ b/Nominal/ExLetRec.thy Sat Mar 27 16:20:39 2010 +0100 @@ -2,11 +2,13 @@ imports "Parser" begin + text {* example 3 or example 5 from Terms.thy *} atom_decl name ML {* val _ = recursive := true *} +ML {* val _ = alpha_type := AlphaLst *} nominal_datatype trm = Vr "name" | Ap "trm" "trm" @@ -18,8 +20,8 @@ binder bn where - "bn Lnil = {}" -| "bn (Lcons x t l) = {atom x} \ (bn l)" + "bn Lnil = []" +| "bn (Lcons x t l) = (atom x) # (bn l)" thm trm_lts.fv thm trm_lts.eq_iff @@ -27,6 +29,7 @@ thm trm_lts.perm thm trm_lts.induct thm trm_lts.distinct +thm trm_lts.supp thm trm_lts.fv[simplified trm_lts.supp] (* why is this not in HOL simpset? *) @@ -66,6 +69,13 @@ apply (simp add: alphas trm_lts.eq_iff fresh_star_def) done +lemma lets_ok4: + "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = + (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))" + apply (simp add: alphas trm_lts.eq_iff) + apply (rule_tac x="(x \ y)" in exI) + apply (simp add: atom_eqvt fresh_star_def) + done end diff -r b9e4c812d2c6 -r 721d92623c9d Nominal/Fv.thy --- a/Nominal/Fv.thy Sat Mar 27 16:17:45 2010 +0100 +++ b/Nominal/Fv.thy Sat Mar 27 16:20:39 2010 +0100 @@ -891,13 +891,9 @@ end *} -lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \ supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" - apply (simp add: supp_abs supp_Pair) - apply blast - done - (* TODO: this is a hack, it assumes that only one type of Abs's is present - in the type and chooses this supp_abs *) + in the type and chooses this supp_abs. Additionally single atoms are + treated properly. *) ML {* fun choose_alpha_abs eqiff = let @@ -905,19 +901,31 @@ val terms = map prop_of eqiff; fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms val no = - if check @{const_name alpha_gen} then 0 else + if check @{const_name alpha_lst} then 2 else if check @{const_name alpha_res} then 1 else - if check @{const_name alpha_lst} then 2 else + if check @{const_name alpha_gen} then 0 else error "Failure choosing supp_abs" in nth @{thms supp_abs[symmetric]} no end *} +lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}" +by (rule supp_abs(1)) + +lemma supp_abs_sum: + "supp (Abs x (a :: 'a :: fs)) \ supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" + "supp (Abs_res x (a :: 'a :: fs)) \ supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))" + "supp (Abs_lst y (a :: 'a :: fs)) \ supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))" + apply (simp_all add: supp_abs supp_Pair) + apply blast+ + done + ML {* fun supp_eq_tac ind fv perm eqiff ctxt = rel_indtac ind THEN_ALL_NEW asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW diff -r b9e4c812d2c6 -r 721d92623c9d Nominal/Lift.thy --- a/Nominal/Lift.thy Sat Mar 27 16:17:45 2010 +0100 +++ b/Nominal/Lift.thy Sat Mar 27 16:20:39 2010 +0100 @@ -64,19 +64,6 @@ *} ML {* -fun quotient_lift_consts_export qtys spec ctxt = -let - val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; - val (ts_loc, defs_loc) = split_list result; - val morphism = ProofContext.export_morphism ctxt' ctxt; - val ts = map (Morphism.term morphism) ts_loc - val defs = Morphism.fact morphism defs_loc -in - (ts, defs, ctxt') -end -*} - -ML {* fun define_fv_alpha_export dt binds bns ctxt = let val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') = diff -r b9e4c812d2c6 -r 721d92623c9d Nominal/Parser.thy --- a/Nominal/Parser.thy Sat Mar 27 16:17:45 2010 +0100 +++ b/Nominal/Parser.thy Sat Mar 27 16:20:39 2010 +0100 @@ -594,7 +594,7 @@ end in - map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type))))) + map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) end *}