# HG changeset patch # User Christian Urban # Date 1280214542 -7200 # Node ID 841b7e34e70ac20d9f9145d7f69ecde44c33e817 # Parent 83f1b16486ee91a1de6d18ff2a7a3dfcffd3710a fixed order of fold_union to make alpha and fv agree diff -r 83f1b16486ee -r 841b7e34e70a Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Mon Jul 26 09:19:28 2010 +0200 +++ b/Nominal-General/nominal_library.ML Tue Jul 27 09:09:02 2010 +0200 @@ -112,7 +112,7 @@ | mk_union (@{term "{}::atom set"}, t2) = t2 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) -fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} +fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} diff -r 83f1b16486ee -r 841b7e34e70a Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Mon Jul 26 09:19:28 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Tue Jul 27 09:09:02 2010 +0200 @@ -21,6 +21,14 @@ where "bn (As x y t) = {atom x}" +thm alpha_bn_imps +thm distinct +thm eq_iff +thm fv_defs +thm perm_simps +thm perm_laws + + typ trm typ assg term Var @@ -28,25 +36,35 @@ term Baz term bn term fv_trm +term alpha_bn -lemma a1: - shows "alpha_trm_raw x1 y1 \ True" - and "alpha_assg_raw x2 y2 \ alpha_bn_raw x2 y2" - and "alpha_bn_raw x3 y3 \ True" -apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) -apply(rule TrueI)+ -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -sorry + lemma a2: shows "alpha_trm_raw x1 y1 \ fv_trm_raw x1 = fv_trm_raw y1" and "alpha_assg_raw x2 y2 \ fv_assg_raw x2 = fv_assg_raw y2 \ bn_raw x2 = bn_raw y2" and "alpha_bn_raw x3 y3 \ fv_bn_raw x3 = fv_bn_raw y3" apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) -apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) -apply(simp_all only: alphas prod_alpha_def) -apply(auto)[1] -apply(auto simp add: prod_alpha_def) +apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) +apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) +apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps) +apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps) +-- "" +apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc) +-- "" +apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps) +apply(simp only: Un_assoc set.simps append.simps) +apply(simp only: Un_insert_left Un_empty_right Un_empty_left) +-- "" +apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps) +apply(simp only: Un_assoc set.simps append.simps) +--"" +apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps) +apply(simp only: Un_assoc set.simps append.simps) +apply(simp (no_asm) only: simp_thms) +--"" +apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps) +apply(simp only: Un_assoc set.simps append.simps) done lemma [quot_respect]: diff -r 83f1b16486ee -r 841b7e34e70a Nominal/NewParser.thy --- a/Nominal/NewParser.thy Mon Jul 26 09:19:28 2010 +0200 +++ b/Nominal/NewParser.thy Tue Jul 27 09:09:02 2010 +0200 @@ -320,14 +320,14 @@ (* definitions of raw permutations *) val _ = warning "Definition of raw permutations"; - val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = + val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = if get_STEPS lthy0 > 1 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0 else raise TEST lthy0 (* noting the raw permutations as eqvt theorems *) val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) - val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_defs) lthy2 + val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2 val thy = Local_Theory.exit_global lthy2a; val thy_name = Context.theory_name thy @@ -371,7 +371,7 @@ val _ = warning "Proving equivariance"; val bn_eqvt = if get_STEPS lthy > 6 - then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 + then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_simps) lthy4 else raise TEST lthy4 (* noting the bn_eqvt lemmas in a temprorary theory *) @@ -380,7 +380,7 @@ val fv_eqvt = if get_STEPS lthy > 7 - then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) + then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) (Local_Theory.restore lthy_tmp) else raise TEST lthy4 @@ -423,6 +423,11 @@ then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 else raise TEST lthy6 + (* auxiliary lemmas for respectfulness proofs *) + (* HERE *) + + + (* defining the quotient type *) val _ = warning "Declaring the quotient types" val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts @@ -452,8 +457,10 @@ val qfv_bns_descr = map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns - (* TODO: probably also needs alpha_bn *) - val ((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), lthy8) = + val qalpha_bns_descr = + map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms + + val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = if get_STEPS lthy > 15 then lthy7 @@ -461,24 +468,24 @@ ||>> qconst_defs qtys qbns_descr ||>> qconst_defs qtys qfvs_descr ||>> qconst_defs qtys qfv_bns_descr + ||>> qconst_defs qtys qalpha_bns_descr else raise TEST lthy7 val qconstrs = map #qconst qconstrs_info val qbns = map #qconst qbns_info val qfvs = map #qconst qfvs_info val qfv_bns = map #qconst qfv_bns_info + val qalpha_bns = map #qconst qalpha_bns_info - (* respectfulness proofs *) - (* HERE *) val (_, lthy8') = lthy8 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) - ||>> Local_Theory.note ((@{binding "perm_defs"}, []), raw_perm_defs) ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) - + ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) + ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) val _ = if get_STEPS lthy > 16 @@ -541,7 +548,7 @@ val perm_names = map (fn x => "permute_" ^ x) qty_names val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs (* use Local_Theory.theory_result *) - val thy' = qperm_defs qtys qty_full_names dd raw_perm_simps thy; + val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy; val lthy13 = Theory_Target.init NONE thy'; val q_name = space_implode "_" qty_names; @@ -558,7 +565,7 @@ [Rule_Cases.name constr_names q_induct]) lthy13; val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; - val q_perm = map (lift_thm qtys lthy14) raw_perm_defs; + val q_perm = map (lift_thm qtys lthy14) raw_perm_simps; val lthy15 = note_simp_suffix "perm" q_perm lthy14a; val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; val lthy16 = note_simp_suffix "fv" q_fv lthy15; diff -r 83f1b16486ee -r 841b7e34e70a Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Mon Jul 26 09:19:28 2010 +0200 +++ b/Nominal/nominal_dt_rawfuns.ML Tue Jul 27 09:09:02 2010 +0200 @@ -213,6 +213,8 @@ fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy = let + val _ = tracing ("bclausesss\n" ^ cat_lines (map (cat_lines o map PolyML.makestring) bclausesss)) + val fv_names = prefix_dt_names descr sorts "fv_" val fv_arg_tys = all_dtyps descr sorts val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;