# HG changeset patch # User Christian Urban # Date 1272947815 -3600 # Node ID 837b889fcf5901703b237fb8e3d54a580ed7a448 # Parent 74bd7bfb484b57190e27bb50268e786aa2414b12# Parent d361a4699176eb9edb05b4db1046fc9848172f6f merged diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/Equivp.thy --- a/Nominal/Equivp.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/Equivp.thy Tue May 04 05:36:55 2010 +0100 @@ -1,5 +1,5 @@ theory Equivp -imports "NewFv" "Tacs" "Rsp" "NewFv" +imports "NewFv" "Tacs" "Rsp" begin ML {* diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/Ex/Classical.thy Tue May 04 05:36:55 2010 +0100 @@ -12,6 +12,10 @@ atom_decl name atom_decl coname +ML {* val _ = cheat_alpha_eqvt := true *} +ML {* val _ = cheat_equivp := true *} +ML {* val _ = cheat_fv_rsp := true *} + nominal_datatype trm = Ax "name" "coname" | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/Ex/Ex2.thy --- a/Nominal/Ex/Ex2.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/Ex/Ex2.thy Tue May 04 05:36:55 2010 +0100 @@ -1,35 +1,31 @@ theory Ex2 -imports "../Parser" +imports "../NewParser" begin text {* example 2 *} atom_decl name -ML {* val _ = recursive := false *} -nominal_datatype trm' = +nominal_datatype trm = Var "name" -| App "trm'" "trm'" -| Lam x::"name" t::"trm'" bind x in t -| Let p::"pat'" "trm'" t::"trm'" bind "f p" in t -and pat' = +| App "trm" "trm" +| Lam x::"name" t::"trm" bind_set x in t +| Let p::"pat" "trm" t::"trm" bind_set "f p" in t +and pat = PN | PS "name" | PD "name" "name" binder - f::"pat' \ atom set" + f::"pat \ atom set" where "f PN = {}" | "f (PD x y) = {atom x, atom y}" | "f (PS x) = {atom x}" - -thm trm'_pat'.fv -thm trm'_pat'.eq_iff -thm trm'_pat'.bn -thm trm'_pat'.perm -thm trm'_pat'.induct -thm trm'_pat'.distinct -thm trm'_pat'.fv[simplified trm'_pat'.supp] +thm trm_pat.bn +thm trm_pat.perm +thm trm_pat.induct +thm trm_pat.distinct +thm trm_pat.fv[simplified trm_pat.supp(1-2)] end diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/Ex/Ex3.thy --- a/Nominal/Ex/Ex3.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/Ex/Ex3.thy Tue May 04 05:36:55 2010 +0100 @@ -1,35 +1,34 @@ theory Ex3 -imports "../Parser" +imports "../NewParser" begin (* Example 3, identical to example 1 from Terms.thy *) atom_decl name -ML {* val _ = recursive := false *} -nominal_datatype trm0 = - Var0 "name" -| App0 "trm0" "trm0" -| Lam0 x::"name" t::"trm0" bind x in t -| Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t -and pat0 = - PN0 -| PS0 "name" -| PD0 "pat0" "pat0" +nominal_datatype trm = + Var "name" +| App "trm" "trm" +| Lam x::"name" t::"trm" bind_set x in t +| Let p::"pat" "trm" t::"trm" bind_set "f p" in t +and pat = + PN +| PS "name" +| PD "pat" "pat" binder - f0::"pat0 \ atom set" + f::"pat \ atom set" where - "f0 PN0 = {}" -| "f0 (PS0 x) = {atom x}" -| "f0 (PD0 p1 p2) = (f0 p1) \ (f0 p2)" + "f PN = {}" +| "f (PS x) = {atom x}" +| "f (PD p1 p2) = (f p1) \ (f p2)" -thm trm0_pat0.fv -thm trm0_pat0.eq_iff -thm trm0_pat0.bn -thm trm0_pat0.perm -thm trm0_pat0.induct -thm trm0_pat0.distinct -thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars] +thm trm_pat.fv +thm trm_pat.eq_iff +thm trm_pat.bn +thm trm_pat.perm +thm trm_pat.induct +thm trm_pat.distinct +thm trm_pat.fv[simplified trm_pat.supp(1-2)] end diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Tue May 04 05:36:55 2010 +0100 @@ -1,16 +1,14 @@ theory SingleLet -imports "../Parser" +imports "../NewParser" begin atom_decl name -ML {* val _ = recursive := false *} - nominal_datatype trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind x in t -| Let a::"assg" t::"trm" bind "bn a" in t +| Lam x::"name" t::"trm" bind_set x in t +| Let a::"assg" t::"trm" bind_set "bn a" in t and assg = As "name" "trm" binder @@ -18,19 +16,23 @@ where "bn (As x t) = {atom x}" -print_theorems -thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] - thm trm_assg.fv thm trm_assg.supp -thm trm_assg.eq_iff[simplified alphas_abs[symmetric]] +thm trm_assg.eq_iff thm trm_assg.bn thm trm_assg.perm thm trm_assg.induct thm trm_assg.inducts thm trm_assg.distinct ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} -thm trm_assg.fv[simplified trm_assg.supp] +thm trm_assg.fv[simplified trm_assg.supp(1-2)] + +(* +setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} +declare permute_trm_raw_permute_assg_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] +equivariance alpha_trm_raw +*) end diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/Fv.thy --- a/Nominal/Fv.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/Fv.thy Tue May 04 05:36:55 2010 +0100 @@ -650,4 +650,29 @@ end *} + +ML {* +fun define_fv_alpha_export dt binds bns ctxt = +let + val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') = + define_fv dt binds bns ctxt; + val (alpha, ctxt'') = + define_alpha dt binds bns fv_ts_loc ctxt'; + val alpha_ts_loc = #preds alpha + val alpha_induct_loc = #induct alpha + val alpha_intros_loc = #intrs alpha; + val alpha_cases_loc = #elims alpha + val morphism = ProofContext.export_morphism ctxt'' ctxt; + val fv_ts = map (Morphism.term morphism) fv_ts_loc; + val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc; + val fv_def = Morphism.fact morphism fv_def_loc; + val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; + val alpha_induct = Morphism.thm morphism alpha_induct_loc; + val alpha_intros = Morphism.fact morphism alpha_intros_loc + val alpha_cases = Morphism.fact morphism alpha_cases_loc +in + ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'') +end; +*} + end diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/Lift.thy --- a/Nominal/Lift.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/Lift.thy Tue May 04 05:36:55 2010 +0100 @@ -1,8 +1,8 @@ theory Lift -imports "../Nominal-General/Nominal2_Atoms" - "../Nominal-General/Nominal2_Eqvt" - "../Nominal-General/Nominal2_Supp" - "Abs" "Perm" "Equivp" "Rsp" "Attic/Fv" +imports "../Nominal-General/Nominal2_Atoms" + "../Nominal-General/Nominal2_Eqvt" + "../Nominal-General/Nominal2_Supp" + "Abs" "Perm" "Equivp" "Rsp" begin @@ -66,32 +66,5 @@ end *} - - - -ML {* -fun define_fv_alpha_export dt binds bns ctxt = -let - val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') = - define_fv dt binds bns ctxt; - val (alpha, ctxt'') = - define_alpha dt binds bns fv_ts_loc ctxt'; - val alpha_ts_loc = #preds alpha - val alpha_induct_loc = #induct alpha - val alpha_intros_loc = #intrs alpha; - val alpha_cases_loc = #elims alpha - val morphism = ProofContext.export_morphism ctxt'' ctxt; - val fv_ts = map (Morphism.term morphism) fv_ts_loc; - val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc; - val fv_def = Morphism.fact morphism fv_def_loc; - val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; - val alpha_induct = Morphism.thm morphism alpha_induct_loc; - val alpha_intros = Morphism.fact morphism alpha_intros_loc - val alpha_cases = Morphism.fact morphism alpha_cases_loc -in - ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'') -end; -*} - end diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/NewParser.thy Tue May 04 05:36:55 2010 +0100 @@ -159,8 +159,9 @@ end *} -text {* What does the prep_bn code do? Cezary's Function? *} - +(* strip_bn_fun takes a bn function defined by the user as a union or + append of elements and returns those elements together with bn functions + applied *) ML {* fun strip_bn_fun t = case t of @@ -258,6 +259,31 @@ end *} +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 {* val cheat_alpha_eqvt = Unsynchronized.ref false *} +ML {* val cheat_equivp = Unsynchronized.ref false *} +ML {* val cheat_fv_rsp = Unsynchronized.ref false *} +ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} +ML {* val cheat_supp_eq = Unsynchronized.ref false *} + +ML {* +fun remove_loop t = + let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end + handle TERM _ => @{thm eqTrueI} OF [t] +*} text {* nominal_datatype2 does the following things in order: @@ -335,7 +361,7 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); val {descr, sorts, ...} = dtinfo; val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; - val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) + val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; @@ -380,21 +406,26 @@ (* definition of raw_alpha_eq_iff lemmas *) val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 - + val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; + val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp); + (* proving equivariance lemmas *) val _ = warning "Proving equivariance"; val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 - fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy + fun alpha_eqvt_tac' _ = + if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy + else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; (* provind alpha equivalence *) val _ = warning "Proving equivalence"; val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; - val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; + val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff_simp lthy6; val alpha_equivp = - build_equivps alpha_ts reflps alpha_induct - inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; + if !cheat_equivp then map (equivp_hack lthy6) alpha_ts + else build_equivps alpha_ts reflps alpha_induct + inject alpha_eq_iff_simp distincts alpha_cases alpha_eqvt lthy6; val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; val qty_full_names = map (Long_Name.qualify thy_name) qty_names @@ -403,8 +434,8 @@ val raw_consts = flat (map (fn (i, (_, _, l)) => map (fn (cname, dts) => - Const (cname, map (typ_of_dtyp descr sorts) dts ---> - typ_of_dtyp descr sorts (DtRec i))) l) descr); + Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> + Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; val _ = warning "Proving respects"; val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; @@ -412,8 +443,9 @@ fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => resolve_tac bns_rsp_pre' 1)) bns lthy8; val bns_rsp = flat (map snd bns_rsp_pre); - (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*) - fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy + + fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy + else fvbv_rsp_tac alpha_induct fv_def lthy8 1; val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; val (fv_rsp_pre, lthy10) = fold_map (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] @@ -421,11 +453,14 @@ val fv_rsp = flat (map snd fv_rsp_pre); val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; + fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy + else + let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] - (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11 + alpha_bn_rsp_tac) alpha_ts_bn lthy11 fun const_rsp_tac _ = - let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a - in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end + let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a + in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] const_rsp_tac) raw_consts lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) @@ -463,7 +498,7 @@ val lthy17 = note_simp_suffix "bn" q_bn lthy16; val _ = warning "Lifting eq-iff"; (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) - val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff + val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; @@ -487,7 +522,10 @@ val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; val (names, supp_eq_t) = supp_eq fv_alpha_all; val _ = warning "Support Equations"; - val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => []; + fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else + supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1; + val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e => + let val _ = warning ("Support eqs failed") in [] end; val lthy23 = note_suffix "supp" q_supp lthy22; in (0, lthy23) @@ -660,7 +698,7 @@ (main_parser >> nominal_datatype2_cmd) *} -atom_decl name +(*atom_decl name nominal_datatype lam = Var name @@ -740,7 +778,7 @@ thm ty_tys.fv[simplified ty_tys.supp] thm ty_tys.eq_iff - +*) (* some further tests *) diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/Parser.thy --- a/Nominal/Parser.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/Parser.thy Tue May 04 05:36:55 2010 +0100 @@ -1,8 +1,8 @@ theory Parser -imports "../Nominal-General/Nominal2_Atoms" - "../Nominal-General/Nominal2_Eqvt" - "../Nominal-General/Nominal2_Supp" - "Perm" "Equivp" "Rsp" "Lift" +imports "../Nominal-General/Nominal2_Atoms" + "../Nominal-General/Nominal2_Eqvt" + "../Nominal-General/Nominal2_Supp" + "Perm" "Equivp" "Rsp" "Lift" "Fv" begin section{* Interface for nominal_datatype *} @@ -372,9 +372,9 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); val {descr, sorts, ...} = dtinfo; - fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i); val raw_tys = map (fn (i, _) => nth_dtyp i) descr; - val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) + val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; val rel_dtinfos = List.take (dtinfos, (length dts)); @@ -423,8 +423,8 @@ val raw_consts = flat (map (fn (i, (_, _, l)) => map (fn (cname, dts) => - Const (cname, map (typ_of_dtyp descr sorts) dts ---> - typ_of_dtyp descr sorts (DtRec i))) l) descr); + Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> + Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; val _ = tracing "Proving respects"; val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; @@ -483,7 +483,7 @@ val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; val lthy17 = note_simp_suffix "bn" q_bn lthy16; val _ = tracing "Lifting eq-iff"; - val _ = map tracing (map PolyML.makestring alpha_eq_iff); +(* val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 diff -r 74bd7bfb484b -r 837b889fcf59 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Tue May 04 05:36:43 2010 +0100 +++ b/Nominal/Rsp.thy Tue May 04 05:36:55 2010 +0100 @@ -97,7 +97,7 @@ ML {* fun alpha_eqvt_tac induct simps ctxt = rel_indtac induct THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps