# HG changeset patch # User Cezary Kaliszyk # Date 1269534646 -3600 # Node ID 4b949985cf5771f91b2915c83f9a25294a060474 # Parent ba837d3ed37f37311ca7061abe978032d862c521 Gathering things to prove by induction together; removed cheat_bn_eqvt. diff -r ba837d3ed37f -r 4b949985cf57 Nominal/ExCoreHaskell.thy --- a/Nominal/ExCoreHaskell.thy Thu Mar 25 15:06:58 2010 +0100 +++ b/Nominal/ExCoreHaskell.thy Thu Mar 25 17:30:46 2010 +0100 @@ -5,7 +5,6 @@ (* core haskell *) ML {* val _ = recursive := false *} -ML {* val _ = cheat_bn_eqvt := true *} ML {* val _ = cheat_bn_rsp := true *} ML {* val _ = cheat_const_rsp := true *} ML {* val _ = cheat_alpha_bn_rsp := true *} diff -r ba837d3ed37f -r 4b949985cf57 Nominal/ExLet.thy --- a/Nominal/ExLet.thy Thu Mar 25 15:06:58 2010 +0100 +++ b/Nominal/ExLet.thy Thu Mar 25 17:30:46 2010 +0100 @@ -7,6 +7,8 @@ atom_decl name ML {* val _ = recursive := false *} + + nominal_datatype trm = Vr "name" | Ap "trm" "trm" diff -r ba837d3ed37f -r 4b949985cf57 Nominal/Fv.thy --- a/Nominal/Fv.thy Thu Mar 25 15:06:58 2010 +0100 +++ b/Nominal/Fv.thy Thu Mar 25 17:30:46 2010 +0100 @@ -1099,4 +1099,55 @@ simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) *} +(* Given function for buildng a goal for an input, prepares a + one common goals for all the inputs and proves it by induction + together *) +ML {* +fun prove_by_induct tys build_goal ind utac inputs ctxt = +let + val names = Datatype_Prop.make_tnames tys; + val (names', ctxt') = Variable.variant_fixes names ctxt; + val frees = map Free (names' ~~ tys); + val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt'; + val gls = flat gls_lists; + fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls; + val trm_gl_lists = map trm_gls_map frees; + val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists + val trm_gls = map mk_conjl trm_gl_lists; + val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls); + fun tac {context,...} = ((fn _ => print_tac (PolyML.makestring names')) THEN' + InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind] + THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1 + val th_loc = Goal.prove ctxt'' [] [] gl tac + val ths_loc = HOLogic.conj_elims th_loc + val ths = Variable.export ctxt'' ctxt ths_loc +in + filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths end +*} + +ML {* +fun build_eqvt_gl pi frees fnctn ctxt = +let + val typ = domain_type (fastype_of fnctn); + val arg = the (AList.lookup (op=) frees typ); +in + ([HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) +end +*} + +ML {* +fun prove_eqvt tys ind simps funs ctxt = +let + val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt; + val pi = Free (pi, @{typ perm}); + val tac = asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: simps @ all_eqvts ctxt')) + val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt' + val ths = Variable.export ctxt' ctxt ths_loc + val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) +in + (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) +end +*} + +end diff -r ba837d3ed37f -r 4b949985cf57 Nominal/Parser.thy --- a/Nominal/Parser.thy Thu Mar 25 15:06:58 2010 +0100 +++ b/Nominal/Parser.thy Thu Mar 25 17:30:46 2010 +0100 @@ -287,8 +287,6 @@ *} ML {* val cheat_equivp = Unsynchronized.ref false *} -ML {* val cheat_bn_eqvt = Unsynchronized.ref false *} -ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} ML {* val cheat_bn_rsp = Unsynchronized.ref false *} ML {* val cheat_fv_rsp = Unsynchronized.ref false *} @@ -314,8 +312,9 @@ val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); - val descr = #descr dtinfo; - val sorts = #sorts dtinfo; + val {descr, sorts, ...} = dtinfo; + fun nth_dtyp i = typ_of_dtyp descr sorts (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_full_tnames = map (fn (_, (n, _, _)) => n) descr; val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; @@ -345,39 +344,26 @@ ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 val _ = tracing "Proving equivariance"; - fun build_bv_eqvt simps inducts (t, n) ctxt = - build_eqvts Binding.empty [t] - (if !cheat_bn_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) - else build_eqvts_tac (nth inducts n) simps ctxt - ) ctxt - val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; - val fv_eqvt_tac = - if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) - else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5 - val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5; - val (fv_bn_eqvts, lthy6a) = - if fv_ts_bn = [] then ([], lthy6) else - fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts) - (fv_ts_bn ~~ bn_nos) lthy6; - val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts) + 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_ts_nobn @ fv_ts_bn) lthy5 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 @ raw_fv_bv_eqvt) lthy6a 1 - val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; + else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1 + val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; val _ = tracing "Proving equivalence"; val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts; val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; - val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6a; + val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; val alpha_equivp = - if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn + if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn else build_equivps alpha_ts reflps alpha_induct - inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a; + inject alpha_eq_iff 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 val lthy7 = define_quotient_type (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) - (ALLGOALS (resolve_tac alpha_equivp)) lthy6a; + (ALLGOALS (resolve_tac alpha_equivp)) lthy6; val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); val raw_consts = flat (map (fn (i, (_, _, l)) => @@ -455,7 +441,7 @@ val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; val q_dis = map (lift_thm lthy18) rel_dists; val lthy19 = note_simp_suffix "distinct" q_dis lthy18; - val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; + val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt); val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; val _ = tracing "Finite Support"; diff -r ba837d3ed37f -r 4b949985cf57 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Thu Mar 25 15:06:58 2010 +0100 +++ b/Nominal/Rsp.thy Thu Mar 25 17:30:46 2010 +0100 @@ -125,37 +125,14 @@ *) ML {* -fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps - (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 -*} - -ML {* fun perm_arg arg = let val ty = fastype_of arg in Const (@{const_name permute}, @{typ perm} --> ty --> ty) end -*} - -ML {* -fun build_eqvts bind funs tac ctxt = -let - val pi = Free ("p", @{typ perm}); - val types = map (domain_type o fastype_of) funs; - val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types); - val args = map Free (indnames ~~ types); - val perm_at = @{term "permute :: perm \ atom set \ atom set"} - fun eqvtc (fnctn, arg) = - HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) - val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args))) - val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames) - val thms = HOLogic.conj_elims thm -in - Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt -end +val perm_at = @{term "permute :: perm \ atom set \ atom set"} *} lemma exi: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (pi \ p)) \ \pi. Q pi"