--- 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
--- /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: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>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: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>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:
+ "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> 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 \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> 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 \<Rightarrow> 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 \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
+ val ty = fastype_of arg;
+ val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
+ val finite = @{term "finite :: atom set \<Rightarrow> 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)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+ "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
+ "supp (Abs_lst y (a :: 'a :: fs)) \<union> 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
--- 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 []"
| "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"
+inductive
+ typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
+where
+ t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
+ | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<or> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
+ | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> 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 \<bullet> 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 \<longrightarrow> valid (p \<bullet> 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\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
-where
- t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
- | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
- | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
-
-
-ML {* Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *}
-
lemma
shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> 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 \<turnstile> t : T"
--- 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 \<Rightarrow> 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: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>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: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>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:
- "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> 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 \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> 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 \<Rightarrow> 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 \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
- val ty = fastype_of arg;
- val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
- val finite = @{term "finite :: atom set \<Rightarrow> 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)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
- "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
- "supp (Abs_lst y (a :: 'a :: fs)) \<union> 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
*}
--- 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;
*}
--- 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 *}