# HG changeset patch # User Christian Urban # Date 1269105386 -3600 # Node ID f65564bcf34209708e08665509750722e89f7a76 # Parent a4743b7cd8872ef3e327ed345672f3773e2dce26# Parent 41294e4fc870c10dc003e139d8db31d1fee545fe merged diff -r a4743b7cd887 -r f65564bcf342 Nominal/Fv.thy --- a/Nominal/Fv.thy Sat Mar 20 16:27:51 2010 +0100 +++ b/Nominal/Fv.thy Sat Mar 20 18:16:26 2010 +0100 @@ -655,7 +655,7 @@ *} ML {* -fun build_alpha_refl_gl alphas (x, y, z) = +fun build_alpha_sym_trans_gl alphas (x, y, z) = let fun build_alpha alpha = let @@ -668,26 +668,84 @@ HOLogic.mk_all (z, ty, HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) in - ((alpha $ var $ var), (symp, transp)) + (symp, transp) end; - val (refl_eqs, eqs) = split_list (map build_alpha alphas) + val eqs = map build_alpha alphas val (sym_eqs, trans_eqs) = split_list eqs fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l in - (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) + (conj sym_eqs, conj trans_eqs) +end +*} + +ML {* +fun build_alpha_refl_gl fv_alphas_lst = +let + val (fvs_alphas, ls) = split_list fv_alphas_lst; + val (_, alpha_ts) = split_list fvs_alphas; + val tys = map (domain_type o fastype_of) alpha_ts; + val names = Datatype_Prop.make_tnames tys; + val args = map Free (names ~~ tys); + fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg; + fun refl_eq_arg ((alpha, arg), l) = + foldr1 HOLogic.mk_conj + ((alpha $ arg $ arg) :: + (map (mk_alpha_refl arg) l)) + val eqs = map refl_eq_arg ((alpha_ts ~~ args) ~~ ls) +in + (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs)) end *} ML {* -fun reflp_tac induct inj ctxt = +fun reflp_tac induct eq_iff ctxt = rtac induct THEN_ALL_NEW - simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW + simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left supp_zero_perm Int_empty_left split_conv}) *} +ML {* +fun build_alpha_refl fv_alphas_lst induct eq_iff ctxt = +let + val (names, gl) = build_alpha_refl_gl fv_alphas_lst; + val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1); +in + HOLogic.conj_elims refl_conj +end +*} + +ML {* +fun build_alpha_alphabn fv_alphas_lst inducts eq_iff ctxt = +let + val (fvs_alphas, ls) = split_list fv_alphas_lst; + val (_, alpha_ts) = split_list fvs_alphas; + val tys = map (domain_type o fastype_of) alpha_ts; + val names = Datatype_Prop.make_tnames tys; + val names2 = Name.variant_list names names; + val args = map Free (names ~~ tys); + val args2 = map Free (names2 ~~ tys); + fun alpha_alphabn ((alpha, (arg, arg2)), (no, l)) = + if l = [] then [] else + let + val alpha_bns = map snd l; + val lhs = alpha $ arg $ arg2; + val rhs = foldr1 HOLogic.mk_conj (map (fn x => x $ arg $ arg2) alpha_bns); + val gl = Logic.mk_implies (HOLogic.mk_Trueprop lhs, HOLogic.mk_Trueprop rhs); + fun tac _ = (etac (nth inducts no) THEN_ALL_NEW TRY o rtac @{thm TrueI} + THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps eq_iff)) 1 + val th = Goal.prove ctxt (names @ names2) [] gl tac; + in + Project_Rule.projects ctxt (1 upto length l) th + end; + val eqs = map alpha_alphabn ((alpha_ts ~~ (args ~~ args2)) ~~ ((0 upto (length ls - 1)) ~~ ls)); +in + flat eqs +end +*} + lemma exi_neg: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (- p)) \ \pi. Q pi" apply (erule exE) @@ -787,25 +845,22 @@ *} ML {* -fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = +fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = let val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; - val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) - fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1; + val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z) fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1; fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; - val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; - val symt = Goal.prove ctxt' [] [] symg symp_tac'; - val transt = Goal.prove ctxt' [] [] transg transp_tac'; - val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] - val reflts = HOLogic.conj_elims refltg - val symts = HOLogic.conj_elims symtg - val transts = HOLogic.conj_elims transtg + val symp_loc = Goal.prove ctxt' [] [] symg symp_tac'; + val transp_loc = Goal.prove ctxt' [] [] transg transp_tac'; + val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc] + val symps = HOLogic.conj_elims symp + val transps = HOLogic.conj_elims transp fun equivp alpha = let val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) val goal = @{term Trueprop} $ (equivp $ alpha) - fun tac _ = equivp_tac reflts symts transts 1 + fun tac _ = equivp_tac reflps symps transps 1 in Goal.prove ctxt [] [] goal tac end diff -r a4743b7cd887 -r f65564bcf342 Nominal/LFex.thy --- a/Nominal/LFex.thy Sat Mar 20 16:27:51 2010 +0100 +++ b/Nominal/LFex.thy Sat Mar 20 18:16:26 2010 +0100 @@ -6,7 +6,7 @@ atom_decl ident ML {* val _ = cheat_fv_rsp := false *} -ML {* val _ = cheat_const_rsp := false *} +ML {* val _ = cheat_alpha_bn_rsp := false *} ML {* val _ = cheat_equivp := false *} nominal_datatype kind = diff -r a4743b7cd887 -r f65564bcf342 Nominal/Parser.thy --- a/Nominal/Parser.thy Sat Mar 20 16:27:51 2010 +0100 +++ b/Nominal/Parser.thy Sat Mar 20 18:16:26 2010 +0100 @@ -267,7 +267,7 @@ (* These 2 are critical, we don't know how to do it in term5 *) ML {* val cheat_fv_rsp = Unsynchronized.ref true *} -ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) +ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *} ML {* val cheat_equivp = Unsynchronized.ref true *} @@ -332,9 +332,11 @@ else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; val _ = tracing "Proving equivalence"; + val fv_alpha_all = combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; + val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a; val alpha_equivp = if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn - else build_equivps alpha_ts induct alpha_induct + else build_equivps alpha_ts reflps alpha_induct inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a; val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; @@ -361,10 +363,13 @@ val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; - fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy - else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1 - val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] - const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 + val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11; + fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 + fun alpha_bn_rsp_tac x = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else const_rsp_tac x + val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] + const_rsp_tac) raw_consts lthy11 + val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] + alpha_bn_rsp_tac) alpha_ts_bn lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; diff -r a4743b7cd887 -r f65564bcf342 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Sat Mar 20 16:27:51 2010 +0100 +++ b/Nominal/Rsp.thy Sat Mar 20 18:16:26 2010 +0100 @@ -95,18 +95,15 @@ *} ML {* -fun constr_rsp_tac inj rsp equivps = -let - val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps -in +fun constr_rsp_tac inj rsp = REPEAT o rtac impI THEN' simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW (asm_simp_tac HOL_ss THEN_ALL_NEW ( - rtac @{thm exI[of _ "0 :: perm"]} THEN' - asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ - @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) + REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps (rsp @ + @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) )) -end *} (* Testing code diff -r a4743b7cd887 -r f65564bcf342 Nominal/TySch.thy --- a/Nominal/TySch.thy Sat Mar 20 16:27:51 2010 +0100 +++ b/Nominal/TySch.thy Sat Mar 20 18:16:26 2010 +0100 @@ -5,7 +5,7 @@ atom_decl name ML {* val _ = cheat_fv_rsp := false *} -ML {* val _ = cheat_const_rsp := false *} +ML {* val _ = cheat_alpha_bn_rsp := false *} ML {* val _ = cheat_equivp := false *} nominal_datatype t = @@ -14,6 +14,51 @@ and tyS = All xs::"name fset" ty::"t" bind xs in ty +lemma size_eqvt: "size (pi \ x) = size x" +sorry (* Can this be shown? *) + +instantiation t and tyS :: size begin + +quotient_definition + "size_t :: t \ nat" +is + "size :: t_raw \ nat" + +quotient_definition + "size_tyS :: tyS \ nat" +is + "size :: tyS_raw \ nat" + +lemma size_rsp: + "alpha_t_raw x y \ size x = size y" + "alpha_tyS_raw a b \ size a = size b" + apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts) + apply (simp_all only: t_raw_tyS_raw.size) + apply (simp_all only: alpha_gen) + apply clarify + apply (simp_all only: size_eqvt) + done + +lemma [quot_respect]: + "(alpha_t_raw ===> op =) size size" + "(alpha_tyS_raw ===> op =) size size" + by (simp_all add: size_rsp) + +lemma [quot_preserve]: + "(rep_t ---> id) size = size" + "(rep_tyS ---> id) size = size" + by (simp_all add: size_t_def size_tyS_def) + +instance + by default + +end + +thm t_raw_tyS_raw.size(4)[quot_lifted] +thm t_raw_tyS_raw.size(5)[quot_lifted] +thm t_raw_tyS_raw.size(6)[quot_lifted] + + thm t_tyS.fv thm t_tyS.eq_iff thm t_tyS.bn diff -r a4743b7cd887 -r f65564bcf342 TODO --- a/TODO Sat Mar 20 16:27:51 2010 +0100 +++ b/TODO Sat Mar 20 18:16:26 2010 +0100 @@ -24,10 +24,10 @@ - strong induction rules -- show support equations +- check support equations for more bindings per constructor - automate the proofs that are currently proved with sorry: - alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp + alpha_equivp, fv_rsp, alpha_bn_rsp - store information about defined nominal datatypes, so that it can be used to define new types that depend on these