# HG changeset patch # User Christian Urban # Date 1282845832 -28800 # Node ID abafea9b39bbe4c22fa9314d7e92cc2aecd2573b # Parent 3885dc2669f9052800210f700a76d2b04720383f corrected bug with fv-function generation (that was the problem with recursive binders) diff -r 3885dc2669f9 -r abafea9b39bb Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Thu Aug 26 02:08:00 2010 +0800 +++ b/Nominal/Ex/ExPS8.thy Fri Aug 27 02:03:52 2010 +0800 @@ -6,6 +6,8 @@ atom_decl name +declare [[STEPS = 15]] + nominal_datatype exp = EVar name | EUnit diff -r 3885dc2669f9 -r abafea9b39bb Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Thu Aug 26 02:08:00 2010 +0800 +++ b/Nominal/Ex/Let.thy Fri Aug 27 02:03:52 2010 +0800 @@ -20,6 +20,7 @@ "bn Lnil = []" | "bn (Lcons x t l) = (atom x) # (bn l)" +text {* *} (* diff -r 3885dc2669f9 -r abafea9b39bb Nominal/Ex/LetRec.thy --- a/Nominal/Ex/LetRec.thy Thu Aug 26 02:08:00 2010 +0800 +++ b/Nominal/Ex/LetRec.thy Fri Aug 27 02:03:52 2010 +0800 @@ -2,22 +2,20 @@ imports "../NewParser" begin -declare [[STEPS = 14]] - atom_decl name nominal_datatype let_rec: - lam = + trm = Var "name" -| App "lam" "lam" -| Lam x::"name" t::"lam" bind (set) x in t -| Let_Rec bp::"bp" t::"lam" bind (set) "bi bp" in bp t +| App "trm" "trm" +| Lam x::"name" t::"trm" bind (set) x in t +| Let_Rec bp::"bp" t::"trm" bind (set) "bn bp" in bp t and bp = - Bp "name" "lam" + Bp "name" "trm" binder - bi::"bp \ atom set" + bn::"bp \ atom set" where - "bi (Bp x t) = {atom x}" + "bn (Bp x t) = {atom x}" thm let_rec.distinct thm let_rec.induct diff -r 3885dc2669f9 -r abafea9b39bb Nominal/Ex/LetRec2.thy --- a/Nominal/Ex/LetRec2.thy Thu Aug 26 02:08:00 2010 +0800 +++ b/Nominal/Ex/LetRec2.thy Fri Aug 27 02:03:52 2010 +0800 @@ -4,6 +4,7 @@ atom_decl name + nominal_datatype trm = Vr "name" | Ap "trm" "trm" @@ -19,14 +20,12 @@ | "bn (Lcons x t l) = (atom x) # (bn l)" -thm trm_lts.fv +thm trm_lts.fv_defs thm trm_lts.eq_iff -thm trm_lts.bn -thm trm_lts.perm +thm trm_lts.bn_defs +thm trm_lts.perm_simps 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? *) @@ -75,7 +74,7 @@ apply (rule_tac x="(x \ y)" in exI) apply (simp add: atom_eqvt fresh_star_def) done - +*) end diff -r 3885dc2669f9 -r abafea9b39bb Nominal/NewParser.thy --- a/Nominal/NewParser.thy Thu Aug 26 02:08:00 2010 +0800 +++ b/Nominal/NewParser.thy Fri Aug 27 02:03:52 2010 +0800 @@ -330,7 +330,7 @@ mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys (* definition of alpha_eq_iff lemmas *) - (* they have a funny shape for the simplifier *) + (* they have a funny shape for the simplifier ---- CHECK WHETHER NEEDED*) val _ = warning "Eq-iff theorems"; val (alpha_eq_iff_simps, alpha_eq_iff) = if get_STEPS lthy > 5 @@ -402,24 +402,44 @@ else raise TEST lthy6 (* respectfulness proofs *) - val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs - raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6 - val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux + val raw_funs_rsp_aux = + if get_STEPS lthy > 15 + then raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs + raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6 + else raise TEST lthy6 + + val raw_funs_rsp = + if get_STEPS lthy > 16 + then map mk_funs_rsp raw_funs_rsp_aux + else raise TEST lthy6 - val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct - (raw_size_thms @ raw_size_eqvt) lthy6 - |> map mk_funs_rsp + val raw_size_rsp = + if get_STEPS lthy > 17 + then + raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct + (raw_size_thms @ raw_size_eqvt) lthy6 + |> map mk_funs_rsp + else raise TEST lthy6 - val raw_constrs_rsp = raw_constrs_rsp raw_constrs alpha_trms alpha_intros - (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 + val raw_constrs_rsp = + if get_STEPS lthy > 18 + then raw_constrs_rsp raw_constrs alpha_trms alpha_intros + (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 + else raise TEST lthy6 - val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt + val alpha_permute_rsp = + if get_STEPS lthy > 19 + then map mk_alpha_permute_rsp alpha_eqvt + else raise TEST lthy6 - val alpha_bn_rsp = raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms + val alpha_bn_rsp = + if get_STEPS lthy > 20 + then raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms + else raise TEST lthy6 (* noting the quot_respects lemmas *) val (_, lthy6a) = - if get_STEPS lthy > 15 + if get_STEPS lthy > 21 then Local_Theory.note ((Binding.empty, [rsp_attrib]), raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 else raise TEST lthy6 @@ -429,7 +449,7 @@ val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts val (qty_infos, lthy7) = - if get_STEPS lthy > 16 + if get_STEPS lthy > 22 then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a else raise TEST lthy6a @@ -462,7 +482,7 @@ map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = - if get_STEPS lthy > 17 + if get_STEPS lthy > 23 then lthy7 |> define_qconsts qtys qconstrs_descr @@ -474,12 +494,12 @@ (* definition of the quotient permfunctions and pt-class *) val lthy9 = - if get_STEPS lthy > 18 + if get_STEPS lthy > 24 then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 else raise TEST lthy8 val lthy9a = - if get_STEPS lthy > 19 + if get_STEPS lthy > 25 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 else raise TEST lthy9 @@ -496,7 +516,7 @@ prod.cases} val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = - if get_STEPS lthy > 20 + if get_STEPS lthy > 26 then lthy9a |> lift_thms qtys [] alpha_distincts @@ -508,7 +528,7 @@ else raise TEST lthy9a val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = - if get_STEPS lthy > 20 + if get_STEPS lthy > 27 then lthyA |> lift_thms qtys [] raw_size_eqvt diff -r 3885dc2669f9 -r abafea9b39bb Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Thu Aug 26 02:08:00 2010 +0800 +++ b/Nominal/nominal_dt_alpha.ML Fri Aug 27 02:03:52 2010 +0800 @@ -110,7 +110,7 @@ if member (op=) bodies i then [] else [lookup alpha_bn_map bn $ nth args i $ nth args' i] -(* generat the premises for an alpha rule; mk_frees is used +(* generate the premises for an alpha rule; mk_frees is used if no binders are present *) fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause = let @@ -626,6 +626,7 @@ val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) + in alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct (K (asm_full_simp_tac ss)) ctxt diff -r 3885dc2669f9 -r abafea9b39bb Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Thu Aug 26 02:08:00 2010 +0800 +++ b/Nominal/nominal_dt_rawfuns.ML Fri Aug 27 02:03:52 2010 +0800 @@ -62,6 +62,9 @@ datatype bmode = Lst | Res | Set datatype bclause = BC of bmode * (term option * int) list * int list +fun lookup xs x = the (AList.lookup (op=) xs x) + + (* testing for concrete atom types *) fun is_atom ctxt ty = Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) @@ -166,7 +169,9 @@ in case bn_option of NONE => (setify lthy arg, @{term "{}::atom set"}) - | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) + | SOME bn => (to_set (bn $ arg), + if member (op=) bodies i then @{term "{}::atom set"} + else lookup fv_bn_map bn $ arg) end val t1 = map (mk_fv_body fv_map args) bodies @@ -189,7 +194,7 @@ NONE => mk_supp arg | SOME fv => fv $ arg) | SOME (NONE) => @{term "{}::atom set"} - | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg + | SOME (SOME bn) => lookup fv_bn_map bn $ arg end in case bclause of @@ -201,7 +206,7 @@ let val arg_names = Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) - val fv = the (AList.lookup (op=) fv_map ty) + val fv = lookup fv_map ty val lhs = fv $ list_comb (constr, args) val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses val rhs = fold_union rhs_trms @@ -213,7 +218,7 @@ let val arg_names = Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) - val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) + val fv_bn = lookup fv_bn_map bn_trm val lhs = fv_bn $ list_comb (constr, args) val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses val rhs = fold_union rhs_trms