# HG changeset patch # User Cezary Kaliszyk # Date 1271254244 -7200 # Node ID 9a8decba77c50cc9cca5017be1db98e909518833 # Parent 9978fc6d91e9865165f240624c5b8e0bbac9246b# Parent edc2a52cd457bb8e40f368ef388e3408ae1fa567 merge diff -r edc2a52cd457 -r 9a8decba77c5 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Wed Apr 14 11:07:42 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Wed Apr 14 16:10:44 2010 +0200 @@ -371,144 +371,4 @@ (* apply(perm_strict_simp) *) oops -atom_decl var - -ML {* -val inductive_atomize = @{thms induct_atomize}; - -val atomize_conv = - MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) - (HOL_basic_ss addsimps inductive_atomize); -val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); -fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 - (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); - -fun map_term f t u = (case f t u of - NONE => map_term' f t u | x => x) -and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u u') of - (NONE, NONE) => NONE - | (SOME t'', NONE) => SOME (t'' $ u) - | (NONE, SOME u'') => SOME (t $ u'') - | (SOME t'', SOME u'') => SOME (t'' $ u'')) - | map_term' f (Abs (s, T, t)) (Abs (s', T', t')) = (case map_term f t t' of - NONE => NONE - | SOME t'' => SOME (Abs (s, T, t''))) - | map_term' _ _ _ = NONE; - - -fun map_thm ctxt f tac monos opt th = - let - val prop = prop_of th; - fun prove t = - Goal.prove ctxt [] [] t (fn _ => - EVERY [cut_facts_tac [th] 1, etac rev_mp 1, - REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), - REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]) - in Option.map prove (map_term f prop (the_default prop opt)) end; - -fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of - Const (name, _) => - if name mem names then SOME (f p q) else NONE - | _ => NONE) - | split_conj _ _ _ _ = NONE; -*} - -ML {* -val perm_bool = @{thm "permute_bool_def"}; -val perm_boolI = @{thm "permute_boolI"}; -val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb - (Drule.strip_imp_concl (cprop_of perm_boolI)))); - -fun mk_perm_bool pi th = th RS Drule.cterm_instantiate - [(perm_boolI_pi, pi)] perm_boolI; - -*} - -ML {* -fun transp ([] :: _) = [] - | transp xs = map hd xs :: transp (map tl xs); - -fun prove_eqvt s xatoms ctxt = - let - val thy = ProofContext.theory_of ctxt; - val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy s); - val raw_induct = atomize_induct ctxt raw_induct; - val elims = map (atomize_induct ctxt) elims; - val intrs = map atomize_intr intrs; - val monos = Inductive.get_monos ctxt; - val intrs' = Inductive.unpartition_rules intrs - (map (fn (((s, ths), (_, k)), th) => - (s, ths ~~ Inductive.infer_intro_vars th k ths)) - (Inductive.partition_rules raw_induct intrs ~~ - Inductive.arities_of raw_induct ~~ elims)); - val k = length (Inductive.params_of raw_induct); - val atoms' = ["var"]; - val atoms = - if null xatoms then atoms' else - let val atoms = map (Sign.intern_type thy) xatoms - in - (case duplicates op = atoms of - [] => () - | xs => error ("Duplicate atoms: " ^ commas xs); - case subtract (op =) atoms' atoms of - [] => () - | xs => error ("No such atoms: " ^ commas xs); - atoms) - end; - val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; - val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps - (Nominal_ThmDecls.get_eqvts_thms ctxt @ perm_pi_simp); - val (([t], [pi]), ctxt') = ctxt |> - Variable.import_terms false [concl_of raw_induct] ||>> - Variable.variant_fixes ["pi"]; - val ps = map (fst o HOLogic.dest_imp) - (HOLogic.dest_conj (HOLogic.dest_Trueprop t)); - fun eqvt_tac ctxt'' pi (intr, vs) st = - let - fun eqvt_err s = - let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt - in error ("Could not prove equivariance for introduction rule\n" ^ - Syntax.string_of_term ctxt''' t ^ "\n" ^ s) - end; - val res = SUBPROOF (fn {prems, params, ...} => - let - val prems' = map (fn th => the_default th (map_thm ctxt' - (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; - val prems'' = map (fn th => Simplifier.simplify eqvt_ss - (mk_perm_bool (cterm_of thy pi) th)) prems'; - val intr' = intr - in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1 - end) ctxt' 1 st - in - case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of - NONE => eqvt_err ("Rule does not match goal\n" ^ - Syntax.string_of_term ctxt'' (hd (prems_of st))) - | SOME (th, _) => Seq.single th - end; - val thss = map (fn atom => - let val pi' = Free (pi, @{typ perm}) - in map (fn th => zero_var_indexes (th RS mp)) - (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p => - let - val (h, ts) = strip_comb p; - val (ts1, ts2) = chop k ts - in - HOLogic.mk_imp (p, list_comb (h, ts1)) - end) ps))) - (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs => - full_simp_tac eqvt_ss 1 THEN - eqvt_tac context pi' intr_vs) intrs')) |> - singleton (ProofContext.export ctxt' ctxt))) - end) atoms - in - ctxt |> - Local_Theory.notes (map (fn (name, ths) => - ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"), - [Attrib.internal (K Nominal_ThmDecls.eqvt_add)]), [(ths, [])])) - (names ~~ transp thss)) |> snd - end; -*} - end diff -r edc2a52cd457 -r 9a8decba77c5 Nominal/Equivp.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Equivp.thy Wed Apr 14 16:10:44 2010 +0200 @@ -0,0 +1,367 @@ +theory Equivp +imports "Fv" +begin + +ML {* +fun build_alpha_sym_trans_gl alphas (x, y, z) = +let + fun build_alpha alpha = + let + val ty = domain_type (fastype_of alpha); + val var = Free(x, ty); + val var2 = Free(y, ty); + val var3 = Free(z, ty); + val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); + val transp = HOLogic.mk_imp (alpha $ var $ var2, + HOLogic.mk_all (z, ty, + HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) + in + (symp, transp) + end; + 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 sym_eqs, conj trans_eqs) +end +*} + +ML {* +fun build_alpha_refl_gl fv_alphas_lst alphas = +let + val (fvs_alphas, _) = 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 find_alphas ty x = + domain_type (fastype_of x) = ty; + fun refl_eq_arg (ty, arg) = + let + val rel_alphas = filter (find_alphas ty) alphas; + in + map (fn x => x $ arg $ arg) rel_alphas + end; + (* Flattening loses the induction structure *) + val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args)) +in + (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs)) +end +*} + +ML {* +fun reflp_tac induct eq_iff = + rtac induct THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW + split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} + THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps + @{thms alphas 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 alphas induct eq_iff ctxt = +let + val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas; + val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1); +in + HOLogic.conj_elims refl_conj +end +*} + +lemma exi_neg: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (- p)) \ \pi. Q pi" +apply (erule exE) +apply (rule_tac x="-pi" in exI) +by auto + +ML {* +fun symp_tac induct inj eqvt ctxt = + rel_indtac induct THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac + THEN_ALL_NEW + REPEAT o etac @{thm exi_neg} + THEN_ALL_NEW + split_conj_tac THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW + TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW + (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) +*} + + +lemma exi_sum: "\(pi :: perm). P pi \ \(pi :: perm). Q pi \ (\(p :: perm) (pi :: perm). P p \ Q pi \ R (pi + p)) \ \pi. R pi" +apply (erule exE)+ +apply (rule_tac x="pia + pi" in exI) +by auto + + +ML {* +fun eetac rule = + Subgoal.FOCUS_PARAMS (fn focus => + let + val concl = #concl focus + val prems = Logic.strip_imp_prems (term_of concl) + val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems + val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs + val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs + in + (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1 + end + ) +*} + +ML {* +fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = + rel_indtac induct THEN_ALL_NEW + (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW + split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac + THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) + THEN_ALL_NEW split_conj_tac THEN_ALL_NEW + TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW + (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) +*} + +lemma transpI: + "(\xa ya. R xa ya \ (\z. R ya z \ R xa z)) \ transp R" + unfolding transp_def + by blast + +ML {* +fun equivp_tac reflps symps transps = + (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *) + simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) + THEN' rtac conjI THEN' rtac allI THEN' + resolve_tac reflps THEN' + rtac conjI THEN' rtac allI THEN' rtac allI THEN' + resolve_tac symps THEN' + rtac @{thm transpI} THEN' resolve_tac transps +*} + +ML {* +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 (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 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 reflps symps transps 1 + in + Goal.prove ctxt [] [] goal tac + end +in + map equivp alphas +end +*} + +lemma not_in_union: "c \ a \ b \ (c \ a \ c \ b)" +by auto + +ML {* +fun supports_tac perm = + simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( + REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN' + asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] + swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh + supp_fset_to_set supp_fmap_atom})) +*} + +ML {* +fun mk_supp ty x = + Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x +*} + +ML {* +fun mk_supports_eq thy cnstr = +let + val (tys, ty) = (strip_type o fastype_of) cnstr + val names = Datatype_Prop.make_tnames tys + val frees = map Free (names ~~ tys) + val rhs = list_comb (cnstr, frees) + + fun mk_supp_arg (x, ty) = + if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else + if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else + if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) + else mk_supp ty x + val lhss = map mk_supp_arg (frees ~~ tys) + val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) + val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) +in + (names, eq) +end +*} + +ML {* +fun prove_supports ctxt perms cnst = +let + val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst +in + Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) +end +*} + +ML {* +fun mk_fs tys = +let + val names = Datatype_Prop.make_tnames tys + val frees = map Free (names ~~ tys) + val supps = map2 mk_supp tys frees + val fin_supps = map (fn x => @{term "finite :: atom set \ bool"} $ x) supps +in + (names, HOLogic.mk_Trueprop (mk_conjl fin_supps)) +end +*} + +ML {* +fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW ( + rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set + supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp}) +*} + +ML {* +fun prove_fs ctxt induct supports tys = +let + val (names, eq) = mk_fs tys +in + Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1) +end +*} + +ML {* +fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x; + +fun mk_supp_neq arg (fv, alpha) = +let + val collect = Const ("Collect", @{typ "(atom \ bool) \ atom \ bool"}); + val ty = fastype_of arg; + val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty); + val finite = @{term "finite :: atom set \ bool"} + val rhs = collect $ Abs ("a", @{typ atom}, + HOLogic.mk_not (finite $ + (collect $ Abs ("b", @{typ atom}, + HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg))))) +in + HOLogic.mk_eq (fv $ arg, rhs) +end; + +fun supp_eq fv_alphas_lst = +let + val (fvs_alphas, ls) = split_list fv_alphas_lst; + val (fv_ts, _) = split_list fvs_alphas; + val tys = map (domain_type o fastype_of) fv_ts; + val names = Datatype_Prop.make_tnames tys; + val args = map Free (names ~~ tys); + fun supp_eq_arg ((fv, arg), l) = + mk_conjl + ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) :: + (map (mk_supp_neq arg) l)) + val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls)) +in + (names, HOLogic.mk_Trueprop eqs) +end +*} + +ML {* +fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos = +if length fv_ts_bn < length alpha_ts_bn then + (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) []) +else let + val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1); + fun filter_fn i (x, j) = if j = i then SOME x else NONE; + val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos; + val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos; +in + (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all +end +*} + +(* TODO: this is a hack, it assumes that only one type of Abs's is present + in the type and chooses this supp_abs. Additionally single atoms are + treated properly. *) +ML {* +fun choose_alpha_abs eqiff = +let + fun exists_subterms f ts = true mem (map (exists_subterm f) ts); + val terms = map prop_of eqiff; + fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms + val no = + if check @{const_name alpha_lst} then 2 else + if check @{const_name alpha_res} then 1 else + if check @{const_name alpha_gen} then 0 else + error "Failure choosing supp_abs" +in + nth @{thms supp_abs[symmetric]} no +end +*} +lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}" +by (rule supp_abs(1)) + +lemma supp_abs_sum: + "supp (Abs x (a :: 'a :: fs)) \ supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" + "supp (Abs_res x (a :: 'a :: fs)) \ supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))" + "supp (Abs_lst y (a :: 'a :: fs)) \ supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))" + apply (simp_all add: supp_abs supp_Pair) + apply blast+ + done + + +ML {* +fun supp_eq_tac ind fv perm eqiff ctxt = + rel_indtac ind THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW + simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) +*} + + + +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_arg (fnctn $ arg) $ 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 (@{thms atom_eqvt permute_list.simps} @ 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 edc2a52cd457 -r 9a8decba77c5 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed Apr 14 11:07:42 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Wed Apr 14 16:10:44 2010 +0200 @@ -120,63 +120,132 @@ "valid []" | "\atom x \ Gamma; valid Gamma\ \ valid ((x, T)#Gamma)" +inductive + typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) +where + t_Var[intro]: "\valid \; (x, T) \ set \\ \ \ \ Var x : T" + | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" + | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" + + ML {* -fun my_tac ctxt intros = - Nominal_Permeq.eqvt_strict_tac ctxt [] [] - THEN' resolve_tac intros - THEN_ALL_NEW - (atac ORELSE' - EVERY' - [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}), - Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], - atac ]) +fun map_term f t = + (case f t of + NONE => map_term' f t + | x => x) +and map_term' f (t $ u) = + (case (map_term f t, map_term f u) of + (NONE, NONE) => NONE + | (SOME t'', NONE) => SOME (t'' $ u) + | (NONE, SOME u'') => SOME (t $ u'') + | (SOME t'', SOME u'') => SOME (t'' $ u'')) + | map_term' f (Abs (s, T, t)) = + (case map_term f t of + NONE => NONE + | SOME t'' => SOME (Abs (s, T, t''))) + | map_term' _ _ = NONE; + +fun map_thm_tac ctxt tac thm = +let + val monos = Inductive.get_monos ctxt +in + EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, + REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), + REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] +end + +(* + proves F[f t] from F[t] where F[t] is the given theorem + + - F needs to be monotone + - f returns either SOME for a term it fires + and NONE elsewhere +*) +fun map_thm ctxt f tac thm = +let + val opt_goal_trm = map_term f (prop_of thm) + fun prove goal = + Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) +in + case opt_goal_trm of + NONE => thm + | SOME goal => prove goal +end + +fun transform_prem ctxt names thm = +let + fun split_conj names (Const ("op &", _) $ p $ q) = + (case head_of p of + Const (name, _) => if name mem names then SOME q else NONE + | _ => NONE) + | split_conj _ _ = NONE; +in + map_thm ctxt (split_conj names) (etac conjunct2 1) thm +end *} +ML {* +open Nominal_Permeq +*} + +ML {* +fun single_case_tac ctxt pred_names pi intro = +let + val rule = Drule.instantiate' [] [SOME pi] @{thm permute_boolE} +in + eqvt_strict_tac ctxt [] [] THEN' + SUBPROOF (fn {prems, context as ctxt, ...} => + let + val prems' = map (transform_prem ctxt pred_names) prems + val side_cond_tac = EVERY' + [ rtac rule, + eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], + resolve_tac prems' ] + in + HEADGOAL (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) + end) ctxt +end +*} + +ML {* +fun eqvt_rel_tac pred_name = +let + val thy = ProofContext.theory_of ctxt + val ({names, ...}, {raw_induct, intrs, ...}) = + Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) + val param_no = length (Inductive.params_of raw_induct) + val (([raw_concl], [pi]), ctxt') = + ctxt |> Variable.import_terms false [concl_of raw_induct] + ||>> Variable.variant_fixes ["pi"]; + val preds = map (fst o HOLogic.dest_imp) + (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); +in + +end +*} + + + lemma [eqvt]: assumes a: "valid Gamma" shows "valid (p \ Gamma)" using a apply(induct) -apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) -done - -lemma - shows "valid Gamma \ valid (p \ Gamma)" -ML_prf {* -val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive @{context} (Sign.intern_const @{theory} "valid") -*} -apply(tactic {* rtac raw_induct 1 *}) -apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) +apply(tactic {* my_tac @{context} ["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(1)} 1 *}) +apply(tactic {* my_tac @{context }["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(2)} 1 *}) done - -thm eqvts -thm eqvts_raw - -inductive - typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) -where - t_Var[intro]: "\valid \; (x, T) \ set \\ \ \ \ Var x : T" - | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" - | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" - - -ML {* Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *} - lemma shows "Gamma \ t : T \ (p \ Gamma) \ (p \ t) : (p \ T)" ML_prf {* -val ({names, ...}, {raw_induct, intrs, elims, ...}) = +val ({names, ...}, {raw_induct, ...}) = Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *} apply(tactic {* rtac raw_induct 1 *}) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -apply(perm_strict_simp) -apply(rule typing.intros) -oops +apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(1)} 1 *}) +apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(2)} 1 *}) +apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(3)} 1 *}) +done lemma uu[eqvt]: assumes a: "Gamma \ t : T" diff -r edc2a52cd457 -r 9a8decba77c5 Nominal/Fv.thy --- a/Nominal/Fv.thy Wed Apr 14 11:07:42 2010 +0200 +++ b/Nominal/Fv.thy Wed Apr 14 16:10:44 2010 +0200 @@ -287,7 +287,6 @@ *} (* We assume no bindings in the type on which bn is defined *) -(* TODO: currently works only with current fv_bn function *) ML {* fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) = let @@ -416,9 +415,8 @@ Const (@{const_name set}, @{typ "atom list \ atom set"}) $ x else x *} -(* TODO: Notice datatypes without bindings and replace alpha with equality *) ML {* -fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = +fun define_fv (dt_info : Datatype_Aux.info) bindsall bns lthy = let val thy = ProofContext.theory_of lthy; val {descr, sorts, ...} = dt_info; @@ -436,18 +434,8 @@ val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns; val fvbns = map snd bn_fv_bns; val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; - val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => - "alpha_" ^ name_of_typ (nth_dtyp i)) descr); - val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; - val alpha_frees = map Free (alpha_names ~~ alpha_types); - (* We assume that a bn is either recursive or not *) - val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; - val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) = - alpha_bns dt_info alpha_frees bns bns_rec - val alpha_bn_frees = map snd bn_alpha_bns; - val alpha_bn_types = map fastype_of alpha_bn_frees; - fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = + fun fv_constr ith_dtyp (cname, dts) bindcs = let val Ts = map (typ_of_dtyp descr sorts) dts; val bindslen = length bindcs @@ -459,21 +447,17 @@ val bindcs = map fst bind_pis; val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); val args = map Free (names ~~ Ts); - val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); - val args2 = map Free (names2 ~~ Ts); val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); val fv_c = nth fv_frees ith_dtyp; - val alpha = nth alpha_frees ith_dtyp; val arg_nos = 0 upto (length dts - 1) fun fv_bind args (NONE, i, _, _) = if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else - (* TODO we do not know what to do with non-atomizable things *) + (* TODO goes the code for preiously defined nominal datatypes *) @{term "{} :: atom set"} | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) - fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant) fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE | find_nonrec_binder _ _ = NONE @@ -490,7 +474,7 @@ if ((is_atom thy) o fastype_of) x then mk_single_atom x else if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else - (* TODO we do not know what to do with non-atomizable things *) + (* TODO goes the code for preiously defined nominal datatypes *) @{term "{} :: atom set"}; (* If i = j then we generate it only once *) val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs; @@ -500,6 +484,81 @@ end; val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) + in + fv_eq + end; + fun fv_eq (i, (_, _, constrs)) binds = map2i (fv_constr i) constrs binds; + val fveqs = map2i fv_eq descr (gather_binds bindsall) + val fv_eqs_perfv = fveqs + val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; + fun filter_fun (_, b) = b mem rel_bns_nos; + val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) + val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) + val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) + val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); + val fv_names_all = fv_names_fst @ fv_bn_names; + val add_binds = map (fn x => (Attrib.empty_binding, x)) +(* Function_Fun.add_fun Function_Common.default_config ... true *) + val (fvs, lthy') = (Primrec.add_primrec + (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) + val (fvs2, lthy'') = + if fv_eqs_snd = [] then (([], []), lthy') else + (Primrec.add_primrec + (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') + val ordered_fvs = fv_frees @ fvbns; + val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) +in + ((all_fvs, ordered_fvs), lthy'') +end +*} + +ML {* +fun define_alpha (dt_info : Datatype_Aux.info) bindsall bns fv_frees lthy = +let + val thy = ProofContext.theory_of lthy; + val {descr, sorts, ...} = dt_info; + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); +(* TODO: We need a transitive closure, but instead we do this hack considering + all binding functions as recursive or not *) + val nr_bns = + if (non_rec_binds bindsall) = [] then [] + else map (fn (bn, _, _) => bn) bns; + val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => + "alpha_" ^ name_of_typ (nth_dtyp i)) descr); + val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; + val alpha_frees = map Free (alpha_names ~~ alpha_types); + (* We assume that a bn is either recursive or not *) + val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; + val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) = + alpha_bns dt_info alpha_frees bns bns_rec + val alpha_bn_frees = map snd bn_alpha_bns; + val alpha_bn_types = map fastype_of alpha_bn_frees; + + fun alpha_constr ith_dtyp (cname, dts) bindcs = + let + val Ts = map (typ_of_dtyp descr sorts) dts; + val bindslen = length bindcs + val pi_strs_same = replicate bindslen "pi" + val pi_strs = Name.variant_list [] pi_strs_same; + val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; + val bind_pis_gath = bindcs ~~ pis; + val bind_pis = un_gather_binds_cons bind_pis_gath; + val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); + val args = map Free (names ~~ Ts); + val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); + val args2 = map Free (names2 ~~ Ts); + val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); + val alpha = nth alpha_frees ith_dtyp; + val arg_nos = 0 upto (length dts - 1) + fun fv_bind args (NONE, i, _, _) = + if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else + if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else + if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else + if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else + (* TODO goes the code for preiously defined nominal datatypes *) + @{term "{} :: atom set"} + | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) + fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) val alpha_rhs = HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); fun alpha_arg ((dt, arg_no), (arg, arg2)) = @@ -574,400 +633,20 @@ fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) in - (fv_eq, alpha_eq) + alpha_eq end; - fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; - val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall) - val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs)) - val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; - fun filter_fun (_, b) = b mem rel_bns_nos; - val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) - val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) - val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) - val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); - val fv_names_all = fv_names_fst @ fv_bn_names; + fun alpha_eq (i, (_, _, constrs)) binds = map2i (alpha_constr i) constrs binds; + val alphaeqs = map2i alpha_eq descr (gather_binds bindsall) + val alpha_eqs = flat alphaeqs val add_binds = map (fn x => (Attrib.empty_binding, x)) -(* Function_Fun.add_fun Function_Common.default_config ... true *) - val (fvs, lthy') = (Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) - val (fvs2, lthy'') = - if fv_eqs_snd = [] then (([], []), lthy') else - (Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') - val (alphas, lthy''') = (Inductive.add_inductive_i + val (alphas, lthy') = (Inductive.add_inductive_i {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names) (alpha_types @ alpha_bn_types)) [] - (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'') - val ordered_fvs = fv_frees @ fvbns; - val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) -in - (((all_fvs, ordered_fvs), alphas), lthy''') -end -*} - - - -ML {* -fun build_alpha_sym_trans_gl alphas (x, y, z) = -let - fun build_alpha alpha = - let - val ty = domain_type (fastype_of alpha); - val var = Free(x, ty); - val var2 = Free(y, ty); - val var3 = Free(z, ty); - val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); - val transp = HOLogic.mk_imp (alpha $ var $ var2, - HOLogic.mk_all (z, ty, - HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) - in - (symp, transp) - end; - 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 sym_eqs, conj trans_eqs) -end -*} - -ML {* -fun build_alpha_refl_gl fv_alphas_lst alphas = -let - val (fvs_alphas, _) = 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 find_alphas ty x = - domain_type (fastype_of x) = ty; - fun refl_eq_arg (ty, arg) = - let - val rel_alphas = filter (find_alphas ty) alphas; - in - map (fn x => x $ arg $ arg) rel_alphas - end; - (* Flattening loses the induction structure *) - val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args)) -in - (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs)) -end -*} - -ML {* -fun reflp_tac induct eq_iff = - rtac induct THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW - split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} - THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps - @{thms alphas 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 alphas induct eq_iff ctxt = -let - val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas; - val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1); -in - HOLogic.conj_elims refl_conj -end -*} - -lemma exi_neg: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (- p)) \ \pi. Q pi" -apply (erule exE) -apply (rule_tac x="-pi" in exI) -by auto - -ML {* -fun symp_tac induct inj eqvt ctxt = - rel_indtac induct THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac - THEN_ALL_NEW - REPEAT o etac @{thm exi_neg} - THEN_ALL_NEW - split_conj_tac THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW - TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) -*} - - -lemma exi_sum: "\(pi :: perm). P pi \ \(pi :: perm). Q pi \ (\(p :: perm) (pi :: perm). P p \ Q pi \ R (pi + p)) \ \pi. R pi" -apply (erule exE)+ -apply (rule_tac x="pia + pi" in exI) -by auto - - -ML {* -fun eetac rule = - Subgoal.FOCUS_PARAMS (fn focus => - let - val concl = #concl focus - val prems = Logic.strip_imp_prems (term_of concl) - val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems - val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs - val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs - in - (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1 - end - ) -*} - -ML {* -fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = - rel_indtac induct THEN_ALL_NEW - (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW - split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac - THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) - THEN_ALL_NEW split_conj_tac THEN_ALL_NEW - TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) -*} - -lemma transpI: - "(\xa ya. R xa ya \ (\z. R ya z \ R xa z)) \ transp R" - unfolding transp_def - by blast - -ML {* -fun equivp_tac reflps symps transps = - (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *) - simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) - THEN' rtac conjI THEN' rtac allI THEN' - resolve_tac reflps THEN' - rtac conjI THEN' rtac allI THEN' rtac allI THEN' - resolve_tac symps THEN' - rtac @{thm transpI} THEN' resolve_tac transps -*} - -ML {* -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 (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 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 reflps symps transps 1 - in - Goal.prove ctxt [] [] goal tac - end + (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy) in - map equivp alphas -end -*} - -lemma not_in_union: "c \ a \ b \ (c \ a \ c \ b)" -by auto - -ML {* -fun supports_tac perm = - simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( - REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN' - asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] - swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh - supp_fset_to_set supp_fmap_atom})) -*} - -ML {* -fun mk_supp ty x = - Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x -*} - -ML {* -fun mk_supports_eq thy cnstr = -let - val (tys, ty) = (strip_type o fastype_of) cnstr - val names = Datatype_Prop.make_tnames tys - val frees = map Free (names ~~ tys) - val rhs = list_comb (cnstr, frees) - - fun mk_supp_arg (x, ty) = - if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else - if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else - if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) - else mk_supp ty x - val lhss = map mk_supp_arg (frees ~~ tys) - val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) - val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) -in - (names, eq) -end -*} - -ML {* -fun prove_supports ctxt perms cnst = -let - val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst -in - Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) -end -*} - -ML {* -fun mk_fs tys = -let - val names = Datatype_Prop.make_tnames tys - val frees = map Free (names ~~ tys) - val supps = map2 mk_supp tys frees - val fin_supps = map (fn x => @{term "finite :: atom set \ bool"} $ x) supps -in - (names, HOLogic.mk_Trueprop (mk_conjl fin_supps)) -end -*} - -ML {* -fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW ( - rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set - supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp}) -*} - -ML {* -fun prove_fs ctxt induct supports tys = -let - val (names, eq) = mk_fs tys -in - Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1) -end -*} - -ML {* -fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x; - -fun mk_supp_neq arg (fv, alpha) = -let - val collect = Const ("Collect", @{typ "(atom \ bool) \ atom \ bool"}); - val ty = fastype_of arg; - val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty); - val finite = @{term "finite :: atom set \ bool"} - val rhs = collect $ Abs ("a", @{typ atom}, - HOLogic.mk_not (finite $ - (collect $ Abs ("b", @{typ atom}, - HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg))))) -in - HOLogic.mk_eq (fv $ arg, rhs) -end; - -fun supp_eq fv_alphas_lst = -let - val (fvs_alphas, ls) = split_list fv_alphas_lst; - val (fv_ts, _) = split_list fvs_alphas; - val tys = map (domain_type o fastype_of) fv_ts; - val names = Datatype_Prop.make_tnames tys; - val args = map Free (names ~~ tys); - fun supp_eq_arg ((fv, arg), l) = - mk_conjl - ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) :: - (map (mk_supp_neq arg) l)) - val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls)) -in - (names, HOLogic.mk_Trueprop eqs) -end -*} - -ML {* -fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos = -if length fv_ts_bn < length alpha_ts_bn then - (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) []) -else let - val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1); - fun filter_fn i (x, j) = if j = i then SOME x else NONE; - val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos; - val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos; -in - (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all -end -*} - -(* TODO: this is a hack, it assumes that only one type of Abs's is present - in the type and chooses this supp_abs. Additionally single atoms are - treated properly. *) -ML {* -fun choose_alpha_abs eqiff = -let - fun exists_subterms f ts = true mem (map (exists_subterm f) ts); - val terms = map prop_of eqiff; - fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms - val no = - if check @{const_name alpha_lst} then 2 else - if check @{const_name alpha_res} then 1 else - if check @{const_name alpha_gen} then 0 else - error "Failure choosing supp_abs" -in - nth @{thms supp_abs[symmetric]} no -end -*} -lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}" -by (rule supp_abs(1)) - -lemma supp_abs_sum: - "supp (Abs x (a :: 'a :: fs)) \ supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" - "supp (Abs_res x (a :: 'a :: fs)) \ supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))" - "supp (Abs_lst y (a :: 'a :: fs)) \ supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))" - apply (simp_all add: supp_abs supp_Pair) - apply blast+ - done - - -ML {* -fun supp_eq_tac ind fv perm eqiff ctxt = - rel_indtac ind THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) -*} - - - -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_arg (fnctn $ arg) $ 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 (@{thms atom_eqvt permute_list.simps} @ 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)) + (alphas, lthy') end *} diff -r edc2a52cd457 -r 9a8decba77c5 Nominal/Lift.thy --- a/Nominal/Lift.thy Wed Apr 14 11:07:42 2010 +0200 +++ b/Nominal/Lift.thy Wed Apr 14 16:10:44 2010 +0200 @@ -2,7 +2,7 @@ imports "../Nominal-General/Nominal2_Atoms" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Abs" "Perm" "Fv" "Rsp" + "Abs" "Perm" "Equivp" "Rsp" begin @@ -69,13 +69,16 @@ ML {* fun define_fv_alpha_export dt binds bns ctxt = let - val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') = - define_fv_alpha dt binds bns ctxt; + val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') = + define_fv dt binds bns ctxt; + val fv_ts_nobn = take (length bns) fv_ts_loc + val (alpha, ctxt'') = + define_alpha dt binds bns fv_ts_nobn 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 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; @@ -84,7 +87,7 @@ 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') + ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'') end; *} diff -r edc2a52cd457 -r 9a8decba77c5 Nominal/Parser.thy --- a/Nominal/Parser.thy Wed Apr 14 11:07:42 2010 +0200 +++ b/Nominal/Parser.thy Wed Apr 14 16:10:44 2010 +0200 @@ -2,7 +2,7 @@ imports "../Nominal-General/Nominal2_Atoms" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Perm" "Fv" "Rsp" "Lift" + "Perm" "Equivp" "Rsp" "Lift" begin section{* Interface for nominal_datatype *}