# HG changeset patch # User Christian Urban # Date 1267714618 -3600 # Node ID 3727e234fe6b9175ddb9e331ffcd1d030aa538d0 # Parent cad5f385156937801b51f471dbd9d441d404994d# Parent c25f797c7e6ec9db7ed98729256bf900514db490 merged diff -r cad5f3851569 -r 3727e234fe6b Nominal/Parser.thy --- a/Nominal/Parser.thy Thu Mar 04 15:31:34 2010 +0100 +++ b/Nominal/Parser.thy Thu Mar 04 15:56:58 2010 +0100 @@ -209,6 +209,21 @@ ML {* add_primrec_wrapper *} +lemma equivp_hack: "equivp x" +sorry +ML {* +fun equivp_hack ctxt rel = +let + val thy = ProofContext.theory_of ctxt + val ty = domain_type (fastype_of rel) + val cty = ctyp_of thy ty + val ct = cterm_of thy rel +in + Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} +end +*} + + ML {* fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = let @@ -249,12 +264,13 @@ val alpha_cases = #elims alpha val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc - val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; +(* val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; + val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; @@ -299,11 +315,15 @@ val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs; val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; + val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj + val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded; + val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre + val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;*) in - ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy17) + ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) end *} - +ML fold ML name_of_typ ML {* diff -r cad5f3851569 -r 3727e234fe6b Nominal/Test.thy --- a/Nominal/Test.thy Thu Mar 04 15:31:34 2010 +0100 +++ b/Nominal/Test.thy Thu Mar 04 15:56:58 2010 +0100 @@ -4,7 +4,7 @@ text {* weirdo example from Peter Sewell's bestiary *} -(*nominal_datatype weird = +nominal_datatype weird = WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" bind x in p1, bind x in p2, bind y in p2, bind y in p3 | WV "name" @@ -19,7 +19,7 @@ local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding weird_inj}, []), (build_alpha_inj @{thms alpha_weird_raw.intros} @{thms weird_raw.distinct weird_raw.inject} @{thms alpha_weird_raw.cases} ctxt)) ctxt)) *} thm weird_inj -local_setup {* +(*local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_eqvt}, []), build_alpha_eqvts [@{term alpha_weird_raw}] [@{term "permute :: perm \ weird_raw \ weird_raw"}] @{thms permute_weird_raw.simps weird_inj} @{thm alpha_weird_raw.induct} ctxt) ctxt)) *} @@ -144,10 +144,11 @@ thm permute_lam_raw_permute_bp_raw.simps thm alpha_lam_raw_alpha_bp_raw.intros[no_vars] thm fv_lam_raw_fv_bp_raw.simps[no_vars] -thm lam_bp_induct +(*thm lam_bp_induct thm lam_bp_perm thm lam_bp_fv thm lam_bp_bn +thm lam_bp_inject*) text {* example 2 *} @@ -171,10 +172,11 @@ thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] thm f_raw.simps -thm trm'_pat'_induct +(*thm trm'_pat'_induct thm trm'_pat'_perm thm trm'_pat'_fv thm trm'_pat'_bn +thm trm'_pat'_inject*) nominal_datatype trm0 = Var0 "name" @@ -193,10 +195,10 @@ | "f0 (PD0 p1 p2) = (f0 p1) \ (f0 p2)" thm f0_raw.simps -thm trm0_pat0_induct +(*thm trm0_pat0_induct thm trm0_pat0_perm thm trm0_pat0_fv -thm trm0_pat0_bn +thm trm0_pat0_bn*) text {* example type schemes *} @@ -210,12 +212,11 @@ *) -(* alpha_eqvt fails... nominal_datatype t = Var "name" | Fun "t" "t" and tyS = - All xs::"name set" ty::"t" bind xs in ty *) + All xs::"name set" ty::"t" bind xs in ty (* example 1 from Terms.thy *) @@ -271,13 +272,13 @@ (* fv_eqvt does not work, we need to repaire defined permute functions defined fv and defined alpha... *) -(*nominal_datatype trm4 = +nominal_datatype trm4 = Vr4 "name" | Ap4 "trm4" "trm4 list" | Lm4 x::"name" t::"trm4" bind x in t thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] -thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*) +thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] (* example 5 from Terms.thy *) @@ -296,7 +297,7 @@ (* example 6 from Terms.thy *) -(* BV is not respectful, needs to fail +(* BV is not respectful, needs to fail*) nominal_datatype trm6 = Vr6 "name" | Lm6 x::"name" t::"trm6" bind x in t @@ -306,11 +307,10 @@ where "bv6 (Vr6 n) = {}" | "bv6 (Lm6 n t) = {atom n} \ bv6 t" -| "bv6 (Lt6 l r) = bv6 l \ bv6 r" *) - +| "bv6 (Lt6 l r) = bv6 l \ bv6 r" (* example 7 from Terms.thy *) -(* BV is not respectful, needs to fail +(* BV is not respectful, needs to fail*) nominal_datatype trm7 = Vr7 "name" | Lm7 l::"name" r::"trm7" bind l in r @@ -320,7 +320,7 @@ where "bv7 (Vr7 n) = {atom n}" | "bv7 (Lm7 n t) = bv7 t - {atom n}" -| "bv7 (Lt7 l r) = bv7 l \ bv7 r" *) +| "bv7 (Lt7 l r) = bv7 l \ bv7 r" (* example 8 from Terms.thy *) @@ -338,7 +338,7 @@ (* example 9 from Terms.thy *) -(* BV is not respectful, needs to fail +(* BV is not respectful, needs to fail*) nominal_datatype lam9 = Var9 "name" | Lam9 n::"name" l::"lam9" bind n in l @@ -348,13 +348,13 @@ bv9 where "bv9 (Var9 x) = {}" -| "bv9 (Lam9 x b) = {atom x}" *) +| "bv9 (Lam9 x b) = {atom x}" (* example from my PHD *) atom_decl coname -(*nominal_datatype phd = +nominal_datatype phd = Ax "name" "coname" | Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 | AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 @@ -365,7 +365,7 @@ thm alpha_phd_raw.intros[no_vars] thm fv_phd_raw.simps[no_vars] -*) + (* example form Leroy 96 about modules; OTT *) @@ -501,7 +501,7 @@ thm quot_respect (* example 6 from Peter Sewell's bestiary *) -(*nominal_datatype exp6 = +nominal_datatype exp6 = EVar name | EPair exp6 exp6 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 @@ -514,10 +514,10 @@ where "bp6 (PVar' x) = {atom x}" | "bp6 (PUnit') = {}" -| "bp6 (PPair' p1 p2) = bp6 p1 \ bp6 p2"*) +| "bp6 (PPair' p1 p2) = bp6 p1 \ bp6 p2" (* example 7 from Peter Sewell's bestiary *) -(*nominal_datatype exp7 = +nominal_datatype exp7 = EVar name | EUnit | EPair exp7 exp7 @@ -533,10 +533,10 @@ where "b7 (Assign x e) = {atom x}" | "b7s (Single a) = b7 a" -| "b7s (More a as) = (b7 a) \ (b7s as)"*) +| "b7s (More a as) = (b7 a) \ (b7s as)" (* example 8 from Peter Sewell's bestiary *) -(*nominal_datatype exp8 = +nominal_datatype exp8 = EVar name | EUnit | EPair exp8 exp8 @@ -570,7 +570,7 @@ | "b_fnclauses (S fc) = (b_fnclause fc)" | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" -| "b_fnclause (K x pat exp8) = {atom x}"*) +| "b_fnclause (K x pat exp8) = {atom x}"