# HG changeset patch # User Christian Urban # Date 1291645457 0 # Node ID 25dcb2b1329e7edf5ad2dd3ed08c198a02394f19 # Parent 98236fbd8aa6e0da548f7fa43aeff622caf3cd06 ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/Ex/CoreHaskell.thy Mon Dec 06 14:24:17 2010 +0000 @@ -86,6 +86,10 @@ (* generated theorems *) +thm core_haskell.perm_bn_alpha +thm core_haskell.perm_bn_simps +thm core_haskell.bn_finite + thm core_haskell.distinct thm core_haskell.induct thm core_haskell.exhaust diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Ex/Ex1.thy --- a/Nominal/Ex/Ex1.thy Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/Ex/Ex1.thy Mon Dec 06 14:24:17 2010 +0000 @@ -20,6 +20,11 @@ "bv (Bar0 x) = {}" | "bv (Bar1 v x b) = {atom v}" +thm foo_bar.perm_bn_alpha +thm foo_bar.perm_bn_simps +thm foo_bar.bn_finite + +thm foo_bar.eq_iff thm foo_bar.distinct thm foo_bar.induct thm foo_bar.inducts diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Ex/Foo1.thy --- a/Nominal/Ex/Foo1.thy Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/Ex/Foo1.thy Mon Dec 06 14:24:17 2010 +0000 @@ -35,6 +35,9 @@ | "bn4 (BNil) = {}" | "bn4 (BAs a as) = {atom a} \ bn4 as" +thm foo.perm_bn_alpha +thm foo.perm_bn_simps +thm foo.bn_finite thm foo.distinct thm foo.induct diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Mon Dec 06 14:24:17 2010 +0000 @@ -24,7 +24,9 @@ "bn (As x y t a) = [atom x] @ bn a" | "bn (As_Nil) = []" +thm foo.perm_bn_alpha thm foo.perm_bn_simps +thm foo.bn_finite thm foo.distinct thm foo.induct @@ -45,19 +47,23 @@ shows "alpha_bn as (permute_bn p as)" apply(induct as rule: foo.inducts(2)) apply(auto)[5] -apply(simp add: foo.perm_bn_simps) -apply(simp add: foo.eq_iff) -apply(simp add: foo.perm_bn_simps) -apply(simp add: foo.eq_iff) +apply(simp only: foo.perm_bn_simps) +apply(simp only: foo.eq_iff) +apply(simp only: foo.perm_bn_simps) +apply(simp only: foo.eq_iff refl) +apply(simp) done lemma tt1: shows "(p \ bn as) = bn (permute_bn p as)" apply(induct as rule: foo.inducts(2)) apply(auto)[5] -apply(simp add: foo.perm_bn_simps foo.bn_defs) -apply(simp add: foo.perm_bn_simps foo.bn_defs) -apply(simp add: atom_eqvt) +apply(simp only: foo.perm_bn_simps foo.bn_defs) +apply(perm_simp) +apply(simp only:) +apply(simp only: foo.perm_bn_simps foo.bn_defs) +apply(perm_simp add: foo.fv_bn_eqvt) +apply(simp only:) done text {* diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Ex/Modules.thy --- a/Nominal/Ex/Modules.thy Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/Ex/Modules.thy Mon Dec 06 14:24:17 2010 +0000 @@ -63,6 +63,10 @@ | "Cbinders (SVal v T) = {atom v}" +thm modules.perm_bn_alpha +thm modules.perm_bn_simps +thm modules.bn_finite + thm modules.distinct thm modules.induct thm modules.exhaust diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Ex/Multi_Recs2.thy --- a/Nominal/Ex/Multi_Recs2.thy Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/Ex/Multi_Recs2.thy Mon Dec 06 14:24:17 2010 +0000 @@ -49,6 +49,54 @@ | "b_lrb (Clause fcs) = (b_fnclauses fcs)" | "b_fnclause (K x pat exp) = {atom x}" + + +thm fun_recs.perm_bn_alpha +thm fun_recs.perm_bn_simps +thm fun_recs.bn_finite +thm fun_recs.inducts +thm fun_recs.distinct +thm fun_recs.induct +thm fun_recs.inducts +thm fun_recs.exhaust +thm fun_recs.fv_defs +thm fun_recs.bn_defs +thm fun_recs.perm_simps +thm fun_recs.eq_iff +thm fun_recs.fv_bn_eqvt +thm fun_recs.size_eqvt +thm fun_recs.supports +thm fun_recs.fsupp +thm fun_recs.supp + +term alpha_b_fnclause +term alpha_b_fnclauses +term alpha_b_lrb +term alpha_b_lrbs +term alpha_b_pat + +term alpha_b_fnclause_raw +term alpha_b_fnclauses_raw +term alpha_b_lrb_raw +term alpha_b_lrbs_raw +term alpha_b_pat_raw + +lemma uu1: + fixes as0::exp and as1::fnclause + shows "(\x::exp. True) (as0::exp)" + and "alpha_b_fnclause as1 (permute_b_fnclause p as1)" + and "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)" + and "alpha_b_lrb as3 (permute_b_lrb p as3)" + and "alpha_b_lrbs as4 (permute_b_lrbs p as4)" + and "alpha_b_pat as5 (permute_b_pat p as5)" +apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts) +apply(simp_all) +apply(simp only: fun_recs.perm_bn_simps) +apply(simp only: fun_recs.eq_iff) +apply(simp) +oops + + thm fun_recs.distinct thm fun_recs.induct thm fun_recs.inducts diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/Nominal2.thy Mon Dec 06 14:24:17 2010 +0000 @@ -146,13 +146,9 @@ ML {* (** definition of the raw binding functions **) -(* TODO: needs cleaning *) -fun find [] _ = error ("cannot find element") - | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y - -fun prep_bn_info lthy dt_names dts eqs = +fun prep_bn_info lthy dt_names dts bn_funs eqs = let - fun aux eq = + fun process_eq eq = let val (lhs, rhs) = eq |> HOLogic.dest_Trueprop @@ -162,32 +158,32 @@ val (ty_name, _) = dest_Type (domain_type ty) val dt_index = find_index (fn x => x = ty_name) dt_names val (cnstr_head, cnstr_args) = strip_comb cnstr + val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) val rhs_elements = strip_bn_fun lthy cnstr_args rhs in - (dt_index, (bn_fun, (cnstr_head, rhs_elements))) + ((bn_fun, dt_index), (cnstr_name, rhs_elements)) end - fun order dts i ts = + (* order according to constructor names *) + fun cntrs_order ((bn, dt_index), data) = let - val dt = nth dts i - val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) - val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts + val dt = nth dts dt_index + val cts = (fn (_, _, _, x) => x) dt + val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts in - map (find ts') cts + (bn, (bn, dt_index, order (op=) ct_names data)) end + +in + eqs + |> map process_eq + |> AList.group (op=) (* eqs grouped according to bn_functions *) + |> map cntrs_order (* inner data ordered according to constructors *) + |> order (op=) bn_funs (* ordered according to bn_functions *) +end +*} - val unordered = AList.group (op=) (map aux eqs) - val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered - val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' - val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) - - (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*) - (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*) - (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*) -in - ordered' -end - +ML {* fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = if null raw_bn_funs then ([], [], [], [], lthy) @@ -203,7 +199,7 @@ val raw_bn_eqs = the simps val raw_bn_info = - prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) + prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs) in (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) end @@ -269,6 +265,8 @@ then define_raw_dts dts bn_funs bn_eqs bclauses lthy else raise TEST lthy + val _ = tracing ("raw_bn_funs\n" ^ cat_lines (map (@{make_string} o #1) raw_bn_funs)) + val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo @@ -311,6 +309,12 @@ (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 else raise TEST lthy3 + (* + val _ = tracing ("RAW_BNS\n" ^ cat_lines (map (Syntax.string_of_term lthy3) raw_bns)) + val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map (Syntax.string_of_term lthy3 o #1) raw_bn_info)) + val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map @{make_string} raw_bn_info)) + *) + (* defining the permute_bn functions *) val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = if get_STEPS lthy3a > 2 @@ -489,6 +493,14 @@ val qalpha_bns_descr = map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms + (* + val _ = tracing ("raw_bn_info\n" ^ cat_lines (map (Syntax.string_of_term lthy7 o #1) raw_bn_info)) + val _ = tracing ("bn_funs\n" ^ cat_lines (map (@{make_string} o #1) bn_funs)) + val _ = tracing ("raw_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_bns)) + val _ = tracing ("raw_fv_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_fv_bns)) + val _ = tracing ("alpha_bn_trms\n" ^ cat_lines (map (Syntax.string_of_term lthy7) alpha_bn_trms)) + *) + val qperm_descr = map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs @@ -499,7 +511,7 @@ map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns - val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qpermute_bns), lthy8) = + val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8)= if get_STEPS lthy > 24 then lthy7 @@ -527,6 +539,7 @@ val qfvs = map #qconst qfvs_info val qfv_bns = map #qconst qfv_bns_info val qalpha_bns = map #qconst qalpha_bns_info + val qperm_bns = map #qconst qperm_bns_info (* lifting of the theorems *) val _ = warning "Lifting of Theorems" @@ -586,12 +599,6 @@ qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC else [] - (* proving that the qbn result is finite *) - val qbn_finite_thms = - if get_STEPS lthy > 33 - then prove_bns_finite qtys qbns qinduct qbn_defs lthyC - else [] - (* postprocessing of eq and fv theorems *) val qeq_iffs' = qeq_iffs @@ -612,6 +619,18 @@ |> map (fn thm => thm RS transform_thm) |> map (simplify (HOL_basic_ss addsimps transform_thms)) + (* proving that the qbn result is finite *) + val qbn_finite_thms = + if get_STEPS lthy > 33 + then prove_bns_finite qtys qbns qinduct qbn_defs lthyC + else [] + + (* proving that perm_bns preserve alpha *) + val qperm_bn_alpha_thms = @{thms TrueI} + (* if get_STEPS lthy > 33 + then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' lthyC + else []*) + (* noting the theorems *) @@ -639,6 +658,7 @@ ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) + ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) in (0, lthy9') end handle TEST ctxt => (0, ctxt) diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/nominal_dt_alpha.ML Mon Dec 06 14:24:17 2010 +0000 @@ -247,6 +247,8 @@ (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) + val _ = tracing ("alpha in def\n" ^ cat_lines (map (@{make_string} o fst o #1) all_alpha_names)) + val (alphas, lthy') = Inductive.add_inductive_i {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/nominal_dt_supp.ML --- a/Nominal/nominal_dt_supp.ML Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/nominal_dt_supp.ML Mon Dec 06 14:24:17 2010 +0000 @@ -17,7 +17,8 @@ thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list - + val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> + Proof.context -> thm list end structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = @@ -150,12 +151,6 @@ val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} -fun p_tac msg i = - if false then print_tac ("ptest: " ^ msg) else all_tac - -fun q_tac msg i = - if true then print_tac ("qtest: " ^ msg) else all_tac - fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps fv_bn_eqvts qinduct bclausess ctxt = let @@ -206,7 +201,29 @@ val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) in - induct_prove qtys props qinduct (K (ss_tac ORELSE' (K no_tac))) ctxt + induct_prove qtys props qinduct (K ss_tac) ctxt + end + +fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs ctxt = + let + val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt + val p = Free (p, @{typ perm}) + + fun mk_goal qperm_bn alpha_bn = + let + val arg_ty = domain_type (fastype_of alpha_bn) + in + (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) + end + + val props = map2 mk_goal qperm_bns alpha_bns + val ss_tac = (K (print_tac "test")) THEN' + asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs)) + in + @{thms TrueI} + (*induct_prove qtys props qinduct (K ss_tac) ctxt' + |> ProofContext.export ctxt' ctxt + |> map (simplify (HOL_basic_ss addsimps @{thms id_def}))*) end diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Fri Dec 03 13:51:07 2010 +0000 +++ b/Nominal/nominal_library.ML Mon Dec 06 14:24:17 2010 +0000 @@ -6,11 +6,14 @@ signature NOMINAL_LIBRARY = sig - val is_true: term -> bool + val last2: 'a list -> 'a * 'a + val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list - val last2: 'a list -> 'a * 'a + val is_true: term -> bool + + val dest_listT: typ -> typ - val dest_listT: typ -> typ + val mk_id: term -> term val size_const: typ -> term @@ -91,17 +94,30 @@ structure Nominal_Library: NOMINAL_LIBRARY = struct -fun is_true @{term "Trueprop True"} = true - | is_true _ = false +(* orders an AList according to keys *) +fun order eq keys list = + map (the o AList.lookup eq list) keys fun last2 [] = raise Empty | last2 [_] = raise Empty | last2 [x, y] = (x, y) | last2 (_ :: xs) = last2 xs + +fun is_true @{term "Trueprop True"} = true + | is_true _ = false + fun dest_listT (Type (@{type_name list}, [T])) = T | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) +fun mk_id trm = + let + val ty = fastype_of trm + in + Const (@{const_name id}, ty --> ty) $ trm + end + + fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) fun sum_case_const ty1 ty2 ty3 =