# HG changeset patch # User Christian Urban # Date 1275903986 -7200 # Node ID ad03df7e80565c0045d68da6a7e95de872d58714 # Parent 4da5c5c29009c131f49a650fd2090acc84b95485# Parent 231a20534950fc3d49057160204dabd0d67cd57f merged diff -r 231a20534950 -r ad03df7e8056 IsaMakefile --- a/IsaMakefile Mon Jun 07 11:33:00 2010 +0200 +++ b/IsaMakefile Mon Jun 07 11:46:26 2010 +0200 @@ -60,6 +60,27 @@ $(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated @cp Quotient-Paper/document.pdf qpaper.pdf +## Slides + +session1: Slides/ROOT.ML \ + Slides/document/root* \ + Slides/Slides1.thy + @$(USEDIR) -D generated1 -f ROOT.ML HOL-Nominal Slides + @perl -i -p -e "s/..isachardoublequoteopen./\\\begin{innerdouble}/g" Sl + @perl -i -p -e "s/..isachardoublequoteclose./\\\end{innerdouble}/g" Sli + @perl -i -p -e "s/..isacharbackquoteopen./\\\begin{innersingle}/g" Slid + @perl -i -p -e "s/..isacharbackquoteclose./\\\end{innersingle}/g" Slide + +slides1: session1 + rm -f Slides/generated1/*.aux # otherwise latex will fall over + cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex + cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex + cp Slides/generated1/root.beamer.pdf Slides/slides.pdf + +slides: slides1 + + + ## clean diff -r 231a20534950 -r ad03df7e8056 Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal-General/Nominal2_Base.thy Mon Jun 07 11:46:26 2010 +0200 @@ -385,6 +385,11 @@ unfolding permute_perm_def by (auto simp add: swap_atom expand_perm_eq) +lemma uminus_eqvt: + fixes p q::"perm" + shows "p \ (- q) = - (p \ q)" + unfolding permute_perm_def + by (simp add: diff_minus minus_add add_assoc) subsection {* Permutations for functions *} diff -r 231a20534950 -r ad03df7e8056 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Mon Jun 07 11:46:26 2010 +0200 @@ -295,14 +295,13 @@ shows "a \ ()" by (simp add: fresh_def supp_unit) - section {* additional eqvt lemmas *} lemmas [eqvt] = imp_eqvt [folded induct_implies_def] (* nominal *) - supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt + supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt (* datatypes *) Pair_eqvt permute_list.simps diff -r 231a20534950 -r ad03df7e8056 Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal-General/nominal_eqvt.ML Mon Jun 07 11:46:26 2010 +0200 @@ -10,7 +10,7 @@ val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic - val equivariance: term list -> thm -> thm list -> Proof.context -> thm list * local_theory + val equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory val equivariance_cmd: string -> Proof.context -> local_theory end @@ -28,66 +28,6 @@ (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); -(** - given the theorem F[t]; proves the theorem F[f t] - - - F needs to be monotone - - f returns either SOME for a term it fires on - and NONE elsewhere -**) -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 - val simps = HOL_basic_ss addsimps @{thms split_def} -in - EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, - REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), - REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] -end - -fun map_thm ctxt f tac thm = -let - val opt_goal_trm = map_term f (prop_of thm) -in - case opt_goal_trm of - NONE => thm - | SOME goal => - Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) -end - -(* - inductive premises can be of the form - R ... /\ P ...; split_conj picks out - the part P ... -*) -fun transform_prem ctxt names thm = -let - fun split_conj names (Const ("op &", _) $ f1 $ f2) = - (case head_of f1 of - Const (name, _) => if member (op =) names name then SOME f2 else NONE - | _ => NONE) - | split_conj _ _ = NONE; -in - map_thm ctxt (split_conj names) (etac conjunct2 1) thm -end - - (** equivariance tactics **) val perm_boolE = @{thm permute_boolE} @@ -104,7 +44,7 @@ eqvt_strict_tac ctxt [] pred_names THEN' SUBPROOF (fn {prems, context as ctxt, ...} => let - val prems' = map (transform_prem ctxt pred_names) prems + val prems' = map (transform_prem2 ctxt pred_names) prems val tac1 = resolve_tac prems' val tac2 = EVERY' [ rtac pi_intro_rule, eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] @@ -147,7 +87,7 @@ (thm', ctxt') end -fun equivariance pred_trms raw_induct intrs ctxt = +fun equivariance note_flag pred_trms raw_induct intrs ctxt = let val is_already_eqvt = filter (is_eqvt ctxt) pred_trms @@ -172,7 +112,9 @@ |> singleton (ProofContext.export ctxt' ctxt)) val thms' = map (fn th => zero_var_indexes (th RS mp)) thms in - ctxt |> fold_map note_named_thm (pred_names ~~ thms') + if note_flag + then ctxt |> fold_map note_named_thm (pred_names ~~ thms') + else (thms', ctxt) end fun equivariance_cmd pred_name ctxt = @@ -181,7 +123,7 @@ val (_, {preds, raw_induct, intrs, ...}) = Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) in - equivariance preds raw_induct intrs ctxt |> snd + equivariance true preds raw_induct intrs ctxt |> snd end local structure P = Parse and K = Keyword in diff -r 231a20534950 -r ad03df7e8056 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal-General/nominal_library.ML Mon Jun 07 11:46:26 2010 +0200 @@ -6,6 +6,8 @@ signature NOMINAL_LIBRARY = sig + val dest_listT: typ -> typ + val mk_minus: term -> term val mk_plus: term -> term -> term @@ -20,17 +22,45 @@ val mk_atom: term -> term val supp_ty: typ -> typ + val supp_const: typ -> term val mk_supp_ty: typ -> term -> term val mk_supp: term -> term val mk_equiv: thm -> thm val safe_mk_equiv: thm -> thm + + val mk_diff: term * term -> term + val mk_append: term * term -> term + val mk_union: term * term -> term + val fold_union: term list -> term + + (* datatype operations *) + val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list + val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ + val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> + (term * typ * typ list * bool list) list list + val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> + (term * typ * typ list * bool list) list + val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list + + (* tactics for function package *) + val pat_completeness_auto: Proof.context -> tactic + val pat_completeness_simp: thm list -> Proof.context -> tactic + val prove_termination: Proof.context -> Function.info * local_theory + + (* transformations of premises in inductions *) + val transform_prem1: Proof.context -> string list -> thm -> thm + val transform_prem2: Proof.context -> string list -> thm -> thm end structure Nominal_Library: NOMINAL_LIBRARY = struct +(* this function should be in hologic.ML *) +fun dest_listT (Type (@{type_name list}, [T])) = T + | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) + fun mk_minus p = @{term "uminus::perm => perm"} $ p; fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q; @@ -42,7 +72,6 @@ fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) | dest_perm t = raise TERM ("dest_perm", [t]); - fun mk_sort_of t = @{term "sort_of"} $ t; fun atom_ty ty = ty --> @{typ "atom"}; @@ -51,7 +80,8 @@ fun supp_ty ty = ty --> @{typ "atom set"}; -fun mk_supp_ty ty t = Const (@{const_name "supp"}, supp_ty ty) $ t; +fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty) +fun mk_supp_ty ty t = supp_const ty $ t; fun mk_supp t = mk_supp_ty (fastype_of t) t; @@ -59,6 +89,165 @@ fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; +(* functions that construct differences, appends and unions + but avoid producing empty atom sets or empty atom lists *) + +fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} + | mk_diff (t1, @{term "{}::atom set"}) = t1 + | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) + +fun mk_append (@{term "[]::atom list"}, @{term "[]::atom list"}) = @{term "[]::atom list"} + | mk_append (t1, @{term "[]::atom list"}) = t1 + | mk_append (@{term "[]::atom list"}, t2) = t2 + | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) + +fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} + | mk_union (t1 , @{term "{}::atom set"}) = t1 + | mk_union (@{term "{}::atom set"}, t2) = t2 + | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) + +fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} + + + + +(** datatypes **) + + +(* returns the type of the nth datatype *) +fun all_dtyps descr sorts = + map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) + +fun nth_dtyp descr sorts n = + Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); + +(* returns info about constructors in a datatype *) +fun all_dtyp_constrs_info descr = + map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr + +(* returns the constants of the constructors plus the + corresponding type and types of arguments *) +fun all_dtyp_constrs_types descr sorts = +let + fun aux ((ty_name, vs), (cname, args)) = + let + val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs + val ty = Type (ty_name, vs_tys) + val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args + val is_rec = map Datatype_Aux.is_rec_type args + in + (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) + end +in + map (map aux) (all_dtyp_constrs_info descr) +end + +fun nth_dtyp_constrs_types descr sorts n = + nth (all_dtyp_constrs_types descr sorts) n + + +(* generates for every datatype a name str ^ dt_name + plus and index for multiple occurences of a string *) +fun prefix_dt_names descr sorts str = +let + fun get_nth_name (i, _) = + Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) +in + Datatype_Prop.indexify_names + (map (prefix str o get_nth_name) descr) +end + + + +(** function package tactics **) + +fun pat_completeness_auto lthy = + Pat_Completeness.pat_completeness_tac lthy 1 + THEN auto_tac (clasimpset_of lthy) + +fun pat_completeness_simp simps lthy = +let + val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) +in + Pat_Completeness.pat_completeness_tac lthy 1 + THEN ALLGOALS (asm_full_simp_tac simp_set) +end + +fun prove_termination lthy = + Function.prove_termination NONE + (Lexicographic_Order.lexicographic_order_tac true lthy) lthy + + +(** transformations of premises (in inductive proofs) **) + +(* + given the theorem F[t]; proves the theorem F[f t] + + - F needs to be monotone + - f returns either SOME for a term it fires on + and NONE elsewhere +*) +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 + val simps = HOL_basic_ss addsimps @{thms split_def} +in + EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, + REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), + REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] +end + +fun map_thm ctxt f tac thm = +let + val opt_goal_trm = map_term f (prop_of thm) +in + case opt_goal_trm of + NONE => thm + | SOME goal => + Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) +end + +(* + inductive premises can be of the form + R ... /\ P ...; split_conj_i picks out + the part R or P part +*) +fun split_conj1 names (Const ("op &", _) $ f1 $ f2) = + (case head_of f1 of + Const (name, _) => if member (op =) names name then SOME f1 else NONE + | _ => NONE) +| split_conj1 _ _ = NONE; + +fun split_conj2 names (Const ("op &", _) $ f1 $ f2) = + (case head_of f1 of + Const (name, _) => if member (op =) names name then SOME f2 else NONE + | _ => NONE) +| split_conj2 _ _ = NONE; + +fun transform_prem1 ctxt names thm = + map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm + +fun transform_prem2 ctxt names thm = + map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm + + + end (* structure *) open Nominal_Library; \ No newline at end of file diff -r 231a20534950 -r ad03df7e8056 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Mon Jun 07 11:46:26 2010 +0200 @@ -155,8 +155,11 @@ (** methods **) -val _ = Keyword.keyword "exclude" -val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; +fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan + +val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- + Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) []; + val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- (Scan.repeat (Args.const true))) [] diff -r 231a20534950 -r ad03df7e8056 Nominal/Abs.thy --- a/Nominal/Abs.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Abs.thy Mon Jun 07 11:46:26 2010 +0200 @@ -51,6 +51,73 @@ by (case_tac [!] bs, case_tac [!] cs) (auto simp add: le_fun_def le_bool_def alphas) +(* equivariance *) +lemma alpha_gen_eqvt[eqvt]: + shows "(bs, x) \gen R f q (cs, y) \ (p \ bs, p \ x) \gen (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" + and "(bs, x) \res R f q (cs, y) \ (p \ bs, p \ x) \res (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" + and "(ds, x) \lst R f q (es, y) \ (p \ ds, p \ x) \lst (p \ R) (p \ f) (p \ q) (p \ es, p \ y)" + unfolding alphas + unfolding permute_eqvt[symmetric] + unfolding set_eqvt[symmetric] + unfolding permute_fun_app_eq[symmetric] + unfolding Diff_eqvt[symmetric] + by (auto simp add: permute_bool_def fresh_star_permute_iff) + +(* equivalence *) +lemma alpha_gen_refl: + assumes a: "R x x" + shows "(bs, x) \gen R f 0 (bs, x)" + and "(bs, x) \res R f 0 (bs, x)" + and "(cs, x) \lst R f 0 (cs, x)" + using a + unfolding alphas + unfolding fresh_star_def + by (simp_all add: fresh_zero_perm) + +lemma alpha_gen_sym: + assumes a: "R (p \ x) y \ R (- p \ y) x" + shows "(bs, x) \gen R f p (cs, y) \ (cs, y) \gen R f (- p) (bs, x)" + and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" + and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" + unfolding alphas fresh_star_def + using a + by (auto simp add: fresh_minus_perm) + +lemma alpha_gen_sym_eqvt: + assumes a: "R (p \ x) y \ R y (p \ x)" + and b: "p \ R = R" + shows "(bs, x) \gen R f p (cs, y) \ (cs, y) \gen R f (- p) (bs, x)" + and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" + and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" +proof - + { assume "R (p \ x) y" + then have "R y (p \ x)" using a by simp + then have "R (- p \ y) x" + apply(rule_tac p="p" in permute_boolE) + apply(perm_simp add: permute_minus_cancel b) + apply(assumption) + done + } + then show "(bs, x) \gen R f p (cs, y) \ (cs, y) \gen R f (- p) (bs, x)" + and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" + and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" + unfolding alphas fresh_star_def + by (auto simp add: fresh_minus_perm) +qed + +lemma alpha_gen_trans: + assumes a: "\R (p \ x) y; R (q \ y) z\ \ R ((q + p) \ x) z" + shows "\(bs, x) \gen R f p (cs, y); (cs, y) \gen R f q (ds, z)\ \ (bs, x) \gen R f (q + p) (ds, z)" + and "\(bs, x) \res R f p (cs, y); (cs, y) \res R f q (ds, z)\ \ (bs, x) \res R f (q + p) (ds, z)" + and "\(es, x) \lst R f p (gs, y); (gs, y) \lst R f q (hs, z)\ \ (es, x) \lst R f (q + p) (hs, z)" + using a + unfolding alphas fresh_star_def + by (simp_all add: fresh_plus_perm) + + + +section {* General Abstractions *} + fun alpha_abs where @@ -731,45 +798,7 @@ lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2 -lemma alpha_gen_refl: - assumes a: "R x x" - shows "(bs, x) \gen R f 0 (bs, x)" - and "(bs, x) \res R f 0 (bs, x)" - and "(cs, x) \lst R f 0 (cs, x)" - using a - unfolding alphas - unfolding fresh_star_def - by (simp_all add: fresh_zero_perm) -lemma alpha_gen_sym: - assumes a: "R (p \ x) y \ R (- p \ y) x" - shows "(bs, x) \gen R f p (cs, y) \ (cs, y) \gen R f (- p) (bs, x)" - and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" - and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" - unfolding alphas fresh_star_def - using a - by (auto simp add: fresh_minus_perm) - -lemma alpha_gen_trans: - assumes a: "\R (p \ x) y; R (q \ y) z\ \ R ((q + p) \ x) z" - shows "\(bs, x) \gen R f p (cs, y); (cs, y) \gen R f q (ds, z)\ \ (bs, x) \gen R f (q + p) (ds, z)" - and "\(bs, x) \res R f p (cs, y); (cs, y) \res R f q (ds, z)\ \ (bs, x) \res R f (q + p) (ds, z)" - and "\(es, x) \lst R f p (gs, y); (gs, y) \lst R f q (hs, z)\ \ (es, x) \lst R f (q + p) (hs, z)" - using a - unfolding alphas fresh_star_def - by (simp_all add: fresh_plus_perm) - - -lemma alpha_gen_eqvt[eqvt]: - shows "(bs, x) \gen R f q (cs, y) \ (p \ bs, p \ x) \gen (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" - and "(bs, x) \res R f q (cs, y) \ (p \ bs, p \ x) \res (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" - and "(ds, x) \lst R f q (es, y) \ (p \ ds, p \ x) \lst (p \ R) (p \ f) (p \ q) (p \ es, p \ y)" - unfolding alphas - unfolding permute_eqvt[symmetric] - unfolding set_eqvt[symmetric] - unfolding permute_fun_app_eq[symmetric] - unfolding Diff_eqvt[symmetric] - by (auto simp add: permute_bool_def fresh_star_permute_iff) lemma alpha_gen_simpler: assumes fv_rsp: "\x y. R y x \ f x = f y" @@ -830,8 +859,14 @@ where "prod_fv fvx fvy (x, y) = (fvx x \ fvy y)" +definition + prod_alpha :: "('a \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b \ 'a \ 'b \ bool)" +where + "prod_alpha = prod_rel" + + lemma [quot_respect]: - "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv" + shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv" by auto lemma [quot_preserve]: @@ -840,11 +875,14 @@ shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv" by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) -lemma [mono]: "A <= B \ C <= D ==> prod_rel A C <= prod_rel B D" +lemma [mono]: + shows "A <= B \ C <= D ==> prod_alpha A C <= prod_alpha B D" + unfolding prod_alpha_def by auto lemma [eqvt]: - shows "p \ prod_rel A B x y = prod_rel (p \ A) (p \ B) (p \ x) (p \ y)" + shows "p \ prod_alpha A B x y = prod_alpha (p \ A) (p \ B) (p \ x) (p \ y)" + unfolding prod_alpha_def unfolding prod_rel.simps by (perm_simp) (rule refl) @@ -853,5 +891,6 @@ unfolding prod_fv.simps by (perm_simp) (rule refl) + end diff -r 231a20534950 -r ad03df7e8056 Nominal/Equivp.thy --- a/Nominal/Equivp.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Equivp.thy Mon Jun 07 11:46:26 2010 +0200 @@ -1,5 +1,5 @@ theory Equivp -imports "NewFv" "Tacs" "Rsp" +imports "Abs" "Perm" "Tacs" "Rsp" begin ML {* @@ -194,7 +194,7 @@ 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) + val eq = HOLogic.mk_Trueprop (supports $ fold_union lhss $ rhs) in (names, eq) end @@ -203,7 +203,7 @@ ML {* fun prove_supports ctxt perms cnst = let - val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst + val (names, eq) = mk_supports_eq ctxt cnst in Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) end @@ -340,28 +340,6 @@ -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 (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm 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 231a20534950 -r ad03df7e8056 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Ex/Classical.thy Mon Jun 07 11:46:26 2010 +0200 @@ -4,26 +4,23 @@ (* example from my Urban's PhD *) -(* - alpha_trm_raw is incorrectly defined, therefore the equivalence proof - does not go through; below the correct definition is given -*) - atom_decl name atom_decl coname -ML {* val _ = cheat_equivp := true *} +declare [[STEPS = 9]] nominal_datatype trm = Ax "name" "coname" -| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 -| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 -| AndL1 n::"name" t::"trm" "name" bind n in t -| AndL2 n::"name" t::"trm" "name" bind n in t -| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 -| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t +| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 +| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 +| AndL1 n::"name" t::"trm" "name" bind n in t +| AndL2 n::"name" t::"trm" "name" bind n in t +| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 +| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t +thm alpha_trm_raw.intros[no_vars] +(* thm trm.fv thm trm.eq_iff thm trm.bn @@ -31,44 +28,7 @@ thm trm.induct thm trm.distinct thm trm.fv[simplified trm.supp] - -(* correct alpha definition *) - -inductive - alpha -where - "\name = namea; coname = conamea\ \ - alpha (Ax_raw name coname) (Ax_raw namea conamea)" -| "\\pi. ({atom coname1}, trm_raw1) \gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a); - \pia. ({atom coname2}, trm_raw2) \gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a)\ \ - alpha (Cut_raw coname1 trm_raw1 coname2 trm_raw2) - (Cut_raw coname1a trm_raw1a coname2a trm_raw2a)" -| "\\pi. ({atom coname1}, trm_raw1) \gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a); - \pia. ({atom coname2}, trm_raw2) \gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a); - coname3 = coname3a\ \ - alpha (AndR_raw coname1 trm_raw1 coname2 trm_raw2 coname3) - (AndR_raw coname1a trm_raw1a coname2a trm_raw2a coname3a)" -| "\\pi. ({atom name1}, trm_raw) \gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa); - name2 = name2a\ \ - alpha (AndL1_raw name1 trm_raw name2) (AndL1_raw name1a trm_rawa name2a)" -| "\\pi. ({atom name1}, trm_raw) \gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa); - name2 = name2a\ \ - alpha (AndL2_raw name1 trm_raw name2) (AndL2_raw name1a trm_rawa name2a)" -| "\\pi. ({atom coname}, trm_raw1) \gen alpha fv_trm_raw pi ({atom conamea}, trm_raw1a); - \pia. ({atom name1}, trm_raw2) \gen alpha fv_trm_raw pia ({atom name1a}, trm_raw2a); - name2 = name2a\ \ - alpha (ImpL_raw coname trm_raw1 name1 trm_raw2 name2) - (ImpL_raw conamea trm_raw1a name1a trm_raw2a name2a)" -| "\\pi.({atom name} \ {atom coname1}, trm_raw) \gen alpha fv_trm_raw pi - ({atom namea} \ {atom coname1a}, trm_rawa); coname2 = coname2a\ \ - alpha (ImpR_raw coname1 name trm_raw coname2) - (ImpR_raw coname1a namea trm_rawa coname2a)" - -thm alpha.intros - -equivariance alpha - -thm eqvts_raw +*) end diff -r 231a20534950 -r ad03df7e8056 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Ex/CoreHaskell.thy Mon Jun 07 11:46:26 2010 +0200 @@ -2,15 +2,14 @@ imports "../NewParser" begin -(* core haskell *) - -(* at the moment it is hard coded that shallow binders - need to use bind_set *) +(* Core Haskell *) atom_decl var atom_decl cvar atom_decl tvar +declare [[STEPS = 10]] + nominal_datatype tkind = KStar | KFun "tkind" "tkind" @@ -86,8 +85,105 @@ | "bv_cvs CvsNil = []" | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" - +lemma alpha_gen_sym_test: + assumes a: "R (p \ x) y \ R y (p \ x)" + and b: "p \ R = R" + shows "(bs, x) \gen R f p (cs, y) \ (cs, y) \gen R f (- p) (bs, x)" + and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" + and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" + unfolding alphas fresh_star_def + apply(auto simp add: fresh_minus_perm) + apply(rule_tac p="p" in permute_boolE) + apply(perm_simp add: permute_minus_cancel b) + apply(simp add: a) + apply(rule_tac p="p" in permute_boolE) + apply(perm_simp add: permute_minus_cancel b) + apply(simp add: a) + apply(rule_tac p="p" in permute_boolE) + apply(perm_simp add: permute_minus_cancel b) + apply(simp add: a) + done + +ML {* +(* for equalities *) +val tac1 = rtac @{thm sym} THEN' atac + +(* for "unbound" premises *) +val tac2 = atac + +fun trans_prem_tac pred_names ctxt = + SUBPROOF (fn {prems, context as ctxt, ...} => + let + val prems' = map (transform_prem1 ctxt pred_names) prems + val _ = tracing ("prems'\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) prems')) + in + print_tac "goal" THEN resolve_tac prems' 1 + end) ctxt + +(* for "bound" premises *) +fun tac3 pred_names ctxt = + EVERY' [etac @{thm exi_neg}, + resolve_tac @{thms alpha_gen_sym_test}, + asm_full_simp_tac (HOL_ss addsimps @{thms split_conv permute_prod.simps + prod_alpha_def prod_rel.simps alphas}), + Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, + trans_prem_tac pred_names ctxt] + +fun tac intro pred_names ctxt = + resolve_tac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3 pred_names ctxt] +*} +lemma [eqvt]: +shows "p \ alpha_tkind_raw = alpha_tkind_raw" +and "p \ alpha_ckind_raw = alpha_ckind_raw" +and "p \ alpha_ty_raw = alpha_ty_raw" +and "p \ alpha_ty_lst_raw = alpha_ty_lst_raw" +and "p \ alpha_co_raw = alpha_co_raw" +and "p \ alpha_co_lst_raw = alpha_co_lst_raw" +and "p \ alpha_trm_raw = alpha_trm_raw" +and "p \ alpha_assoc_lst_raw = alpha_assoc_lst_raw" +and "p \ alpha_pat_raw = alpha_pat_raw" +and "p \ alpha_vars_raw = alpha_vars_raw" +and "p \ alpha_tvars_raw = alpha_tvars_raw" +and "p \ alpha_cvars_raw = alpha_cvars_raw" +and "p \ alpha_bv_raw = alpha_bv_raw" +and "p \ alpha_bv_vs_raw = alpha_bv_vs_raw" +and "p \ alpha_bv_tvs_raw = alpha_bv_tvs_raw" +and "p \ alpha_bv_cvs_raw = alpha_bv_cvs_raw" +sorry + +lemmas ii = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts + +lemmas ij = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros + +ML {* +val pp = ["CoreHaskel.alpha_tkind_raw", "CoreHaskell.alpha_ckind_raw", "CoreHaskell.alpha_ty_raw", "CoreHaskell.alpha_ty_lst_raw", "CoreHaskell.alpha_co_raw", "CoreHaskell.alpha_co_lst_raw", "CoreHaskell.alpha_trm_raw", "CoreHaskell.alpha_assoc_lst_raw", "CoreHaskell.alpha_pat_raw", "CoreHaskell.alpha_vars_raw", "CoreHaskell.alpha_tvars_raw", "CoreHaskell.alpha_cvars_raw", "CoreHaskell.alpha_bv_raw", "CoreHaskell.alpha_bv_vs_raw", "CoreHaskell.alpha_bv_tvs_raw", "CoreHaskell.alpha_bv_cvs_raw"] +*} + +lemma +shows "alpha_tkind_raw x1 y1 ==> alpha_tkind_raw y1 x1" +and "alpha_ckind_raw x2 y2 ==> alpha_ckind_raw y2 x2" +and "alpha_ty_raw x3 y3 ==> alpha_ty_raw y3 x3" +and "alpha_ty_lst_raw x4 y4 ==> alpha_ty_lst_raw y4 x4" +and "alpha_co_raw x5 y5 ==> alpha_co_raw y5 x5" +and "alpha_co_lst_raw x6 y6 ==> alpha_co_lst_raw y6 x6" +and "alpha_trm_raw x7 y7 ==> alpha_trm_raw y7 x7" +and "alpha_assoc_lst_raw x8 y8 ==> alpha_assoc_lst_raw y8 x8" +and "alpha_pat_raw x9 y9 ==> alpha_pat_raw y9 x9" +and "alpha_vars_raw xa ya ==> alpha_vars_raw ya xa" +and "alpha_tvars_raw xb yb ==> alpha_tvars_raw yb xb" +and "alpha_cvars_raw xc yc ==> alpha_cvars_raw yc xc" +and "alpha_bv_raw xd yd ==> alpha_bv_raw yd xd" +and "alpha_bv_vs_raw xe ye ==> alpha_bv_vs_raw ye xe" +and "alpha_bv_tvs_raw xf yf ==> alpha_bv_tvs_raw yf xf" +and "alpha_bv_cvs_raw xg yg ==> alpha_bv_cvs_raw yg xg" +apply(induct rule: ii) +apply(tactic {* tac @{thms ij} pp @{context} 1 *})+ +done + + +lemma +alpha_tkind_raw, alpha_ckind_raw, alpha_ty_raw, alpha_ty_lst_raw, alpha_co_raw, alpha_co_lst_raw, alpha_trm_raw, alpha_assoc_lst_raw, alpha_pat_raw, alpha_vars_raw, alpha_tvars_raw, alpha_cvars_raw, alpha_bv_raw, alpha_bv_vs_raw, alpha_bv_tvs_raw, alpha_bv_cvs_raw lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm diff -r 231a20534950 -r ad03df7e8056 Nominal/Ex/Ex1rec.thy --- a/Nominal/Ex/Ex1rec.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Ex/Ex1rec.thy Mon Jun 07 11:46:26 2010 +0200 @@ -2,10 +2,9 @@ imports "../NewParser" begin -atom_decl name +declare [[STEPS = 9]] -ML {* val _ = cheat_supp_eq := true *} -ML {* val _ = cheat_equivp := true *} +atom_decl name nominal_datatype lam = Var "name" @@ -19,6 +18,9 @@ where "bi (Bp x t) = {atom x}" + +thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros + thm lam_bp.fv thm lam_bp.eq_iff[no_vars] thm lam_bp.bn diff -r 231a20534950 -r ad03df7e8056 Nominal/Ex/Ex2.thy --- a/Nominal/Ex/Ex2.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Ex/Ex2.thy Mon Jun 07 11:46:26 2010 +0200 @@ -3,6 +3,7 @@ begin text {* example 2 *} +declare [[STEPS = 9]] atom_decl name @@ -10,17 +11,23 @@ Var "name" | App "trm" "trm" | Lam x::"name" t::"trm" bind_set x in t -| Let p::"pat" "trm" t::"trm" bind "f p" in t +| Let p::"pat" "trm" t::"trm" bind_set "f p" in t and pat = PN | PS "name" | PD "name" "name" binder - f::"pat \ atom list" + f::"pat \ atom set" where - "f PN = []" -| "f (PS x) = [atom x]" -| "f (PD x y) = [atom x, atom y]" + "f PN = {}" +| "f (PD x y) = {atom x, atom y}" +| "f (PS x) = {atom x}" + +thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars] +thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars] + + + thm trm_pat.bn thm trm_pat.perm @@ -28,24 +35,6 @@ thm trm_pat.distinct thm trm_pat.fv[simplified trm_pat.supp(1-2)] -lemma lets_overlap1: - "atom a \ atom b \ Let (PD a a) x y \ Let (PD a b) x y" - by (simp add: trm_pat.eq_iff alphas) - -lemma lets_overlap2: - "atom a \ supp y \ atom b \ supp y \ Let (PD a a) x y = Let (PD b b) x y" - apply (simp add: trm_pat.eq_iff alphas trm_pat.supp) - apply (rule_tac x="(a\b)" in exI) - apply (simp add: eqvts) - apply (rule conjI) - prefer 2 - apply (rule Nominal2_Supp.supp_perm_eq) - apply (unfold fresh_star_def) - apply (unfold fresh_def) - apply (unfold flip_def) - apply (simp_all add: supp_swap) - apply auto - done end diff -r 231a20534950 -r ad03df7e8056 Nominal/Ex/LF.thy --- a/Nominal/Ex/LF.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Ex/LF.thy Mon Jun 07 11:46:26 2010 +0200 @@ -2,21 +2,23 @@ imports "../NewParser" begin +declare [[STEPS = 9]] + atom_decl name atom_decl ident nominal_datatype kind = Type - | KPi "ty" n::"name" k::"kind" bind_set n in k + | KPi "ty" n::"name" k::"kind" bind n in k and ty = TConst "ident" | TApp "ty" "trm" - | TPi "ty" n::"name" t::"ty" bind_set n in t + | TPi "ty" n::"name" t::"ty" bind n in t and trm = Const "ident" | Var "name" | App "trm" "trm" - | Lam "ty" n::"name" t::"trm" bind_set n in t + | Lam "ty" n::"name" t::"trm" bind n in t thm kind_ty_trm.supp diff -r 231a20534950 -r ad03df7e8056 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Mon Jun 07 11:46:26 2010 +0200 @@ -3,11 +3,12 @@ begin atom_decl name +declare [[STEPS = 9]] nominal_datatype lam = Var "name" | App "lam" "lam" -| Lam x::"name" l::"lam" bind_set x in l +| Lam x::"name" l::"lam" bind x in l thm lam.fv thm lam.supp diff -r 231a20534950 -r ad03df7e8056 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Mon Jun 07 11:46:26 2010 +0200 @@ -4,18 +4,160 @@ atom_decl name +declare [[STEPS = 10]] + nominal_datatype trm = Var "name" | App "trm" "trm" | Lam x::"name" t::"trm" bind_set x in t -| Let a::"assg" t1::"trm" t2::"trm" bind_set "bn a" in t1 t2 - +| Let a::"assg" t::"trm" bind_set "bn a" in t +| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2 +| Bar x::"name" y::"name" t::"trm" bind y x in t x y and assg = - As "name" "trm" + As "name" "name" "trm" "name" binder bn::"assg \ atom set" where - "bn (As x t) = {atom x}" + "bn (As x y t z) = {atom x}" + +thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros +thm alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases + + +lemma [eqvt]: + "p \ alpha_trm_raw x1 y1 = alpha_trm_raw (p \ x1) (p \ y1)" + "p \ alpha_assg_raw x2 y2 = alpha_assg_raw (p \ x2) (p \ y2)" + "p \ alpha_bn_raw x3 y3 = alpha_bn_raw (p \ x3) (p \ y3)" +sorry + +lemmas ii = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros +lemmas cc = alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases + +ML {* +length @{thms cc} +*} + +ML {* + val pp = ["SingleLet.alpha_trm_raw", "SingleLet.alpha_assg_raw", "SingleLet.alpha_bn_raw"] +*} + +lemma exi_sum: "\(q :: perm). P q \ \q. Q q \ (\p q. P p \ Q q \ R (p + q)) \ \r. R r" +apply(erule exE)+ +apply(rule_tac x="q + qa" in exI) +apply(simp) +done + +lemma alpha_gen_compose_trans: + assumes b: "(as, t) \gen (\x1 x2. R x1 x2 \ (\x. R x2 x \ R x1 x)) f pi (bs, s)" + shows "(\x. R s x \ R (pi \ t) x)" + using b + by (simp add: alphas) + +lemma test: + assumes b: "(as, t) \gen R f pi (bs, s)" + shows "R (pi \ t) s" + using b + by (simp add: alphas) + +lemma alpha_gen_trans_eqvt: + assumes a: "(bs, x) \gen R f p (cs, y)" and a1: "(cs, y) \gen R f q (ds, z)" + and b: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" + shows "(bs, x) \gen R f (q + p) (ds, z)" + sorry + + +lemma + "alpha_trm_raw x1 y1 \ (\z1. alpha_trm_raw y1 z1 \ alpha_trm_raw x1 z1)" + "alpha_assg_raw x2 y2 \ (\z2. alpha_assg_raw y2 z2 \ alpha_assg_raw x2 z2)" + "alpha_bn_raw x3 y3 \ (\z3. alpha_bn_raw y3 z3 \ alpha_bn_raw x3 z3)" +apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) +(* 8 *) +prefer 8 +thm alpha_bn_raw.cases +apply(rotate_tac -1) +apply(erule alpha_bn_raw.cases) +apply(simp_all)[6] + + +apply(rotate_tac -1) +apply(erule cc) +apply(simp_all)[6] +apply(rule ii) +apply(simp) +(* 1 *) +apply(rotate_tac -1) +apply(erule cc) +apply(simp_all)[6] +apply(rule ii) +apply(simp) +apply(simp) +(* 2 *) +apply(rotate_tac -1) +apply(erule cc) +apply(simp_all)[6] +apply(rule ii) +apply(erule exE)+ +apply(rule_tac x="pa + p" in exI) +apply(rule alpha_gen_trans_eqvt) +prefer 2 +apply(assumption) +apply(simp add: alphas) +apply(metis) +apply(drule test) +apply(simp) +(* 3 *) +apply(rotate_tac -1) +apply(erule cc) +apply(simp_all)[6] +apply(rule ii) +apply(erule exE)+ +apply(rule_tac x="pa + p" in exI) +apply(rule alpha_gen_trans_eqvt) +prefer 2 +apply(assumption) +apply(simp add: alphas) +apply(metis) +apply(drule alpha_gen_compose_trans) +apply(simp) +apply(simp) +(* 4 *) +apply(rotate_tac -1) +apply(erule cc) +apply(simp_all)[6] +apply(rule ii) +apply(erule exE)+ +apply(rule_tac x="pa + p" in exI) +apply(rule alpha_gen_trans_eqvt) +prefer 2 +apply(assumption) +prefer 2 +apply(drule test) +apply(simp add: prod_alpha_def) +apply(simp add: alphas) + +apply(drule alpha_gen_compose_trans) +apply(drule_tac x="(- pa \ trm_rawaa)" in spec) +apply(simp) +apply(simp) +(* 4 *) +apply(assumption) +apply(simp) +apply(simp) + +(* 3 *) + +(* 4 *) + +(* 5 *) + +(* 6 *) + +(* 7 *) + +(* 8 *) + +(* 9 *) +done ML {* Inductive.the_inductive *} thm trm_assg.fv @@ -27,8 +169,10 @@ thm trm_assg.inducts thm trm_assg.distinct ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} + +(* TEMPORARY thm trm_assg.fv[simplified trm_assg.supp(1-2)] - +*) end diff -r 231a20534950 -r ad03df7e8056 Nominal/Ex/Test.thy --- a/Nominal/Ex/Test.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Ex/Test.thy Mon Jun 07 11:46:26 2010 +0200 @@ -13,6 +13,7 @@ thm fv_trm_raw.simps[no_vars] *) + (* This file contains only the examples that are not supposed to work yet. *) @@ -29,7 +30,6 @@ | Ap "trm" "trm list" | Lm x::"name" t::"trm" bind x in t - (* thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] diff -r 231a20534950 -r ad03df7e8056 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Ex/TypeSchemes.thy Mon Jun 07 11:46:26 2010 +0200 @@ -5,6 +5,7 @@ section {*** Type Schemes ***} atom_decl name +declare [[STEPS = 9]] nominal_datatype ty = Var "name" @@ -12,6 +13,15 @@ and tys = All xs::"name fset" ty::"ty" bind_res xs in ty +nominal_datatype ty2 = + Var2 "name" +| Fun2 "ty2" "ty2" + +(* PROBLEM: this only works once the type is defined +nominal_datatype tys2 = + All2 xs::"name fset" ty::"ty2" bind_res xs in ty +*) + lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] diff -r 231a20534950 -r ad03df7e8056 Nominal/Lift.thy --- a/Nominal/Lift.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Lift.thy Mon Jun 07 11:46:26 2010 +0200 @@ -2,7 +2,7 @@ imports "../Nominal-General/Nominal2_Atoms" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Abs" "Perm" "Equivp" "Rsp" + "Abs" "Perm" "Rsp" begin diff -r 231a20534950 -r ad03df7e8056 Nominal/NewAlpha.thy --- a/Nominal/NewAlpha.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/NewAlpha.thy Mon Jun 07 11:46:26 2010 +0200 @@ -1,226 +1,228 @@ theory NewAlpha -imports "NewFv" +imports "Abs" "Perm" begin ML {* -fun mk_binop2 ctxt s (l, r) = - Syntax.check_term ctxt (Const (s, dummyT) $ l $ r) +fun mk_prod_fv (t1, t2) = +let + val ty1 = fastype_of t1 + val ty2 = fastype_of t2 + val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"} +in + Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2 +end *} ML {* -fun mk_compound_fv' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_fv}) -fun mk_compound_alpha' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_rel}) +fun mk_prod_alpha (t1, t2) = +let + val ty1 = fastype_of t1 + val ty2 = fastype_of t2 + val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) + val resT = [prodT, prodT] ---> @{typ "bool"} +in + Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2 +end *} ML {* -fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees - bn_alphabn alpha_const binds bodys = +fun mk_binders lthy bmode args bodies = +let + fun bind_set lthy args (NONE, i) = setify lthy (nth args i) + | bind_set _ args (SOME bn, i) = bn $ (nth args i) + fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) + | bind_lst _ args (SOME bn, i) = bn $ (nth args i) + + val (connect_fn, bind_fn) = + case bmode of + Lst => (mk_append, bind_lst) + | Set => (mk_union, bind_set) + | Res => (mk_union, bind_set) +in + foldl1 connect_fn (map (bind_fn lthy args) bodies) +end +*} + +ML {* +fun mk_alpha_prem bmode fv alpha args args' binders binders' = let - val thy = ProofContext.theory_of lthy; - fun bind_set args (NONE, no) = setify thy (nth args no) - | bind_set args (SOME f, no) = f $ (nth args no) - fun bind_lst args (NONE, no) = listify thy (nth args no) - | bind_lst args (SOME f, no) = f $ (nth args no) - fun append (t1, t2) = - Const(@{const_name append}, @{typ "atom list \ atom list \ atom list"}) $ t1 $ t2; - fun binds_fn args nos = - if alpha_const = @{const_name alpha_lst} - then foldr1 append (map (bind_lst args) nos) - else mk_union (map (bind_set args) nos); - val lhs_binds = binds_fn args binds; - val rhs_binds = binds_fn args2 binds; - val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys); - val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys); - val lhs = HOLogic.mk_prod (lhs_binds, lhs_bodys); - val rhs = HOLogic.mk_prod (rhs_binds, rhs_bodys); - val body_dts = map (nth dts) bodys; - fun fv_for_dt dt = - if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) - else Const (@{const_name supp}, - Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ "atom set"}) - val fvs = map fv_for_dt body_dts; - val fv = mk_compound_fv' lthy fvs; - fun alpha_for_dt dt = - if Datatype_Aux.is_rec_type dt - then nth alpha_frees (Datatype_Aux.body_index dt) - else Const (@{const_name "op ="}, - Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> - Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ bool}) - val alphas = map alpha_for_dt body_dts; - val alpha = mk_compound_alpha' lthy alphas; - val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs - val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre) - val t = Syntax.check_term lthy alpha_gen_ex - fun alpha_bn_bind (SOME bn, i) = - if member (op =) bodys i then NONE - else SOME ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i) - | alpha_bn_bind (NONE, _) = NONE + val (alpha_name, binder_ty) = + case bmode of + Lst => (@{const_name "alpha_lst"}, @{typ "atom list"}) + | Set => (@{const_name "alpha_gen"}, @{typ "atom set"}) + | Res => (@{const_name "alpha_res"}, @{typ "atom set"}) + val ty = fastype_of args + val pair_ty = HOLogic.mk_prodT (binder_ty, ty) + val alpha_ty = [ty, ty] ---> @{typ "bool"} + val fv_ty = ty --> @{typ "atom set"} in - t :: (map_filter alpha_bn_bind binds) + HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, + Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) + $ HOLogic.mk_prod (binders, args) $ alpha $ fv $ (Bound 0) $ HOLogic.mk_prod (binders', args')) end *} ML {* -fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm = -case bm of - BEmy i => - let - val arg = nth args i; - val arg2 = nth args2 i; - val dt = nth dts i; - in - case AList.lookup (op=) args_in_bn i of - NONE => if Datatype_Aux.is_rec_type dt - then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2] - else [HOLogic.mk_eq (arg, arg2)] - | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2] - | SOME NONE => [] - end -| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees - fv_frees bn_alphabn @{const_name alpha_lst} x y -| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees - fv_frees bn_alphabn @{const_name alpha_gen} x y -| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees - fv_frees bn_alphabn @{const_name alpha_res} x y +fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = + case binder of + (NONE, i) => [] + | (SOME bn, i) => + if member (op=) bodies i + then [] + else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)] *} - ML {* -fun alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess - (alphabn, (_, ith_dtyp, args_in_bns)) = +fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause = let - fun alpha_bn_constr (cname, dts) (args_in_bn, bclauses) = - let - val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; - val names = Datatype_Prop.make_tnames Ts; - val names2 = Name.variant_list names (Datatype_Prop.make_tnames Ts); - val args = map Free (names ~~ Ts); - val args2 = map Free (names2 ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp)); - val alpha_bn_bm = alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees - fv_frees bn_alphabn args_in_bn; - val rhs = HOLogic.mk_Trueprop - (alphabn $ (list_comb (c, args)) $ (list_comb (c, args2))); - val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bn_bm bclauses)) - in - Library.foldr Logic.mk_implies (lhss, rhs) - end; - val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; + fun mk_frees i = + let + val arg = nth args i + val arg' = nth args' i + val ty = fastype_of arg + in + if nth is_rec i + then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg' + else HOLogic.mk_eq (arg, arg') + end + fun mk_alpha_fv i = + let + val ty = fastype_of (nth args i) + in + case AList.lookup (op=) alpha_map ty of + NONE => (HOLogic.eq_const ty, supp_const ty) + | SOME (alpha, fv) => (alpha, fv) + end + in - map2 alpha_bn_constr constrs (args_in_bns ~~ bclausess) + case bclause of + BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies + | BC (bmode, binders, bodies) => + let + val (alphas, fvs) = split_list (map mk_alpha_fv bodies) + val comp_fv = foldl1 mk_prod_fv fvs + val comp_alpha = foldl1 mk_prod_alpha alphas + val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies) + val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies) + val comp_binders = mk_binders lthy bmode args binders + val comp_binders' = mk_binders lthy bmode args' binders + val alpha_prem = + mk_alpha_prem bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders' + val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders) + in + map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems) + end end *} ML {* -fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss = +fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = let - fun mk_alphabn_free (bn, ith, _) = - let - val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); - val ty = nth_dtyp dt_descr sorts ith; - val alphabn_type = ty --> ty --> @{typ bool}; - val alphabn_free = Free(alphabn_name, alphabn_type); - in - (alphabn_name, alphabn_free) - end; - val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free bn_funs); - val bn_alphabn = (map (fn (bn, _, _) => bn) bn_funs) ~~ alphabn_frees - val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs; - val eqs = map2 (alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausessl - (alphabn_frees ~~ bn_funs); + val arg_names = Datatype_Prop.make_tnames arg_tys + val arg_names' = Name.variant_list arg_names arg_names + val args = map Free (arg_names ~~ arg_tys) + val args' = map Free (arg_names' ~~ arg_tys) + val alpha = fst (the (AList.lookup (op=) alpha_map ty)) + val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args')) + val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses in - (bn_alphabn, alphabn_names, eqs) + Library.foldr Logic.mk_implies (flat prems, concl) end *} ML {* -fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm = -case bm of - BEmy i => - let - val arg = nth args i; - val arg2 = nth args2 i; - val dt = nth dts i; - in - if Datatype_Aux.is_rec_type dt - then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2] - else [HOLogic.mk_eq (arg, arg2)] - end -| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees - fv_frees bn_alphabn @{const_name alpha_lst} x y -| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees - fv_frees bn_alphabn @{const_name alpha_gen} x y -| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees - fv_frees bn_alphabn @{const_name alpha_res} x y +fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause = +let + fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i = + let + val arg = nth args i + val arg' = nth args' i + val ty = fastype_of arg + in + case AList.lookup (op=) bn_args i of + NONE => (case (AList.lookup (op=) alpha_map ty) of + NONE => [HOLogic.mk_eq (arg, arg')] + | SOME (alpha, _) => [alpha $ arg $ arg']) + | SOME (NONE) => [] + | SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg'] + end +in + case bclause of + BC (_, [], bodies) => + map HOLogic.mk_Trueprop + (flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies)) + | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause +end *} ML {* -fun alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess (alpha_free, ith_dtyp) = +fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses = let - fun alpha_constr (cname, dts) bclauses = - let - val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; - val names = Datatype_Prop.make_tnames Ts; - val names2 = Name.variant_list names (Datatype_Prop.make_tnames Ts); - val args = map Free (names ~~ Ts); - val args2 = map Free (names2 ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp)); - val alpha_bm = alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn - val rhs = HOLogic.mk_Trueprop - (alpha_free $ (list_comb (c, args)) $ (list_comb (c, args2))); - val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bm bclauses)) - in - Library.foldr Logic.mk_implies (lhss, rhs) - end; - val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; + val arg_names = Datatype_Prop.make_tnames arg_tys + val arg_names' = Name.variant_list arg_names arg_names + val args = map Free (arg_names ~~ arg_tys) + val args' = map Free (arg_names' ~~ arg_tys) + val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm) + val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args')) + val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses in - map2 alpha_constr constrs bclausess + Library.foldr Logic.mk_implies (flat prems, concl) end *} ML {* -fun define_raw_alpha (dt_info : Datatype_Aux.info) bn_funs bclausesss fv_frees lthy = +fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let - val {descr as dt_descr, sorts, ...} = dt_info; - - val alpha_names = prefix_dt_names dt_descr sorts "alpha_"; - val alpha_types = map (fn (i, _) => - nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr; - val alpha_frees = map Free (alpha_names ~~ alpha_types); + val nth_constrs_info = nth constrs_info bn_n + val nth_bclausess = nth bclausesss bn_n +in + map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess +end +*} - val (bn_alphabn, alpha_bn_names, alpha_bn_eqs) = - alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss +ML {* +fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy = +let + val alpha_names = prefix_dt_names descr sorts "alpha_" + val alpha_arg_tys = all_dtyps descr sorts + val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys + val alpha_frees = map Free (alpha_names ~~ alpha_tys) + val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs) - val alpha_bns = map snd bn_alphabn; - val alpha_bn_types = map fastype_of alpha_bns; + val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) + val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns + val alpha_bn_names = map (prefix "alpha_") bn_names + val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys + val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys + val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) + val alpha_bn_map = bns ~~ alpha_bn_frees - val alpha_nums = 0 upto (length alpha_frees - 1) + val constrs_info = all_dtyp_constrs_types descr sorts - val alpha_eqs = map2 (alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausesss - (alpha_frees ~~ alpha_nums); + val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss + val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn)) - (alpha_names @ alpha_bn_names) (alpha_types @ alpha_bn_types) - val all_alpha_eqs = map (pair Attrib.empty_binding) (flat alpha_eqs @ flat alpha_bn_eqs) - + (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys) + val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) + 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 = false, fork_mono = false} - all_alpha_names [] all_alpha_eqs [] lthy + coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} + all_alpha_names [] all_alpha_intros [] lthy - val alpha_ts_loc = #preds alphas; + val alpha_trms_loc = #preds alphas; val alpha_induct_loc = #raw_induct alphas; val alpha_intros_loc = #intrs alphas; val alpha_cases_loc = #elims alphas; - val morphism = ProofContext.export_morphism lthy' lthy; + val phi = ProofContext.export_morphism lthy' lthy; - val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; - val alpha_induct = Morphism.thm morphism alpha_induct_loc; - val alpha_intros = Morphism.fact morphism alpha_intros_loc - val alpha_cases = Morphism.fact morphism alpha_cases_loc + val alpha_trms = map (Morphism.term phi) alpha_trms_loc; + val alpha_induct = Morphism.thm phi alpha_induct_loc; + val alpha_intros = map (Morphism.thm phi) alpha_intros_loc + val alpha_cases = map (Morphism.thm phi) alpha_cases_loc in - (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy') + (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy') end *} diff -r 231a20534950 -r ad03df7e8056 Nominal/NewFv.thy --- a/Nominal/NewFv.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/NewFv.thy Mon Jun 07 11:46:26 2010 +0200 @@ -4,38 +4,42 @@ begin ML {* -(* binding modes *) +(* binding modes and binding clauses *) -datatype bmodes = - BEmy of int -| BLst of ((term option * int) list) * (int list) -| BSet of ((term option * int) list) * (int list) -| BRes of ((term option * int) list) * (int list) +datatype bmode = Lst | Res | Set + +datatype bclause = + BC of bmode * (term option * int) list * int list *} ML {* -fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x]; - -val noatoms = @{term "{} :: atom set"}; +fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} + | mk_diff (t1, @{term "{}::atom set"}) = t1 + | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) -fun mk_union sets = - fold (fn a => fn b => - if a = noatoms then b else - if b = noatoms then a else - if a = b then a else - HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; +fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} + | mk_union (t1 , @{term "{}::atom set"}) = t1 + | mk_union (@{term "{}::atom set"}, t2) = t2 + | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2) + +fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} *} ML {* -fun is_atom thy ty = - Sign.of_sort thy (ty, @{sort at_base}) +fun is_atom ctxt ty = + Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) -fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t +fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t | is_atom_set _ _ = false; -fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t +fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t | is_atom_fset _ _ = false; +fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t + | is_atom_list _ _ = false +*} + +ML {* fun mk_atom_set t = let val ty = fastype_of t; @@ -55,23 +59,6 @@ fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) end; -fun mk_diff a b = - if b = noatoms then a else - if b = a then noatoms else - HOLogic.mk_binop @{const_name minus} (a, b); -*} - -ML {* -fun is_atom_list (Type (@{type_name list}, [T])) = true - | is_atom_list _ = false -*} - -ML {* -fun dest_listT (Type (@{type_name list}, [T])) = T - | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) -*} - -ML {* fun mk_atom_list t = let val ty = fastype_of t; @@ -83,193 +70,170 @@ *} ML {* -fun setify thy t = +fun setify ctxt t = let val ty = fastype_of t; in - if is_atom thy ty - then mk_singleton_atom t - else if is_atom_set thy ty + if is_atom ctxt ty + then HOLogic.mk_set @{typ atom} [mk_atom t] + else if is_atom_set ctxt ty then mk_atom_set t - else if is_atom_fset thy ty + else if is_atom_fset ctxt ty then mk_atom_fset t else error ("setify" ^ (PolyML.makestring (t, ty))) end *} ML {* -fun listify thy t = +fun listify ctxt t = let val ty = fastype_of t; in - if is_atom thy ty + if is_atom ctxt ty then HOLogic.mk_list @{typ atom} [mk_atom t] - else if is_atom_list ty + else if is_atom_list ctxt ty then mk_atom_set t else error "listify" end *} ML {* -fun set x = +fun to_set x = if fastype_of x = @{typ "atom list"} then @{term "set::atom list \ atom set"} $ x else x *} ML {* -fun fv_body thy dts args fv_frees supp i = +fun make_body fv_map args i = let - val x = nth args i; - val dt = nth dts i; + val arg = nth args i + val ty = fastype_of arg in - if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) $ x - else (if supp then mk_supp x else setify thy x) -end + case (AList.lookup (op=) fv_map ty) of + NONE => mk_supp arg + | SOME fv => fv $ arg +end *} ML {* -fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = +fun make_binder lthy fv_bn_map args (bn_option, i) = let - val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys) - fun bound_var (SOME bn, i) = set (bn $ nth args i) - | bound_var (NONE, i) = fv_body thy dts args fv_frees false i - val bound_vars = mk_union (map bound_var binds); - fun non_rec_var (SOME bn, i) = - if member (op =) bodys i - then noatoms - else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i) - | non_rec_var (NONE, _) = noatoms + val arg = nth args i in - mk_union ((mk_diff fv_bodys bound_vars) :: (map non_rec_var binds)) + case bn_option of + NONE => (setify lthy arg, @{term "{}::atom set"}) + | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) +end +*} + +ML {* +fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = +let + val t1 = map (make_body fv_map args) bodies + val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders) +in + fold_union (mk_diff (fold_union t1, fold_union t2)::t3) end *} ML {* -fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm = -case bm of - BEmy i => - let - val x = nth args i; - val dt = nth dts i; - in - case AList.lookup (op=) args_in_bn i of - NONE => if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) $ x - else mk_supp x - | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x - | SOME NONE => noatoms - end -| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -*} - -ML {* -fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bclausess (fvbn, (_, ith_dtyp, args_in_bns)) = +fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = let - fun fv_bn_constr (cname, dts) (args_in_bn, bclauses) = - let - val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; - val names = Datatype_Prop.make_tnames Ts; - val args = map Free (names ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp)); - val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn - in - HOLogic.mk_Trueprop (HOLogic.mk_eq - (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bclauses))) - end; - val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv = the (AList.lookup (op=) fv_map ty) + val lhs = fv $ list_comb (constr, args) + val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses + val rhs = fold_union rhs_trms in - map2 fv_bn_constr constrs (args_in_bns ~~ bclausess) + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end *} ML {* -fun fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss = +fun make_bn_body fv_map fv_bn_map bn_args args i = let - fun mk_fvbn_free (bn, ith, _) = - let - val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); - in - (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) - end; + val arg = nth args i + val ty = fastype_of arg +in + case AList.lookup (op=) bn_args i of + NONE => (case (AList.lookup (op=) fv_map ty) of + NONE => mk_supp arg + | SOME fv => fv $ arg) + | SOME (NONE) => @{term "{}::atom set"} + | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg +end +*} - val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs); - val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees - val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs; - val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs); +ML {* +fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = + case bclause of + BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies) + | BC (_, binders, bodies) => + let + val t1 = map (make_body fv_map args) bodies + val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders) + in + fold_union (mk_diff (fold_union t1, fold_union t2)::t3) + end +*} + +ML {* +fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, ty, arg_tys)) bclauses = +let + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) + val lhs = fv_bn $ list_comb (constr, args) + val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses + val rhs = fold_union rhs_trms in - (bn_fvbn, fvbn_names, eqs) + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end *} ML {* -fun fv_bm thy dts args fv_frees bn_fvbn bm = -case bm of - BEmy i => - let - val x = nth args i; - val dt = nth dts i; - in - if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) $ x - else mk_supp x - end -| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -*} - -ML {* -fun fv thy dt_descr sorts fv_frees bn_fvbn bclausess (fv_free, ith_dtyp) = +fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let - fun fv_constr (cname, dts) bclauses = - let - val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; - val names = Datatype_Prop.make_tnames Ts; - val args = map Free (names ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp)); - val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn - in - HOLogic.mk_Trueprop (HOLogic.mk_eq - (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bclauses))) - end; - val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; + val nth_constrs_info = nth constrs_info bn_n + val nth_bclausess = nth bclausesss bn_n in - map2 fv_constr constrs bclausess + map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end *} ML {* -fun define_raw_fvs dt_descr sorts bn_funs bclausesss lthy = +fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy = let - val thy = ProofContext.theory_of lthy; val fv_names = prefix_dt_names dt_descr sorts "fv_" - val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr; - val fv_frees = map Free (fv_names ~~ fv_types); + val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr; + val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; + val fv_frees = map Free (fv_names ~~ fv_tys); + val fv_map = fv_arg_tys ~~ fv_frees - (* free variables for the bn-functions *) - val (bn_fvbn_map, fv_bn_names, fv_bn_eqs) = - fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; + val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs) + val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2) + val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2 + val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2 + val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2 + val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2 + val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2) + val fv_bn_map2 = bns ~~ fv_bn_frees2 + val fv_bn_map3 = bns2 ~~ fv_bn_frees2 + + val constrs_info = all_dtyp_constrs_types dt_descr sorts - val _ = tracing ("bn_fvbn_map" ^ commas (map @{make_string} bn_fvbn_map)) + val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss + val fv_bn_eqs2 = map (make_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 - val fv_bns = map snd bn_fvbn_map; - val fv_nums = 0 upto (length fv_frees - 1) - - val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn_map) bclausesss (fv_frees ~~ fv_nums); + val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2) + val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2) - val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) - val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) - - val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_bn_eqs))) - - fun pat_completeness_auto ctxt = - Pat_Completeness.pat_completeness_tac ctxt 1 - THEN auto_tac (clasimpset_of ctxt) + fun pat_completeness_auto lthy = + Pat_Completeness.pat_completeness_tac lthy 1 + THEN auto_tac (clasimpset_of lthy) fun prove_termination lthy = Function.prove_termination NONE @@ -292,21 +256,8 @@ end *} -(**************************************************) -datatype foo = - C1 nat -| C2 foo int -(* -ML {* -fun mk_body descr sorts fv_ty_map dtyp = -let - val nth_dtyp_constr_tys descr sorts -in - true -end -*} -*) + end diff -r 231a20534950 -r ad03df7e8056 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/NewParser.thy Mon Jun 07 11:46:26 2010 +0200 @@ -2,9 +2,10 @@ imports "../Nominal-General/Nominal2_Base" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp" "Lift" + "Perm" "Tacs" "Equivp" "Lift" begin + section{* Interface for nominal_datatype *} @@ -139,7 +140,7 @@ fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = let val bn_funs' = map (fn (bn, ty, mx) => - (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs + (raw_bind bn, SOME (replace_typ dts_env ty), mx)) bn_funs val bn_eqs' = map (fn (attr, trm) => (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs @@ -154,10 +155,7 @@ fun rawify_bnds bnds = map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds - fun rawify_bclause (BEmy n) = BEmy n - | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys) - | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys) - | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys) + fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys) in map (map (map rawify_bclause)) bclauses end @@ -167,18 +165,23 @@ appends of elements; in case of recursive calls it retruns also the applied bn function *) ML {* -fun strip_bn_fun t = - case t of - Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r - | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r - | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => - (i, NONE) :: strip_bn_fun y - | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => - (i, NONE) :: strip_bn_fun y - | Const (@{const_name bot}, _) => [] - | Const (@{const_name Nil}, _) => [] - | (f as Free _) $ Bound i => [(i, SOME f)] - | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t)) +fun strip_bn_fun lthy args t = +let + fun aux t = + case t of + Const (@{const_name sup}, _) $ l $ r => aux l @ aux r + | Const (@{const_name append}, _) $ l $ r => aux l @ aux r + | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => + (find_index (equal x) args, NONE) :: aux y + | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => + (find_index (equal x) args, NONE) :: aux y + | Const (@{const_name bot}, _) => [] + | Const (@{const_name Nil}, _) => [] + | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] + | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t)) +in + aux t +end *} ML {* @@ -187,23 +190,21 @@ *} ML {* -fun prep_bn lthy dt_names dts eqs = +fun prep_bn_info lthy dt_names dts eqs = let fun aux eq = let val (lhs, rhs) = eq - |> strip_qnt_body "all" |> HOLogic.dest_Trueprop |> HOLogic.dest_eq val (bn_fun, [cnstr]) = strip_comb lhs - val (_, ty) = dest_Free bn_fun + val (_, ty) = dest_Const bn_fun val (ty_name, _) = dest_Type (domain_type ty) val dt_index = find_index (fn x => x = ty_name) dt_names - val (cnstr_head, cnstr_args) = strip_comb cnstr - val rhs_elements = strip_bn_fun rhs - val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements + val (cnstr_head, cnstr_args) = strip_comb cnstr + val rhs_elements = strip_bn_fun lthy cnstr_args rhs in - (dt_index, (bn_fun, (cnstr_head, included))) + (dt_index, (bn_fun, (cnstr_head, rhs_elements))) end fun order dts i ts = let @@ -219,9 +220,9 @@ val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) - val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) + (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*) (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*) - val _ = tracing ("ordered'\n" ^ @{make_string} ordered') + (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*) in ordered' end @@ -254,19 +255,37 @@ val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds - val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs) - val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy - val (raw_bn_funs, raw_bn_eqs, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 - - val morphism_2_0 = ProofContext.export_morphism lthy2 lthy - fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); - val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; + val (raw_dt_full_names, lthy1) = + add_datatype_wrapper raw_dt_names raw_dts lthy in - (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, lthy2) + (dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) end *} +ML {* +fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy = + if null raw_bn_funs + then ([], [], [], [], lthy) + else + let + val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs + Function_Common.default_config (pat_completeness_simp constr_thms) lthy + + val (info, lthy2) = prove_termination (Local_Theory.restore lthy1) + val {fs, simps, inducts, ...} = info; + + val raw_bn_induct = (the inducts) + val raw_bn_eqs = the simps + + val raw_bn_info = + prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) + in + (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) + end +*} + + lemma equivp_hack: "equivp x" sorry ML {* @@ -286,76 +305,6 @@ ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} ML {* val cheat_supp_eq = Unsynchronized.ref false *} -ML {* -fun remove_loop t = - let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end - handle TERM _ => @{thm eqTrueI} OF [t] -*} - -text {* - nominal_datatype2 does the following things in order: - -Parser.thy/raw_nominal_decls - 1) define the raw datatype - 2) define the raw binding functions - -Perm.thy/define_raw_perms - 3) define permutations of the raw datatype and show that the raw type is - in the pt typeclass - -Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha - 4) define fv and fv_bn - 5) define alpha and alpha_bn - -Perm.thy/distinct_rel - 6) prove alpha_distincts (C1 x \ C2 y ...) (Proof by cases; simp) - -Tacs.thy/build_rel_inj - 6) prove alpha_eq_iff (C1 x = C2 y \ P x y ...) - (left-to-right by intro rule, right-to-left by cases; simp) -Equivp.thy/prove_eqvt - 7) prove bn_eqvt (common induction on the raw datatype) - 8) prove fv_eqvt (common induction on the raw datatype with help of above) -Rsp.thy/build_alpha_eqvts - 9) prove alpha_eqvt and alpha_bn_eqvt - (common alpha-induction, unfolding alpha_gen, permute of #* and =) -Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps - 10) prove that alpha and alpha_bn are equivalence relations - (common induction and application of 'compose' lemmas) -Lift.thy/define_quotient_types - 11) define quotient types -Rsp.thy/build_fvbv_rsps - 12) prove bn respects (common induction and simp with alpha_gen) -Rsp.thy/prove_const_rsp - 13) prove fv respects (common induction and simp with alpha_gen) - 14) prove permute respects (unfolds to alpha_eqvt) -Rsp.thy/prove_alpha_bn_rsp - 15) prove alpha_bn respects - (alpha_induct then cases then sym and trans of the relations) -Rsp.thy/prove_alpha_alphabn - 16) show that alpha implies alpha_bn (by unduction, needed in following step) -Rsp.thy/prove_const_rsp - 17) prove respects for all datatype constructors - (unfold eq_iff and alpha_gen; introduce zero permutations; simp) -Perm.thy/quotient_lift_consts_export - 18) define lifted constructors, fv, bn, alpha_bn, permutations -Perm.thy/define_lifted_perms - 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass -Lift.thy/lift_thm - 20) lift permutation simplifications - 21) lift induction - 22) lift fv - 23) lift bn - 24) lift eq_iff - 25) lift alpha_distincts - 26) lift fv and bn eqvts -Equivp.thy/prove_supports - 27) prove that union of arguments supports constructors -Equivp.thy/prove_fs - 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) -Equivp.thy/supp_eq - 29) prove supp = fv -*} ML {* (* for testing porposes - to exit the procedure early *) @@ -371,29 +320,32 @@ ML {* fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = let - (* definition of the raw datatypes and raw bn-functions *) - val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) = - if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy + (* definition of the raw datatypes *) + + val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = + if get_STEPS lthy > 0 + then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy else raise TEST lthy - val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) + val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr val all_full_tnames = map (fn (_, (n, _, _)) => n) descr - val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_full_tnames val inject_thms = flat (map #inject dtinfos); val distinct_thms = flat (map #distinct dtinfos); + val constr_thms = inject_thms @ distinct_thms val rel_dtinfos = List.take (dtinfos, (length dts)); - val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) + val raw_constrs_distinct = (map #distinct rel_dtinfos); val induct_thm = #induct dtinfo; val exhaust_thms = map #exhaust dtinfos; (* definitions of raw permutations *) - val ((perms, raw_perm_defs, raw_perm_simps), lthy2) = - if get_STEPS lthy1 > 2 - then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 - else raise TEST lthy1 + val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = + if get_STEPS lthy0 > 1 + then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0 + else raise TEST lthy0 (* noting the raw permutations as eqvt theorems *) val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) @@ -404,53 +356,94 @@ (* definition of raw fv_functions *) val lthy3 = Theory_Target.init NONE thy; - val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; - val (fv, fvbn, fv_def, lthy3a) = - if get_STEPS lthy2 > 3 - then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3 + val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = + if get_STEPS lthy3 > 2 + then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 else raise TEST lthy3 - + + val bn_nos = map (fn (_, i, _) => i) raw_bn_info; + val bns = raw_bn_funs ~~ bn_nos; + + val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = + if get_STEPS lthy3a > 3 + then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a + else raise TEST lthy3a + (* definition of raw alphas *) - val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = - if get_STEPS lthy > 4 - then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a - else raise TEST lthy3a - - val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts + val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = + if get_STEPS lthy3b > 4 + then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b + else raise TEST lthy3b - val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); - val bn_tys = map (domain_type o fastype_of) raw_bn_funs; - val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; - val bns = raw_bn_funs ~~ bn_nos; - val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) - (rel_distinct ~~ alpha_ts_nobn)); - val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) - ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) - + (* definition of alpha-distinct lemmas *) + val (alpha_distincts, alpha_bn_distincts) = + mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info + (* definition of raw_alpha_eq_iff lemmas *) - val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 - val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; - val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp); + val alpha_eq_iff = + if get_STEPS lthy > 5 + then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases + else raise TEST lthy4 + + (* proving equivariance lemmas for bns, fvs and alpha *) + val _ = warning "Proving equivariance"; + val bn_eqvt = + if get_STEPS lthy > 6 + then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 + else raise TEST lthy4 - (* proving equivariance lemmas *) - val _ = warning "Proving equivariance"; - val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 - val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5 - val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; + (* noting the bn_eqvt lemmas in a temprorary theory *) + val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) + val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) + + val fv_eqvt = + if get_STEPS lthy > 7 + then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) + (Local_Theory.restore lthy_tmp) + else raise TEST lthy4 + + val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) + + val (alpha_eqvt, lthy_tmp'') = + if get_STEPS lthy > 8 + then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy_tmp' + else raise TEST lthy4 (* proving alpha equivalence *) - val _ = warning "Proving equivalence"; - val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; - val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; + val _ = warning "Proving equivalence" + + val alpha_sym_thms = + if get_STEPS lthy > 9 + then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp'' + else raise TEST lthy4 + + val alpha_trans_thms = + if get_STEPS lthy > 10 + then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) + alpha_intros alpha_induct alpha_cases lthy_tmp'' + else raise TEST lthy4 + + + val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) + val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) + + val _ = + if get_STEPS lthy > 11 + then true else raise TEST lthy4 + + val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos + + val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; val alpha_equivp = - if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts - else build_equivps alpha_ts reflps alpha_induct - inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a; + if !cheat_equivp then map (equivp_hack lthy4) alpha_trms + else build_equivps alpha_trms reflps alpha_induct + inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; + val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; val qty_full_names = map (Long_Name.qualify thy_name) qty_names - val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts_nobn alpha_equivp lthy6a; + val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy4; val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); val raw_consts = flat (map (fn (i, (_, _, l)) => @@ -459,43 +452,43 @@ Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; val _ = warning "Proving respects"; - val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; + val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8; val (bns_rsp_pre, lthy9) = fold_map ( fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => resolve_tac bns_rsp_pre' 1)) bns lthy8; val bns_rsp = flat (map snd bns_rsp_pre); fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy - else fvbv_rsp_tac alpha_induct fv_def lthy8 1; - val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; + else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1; + val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9; val (fv_rsp_pre, lthy10) = fold_map (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] - (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; + (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9; val fv_rsp = flat (map snd fv_rsp_pre); - val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms + val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else - let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; + let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] - alpha_bn_rsp_tac) alpha_ts_bn lthy11 + alpha_bn_rsp_tac) alpha_bn_trms lthy11 fun const_rsp_tac _ = - let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a - in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end + let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a + in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] const_rsp_tac) raw_consts lthy11a - val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) - val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; - val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; + val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) + val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12; + val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; - val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn - val (qalpha_ts_bn, qalphabn_defs, lthy12c) = - quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; + val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms + val (qalpha_bn_trms, qalphabn_defs, lthy12c) = + quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_trms) lthy12b; val _ = warning "Lifting permutations"; val thy = Local_Theory.exit_global lthy12c; val perm_names = map (fn x => "permute_" ^ x) qty_names - val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy; + val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) raw_perm_simps thy; val lthy13 = Theory_Target.init NONE thy'; val q_name = space_implode "_" qty_names; fun suffix_bind s = Binding.qualify true q_name (Binding.name s); @@ -509,26 +502,26 @@ val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; - val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct + val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; val q_perm = map (lift_thm qtys lthy14) raw_perm_defs; val lthy15 = note_simp_suffix "perm" q_perm lthy14a; - val q_fv = map (lift_thm qtys lthy15) fv_def; + val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; val lthy16 = note_simp_suffix "fv" q_fv lthy15; val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; val lthy17 = note_simp_suffix "bn" q_bn lthy16; val _ = warning "Lifting eq-iff"; (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) - val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff_simp + val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded1; val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; - val q_dis = map (lift_thm qtys lthy18) rel_dists; + val q_dis = map (lift_thm qtys lthy18) alpha_distincts; val lthy19 = note_simp_suffix "distinct" q_dis lthy18; - val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); + val q_eqvt = map (lift_thm qtys lthy19) (bn_eqvt @ fv_eqvt); val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; val _ = warning "Supports"; @@ -539,7 +532,7 @@ val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) val lthy22 = Class.prove_instantiation_instance tac lthy21 - val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; + val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos; val (names, supp_eq_t) = supp_eq fv_alpha_all; val _ = warning "Support Equations"; fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else @@ -639,16 +632,16 @@ fun prep_body env bn_str = index_lookup env bn_str - fun prep_mode "bind" = BLst - | prep_mode "bind_set" = BSet - | prep_mode "bind_res" = BRes + fun prep_mode "bind" = Lst + | prep_mode "bind_set" = Set + | prep_mode "bind_res" = Res fun prep_bclause env (mode, binders, bodies) = let val binders' = map (prep_binder env) binders val bodies' = map (prep_body env) bodies in - prep_mode mode (binders', bodies') + BC (prep_mode mode, binders', bodies') end fun prep_bclauses (annos, bclause_strs) = @@ -670,10 +663,7 @@ ML {* fun included i bcs = let - fun incl (BEmy j) = i = j - | incl (BLst (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) - | incl (BSet (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) - | incl (BRes (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) + fun incl (BC (_, bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) in exists incl bcs end @@ -688,7 +678,7 @@ fun complt n bcs = let - fun add bcs i = (if included i bcs then [] else [BEmy i]) + fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) in bcs @ (flat (map_range (add bcs) n)) end @@ -718,108 +708,71 @@ (main_parser >> nominal_datatype2_cmd) *} -(* -atom_decl name + +text {* + nominal_datatype2 does the following things in order: -nominal_datatype lam = - Var name -| App lam lam -| Lam x::name t::lam bind_set x in t -| Let p::pt t::lam bind_set "bn p" in t -and pt = - P1 name -| P2 pt pt -binder - bn::"pt \ atom set" -where - "bn (P1 x) = {atom x}" -| "bn (P2 p1 p2) = bn p1 \ bn p2" - -find_theorems Var_raw - - +Parser.thy/raw_nominal_decls + 1) define the raw datatype + 2) define the raw binding functions -thm lam_pt.bn -thm lam_pt.fv[simplified lam_pt.supp(1-2)] -thm lam_pt.eq_iff -thm lam_pt.induct -thm lam_pt.perm - -nominal_datatype exp = - EVar name -| EUnit -| EPair q1::exp q2::exp -| ELetRec l::lrbs e::exp bind "b_lrbs l" in e l +Perm.thy/define_raw_perms + 3) define permutations of the raw datatype and show that the raw type is + in the pt typeclass + +Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha + 4) define fv and fv_bn + 5) define alpha and alpha_bn -and fnclause = - K x::name p::pat f::exp bind_res "b_pat p" in f - -and fnclauses = - S fnclause -| ORs fnclause fnclauses - -and lrb = - Clause fnclauses - -and lrbs = - Single lrb -| More lrb lrbs +Perm.thy/distinct_rel + 6) prove alpha_distincts (C1 x \ C2 y ...) (Proof by cases; simp) -and pat = - PVar name -| PUnit -| PPair pat pat - -binder - b_lrbs :: "lrbs \ atom list" and - b_pat :: "pat \ atom set" and - b_fnclauses :: "fnclauses \ atom list" and - b_fnclause :: "fnclause \ atom list" and - b_lrb :: "lrb \ atom list" - -where - "b_lrbs (Single l) = b_lrb l" -| "b_lrbs (More l ls) = append (b_lrb l) (b_lrbs ls)" -| "b_pat (PVar x) = {atom x}" -| "b_pat (PUnit) = {}" -| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" -| "b_fnclauses (S fc) = (b_fnclause fc)" -| "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)" -| "b_lrb (Clause fcs) = (b_fnclauses fcs)" -| "b_fnclause (K x pat exp) = [atom x]" - -thm exp_fnclause_fnclauses_lrb_lrbs_pat.bn -thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv -thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff -thm exp_fnclause_fnclauses_lrb_lrbs_pat.induct -thm exp_fnclause_fnclauses_lrb_lrbs_pat.perm - -nominal_datatype ty = - Vr "name" -| Fn "ty" "ty" -and tys = - Al xs::"name fset" t::"ty" bind_res xs in t - -thm ty_tys.fv[simplified ty_tys.supp] -thm ty_tys.eq_iff - -*) - -(* some further tests *) - -(* -nominal_datatype ty2 = - Vr2 "name" -| Fn2 "ty2" "ty2" - -nominal_datatype tys2 = - All2 xs::"name fset" ty::"ty2" bind_res xs in ty - -nominal_datatype lam2 = - Var2 "name" -| App2 "lam2" "lam2 list" -| Lam2 x::"name" t::"lam2" bind x in t -*) +Tacs.thy/build_rel_inj + 6) prove alpha_eq_iff (C1 x = C2 y \ P x y ...) + (left-to-right by intro rule, right-to-left by cases; simp) +Equivp.thy/prove_eqvt + 7) prove bn_eqvt (common induction on the raw datatype) + 8) prove fv_eqvt (common induction on the raw datatype with help of above) +Rsp.thy/build_alpha_eqvts + 9) prove alpha_eqvt and alpha_bn_eqvt + (common alpha-induction, unfolding alpha_gen, permute of #* and =) +Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps + 10) prove that alpha and alpha_bn are equivalence relations + (common induction and application of 'compose' lemmas) +Lift.thy/define_quotient_types + 11) define quotient types +Rsp.thy/build_fvbv_rsps + 12) prove bn respects (common induction and simp with alpha_gen) +Rsp.thy/prove_const_rsp + 13) prove fv respects (common induction and simp with alpha_gen) + 14) prove permute respects (unfolds to alpha_eqvt) +Rsp.thy/prove_alpha_bn_rsp + 15) prove alpha_bn respects + (alpha_induct then cases then sym and trans of the relations) +Rsp.thy/prove_alpha_alphabn + 16) show that alpha implies alpha_bn (by unduction, needed in following step) +Rsp.thy/prove_const_rsp + 17) prove respects for all datatype constructors + (unfold eq_iff and alpha_gen; introduce zero permutations; simp) +Perm.thy/quotient_lift_consts_export + 18) define lifted constructors, fv, bn, alpha_bn, permutations +Perm.thy/define_lifted_perms + 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass +Lift.thy/lift_thm + 20) lift permutation simplifications + 21) lift induction + 22) lift fv + 23) lift bn + 24) lift eq_iff + 25) lift alpha_distincts + 26) lift fv and bn eqvts +Equivp.thy/prove_supports + 27) prove that union of arguments supports constructors +Equivp.thy/prove_fs + 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) +Equivp.thy/supp_eq + 29) prove supp = fv +*} diff -r 231a20534950 -r ad03df7e8056 Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Nominal2_FSet.thy Mon Jun 07 11:46:26 2010 +0200 @@ -1,8 +1,14 @@ theory Nominal2_FSet imports "../Nominal-General/Nominal2_Supp" + "../Nominal-General/Nominal2_Atoms" + "../Nominal-General/Nominal2_Eqvt" FSet begin +lemma "p \ {} = {}" +apply(perm_simp) +by simp + lemma permute_rsp_fset[quot_respect]: "(op = ===> list_eq ===> list_eq) permute permute" apply (simp add: eqvts[symmetric]) @@ -34,12 +40,29 @@ end -lemma permute_fset[simp, eqvt]: +lemma "p \ {} = {}" +apply(perm_simp) +by simp + +lemma permute_fset[simp]: fixes S::"('a::pt) fset" shows "(p \ {||}) = ({||} ::('a::pt) fset)" and "p \ finsert x S = finsert (p \ x) (p \ S)" by (lifting permute_list.simps) +lemma "p \ {} = {}" +apply(perm_simp) +by simp + +ML {* @{term "{}"} ; @{term "{||}"} *} + +declare permute_fset[eqvt] + +lemma "p \ {} = {}" +apply(perm_simp) +by simp + + lemma fmap_eqvt[eqvt]: shows "p \ (fmap f S) = fmap (p \ f) (p \ S)" by (lifting map_eqvt) @@ -119,4 +142,8 @@ apply auto done +lemma "p \ {} = {}" +apply(perm_simp) +by simp + end diff -r 231a20534950 -r ad03df7e8056 Nominal/Perm.thy --- a/Nominal/Perm.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Perm.thy Mon Jun 07 11:46:26 2010 +0200 @@ -1,185 +1,26 @@ theory Perm -imports "../Nominal-General/Nominal2_Atoms" +imports + "../Nominal-General/Nominal2_Base" + "../Nominal-General/Nominal2_Atoms" + "../Nominal-General/Nominal2_Eqvt" + "Nominal2_FSet" + "Abs" +uses ("nominal_dt_rawperm.ML") + ("nominal_dt_rawfuns.ML") + ("nominal_dt_alpha.ML") begin -(* definitions of the permute function for raw nominal datatypes *) - - -ML {* -(* returns the type of the nth datatype *) -fun nth_dtyp descr sorts n = - Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); - -(* returns the constructors of the nth datatype *) -fun nth_dtyp_constrs descr n = -let - val (_, (_, _, constrs)) = nth descr n -in - constrs -end - -(* returns the types of the constructors of the nth datatype *) -fun nth_dtyp_constr_typs descr sorts n = - map (map (Datatype_Aux.typ_of_dtyp descr sorts) o snd) (nth_dtyp_constrs descr n) -*} - -ML {* -(* generates for every datatype a name str ^ dt_name - plus and index for multiple occurences of a string *) -fun prefix_dt_names descr sorts str = -let - fun get_nth_name (i, _) = - Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) -in - Datatype_Prop.indexify_names - (map (prefix str o get_nth_name) descr) -end -*} - - -ML {* -(* permutation function for one argument - - - in case the argument is recursive it returns - - permute_fn p arg - - - in case the argument is non-recursive it will return - - p o arg - -*) -fun perm_arg permute_fn_frees p (arg_dty, arg) = - if Datatype_Aux.is_rec_type arg_dty - then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg - else mk_perm p arg -*} - -ML {* -(* generates the equation for the permutation function for one constructor; - i is the index of the corresponding datatype *) -fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) = -let - val p = Free ("p", @{typ perm}) - val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts - val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) - val args = map Free (arg_names ~~ arg_tys) - val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) - val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args) - val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args)) - val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) -in - (Attrib.empty_binding, eq) -end -*} - -ML {* -(* proves the two pt-type class properties *) -fun prove_permute_zero lthy induct perm_defs perm_fns = -let - val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = Datatype_Prop.make_tnames perm_types - - fun single_goal ((perm_fn, T), x) = - HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) - - val goals = - HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) - - val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) +use "nominal_dt_rawperm.ML" +ML {* open Nominal_Dt_RawPerm *} - val tac = (Datatype_Aux.indtac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 -in - Goal.prove lthy perm_indnames [] goals (K tac) - |> Datatype_Aux.split_conj_thm -end -*} - -ML {* -fun prove_permute_plus lthy induct perm_defs perm_fns = -let - val p = Free ("p", @{typ perm}) - val q = Free ("q", @{typ perm}) - val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = Datatype_Prop.make_tnames perm_types - - fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq - (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) - - val goals = - HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) - - val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) - - val tac = (Datatype_Aux.indtac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 -in - Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) - |> Datatype_Aux.split_conj_thm -end -*} - -ML {* -(* defines the permutation functions for raw datatypes and - proves that they are instances of pt +use "nominal_dt_rawfuns.ML" +ML {* open Nominal_Dt_RawFuns *} - user_dt_nos refers to the number of "un-unfolded" datatypes - given by the user -*) -fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy = -let - val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; - val user_full_tnames = List.take (all_full_tnames, user_dt_nos); - - val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" - val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr - val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) - - fun perm_eq (i, (_, _, constrs)) = - map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; - - val perm_eqs = maps perm_eq dt_descr; - - val lthy = - Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; - - val ((perm_funs, perm_eq_thms), lthy') = - Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; - - val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs - val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs - val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); - val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) - val perms_name = space_implode "_" perm_fn_names - val perms_zero_bind = Binding.name (perms_name ^ "_zero") - val perms_plus_bind = Binding.name (perms_name ^ "_plus") - - fun tac _ (_, _, simps) = - Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) - - fun morphism phi (fvs, dfs, simps) = - (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); -in - lthy' - |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) - |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) - |> Class_Target.prove_instantiation_exit_result morphism tac - (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') -end -*} - - - - +use "nominal_dt_alpha.ML" +ML {* open Nominal_Dt_Alpha *} (* permutations for quotient types *) -ML {* Class_Target.prove_instantiation_exit_result *} - ML {* fun quotient_lift_consts_export qtys spec ctxt = let @@ -209,60 +50,5 @@ end *} -ML {* -fun neq_to_rel r neq = -let - val neq = HOLogic.dest_Trueprop (prop_of neq) - val eq = HOLogic.dest_not neq - val (lhs, rhs) = HOLogic.dest_eq eq - val rel = r $ lhs $ rhs - val nrel = HOLogic.mk_not rel -in - HOLogic.mk_Trueprop nrel -end -*} - -ML {* -fun neq_to_rel_tac cases distinct = - rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct) -*} - -ML {* -fun distinct_rel ctxt cases (dists, rel) = -let - val ((_, thms), ctxt') = Variable.import false dists ctxt - val terms = map (neq_to_rel rel) thms - val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms -in - Variable.export ctxt' ctxt nrels -end -*} - - - -(* Test *) -(* -atom_decl name - -datatype trm = - Var "name" -| App "trm" "(trm list) list" -| Lam "name" "trm" -| Let "bp" "trm" "trm" -and bp = - BUnit -| BVar "name" -| BPair "bp" "bp" - -setup {* fn thy => -let - val info = Datatype.the_info thy "Perm.trm" -in - define_raw_perms info 2 thy |> snd -end -*} - -print_theorems -*) end diff -r 231a20534950 -r ad03df7e8056 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/ROOT.ML Mon Jun 07 11:46:26 2010 +0200 @@ -14,6 +14,6 @@ "Ex/ExPS3", "Ex/ExPS7", "Ex/CoreHaskell", - "Ex/Test", - "Manual/Term4" + "Ex/Test"(*, + "Manual/Term4"*) ]; diff -r 231a20534950 -r ad03df7e8056 Nominal/Tacs.thy --- a/Nominal/Tacs.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Nominal/Tacs.thy Mon Jun 07 11:46:26 2010 +0200 @@ -29,32 +29,6 @@ val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) *} -(* Given function for buildng a goal for an input, prepares a - one common goals for all the inputs and proves it by induction - together *) -ML {* -fun prove_by_induct tys build_goal ind utac inputs ctxt = -let - val names = Datatype_Prop.make_tnames tys; - val (names', ctxt') = Variable.variant_fixes names ctxt; - val frees = map Free (names' ~~ tys); - val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt'; - val gls = flat gls_lists; - fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls; - val trm_gl_lists = map trm_gls_map frees; - val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists - val trm_gls = map mk_conjl trm_gl_lists; - val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls); - fun tac {context,...} = ( - InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind] - THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1 - val th_loc = Goal.prove ctxt'' [] [] gl tac - val ths_loc = HOLogic.conj_elims th_loc - val ths = Variable.export ctxt'' ctxt ths_loc -in - filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths -end -*} ML {* fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt = @@ -83,41 +57,6 @@ filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths end *} -(* Code for transforming an inductive relation to a function *) -ML {* -fun rel_inj_tac dist_inj intrs elims = - SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' - (rtac @{thm iffI} THEN' RANGE [ - (eresolve_tac elims THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps dist_inj) - ), - asm_full_simp_tac (HOL_ss addsimps intrs)]) -*} - -ML {* -fun build_rel_inj_gl thm = - let - val prop = prop_of thm; - val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); - val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); - fun list_conj l = foldr1 HOLogic.mk_conj l; - in - if hyps = [] then concl - else HOLogic.mk_eq (concl, list_conj hyps) - end; -*} - -ML {* -fun build_rel_inj intrs dist_inj elims ctxt = -let - val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt; - val gls = map (HOLogic.mk_Trueprop o build_rel_inj_gl) thms_imp; - fun tac _ = rel_inj_tac dist_inj intrs elims 1; - val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls; -in - Variable.export ctxt' ctxt thms -end -*} ML {* fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm diff -r 231a20534950 -r ad03df7e8056 Nominal/nominal_dt_alpha.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_alpha.ML Mon Jun 07 11:46:26 2010 +0200 @@ -0,0 +1,449 @@ +(* Title: nominal_dt_alpha.ML + Author: Cezary Kaliszyk + Author: Christian Urban + + Definitions of the alpha relations. +*) + +signature NOMINAL_DT_ALPHA = +sig + val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info -> + bclause list list list -> term list -> Proof.context -> + term list * term list * thm list * thm list * thm * local_theory + + val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> + term list -> term list -> bn_info -> thm list * thm list + + val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list + + val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list + val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list +end + +structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = +struct + +(** definition of the inductive rules for alpha and alpha_bn **) + +(* construct the compound terms for prod_fv and prod_alpha *) +fun mk_prod_fv (t1, t2) = +let + val ty1 = fastype_of t1 + val ty2 = fastype_of t2 + val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"} +in + Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2 +end + +fun mk_prod_alpha (t1, t2) = +let + val ty1 = fastype_of t1 + val ty2 = fastype_of t2 + val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) + val resT = [prodT, prodT] ---> @{typ "bool"} +in + Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2 +end + +(* generates the compound binder terms *) +fun mk_binders lthy bmode args bodies = +let + fun bind_set lthy args (NONE, i) = setify lthy (nth args i) + | bind_set _ args (SOME bn, i) = bn $ (nth args i) + fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) + | bind_lst _ args (SOME bn, i) = bn $ (nth args i) + + val (combine_fn, bind_fn) = + case bmode of + Lst => (mk_append, bind_lst) + | Set => (mk_union, bind_set) + | Res => (mk_union, bind_set) +in + foldl1 combine_fn (map (bind_fn lthy args) bodies) +end + +(* produces the term for an alpha with abstraction *) +fun mk_alpha_term bmode fv alpha args args' binders binders' = +let + val (alpha_name, binder_ty) = + case bmode of + Lst => (@{const_name "alpha_lst"}, @{typ "atom list"}) + | Set => (@{const_name "alpha_gen"}, @{typ "atom set"}) + | Res => (@{const_name "alpha_res"}, @{typ "atom set"}) + val ty = fastype_of args + val pair_ty = HOLogic.mk_prodT (binder_ty, ty) + val alpha_ty = [ty, ty] ---> @{typ "bool"} + val fv_ty = ty --> @{typ "atom set"} + val pair_lhs = HOLogic.mk_prod (binders, args) + val pair_rhs = HOLogic.mk_prod (binders', args') +in + HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, + Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) + $ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs) +end + +(* for non-recursive binders we have to produce alpha_bn premises *) +fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = + case binder of + (NONE, _) => [] + | (SOME bn, i) => + if member (op=) bodies i then [] + else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)] + +(* generat the premises for an alpha rule; mk_frees is used + if no binders are present *) +fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause = +let + fun mk_frees i = + let + val arg = nth args i + val arg' = nth args' i + val ty = fastype_of arg + in + if nth is_rec i + then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg' + else HOLogic.mk_eq (arg, arg') + end + + fun mk_alpha_fv i = + let + val ty = fastype_of (nth args i) + in + case AList.lookup (op=) alpha_map ty of + NONE => (HOLogic.eq_const ty, supp_const ty) + | SOME (alpha, fv) => (alpha, fv) + end +in + case bclause of + BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies + | BC (bmode, binders, bodies) => + let + val (alphas, fvs) = split_list (map mk_alpha_fv bodies) + val comp_fv = foldl1 mk_prod_fv fvs + val comp_alpha = foldl1 mk_prod_alpha alphas + val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies) + val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies) + val comp_binders = mk_binders lthy bmode args binders + val comp_binders' = mk_binders lthy bmode args' binders + val alpha_prem = + mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders' + val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders) + in + map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems) + end +end + +(* produces the introduction rule for an alpha rule *) +fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = +let + val arg_names = Datatype_Prop.make_tnames arg_tys + val arg_names' = Name.variant_list arg_names arg_names + val args = map Free (arg_names ~~ arg_tys) + val args' = map Free (arg_names' ~~ arg_tys) + val alpha = fst (the (AList.lookup (op=) alpha_map ty)) + val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args')) + val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses +in + Library.foldr Logic.mk_implies (flat prems, concl) +end + +(* produces the premise of an alpha-bn rule; we only need to + treat the case special where the binding clause is empty; + + - if the body is not included in the bn_info, then we either + produce an equation or an alpha-premise + + - if the body is included in the bn_info, then we create + either a recursive call to alpha-bn, or no premise *) +fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause = +let + fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i = + let + val arg = nth args i + val arg' = nth args' i + val ty = fastype_of arg + in + case AList.lookup (op=) bn_args i of + NONE => (case (AList.lookup (op=) alpha_map ty) of + NONE => [HOLogic.mk_eq (arg, arg')] + | SOME (alpha, _) => [alpha $ arg $ arg']) + | SOME (NONE) => [] + | SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg'] + end +in + case bclause of + BC (_, [], bodies) => + map HOLogic.mk_Trueprop + (flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies)) + | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause +end + +fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses = +let + val arg_names = Datatype_Prop.make_tnames arg_tys + val arg_names' = Name.variant_list arg_names arg_names + val args = map Free (arg_names ~~ arg_tys) + val args' = map Free (arg_names' ~~ arg_tys) + val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm) + val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args')) + val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses +in + Library.foldr Logic.mk_implies (flat prems, concl) +end + +fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = +let + val nth_constrs_info = nth constrs_info bn_n + val nth_bclausess = nth bclausesss bn_n +in + map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess +end + +fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy = +let + val alpha_names = prefix_dt_names descr sorts "alpha_" + val alpha_arg_tys = all_dtyps descr sorts + val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys + val alpha_frees = map Free (alpha_names ~~ alpha_tys) + val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs) + + val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) + val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns + val alpha_bn_names = map (prefix "alpha_") bn_names + val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys + val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys + val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) + val alpha_bn_map = bns ~~ alpha_bn_frees + + val constrs_info = all_dtyp_constrs_types descr sorts + + val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss + val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info + + val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) + (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) + val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) + + 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 = false, fork_mono = false} + all_alpha_names [] all_alpha_intros [] lthy + + val all_alpha_trms_loc = #preds alphas; + val alpha_induct_loc = #raw_induct alphas; + val alpha_intros_loc = #intrs alphas; + val alpha_cases_loc = #elims alphas; + val phi = ProofContext.export_morphism lthy' lthy; + + val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc; + val alpha_induct = Morphism.thm phi alpha_induct_loc; + val alpha_intros = map (Morphism.thm phi) alpha_intros_loc + val alpha_cases = map (Morphism.thm phi) alpha_cases_loc + + val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms +in + (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') +end + + +(** produces the distinctness theorems **) + +(* transforms the distinctness theorems of the constructors + to "not-alphas" of the constructors *) +fun mk_alpha_distinct_goal alpha neq = +let + val (lhs, rhs) = + neq + |> HOLogic.dest_Trueprop + |> HOLogic.dest_not + |> HOLogic.dest_eq +in + alpha $ lhs $ rhs + |> HOLogic.mk_not + |> HOLogic.mk_Trueprop +end + +fun distinct_tac cases distinct_thms = + rtac notI THEN' eresolve_tac cases + THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) + +fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) = +let + val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt + val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms + val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals +in + Variable.export ctxt' ctxt nrels +end + +fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos = +let + val alpha_distincts = + map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms) + val distinc_thms = map + val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos + val alpha_bn_distincts = + map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_trms) +in + (flat alpha_distincts, flat alpha_bn_distincts) +end + + +(** produces the alpha_eq_iff simplification rules **) + + +(* in case a theorem is of the form (C.. = C..), it will be + rewritten to ((C.. = C..) = True) *) +fun mk_simp_rule thm = + case (prop_of thm) of + @{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm] + | _ => thm + +fun alpha_eq_iff_tac dist_inj intros elims = + SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE' + (rtac @{thm iffI} THEN' + RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj), + asm_full_simp_tac (HOL_ss addsimps intros)]) + +fun mk_alpha_eq_iff_goal thm = + let + val prop = prop_of thm; + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); + val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); + fun list_conj l = foldr1 HOLogic.mk_conj l; + in + if hyps = [] then HOLogic.mk_Trueprop concl + else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) + end; + +fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims = +let + val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; + val goals = map mk_alpha_eq_iff_goal thms_imp; + val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; + val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; +in + Variable.export ctxt' ctxt thms + |> map mk_simp_rule +end + + + +(** symmetry proof for the alphas **) + +val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p" + by (erule exE, rule_tac x="-p" in exI, auto)} + +(* for premises that contain binders *) +fun prem_bound_tac pred_names ctxt = +let + fun trans_prem_tac pred_names ctxt = + SUBPROOF (fn {prems, context, ...} => + let + val prems' = map (transform_prem1 context pred_names) prems + in + resolve_tac prems' 1 + end) ctxt + val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas} +in + EVERY' + [ etac exi_neg, + resolve_tac @{thms alpha_gen_sym_eqvt}, + asm_full_simp_tac (HOL_ss addsimps prod_simps), + Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, + trans_prem_tac pred_names ctxt ] +end + +fun prove_sym_tac pred_names intros induct ctxt = +let + val prem_eq_tac = rtac @{thm sym} THEN' atac + val prem_unbound_tac = atac + + val prem_cases_tacs = FIRST' + [prem_eq_tac, prem_unbound_tac, prem_bound_tac pred_names ctxt] +in + HEADGOAL (rtac induct THEN_ALL_NEW + (resolve_tac intros THEN_ALL_NEW prem_cases_tacs)) +end + +fun prep_sym_goal alpha_trm (arg1, arg2) = +let + val lhs = alpha_trm $ arg1 $ arg2 + val rhs = alpha_trm $ arg2 $ arg1 +in + HOLogic.mk_imp (lhs, rhs) +end + +fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt = +let + val alpha_names = map (fst o dest_Const) alpha_trms + val arg_tys = + alpha_trms + |> map fastype_of + |> map domain_type + val (arg_names1, (arg_names2, ctxt')) = + ctxt + |> Variable.variant_fixes (replicate (length arg_tys) "x") + ||> Variable.variant_fixes (replicate (length arg_tys) "y") + val args1 = map Free (arg_names1 ~~ arg_tys) + val args2 = map Free (arg_names2 ~~ arg_tys) + val goal = HOLogic.mk_Trueprop + (foldr1 HOLogic.mk_conj (map2 prep_sym_goal alpha_trms (args1 ~~ args2))) +in + Goal.prove ctxt' [] [] goal + (fn {context,...} => prove_sym_tac alpha_names alpha_intros alpha_induct context) + |> singleton (ProofContext.export ctxt' ctxt) + |> Datatype_Aux.split_conj_thm + |> map (fn th => zero_var_indexes (th RS mp)) +end + + +(** transitivity proof for alphas **) + +fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt = +let + val _ = ("induct\n" ^ Syntax.string_of_term ctxt (prop_of induct)) + + val tac1 = asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) + fun tac i = (EVERY' [rtac @{thm allI}, rtac @{thm impI}, rotate_tac ~1, + etac (nth cases i) THEN_ALL_NEW tac1]) i +in + HEADGOAL (rtac induct THEN_ALL_NEW tac) +end + +fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = +let + val lhs = alpha_trm $ arg1 $ arg2 + val mid = alpha_trm $ arg2 $ (Bound 0) + val rhs = alpha_trm $ arg1 $ (Bound 0) +in + HOLogic.mk_imp (lhs, + HOLogic.all_const arg_ty $ Abs ("z", arg_ty, + HOLogic.mk_imp (mid, rhs))) +end + +fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = +let + val alpha_names = map (fst o dest_Const) alpha_trms + val arg_tys = + alpha_trms + |> map fastype_of + |> map domain_type + val (arg_names1, (arg_names2, ctxt')) = + ctxt + |> Variable.variant_fixes (replicate (length arg_tys) "x") + ||> Variable.variant_fixes (replicate (length arg_tys) "y") + val args1 = map Free (arg_names1 ~~ arg_tys) + val args2 = map Free (arg_names2 ~~ arg_tys) + val goal = HOLogic.mk_Trueprop + (foldr1 HOLogic.mk_conj (map2 prep_trans_goal alpha_trms (args1 ~~ args2 ~~ arg_tys))) +in + Goal.prove ctxt' [] [] goal + (fn {context,...} => + prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_induct alpha_cases context) + |> singleton (ProofContext.export ctxt' ctxt) + |> Datatype_Aux.split_conj_thm +end + +end (* structure *) + diff -r 231a20534950 -r ad03df7e8056 Nominal/nominal_dt_rawfuns.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Mon Jun 07 11:46:26 2010 +0200 @@ -0,0 +1,295 @@ +(* Title: nominal_dt_rawfuns.ML + Author: Cezary Kaliszyk + Author: Christian Urban + + Definitions of the raw fv and fv_bn functions +*) + +signature NOMINAL_DT_RAWFUNS = +sig + (* info of binding functions *) + type bn_info = (term * int * (int * term option) list list) list + + (* binding modes and binding clauses *) + datatype bmode = Lst | Res | Set + datatype bclause = BC of bmode * (term option * int) list * int list + + val is_atom: Proof.context -> typ -> bool + val is_atom_set: Proof.context -> typ -> bool + val is_atom_fset: Proof.context -> typ -> bool + val is_atom_list: Proof.context -> typ -> bool + val mk_atom_set: term -> term + val mk_atom_fset: term -> term + + val setify: Proof.context -> term -> term + val listify: Proof.context -> term -> term + + val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> + bclause list list list -> thm list -> Proof.context -> + term list * term list * thm list * thm list * local_theory + + val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list +end + + +structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = +struct + +type bn_info = (term * int * (int * term option) list list) list + +datatype bmode = Lst | Res | Set +datatype bclause = BC of bmode * (term option * int) list * int list + +(* testing for concrete atom types *) +fun is_atom ctxt ty = + Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) + +fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t + | is_atom_set _ _ = false; + +fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t + | is_atom_fset _ _ = false; + +fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t + | is_atom_list _ _ = false + + +(* functions for producing sets, fsets and lists of general atom type + out from concrete atom types *) +fun mk_atom_set t = +let + val ty = fastype_of t; + val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; + val img_ty = atom_ty --> ty --> @{typ "atom set"}; +in + Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t +end + +fun mk_atom_fset t = +let + val ty = fastype_of t; + val atom_ty = dest_fsetT ty --> @{typ "atom"}; + val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; + val fset_to_set = @{term "fset_to_set :: atom fset => atom set"} +in + fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) +end + +fun mk_atom_list t = +let + val ty = fastype_of t; + val atom_ty = dest_listT ty --> @{typ atom}; + val map_ty = atom_ty --> ty --> @{typ "atom list"}; +in + Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t +end + +(* functions that coerces singletons, sets and fsets of concrete atoms + into sets of general atoms *) +fun setify ctxt t = +let + val ty = fastype_of t; +in + if is_atom ctxt ty + then HOLogic.mk_set @{typ atom} [mk_atom t] + else if is_atom_set ctxt ty + then mk_atom_set t + else if is_atom_fset ctxt ty + then mk_atom_fset t + else raise TERM ("setify", [t]) +end + +(* functions that coerces singletons and lists of concrete atoms + into lists of general atoms *) +fun listify ctxt t = +let + val ty = fastype_of t; +in + if is_atom ctxt ty + then HOLogic.mk_list @{typ atom} [mk_atom t] + else if is_atom_list ctxt ty + then mk_atom_set t + else raise TERM ("listify", [t]) +end + +(* coerces a list into a set *) +fun to_set t = + if fastype_of t = @{typ "atom list"} + then @{term "set::atom list => atom set"} $ t + else t + + +(** functions that construct the equations for fv and fv_bn **) + +fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = +let + fun mk_fv_body fv_map args i = + let + val arg = nth args i + val ty = fastype_of arg + in + case AList.lookup (op=) fv_map ty of + NONE => mk_supp arg + | SOME fv => fv $ arg + end + + fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = + let + val arg = nth args i + in + case bn_option of + NONE => (setify lthy arg, @{term "{}::atom set"}) + | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) + end + + val t1 = map (mk_fv_body fv_map args) bodies + val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) +in + fold_union (mk_diff (fold_union t1, fold_union t2)::t3) +end + +(* in case of fv_bn we have to treat the case special, where an + "empty" binding clause is given *) +fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = +let + fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = + let + val arg = nth args i + val ty = fastype_of arg + in + case AList.lookup (op=) bn_args i of + NONE => (case (AList.lookup (op=) fv_map ty) of + NONE => mk_supp arg + | SOME fv => fv $ arg) + | SOME (NONE) => @{term "{}::atom set"} + | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg + end +in + case bclause of + BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) + | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause +end + +fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = +let + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv = the (AList.lookup (op=) fv_map ty) + val lhs = fv $ list_comb (constr, args) + val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses + val rhs = fold_union rhs_trms +in + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) +end + +fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses = +let + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) + val lhs = fv_bn $ list_comb (constr, args) + val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses + val rhs = fold_union rhs_trms +in + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) +end + +fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = +let + val nth_constrs_info = nth constrs_info bn_n + val nth_bclausess = nth bclausesss bn_n +in + map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess +end + +fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy = +let + val fv_names = prefix_dt_names descr sorts "fv_" + val fv_arg_tys = all_dtyps descr sorts + val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; + val fv_frees = map Free (fv_names ~~ fv_tys); + val fv_map = fv_arg_tys ~~ fv_frees + + val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) + val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns + val fv_bn_names = map (prefix "fv_") bn_names + val fv_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys + val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys + val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) + val fv_bn_map = bns ~~ fv_bn_frees + + val constrs_info = all_dtyp_constrs_types descr sorts + + val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss + val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info + + val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) + val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) + + val (_, lthy') = Function.add_function all_fun_names all_fun_eqs + Function_Common.default_config (pat_completeness_simp constr_thms) lthy + + val (info, lthy'') = prove_termination (Local_Theory.restore lthy') + + val {fs, simps, inducts, ...} = info; + + val morphism = ProofContext.export_morphism lthy'' lthy + val fs_exp = map (Morphism.term morphism) fs + + val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp + val simps_exp = map (Morphism.thm morphism) (the simps) + val fv_bns_inducts_exp = map (Morphism.thm morphism) (the inducts) +in + (fv_frees_exp, fv_bns_exp, simps_exp, fv_bns_inducts_exp, lthy'') +end + + +(** equivarance proofs **) + +val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} + +fun subproof_tac const_names simps = + Subgoal.FOCUS (fn {prems, context, ...} => + HEADGOAL + (simp_tac (HOL_basic_ss addsimps simps) + THEN' Nominal_Permeq.eqvt_tac context [] const_names + THEN' simp_tac (HOL_basic_ss addsimps (eqvt_apply_sym :: prems)))) + +fun prove_eqvt_tac insts ind_thms const_names simps ctxt = + HEADGOAL + (Object_Logic.full_atomize_tac + THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) + THEN_ALL_NEW subproof_tac const_names simps ctxt) + +fun mk_eqvt_goal pi const arg = +let + val lhs = mk_perm pi (const $ arg) + val rhs = const $ (mk_perm pi arg) +in + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) +end + +fun raw_prove_eqvt consts ind_thms simps ctxt = + if null consts then [] + else + let + val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt + val p = Free (p, @{typ perm}) + val arg_tys = + consts + |> map fastype_of + |> map domain_type + val (arg_names, ctxt'') = + Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt' + val args = map Free (arg_names ~~ arg_tys) + val goals = map2 (mk_eqvt_goal p) consts args + val insts = map (single o SOME) arg_names + val const_names = map (fst o dest_Const) consts + in + Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => + prove_eqvt_tac insts ind_thms const_names simps context) + |> ProofContext.export ctxt'' ctxt + end + +end (* structure *) + diff -r 231a20534950 -r ad03df7e8056 Nominal/nominal_dt_rawperm.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_rawperm.ML Mon Jun 07 11:46:26 2010 +0200 @@ -0,0 +1,149 @@ +(* Title: nominal_dt_rawperm.ML + Author: Cezary Kaliszyk + Author: Christian Urban + + Definitions of the raw permutations and + proof that the raw datatypes are in the + pt-class. +*) + +signature NOMINAL_DT_RAWPERM = +sig + val define_raw_perms: Datatype.descr -> (string * sort) list -> thm -> int -> theory -> + (term list * thm list * thm list) * theory +end + + +structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM = +struct + + +(* permutation function for one argument + + - in case the argument is recursive it returns + + permute_fn p arg + + - in case the argument is non-recursive it will return + + p o arg +*) +fun perm_arg permute_fn_frees p (arg_dty, arg) = + if Datatype_Aux.is_rec_type arg_dty + then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg + else mk_perm p arg + + +(* generates the equation for the permutation function for one constructor; + i is the index of the corresponding datatype *) +fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) = +let + val p = Free ("p", @{typ perm}) + val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts + val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) + val args = map Free (arg_names ~~ arg_tys) + val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) + val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args) + val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args)) + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) +in + (Attrib.empty_binding, eq) +end + + +(** proves the two pt-type class properties **) + +fun prove_permute_zero lthy induct perm_defs perm_fns = +let + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = Datatype_Prop.make_tnames perm_types + + fun single_goal ((perm_fn, T), x) = + HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) + + val goals = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) + + val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) + + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 +in + Goal.prove lthy perm_indnames [] goals (K tac) + |> Datatype_Aux.split_conj_thm +end + + +fun prove_permute_plus lthy induct perm_defs perm_fns = +let + val p = Free ("p", @{typ perm}) + val q = Free ("q", @{typ perm}) + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = Datatype_Prop.make_tnames perm_types + + fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq + (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) + + val goals = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) + + val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) + + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 +in + Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) + |> Datatype_Aux.split_conj_thm +end + + +(* user_dt_nos refers to the number of "un-unfolded" datatypes + given by the user +*) +fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy = +let + val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; + val user_full_tnames = List.take (all_full_tnames, user_dt_nos); + + val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" + val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr + val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) + + fun perm_eq (i, (_, _, constrs)) = + map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; + + val perm_eqs = maps perm_eq dt_descr; + + val lthy = + Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; + + val ((perm_funs, perm_eq_thms), lthy') = + Primrec.add_primrec + (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; + + val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs + val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs + val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); + val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) + val perms_name = space_implode "_" perm_fn_names + val perms_zero_bind = Binding.name (perms_name ^ "_zero") + val perms_plus_bind = Binding.name (perms_name ^ "_plus") + + fun tac _ (_, _, simps) = + Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) + + fun morphism phi (fvs, dfs, simps) = + (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); +in + lthy' + |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) + |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) + |> Class_Target.prove_instantiation_exit_result morphism tac + (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') +end + + +end (* structure *) + diff -r 231a20534950 -r ad03df7e8056 Slides/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/ROOT.ML Mon Jun 07 11:46:26 2010 +0200 @@ -0,0 +1,6 @@ +show_question_marks := false; +quick_and_dirty := true; + +no_document use_thy "LaTeXsugar"; + +use_thy "Slides1" \ No newline at end of file diff -r 231a20534950 -r ad03df7e8056 Slides/Slides1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/Slides1.thy Mon Jun 07 11:46:26 2010 +0200 @@ -0,0 +1,1080 @@ +(*<*) +theory Slides1 +imports "LaTeXsugar" "Nominal" +begin + +notation (latex output) + set ("_") and + Cons ("_::/_" [66,65] 65) + +(*>*) + + +text_raw {* + \renewcommand{\slidecaption}{Cambridge, 8.~June 2010} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1>[t] + \frametitle{% + \begin{tabular}{@ {\hspace{-3mm}}c@ {}} + \\ + \huge Nominal 2\\[-2mm] + \large Or, How to Reason Conveniently with\\[-5mm] + \large General Bindings in Isabelle/HOL\\[5mm] + \end{tabular}} + \begin{center} + Christian Urban + \end{center} + \begin{center} + joint work with {\bf Cezary Kaliszyk}\\[0mm] + \end{center} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2> + \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}} + \mbox{}\\[-6mm] + + \begin{itemize} + \item the old Nominal Isabelle provided a reasoning infrastructure for single binders\medskip + + \begin{center} + Lam [a].(Var a) + \end{center}\bigskip + + \item<2-> but representing + + \begin{center} + $\forall\{a_1,\ldots,a_n\}.\; T$ + \end{center}\medskip + + with single binders and reasoning about it is a \alert{\bf major} pain; + take my word for it! + \end{itemize} + + \only<1>{ + \begin{textblock}{6}(1.5,11) + \small + for example\\ + \begin{tabular}{l@ {\hspace{2mm}}l} + \pgfuseshading{smallspherered} & a $\fresh$ Lam [a]. t\\ + \pgfuseshading{smallspherered} & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\ + \pgfuseshading{smallspherered} & Barendregt-style reasoning about bound variables\\ + \end{tabular} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-4> + \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item binding sets of names has some interesting properties:\medskip + + \begin{center} + \begin{tabular}{l} + $\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$ + \bigskip\smallskip\\ + + \onslide<2->{% + $\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$ + }\bigskip\smallskip\\ + + \onslide<3->{% + $\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$ + }\medskip\\ + \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type} + \end{tabular} + \end{center} + \end{itemize} + + \begin{textblock}{8}(2,14.5) + \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct + \end{textblock} + + \only<4>{ + \begin{textblock}{6}(2.5,4) + \begin{tikzpicture} + \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\normalsize\color{darkgray} + \begin{minipage}{8cm}\raggedright + For type-schemes the order of bound names does not matter, and + alpha-equivalence is preserved under \alert{vacuous} binders. + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-3> + \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item alpha-equivalence being preserved under vacuous binders is \underline{not} always + wanted:\bigskip\bigskip\normalsize + + \begin{tabular}{@ {\hspace{-8mm}}l} + $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\ + \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}} + \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and} + \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$} + \end{tabular} + + + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}\LARGE{}Even Another Binding Mode\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip + + \begin{center} + \begin{tabular}{@ {\hspace{-8mm}}l} + $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\ + $\;\;\;\not\approx_\alpha + \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$ + \end{tabular} + \end{center} + + + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2> + \frametitle{\begin{tabular}{c}\LARGE{}Three Binding Modes\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item the order does not matter and alpha-equivelence is preserved under + vacuous binders \textcolor{gray}{(restriction)}\medskip + + \item the order does not matter, but the cardinality of the binders + must be the same \textcolor{gray}{(abstraction)}\medskip + + \item the order does matter + \end{itemize} + + \onslide<2->{ + \begin{center} + \isacommand{bind\_res}\hspace{6mm} + \isacommand{bind\_set}\hspace{6mm} + \isacommand{bind} + \end{center}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-3> + \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}} + \mbox{}\\[-6mm] + + \mbox{}\hspace{10mm} + \begin{tabular}{ll} + \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ + \hspace{5mm}\phantom{$|$} Var name\\ + \hspace{5mm}$|$ App trm trm\\ + \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm + & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\ + \hspace{5mm}$|$ Let \only<2->{as::}assn \only<2->{t::}trm + & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\ + \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ + \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ + \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ + \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\ + \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\ + \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\ + \end{tabular} + + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-5> + \frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item this way of specifying binding is inspired by + {\bf Ott}\onslide<2->{, \alert{\bf but} we made some adjustments:}\medskip + + + \only<2>{ + \begin{itemize} + \item Ott allows specifications like\smallskip + \begin{center} + $t ::= t\;t\; |\;\lambda x.t$ + \end{center} + \end{itemize}} + + \only<3-4>{ + \begin{itemize} + \item whether something is bound can depend in Ott on other bound things\smallskip + \begin{center} + \begin{tikzpicture} + \node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$}; + \node (B) at ( 1.1,1) {$s$}; + \onslide<4>{\node (C) at (0.5,0) {$\{y, x\}$};} + \onslide<4>{\draw[->,red,line width=1mm] (A) -- (C);} + \onslide<4>{\draw[->,red,line width=1mm] (C) -- (B);} + \end{tikzpicture} + \end{center} + \onslide<4>{this might make sense for ``raw'' terms, but not at all + for $\alpha$-equated terms} + \end{itemize}} + + \only<5>{ + \begin{itemize} + \item we allow multiple ``binders'' and ``bodies''\smallskip + \begin{center} + \isacommand{bind} a b c \isacommand{in} x y z + \end{center}\bigskip\medskip + the reason is that with our definitions of $\alpha$-equivalence + \begin{center} + \begin{tabular}{rcl} + \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ & + \begin{tabular}{@ {}l} + \isacommand{bind\_res} as \isacommand{in} x,\\ + \isacommand{bind\_res} as \isacommand{in} y + \end{tabular} + \end{tabular} + \end{center}\smallskip + + same with \isacommand{bind\_set} + \end{itemize}} + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item in the old Nominal Isabelle, we represented single binders as partial functions:\bigskip + + \begin{center} + \begin{tabular}{l} + Lam [$a$].\,$t$ $\;{^\text{``}}\!\dn{}\!^{\text{''}}$\\[2mm] + \;\;\;\;$\lambda b.$\;$\text{if}\;a = b\;\text{then}\;t\;\text{else}$\\ + \phantom{\;\;\;\;$\lambda b.$\;\;\;\;\;\;}$\text{if}\;b \fresh t\; + \text{then}\;(a\;b)\act t\;\text{else}\;\text{error}$ + \end{tabular} + \end{center} + \end{itemize} + + \begin{textblock}{10}(2,14) + \footnotesize $^*$ alpha-equality coincides with equality on functions + \end{textblock} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}New Design\end{tabular}} + \mbox{}\\[4mm] + + \begin{center} + \begin{tikzpicture} + \alt<2> + {\draw (0,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] + (A) {\textcolor{red}{\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}}};} + {\draw (0,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] + (A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};} + + \alt<3> + {\draw (3,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] + (B) {\textcolor{red}{\begin{minipage}{1.1cm}raw\\terms\end{minipage}}};} + {\draw (3,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] + (B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};} + + \alt<4> + {\draw (6,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] + (C) {\textcolor{red}{\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}}};} + {\draw (6,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] + (C) {\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}};} + + \alt<5> + {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] + (D) {\textcolor{red}{\begin{minipage}{1.1cm}quot.\\type\end{minipage}}};} + {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] + (D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};} + + \alt<6> + {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] + (E) {\textcolor{red}{\begin{minipage}{1.1cm}lift\\thms\end{minipage}}};} + {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] + (E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};} + + \alt<7> + {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] + (F) {\textcolor{red}{\begin{minipage}{1.1cm}add.\\thms\end{minipage}}};} + {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] + (F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};} + + \draw[->,white!50,line width=1mm] (A) -- (B); + \draw[->,white!50,line width=1mm] (B) -- (C); + \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] + (C) -- (8,0) -- (8,-1.5) -- (-2,-1.5) -- (-2,-3) -- (D); + \draw[->,white!50,line width=1mm] (D) -- (E); + \draw[->,white!50,line width=1mm] (E) -- (F); + \end{tikzpicture} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-9> + \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item lets first look at pairs\bigskip\medskip + + \begin{tabular}{@ {\hspace{1cm}}l} + $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-7>{${}_{\text{set}}$}% + \only<8>{${}_{\text{\alert{list}}}$}% + \only<9>{${}_{\text{\alert{res}}}$}}% + \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$ + \end{tabular}\bigskip + \end{itemize} + + \only<1>{ + \begin{textblock}{8}(3,8.5) + \begin{tabular}{l@ {\hspace{2mm}}p{8cm}} + \pgfuseshading{smallspherered} & $as$ is a set of names\ldots the binders\\ + \pgfuseshading{smallspherered} & $x$ is the body\\ + \pgfuseshading{smallspherered} & $\approx_{\text{set}}$ is where the cardinality + of the binders has to be the same\\ + \end{tabular} + \end{textblock}} + + \only<4->{ + \begin{textblock}{12}(5,8) + \begin{tabular}{ll@ {\hspace{1mm}}l} + $\dn$ & \onslide<5->{$\exists \pi.\,$} & $\text{fv}(x) - as = \text{fv}(y) - bs$\\[1mm] + & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$\text{fv}(x) - as \fresh^* \pi$}\\[1mm] + & \onslide<6->{$\;\;\;\wedge$} & \onslide<6->{$(\pi \act x)\;R\;y$}\\[1mm] + & \onslide<7-8>{$\;\;\;\wedge$} & \onslide<7-8>{$\pi \act as = bs$}\\ + \end{tabular} + \end{textblock}} + + \only<8>{ + \begin{textblock}{8}(3,13.8) + \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names + \end{textblock}} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-3> + \frametitle{\begin{tabular}{c}Examples\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item lets look at ``type-schemes'':\medskip\medskip + + \begin{center} + $(as, x) \approx\!\makebox[0mm][l]{${}_{\text{set}}$}\only<1>{{}^{R,\text{fv}}}\only<2->{{}^{\alert{=},\alert{\text{fv}}}} (bs, y)$ + \end{center}\medskip + + \onslide<2->{ + \begin{center} + \begin{tabular}{l} + $\text{fv}(x) = \{x\}$\\[1mm] + $\text{fv}(T_1 \rightarrow T_2) = \text{fv}(T_1) \cup \text{fv}(T_2)$\\ + \end{tabular} + \end{center}} + \end{itemize} + + + \only<3->{ + \begin{textblock}{4}(0.3,12) + \begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\tiny\color{darkgray} + \begin{minipage}{3.4cm}\raggedright + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {}l}{res:}\\ + $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ + $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \cdot x = y$\\ + \\ + \end{tabular} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + \only<3->{ + \begin{textblock}{4}(5.2,12) + \begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\tiny\color{darkgray} + \begin{minipage}{3.4cm}\raggedright + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {}l}{set:}\\ + $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ + $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \cdot x = y$\\ + $\wedge$ & $\pi \cdot as = bs$\\ + \end{tabular} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + \only<3->{ + \begin{textblock}{4}(10.2,12) + \begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\tiny\color{darkgray} + \begin{minipage}{3.4cm}\raggedright + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {}l}{list:}\\ + $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ + $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \cdot x = y$\\ + $\wedge$ & $\pi \cdot as = bs$\\ + \end{tabular} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2> + \frametitle{\begin{tabular}{c}Examples\end{tabular}} + \mbox{}\\[-3mm] + + \begin{center} + \only<1>{$(\{x, y\}, x \rightarrow y) \approx_? (\{x, y\}, y \rightarrow x)$} + \only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$} + \end{center} + + \begin{itemize} + \item $\approx_{\text{res}}$, $\approx_{\text{set}}$% + \only<2>{, \alert{$\not\approx_{\text{list}}$}} + \end{itemize} + + + \only<1->{ + \begin{textblock}{4}(0.3,12) + \begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\tiny\color{darkgray} + \begin{minipage}{3.4cm}\raggedright + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {}l}{res:}\\ + $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ + $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \cdot x = y$\\ + \\ + \end{tabular} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + \only<1->{ + \begin{textblock}{4}(5.2,12) + \begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\tiny\color{darkgray} + \begin{minipage}{3.4cm}\raggedright + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {}l}{set:}\\ + $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ + $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \cdot x = y$\\ + $\wedge$ & $\pi \cdot as = bs$\\ + \end{tabular} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + \only<1->{ + \begin{textblock}{4}(10.2,12) + \begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\tiny\color{darkgray} + \begin{minipage}{3.4cm}\raggedright + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {}l}{list:}\\ + $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ + $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \cdot x = y$\\ + $\wedge$ & $\pi \cdot as = bs$\\ + \end{tabular} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2> + \frametitle{\begin{tabular}{c}Examples\end{tabular}} + \mbox{}\\[-3mm] + + \begin{center} + \only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$} + \end{center} + + \begin{itemize} + \item $\approx_{\text{res}}$, $\not\approx_{\text{set}}$, + $\not\approx_{\text{list}}$ + \end{itemize} + + + \only<1->{ + \begin{textblock}{4}(0.3,12) + \begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\tiny\color{darkgray} + \begin{minipage}{3.4cm}\raggedright + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {}l}{res:}\\ + $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ + $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \cdot x = y$\\ + \\ + \end{tabular} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + \only<1->{ + \begin{textblock}{4}(5.2,12) + \begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\tiny\color{darkgray} + \begin{minipage}{3.4cm}\raggedright + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {}l}{set:}\\ + $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ + $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \cdot x = y$\\ + $\wedge$ & $\pi \cdot as = bs$\\ + \end{tabular} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + \only<1->{ + \begin{textblock}{4}(10.2,12) + \begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\tiny\color{darkgray} + \begin{minipage}{3.4cm}\raggedright + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {}l}{list:}\\ + $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ + $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \cdot x = y$\\ + $\wedge$ & $\pi \cdot as = bs$\\ + \end{tabular} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + + \only<2>{ + \begin{textblock}{6}(2.5,4) + \begin{tikzpicture} + \draw (0,0) node[inner sep=5mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\normalsize + \begin{minipage}{8cm}\raggedright + \begin{itemize} + \item \color{darkgray}$\alpha$-equivalences coincide when a single name is + abstracted + \item \color{darkgray}in that case they are equivalent to ``old-fashioned'' definitions of $\alpha$ + \end{itemize} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-3> + \frametitle{\begin{tabular}{c}General Abstractions\end{tabular}} + \mbox{}\\[-7mm] + + \begin{itemize} + \item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{{}*{}}$}^{=,\text{supp}} (bs, y)$\medskip + \item they are equivalence relations\medskip + \item we can therefore use the quotient package to introduce the + types $\beta\;\text{abs}_*$\bigskip + \begin{center} + \only<1>{$[as].\,x$} + \only<2>{$\text{supp}([as].x) = \text{supp}(x) - as$} + \only<3>{% + \begin{tabular}{r@ {\hspace{1mm}}l} + \multicolumn{2}{@ {\hspace{-7mm}}l}{$[as]. x \alert{=} [bs].y\;\;\;\text{if\!f}$}\\[2mm] + $\exists \pi.$ & $\text{supp}(x) - as = \text{supp}(y) - bs$\\ + $\wedge$ & $\text{supp}(x) - as \fresh^* \pi$\\ + $\wedge$ & $\pi \act x = y $\\ + $(\wedge$ & $\pi \act as = bs)\;^*$\\ + \end{tabular}} + \end{center} + \end{itemize} + + \only<1->{ + \begin{textblock}{8}(12,3.8) + \footnotesize $^*$ set, res, list + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}A Problem\end{tabular}} + \mbox{}\\[-3mm] + + \begin{center} + $\text{let}\;x_1=t_1 \ldots x_n=t_n\;\text{in}\;s$ + \end{center} + + \begin{itemize} + \item we cannot represent this as\medskip + \begin{center} + $\text{let}\;[x_1,\ldots,x_n]\alert{.}s\;\;[t_1,\ldots,t_n]$ + \end{center}\bigskip + + because\medskip + \begin{center} + $\text{let}\;[x].s\;\;[t_1,t_2]$ + \end{center} + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}Our Specifications\end{tabular}} + \mbox{}\\[-6mm] + + \mbox{}\hspace{10mm} + \begin{tabular}{ll} + \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ + \hspace{5mm}\phantom{$|$} Var name\\ + \hspace{5mm}$|$ App trm trm\\ + \hspace{5mm}$|$ Lam x::name t::trm + & \isacommand{bind} x \isacommand{in} t\\ + \hspace{5mm}$|$ Let as::assn t::trm + & \isacommand{bind} bn(as) \isacommand{in} t\\ + \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ + \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ + \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ + \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\ + \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ + \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ + \end{tabular} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2> + \frametitle{\begin{tabular}{c}``Raw'' Definitions\end{tabular}} + \mbox{}\\[-6mm] + + \mbox{}\hspace{10mm} + \begin{tabular}{ll} + \multicolumn{2}{l}{\isacommand{datatype} trm $=$}\\ + \hspace{5mm}\phantom{$|$} Var name\\ + \hspace{5mm}$|$ App trm trm\\ + \hspace{5mm}$|$ Lam name trm\\ + \hspace{5mm}$|$ Let assn trm\\ + \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ + \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ + \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\[5mm] + \multicolumn{2}{l}{\isacommand{function} bn \isacommand{where}}\\ + \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ + \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ + \end{tabular} + + \only<2>{ + \begin{textblock}{5}(10,5) + $+$ \begin{tabular}{l}automatically\\ + generate fv's\end{tabular} + \end{textblock}} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} + \mbox{}\\[6mm] + + \begin{center} + Lam x::name t::trm \hspace{10mm}\isacommand{bind} x \isacommand{in} t\\ + \end{center} + + + \[ + \infer[\text{Lam-}\!\approx_\alpha] + {\text{Lam}\;x\;t \approx_\alpha \text{Lam}\;x'\;t'} + {([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} + ^{\approx_\alpha,\text{fv}} ([x'], t')} + \] + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} + \mbox{}\\[6mm] + + \begin{center} + Lam x::name y::name t::trm s::trm \hspace{5mm}\isacommand{bind} x y \isacommand{in} t s\\ + \end{center} + + + \[ + \infer[\text{Lam-}\!\approx_\alpha] + {\text{Lam}\;x\;y\;t\;s \approx_\alpha \text{Lam}\;x'\;y'\;t'\;s'} + {([x, y], (t, s)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} + ^{R, fv} ([x', y'], (t', s'))} + \] + + \footnotesize + where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\cup\text{fv}$ + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2> + \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} + \mbox{}\\[6mm] + + \begin{center} + Let as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t\\ + \end{center} + + + \[ + \infer[\text{Let-}\!\approx_\alpha] + {\text{Let}\;as\;t \approx_\alpha \text{Let}\;as'\;t'} + {(\text{bn}(as), t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} + ^{\approx_\alpha,\text{fv}} (\text{bn}(as'), t') & + \onslide<2->{as \approx_\alpha^{\text{bn}} as'}} + \]\bigskip + + + \onslide<1->{\small{}bn-function $\Rightarrow$ \alert{deep binders}} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}\LARGE{}$\alpha$ for Binding Functions\end{tabular}} + \mbox{}\\[-6mm] + + \mbox{}\hspace{10mm} + \begin{tabular}{l} + \ldots\\ + \isacommand{binder} bn \isacommand{where}\\ + \phantom{$|$} bn(ANil) $=$ $[]$\\ + $|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)\\ + \end{tabular}\bigskip + + \begin{center} + \mbox{\infer{\text{ANil} \approx_\alpha^{\text{bn}} \text{ANil}}{}}\bigskip + + \mbox{\infer{\text{ACons}\;a\;t\;as \approx_\alpha^{\text{bn}} \text{ACons}\;a'\;t'\;as'} + {t \approx_\alpha t' & as \approx_\alpha^{bn} as'}} + \end{center} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} + \mbox{}\\[6mm] + + \begin{center} + LetRec as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t \alert{as}\\ + \end{center} + + + \[\mbox{}\hspace{-4mm} + \infer[\text{LetRec-}\!\approx_\alpha] + {\text{LetRec}\;as\;t \approx_\alpha \text{LetRec}\;as'\;t'} + {(\text{bn}(as), (t, as)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} + ^{R,fv} (\text{bn}(as'), (t', as'))} + \]\bigskip + + \onslide<1->{\alert{deep recursive binders}} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}Restrictions\end{tabular}} + \mbox{}\\[-6mm] + + Our restrictions on binding specifications: + + \begin{itemize} + \item a body can only occur once in a list of binding clauses\medskip + \item you can only have one binding function for a deep binder\medskip + \item binding functions can return: the empty set, singletons, unions (similarly for lists) + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}Automatic Proofs\end{tabular}} + \mbox{}\\[-6mm] + + \begin{itemize} + \item we can show that $\alpha$'s are equivalence relations\medskip + \item as a result we can use our quotient package to introduce the type(s) + of $\alpha$-equated terms + + \[ + \infer + {\text{Lam}\;x\;t \alert{=} \text{Lam}\;x'\;t'} + {\only<1>{([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} + ^{=,\text{supp}} ([x'], t')}% + \only<2>{[x].t = [x'].t'}} + \] + + + \item the properties for support are implied by the properties of $[\_].\_$ + \item we can derive strong induction principles (almost automatic---matter of time) + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1>[t] + \frametitle{\begin{tabular}{c}Runtime is Acceptable\end{tabular}} + \mbox{}\\[-7mm]\mbox{} + + \footnotesize + \begin{center} + \begin{tikzpicture} + \draw (0,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] + (A) {\begin{minipage}{0.8cm}bind.\\spec.\end{minipage}}; + + \draw (2,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] + (B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}}; + + \draw (4,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] + (C) {\begin{minipage}{0.8cm}$\alpha$-\\equiv.\end{minipage}}; + + \draw (0,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] + (D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}}; + + \draw (2,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] + (E) {\begin{minipage}{0.8cm}lift\\thms\end{minipage}}; + + \draw (4,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] + (F) {\begin{minipage}{0.8cm}add.\\thms\end{minipage}}; + + \draw[->,white!50,line width=1mm] (A) -- (B); + \draw[->,white!50,line width=1mm] (B) -- (C); + \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] + (C) -- (5,0) -- (5,-1) -- (-1,-1) -- (-1,-2) -- (D); + \draw[->,white!50,line width=1mm] (D) -- (E); + \draw[->,white!50,line width=1mm] (E) -- (F); + \end{tikzpicture} + \end{center} + + \begin{itemize} + \item Core Haskell: 11 types, 49 term-constructors, 7 binding functions + \begin{center} + $\sim$ 1 min + \end{center} + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}Interesting Phenomenon\end{tabular}} + \mbox{}\\[-6mm] + + \small + \mbox{}\hspace{10mm} + \begin{tabular}{ll} + \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ + \hspace{5mm}\phantom{$|$} Var name\\ + \hspace{5mm}$|$ App trm trm\\ + \hspace{5mm}$|$ Lam x::name t::trm + & \isacommand{bind} x \isacommand{in} t\\ + \hspace{5mm}$|$ Let as::assn t::trm + & \isacommand{bind} bn(as) \isacommand{in} t\\ + \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ + \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ + \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ + \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\ + \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ + \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ + \end{tabular}\bigskip\medskip + + we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}Conclusion\end{tabular}} + \mbox{}\\[-6mm] + + \begin{itemize} + \item the user does not see anything of the raw level\medskip + \only<1>{\begin{center} + Lam a (Var a) \alert{$=$} Lam b (Var b) + \end{center}\bigskip} + + \item<2-> we have not yet done function definitions (will come soon and + we hope to make improvements over the old way there too)\medskip + \item<3-> it took quite some time to get here, but it seems worthwhile + (Barendregt's variable convention is unsound in general, + found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1->[c] + \frametitle{\begin{tabular}{c}Questions?\end{tabular}} + \mbox{}\\[-6mm] + + \begin{center} + \alert{\huge{Thanks!}} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +(*<*) +end +(*>*) \ No newline at end of file diff -r 231a20534950 -r ad03df7e8056 Slides/document/root.beamer.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/document/root.beamer.tex Mon Jun 07 11:46:26 2010 +0200 @@ -0,0 +1,12 @@ +\documentclass[14pt,t]{beamer} +%%%\usepackage{pstricks} + +\input{root.tex} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% TeX-command-default: "Slides" +%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f")) +%%% End: + diff -r 231a20534950 -r ad03df7e8056 Slides/document/root.notes.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/document/root.notes.tex Mon Jun 07 11:46:26 2010 +0200 @@ -0,0 +1,18 @@ +\documentclass[11pt]{article} +%%\usepackage{pstricks} +\usepackage{dina4} +\usepackage{beamerarticle} +\usepackage{times} +\usepackage{hyperref} +\usepackage{pgf} +\usepackage{amssymb} +\setjobnamebeamerversion{root.beamer} +\input{root.tex} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% TeX-command-default: "Slides" +%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f")) +%%% End: + diff -r 231a20534950 -r ad03df7e8056 Slides/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/document/root.tex Mon Jun 07 11:46:26 2010 +0200 @@ -0,0 +1,156 @@ +\usepackage{beamerthemeplaincu} +\usepackage[T1]{fontenc} +\usepackage{proof} +\usepackage{german} +\usepackage[latin1]{inputenc} +\usepackage{isabelle} +\usepackage{isabellesym} +\usepackage{mathpartir} +\usepackage[absolute,overlay]{textpos} +\usepackage{proof} +\usepackage{ifthen} +\usepackage{animate} +\usepackage{tikz} +\usepackage{pgf} +\usepackage{calc} +%%%\usepackage{ulem} +%%%\newcommand{\uline}[1]{} +\usetikzlibrary{arrows} +\usetikzlibrary{automata} +\usetikzlibrary{shapes} +\usetikzlibrary{shadows} +%%%\usetikzlibrary{mindmap} + +\usepackage{graphicx} +\usepackage{xcolor} + +% general math stuff +\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions +\newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}} +\renewcommand{\emptyset}{\varnothing}% nice round empty set +\renewcommand{\Gamma}{\varGamma} +\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}} +\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}} +\newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}} +\newcommand{\fresh}{\mathrel{\#}} +\newcommand{\act}{{\raisebox{-0.5mm}{\Large$\boldsymbol{\cdot}$}}}% swapping action +\newcommand{\swap}[2]{(#1\,#2)}% swapping operation + + + +% Isabelle configuration +%%\urlstyle{rm} +\isabellestyle{rm} +\renewcommand{\isastyle}{\rm}% +\renewcommand{\isastyleminor}{\rm}% +\renewcommand{\isastylescript}{\footnotesize\rm\slshape}% +\renewcommand{\isatagproof}{} +\renewcommand{\endisatagproof}{} +\renewcommand{\isamarkupcmt}[1]{#1} + +% Isabelle characters +\renewcommand{\isacharunderscore}{\_} +\renewcommand{\isacharbar}{\isamath{\mid}} +\renewcommand{\isasymiota}{} +\renewcommand{\isacharbraceleft}{\{} +\renewcommand{\isacharbraceright}{\}} +\renewcommand{\isacharless}{$\langle$} +\renewcommand{\isachargreater}{$\rangle$} +\renewcommand{\isasymsharp}{\isamath{\#}} +\renewcommand{\isasymdots}{\isamath{...}} +\renewcommand{\isasymbullet}{\act} +\renewcommand{\isasymequiv}{$\dn$} + +% mathpatir +\mprset{sep=1em} + + +% beamer stuff +\renewcommand{\slidecaption}{Salvador, 26.~August 2008} + + +% colours for Isar Code (in article mode everything is black and white) +\mode{ +\definecolor{isacol:brown}{rgb}{.823,.411,.117} +\definecolor{isacol:lightblue}{rgb}{.274,.509,.705} +\definecolor{isacol:green}{rgb}{0,.51,0.14} +\definecolor{isacol:red}{rgb}{.803,0,0} +\definecolor{isacol:blue}{rgb}{0,0,.803} +\definecolor{isacol:darkred}{rgb}{.545,0,0} +\definecolor{isacol:black}{rgb}{0,0,0}} +\mode
{ +\definecolor{isacol:brown}{rgb}{0,0,0} +\definecolor{isacol:lightblue}{rgb}{0,0,0} +\definecolor{isacol:green}{rgb}{0,0,0} +\definecolor{isacol:red}{rgb}{0,0,0} +\definecolor{isacol:blue}{rgb}{0,0,0} +\definecolor{isacol:darkred}{rgb}{0,0,0} +\definecolor{isacol:black}{rgb}{0,0,0} +} + + +\newcommand{\strong}[1]{{\bfseries {#1}}} +\newcommand{\bluecmd}[1]{{\color{isacol:lightblue}{\strong{#1}}}} +\newcommand{\browncmd}[1]{{\color{isacol:brown}{\strong{#1}}}} +\newcommand{\redcmd}[1]{{\color{isacol:red}{\strong{#1}}}} + +\renewcommand{\isakeyword}[1]{% +\ifthenelse{\equal{#1}{show}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{case}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{assume}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{obtain}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{fix}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{oops}}{\redcmd{#1}}{% +\ifthenelse{\equal{#1}{thm}}{\redcmd{#1}}{% +{\bluecmd{#1}}}}}}}}}}% + +% inner syntax colour +\chardef\isachardoublequoteopen=`\"% +\chardef\isachardoublequoteclose=`\"% +\chardef\isacharbackquoteopen=`\`% +\chardef\isacharbackquoteclose=`\`% +\newenvironment{innersingle}% +{\isacharbackquoteopen\color{isacol:green}}% +{\color{isacol:black}\isacharbackquoteclose} +\newenvironment{innerdouble}% +{\isachardoublequoteopen\color{isacol:green}}% +{\color{isacol:black}\isachardoublequoteclose} + +%% misc +\newcommand{\gb}[1]{\textcolor{isacol:green}{#1}} +\newcommand{\rb}[1]{\textcolor{red}{#1}} + +%% animations +\newcounter{growcnt} +\newcommand{\grow}[2] +{\begin{tikzpicture}[baseline=(n.base)]% + \node[scale=(0.1 *#1 + 0.001),inner sep=0pt] (n) {#2}; + \end{tikzpicture}% +} + +%% isatabbing +%\renewcommand{\isamarkupcmt}[1]% +%{\ifthenelse{\equal{TABSET}{#1}}{\=}% +% {\ifthenelse{\equal{TAB}{#1}}{\>}% +% {\ifthenelse{\equal{NEWLINE}{#1}}{\\}% +% {\ifthenelse{\equal{DOTS}{#1}}{\ldots}{\isastylecmt--- {#1}}}% +% }% +% }% +%}% + + +\newenvironment{isatabbing}% +{\renewcommand{\isanewline}{\\}\begin{tabbing}}% +{\end{tabbing}} + +\begin{document} +\input{session} +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% TeX-command-default: "Slides" +%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f")) +%%% End: +