# HG changeset patch # User Christian Urban # Date 1275471471 -7200 # Node ID 387fcbd33820d3554f4c5f89604287576f0236fe # Parent 118a0ca16381e87edad5dd3939dbfe2b2ac74ea1 fixed problem with bn_info diff -r 118a0ca16381 -r 387fcbd33820 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Tue Jun 01 15:46:07 2010 +0200 +++ b/Nominal/Ex/Classical.thy Wed Jun 02 11:37:51 2010 +0200 @@ -4,26 +4,23 @@ (* example from my Urban's PhD *) -(* - alpha_trm_raw is incorrectly defined, therefore the equivalence proof - does not go through; below the correct definition is given -*) - atom_decl name atom_decl coname -ML {* val _ = cheat_equivp := true *} +declare [[STEPS = 9]] nominal_datatype trm = Ax "name" "coname" -| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 -| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 -| AndL1 n::"name" t::"trm" "name" bind n in t -| AndL2 n::"name" t::"trm" "name" bind n in t -| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 -| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t +| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind_set n in t1, bind_set c in t2 +| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind_set c1 in t1, bind_set c2 in t2 +| AndL1 n::"name" t::"trm" "name" bind_set n in t +| AndL2 n::"name" t::"trm" "name" bind_set n in t +| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind_set c in t1, bind_set n in t2 +| ImpR c::"coname" n::"name" t::"trm" "coname" bind_set n c in t +thm alpha_trm_raw.intros[no_vars] +(* thm trm.fv thm trm.eq_iff thm trm.bn @@ -31,44 +28,7 @@ thm trm.induct thm trm.distinct thm trm.fv[simplified trm.supp] - -(* correct alpha definition *) - -inductive - alpha -where - "\name = namea; coname = conamea\ \ - alpha (Ax_raw name coname) (Ax_raw namea conamea)" -| "\\pi. ({atom coname1}, trm_raw1) \gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a); - \pia. ({atom coname2}, trm_raw2) \gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a)\ \ - alpha (Cut_raw coname1 trm_raw1 coname2 trm_raw2) - (Cut_raw coname1a trm_raw1a coname2a trm_raw2a)" -| "\\pi. ({atom coname1}, trm_raw1) \gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a); - \pia. ({atom coname2}, trm_raw2) \gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a); - coname3 = coname3a\ \ - alpha (AndR_raw coname1 trm_raw1 coname2 trm_raw2 coname3) - (AndR_raw coname1a trm_raw1a coname2a trm_raw2a coname3a)" -| "\\pi. ({atom name1}, trm_raw) \gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa); - name2 = name2a\ \ - alpha (AndL1_raw name1 trm_raw name2) (AndL1_raw name1a trm_rawa name2a)" -| "\\pi. ({atom name1}, trm_raw) \gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa); - name2 = name2a\ \ - alpha (AndL2_raw name1 trm_raw name2) (AndL2_raw name1a trm_rawa name2a)" -| "\\pi. ({atom coname}, trm_raw1) \gen alpha fv_trm_raw pi ({atom conamea}, trm_raw1a); - \pia. ({atom name1}, trm_raw2) \gen alpha fv_trm_raw pia ({atom name1a}, trm_raw2a); - name2 = name2a\ \ - alpha (ImpL_raw coname trm_raw1 name1 trm_raw2 name2) - (ImpL_raw conamea trm_raw1a name1a trm_raw2a name2a)" -| "\\pi.({atom name} \ {atom coname1}, trm_raw) \gen alpha fv_trm_raw pi - ({atom namea} \ {atom coname1a}, trm_rawa); coname2 = coname2a\ \ - alpha (ImpR_raw coname1 name trm_raw coname2) - (ImpR_raw coname1a namea trm_rawa coname2a)" - -thm alpha.intros - -equivariance alpha - -thm eqvts_raw +*) end diff -r 118a0ca16381 -r 387fcbd33820 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Tue Jun 01 15:46:07 2010 +0200 +++ b/Nominal/Ex/CoreHaskell.thy Wed Jun 02 11:37:51 2010 +0200 @@ -2,15 +2,14 @@ imports "../NewParser" begin -(* core haskell *) - -(* at the moment it is hard coded that shallow binders - need to use bind_set *) +(* Core Haskell *) atom_decl var atom_decl cvar atom_decl tvar +declare [[STEPS = 4]] + nominal_datatype tkind = KStar | KFun "tkind" "tkind" @@ -85,6 +84,8 @@ | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" | "bv_cvs CvsNil = []" | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" + + lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] diff -r 118a0ca16381 -r 387fcbd33820 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue Jun 01 15:46:07 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Wed Jun 02 11:37:51 2010 +0200 @@ -4,9 +4,6 @@ atom_decl name -ML {* Function.add_function *} - -ML {* print_depth 50 *} declare [[STEPS = 9]] @@ -18,11 +15,11 @@ | Foo x::"name" y::"name" t::"trm" bind_set x in y t | Bar x::"name" y::"name" t::"trm" bind y x in t x y and assg = - As "name" "trm" + As "name" "name" "trm" "name" binder bn::"assg \ atom set" where - "bn (As x t) = {atom x}" + "bn (As x y t z) = {atom x}" ML {* Inductive.the_inductive *} thm trm_assg.fv diff -r 118a0ca16381 -r 387fcbd33820 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Tue Jun 01 15:46:07 2010 +0200 +++ b/Nominal/Ex/TypeSchemes.thy Wed Jun 02 11:37:51 2010 +0200 @@ -5,6 +5,7 @@ section {*** Type Schemes ***} atom_decl name +declare [[STEPS = 9]] nominal_datatype ty = Var "name" @@ -12,6 +13,15 @@ and tys = All xs::"name fset" ty::"ty" bind_res xs in ty +nominal_datatype ty2 = + Var2 "name" +| Fun2 "ty2" "ty2" + +(* PROBLEM: this only works once the type is defined +nominal_datatype tys2 = + All2 xs::"name fset" ty::"ty2" bind_res xs in ty +*) + lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] diff -r 118a0ca16381 -r 387fcbd33820 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Tue Jun 01 15:46:07 2010 +0200 +++ b/Nominal/NewParser.thy Wed Jun 02 11:37:51 2010 +0200 @@ -203,9 +203,8 @@ val dt_index = find_index (fn x => x = ty_name) dt_names val (cnstr_head, cnstr_args) = strip_comb cnstr val rhs_elements = strip_bn_fun lthy cnstr_args rhs - val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements in - (dt_index, (bn_fun, (cnstr_head, included))) + (dt_index, (bn_fun, (cnstr_head, rhs_elements))) end fun order dts i ts = let @@ -229,8 +228,6 @@ end *} -ML {* rawify_bn_funs *} - ML {* fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = let @@ -259,8 +256,8 @@ val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds - val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy - + val (raw_dt_full_names, lthy1) = + add_datatype_wrapper raw_dt_names raw_dts lthy in (dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) end @@ -268,22 +265,24 @@ ML {* fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy = -let - val (_, lthy2) = Function.add_function raw_bn_funs raw_bn_eqs - Function_Common.default_config (pat_completeness_simp constr_thms) lthy - - val (info, lthy3) = prove_termination (Local_Theory.restore lthy2) - val {fs, simps, inducts, ...} = info; + if null raw_bn_funs + then ([], [], [], [], lthy) + else + let + val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs + Function_Common.default_config (pat_completeness_simp constr_thms) lthy - val raw_bn_induct = (the inducts) - val raw_bn_eqs = the simps + val (info, lthy2) = prove_termination (Local_Theory.restore lthy1) + val {fs, simps, inducts, ...} = info; + + val raw_bn_induct = (the inducts) + val raw_bn_eqs = the simps - val raw_bn_info = - prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) - -in - (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3) -end + val raw_bn_info = + prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) + in + (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) + end *} @@ -322,8 +321,9 @@ fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = let (* definition of the raw datatypes *) + val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = - if get_STEPS lthy > 1 + if get_STEPS lthy > 0 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy else raise TEST lthy @@ -341,19 +341,11 @@ val induct_thm = #induct dtinfo; val exhaust_thms = map #exhaust dtinfos; - val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy1) = - if get_STEPS lthy0 > 1 - then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy0 - else raise TEST lthy0 - - val bn_nos = map (fn (_, i, _) => i) raw_bn_info; - val bns = raw_bn_funs ~~ bn_nos; - (* definitions of raw permutations *) val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = - if get_STEPS lthy1 > 2 - then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 - else raise TEST lthy1 + 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) @@ -365,16 +357,24 @@ (* definition of raw fv_functions *) val lthy3 = Theory_Target.init NONE thy; - val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3a) = - if get_STEPS lthy2 > 3 - then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3 + val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = + if get_STEPS lthy3 > 2 + then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 else raise TEST lthy3 + val bn_nos = map (fn (_, i, _) => i) raw_bn_info; + val bns = raw_bn_funs ~~ bn_nos; + + val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = + if get_STEPS lthy3a > 3 + then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a + else raise TEST lthy3a + (* definition of raw alphas *) val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = - if get_STEPS lthy > 4 - then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a - else raise TEST lthy3a + if get_STEPS lthy3b > 4 + then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b + else raise TEST lthy3b (* definition of alpha-distinct lemmas *) val (alpha_distincts, alpha_bn_distincts) = @@ -393,28 +393,25 @@ then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 else raise TEST lthy4 + (* noting the bn_eqvt lemmas in a temprorary theory *) val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) - val (_, lthy_tmp) = Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4 + val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) 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) lthy_tmp else raise TEST lthy4 - val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp - - + val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) val (alpha_eqvt, _) = if get_STEPS lthy > 8 then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' else raise TEST lthy4 - (* val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt)) val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt)) val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt)) - *) val _ = if get_STEPS lthy > 9 diff -r 118a0ca16381 -r 387fcbd33820 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Tue Jun 01 15:46:07 2010 +0200 +++ b/Nominal/nominal_dt_rawfuns.ML Wed Jun 02 11:37:51 2010 +0200 @@ -226,6 +226,9 @@ val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) + val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) ((flat fv_eqs) @ (flat fv_bn_eqs)))) + + val (_, lthy') = Function.add_function all_fun_names all_fun_eqs Function_Common.default_config (pat_completeness_simp constr_thms) lthy @@ -255,29 +258,31 @@ end fun raw_prove_eqvt consts ind_thms simps ctxt = -let - val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt - val p = Free (p, @{typ perm}) - val arg_tys = - consts - |> map fastype_of - |> map domain_type - val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt' - val args = map Free (arg_names ~~ arg_tys) - val goals = map2 (mk_eqvt_goal p) consts args - val insts = map (single o SOME) arg_names - val const_names = map (fst o dest_Const) consts - fun tac ctxt = - Object_Logic.full_atomize_tac - THEN' InductTacs.induct_rules_tac ctxt insts ind_thms - THEN_ALL_NEW - (asm_full_simp_tac (HOL_basic_ss addsimps simps) - THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names - THEN' asm_simp_tac HOL_basic_ss) -in - Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) - |> ProofContext.export ctxt'' ctxt -end + if null consts then [] + else + let + val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt + val p = Free (p, @{typ perm}) + val arg_tys = + consts + |> map fastype_of + |> map domain_type + val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt' + val args = map Free (arg_names ~~ arg_tys) + val goals = map2 (mk_eqvt_goal p) consts args + val insts = map (single o SOME) arg_names + val const_names = map (fst o dest_Const) consts + fun tac ctxt = + Object_Logic.full_atomize_tac + THEN' InductTacs.induct_rules_tac ctxt insts ind_thms + THEN_ALL_NEW + (asm_full_simp_tac (HOL_basic_ss addsimps simps) + THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names + THEN' asm_simp_tac HOL_basic_ss) + in + Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) + |> ProofContext.export ctxt'' ctxt + end end (* structure *)