# HG changeset patch # User Christian Urban # Date 1275399967 -7200 # Node ID 118a0ca16381e87edad5dd3939dbfe2b2ac74ea1 # Parent 86c977b4a9bbcb62249e264598700824d6f45b15# Parent 530b0adbcf77db8561edf106f89295eec7076aa7 merged diff -r 530b0adbcf77 -r 118a0ca16381 IsaMakefile --- a/IsaMakefile Tue Jun 01 15:45:43 2010 +0200 +++ b/IsaMakefile Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal-General/nominal_eqvt.ML Tue Jun 01 15:46:07 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 @@ -147,7 +147,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 +172,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 +183,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 530b0adbcf77 -r 118a0ca16381 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal-General/nominal_library.ML Tue Jun 01 15:46:07 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,43 @@ 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 + + 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 +70,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 +78,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 +87,92 @@ 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 **) +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 + end (* structure *) open Nominal_Library; \ No newline at end of file diff -r 530b0adbcf77 -r 118a0ca16381 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Nominal/Abs.thy --- a/Nominal/Abs.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/Abs.thy Tue Jun 01 15:46:07 2010 +0200 @@ -830,8 +830,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 +846,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 +862,6 @@ unfolding prod_fv.simps by (perm_simp) (rule refl) + end diff -r 530b0adbcf77 -r 118a0ca16381 Nominal/Equivp.thy --- a/Nominal/Equivp.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/Equivp.thy Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Nominal/Ex/Ex2.thy --- a/Nominal/Ex/Ex2.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/Ex/Ex2.thy Tue Jun 01 15:46:07 2010 +0200 @@ -3,6 +3,7 @@ begin text {* example 2 *} +declare [[STEPS = 8]] 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 530b0adbcf77 -r 118a0ca16381 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Tue Jun 01 15:46:07 2010 +0200 @@ -4,11 +4,19 @@ atom_decl name +ML {* Function.add_function *} + +ML {* print_depth 50 *} +declare [[STEPS = 9]] + + nominal_datatype trm = Var "name" | App "trm" "trm" | Lam x::"name" t::"trm" bind_set x in t | Let a::"assg" t::"trm" bind_set "bn a" in t +| Foo x::"name" y::"name" t::"trm" bind_set x in y t +| Bar x::"name" y::"name" t::"trm" bind y x in t x y and assg = As "name" "trm" binder @@ -26,8 +34,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 530b0adbcf77 -r 118a0ca16381 Nominal/Ex/Test.thy --- a/Nominal/Ex/Test.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/Ex/Test.thy Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Nominal/Lift.thy --- a/Nominal/Lift.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/Lift.thy Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Nominal/NewAlpha.thy --- a/Nominal/NewAlpha.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/NewAlpha.thy Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Nominal/NewFv.thy --- a/Nominal/NewFv.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/NewFv.thy Tue Jun 01 15:46:07 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,191 +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) - - 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 @@ -290,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 530b0adbcf77 -r 118a0ca16381 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/NewParser.thy Tue Jun 01 15:46:07 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,20 +190,19 @@ *} 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 (cnstr_head, cnstr_args) = strip_comb cnstr + val rhs_elements = strip_bn_fun lthy cnstr_args rhs val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements in (dt_index, (bn_fun, (cnstr_head, included))) @@ -219,14 +221,16 @@ 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 *} +ML {* rawify_bn_funs *} + ML {* fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = let @@ -254,19 +258,35 @@ 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 = +let + val (_, lthy2) = Function.add_function raw_bn_funs raw_bn_eqs + Function_Common.default_config (pat_completeness_simp constr_thms) lthy + + val (info, lthy3) = prove_termination (Local_Theory.restore lthy2) + 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, lthy3) +end +*} + + lemma equivp_hack: "equivp x" sorry ML {* @@ -286,76 +306,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,26 +321,36 @@ 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 > 1 + 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; + val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy1) = + if get_STEPS lthy0 > 1 + then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy0 + else raise TEST lthy0 + + val bn_nos = map (fn (_, i, _) => i) raw_bn_info; + val bns = raw_bn_funs ~~ bn_nos; + (* definitions of raw permutations *) - val ((perms, raw_perm_defs, raw_perm_simps), lthy2) = + val ((raw_perm_funs, 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 @@ -404,53 +364,76 @@ (* 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) = + val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3a) = if get_STEPS lthy2 > 3 - then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3 + then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3 else raise TEST lthy3 - + (* definition of raw alphas *) - val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = + val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = if get_STEPS lthy > 4 - then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a + then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a else raise TEST lthy3a - val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts - - 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 = + 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 + + val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) + val (_, lthy_tmp) = 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) lthy_tmp + else raise TEST lthy4 + + val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp + - (* 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_eqvt, _) = + if get_STEPS lthy > 8 + then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' + 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; + (* + val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt)) + val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt)) + val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt)) + *) + + val _ = + if get_STEPS lthy > 9 + then true 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 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 +442,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 +492,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 +522,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 +622,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 +653,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 +668,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 +698,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 530b0adbcf77 -r 118a0ca16381 Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/Nominal2_FSet.thy Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Nominal/Perm.thy --- a/Nominal/Perm.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/Perm.thy Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/ROOT.ML Tue Jun 01 15:46:07 2010 +0200 @@ -14,6 +14,6 @@ "Ex/ExPS3", "Ex/ExPS7", "Ex/CoreHaskell", - "Ex/Test", - "Manual/Term4" + "Ex/Test"(*, + "Manual/Term4"*) ]; diff -r 530b0adbcf77 -r 118a0ca16381 Nominal/Tacs.thy --- a/Nominal/Tacs.thy Tue Jun 01 15:45:43 2010 +0200 +++ b/Nominal/Tacs.thy Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Nominal/nominal_dt_alpha.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_alpha.ML Tue Jun 01 15:46:07 2010 +0200 @@ -0,0 +1,327 @@ +(* 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 +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 + +end (* structure *) + diff -r 530b0adbcf77 -r 118a0ca16381 Nominal/nominal_dt_rawfuns.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Tue Jun 01 15:46:07 2010 +0200 @@ -0,0 +1,283 @@ +(* 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 **) + +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 = +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 (replicate (length 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 + fun tac ctxt = + Object_Logic.full_atomize_tac + THEN' InductTacs.induct_rules_tac ctxt insts ind_thms + THEN_ALL_NEW + (asm_full_simp_tac (HOL_basic_ss addsimps simps) + THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names + THEN' asm_simp_tac HOL_basic_ss) +in + Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) + |> ProofContext.export ctxt'' ctxt +end + +end (* structure *) + diff -r 530b0adbcf77 -r 118a0ca16381 Nominal/nominal_dt_rawperm.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_rawperm.ML Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Slides/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/ROOT.ML Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Slides/Slides1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/Slides1.thy Tue Jun 01 15:46:07 2010 +0200 @@ -0,0 +1,1015 @@ +(*<*) +theory Slides1 +imports "LaTeXsugar" "Nominal" +begin + +notation (latex output) + set ("_") and + Cons ("_::/_" [66,65] 65) + +(*>*) + + +text_raw {* + \renewcommand{\slidecaption}{TU Munich, 28.~May 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\\[15mm] + \end{tabular}} + \begin{center} + joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] + \end{center} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2> + \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item sorted atoms and sort-respecting permutations\medskip + + \onslide<2->{ + \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip + + \begin{center} + \begin{tabular}{c@ {\hspace{7mm}}c} + $[]\;\act\;c \dn c$ & + $(a\;b)\!::\!\pi\;\act\;c \dn$ + $\begin{cases} + b & \text{if}\; \pi \act c = a\\ + a & \text{if}\; \pi \act c = b\\ + \pi \act c & \text{otherwise} + \end{cases}$ + \end{tabular} + \end{center}} + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}Problems\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item @{text "_ \ _ :: \ perm \ \ \ \"}\bigskip + + \item @{text "supp _ :: \ \ \ set"} + + \begin{center} + $\text{finite} (\text{supp}\;x)_{\,\alpha_1\,\text{set}}$ \ldots + $\text{finite} (\text{supp}\;x)_{\,\alpha_n\,\text{set}}$ + \end{center}\bigskip + + \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip + + \item type-classes + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-4> + \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}} + \mbox{}\\[-3mm] +*} +datatype atom = Atom string nat + +text_raw {* + \mbox{}\bigskip + \begin{itemize} + \item<2-> permutations are (restricted) bijective functions from @{text "atom \ atom"} + + \begin{itemize} + \item sort-respecting \hspace{5mm}($\forall a.\;\text{sort}(f a) = \text{sort}(a)$) + \item finite domain \hspace{5mm}($\text{finite} \{a.\;f a \not= a\}$) + \end{itemize}\medskip + + \item<3-> swappings: + \small + \[ + \begin{array}{l@ {\hspace{1mm}}l} + (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\ + & \text{then}\;\lambda c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\; + \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\ + & \text{else}\;\only<3>{\mbox{\textcolor{red}{\bf ?}}}\only<4->{\text{id}} + \end{array} + \] + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-6> + \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip + + \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip + + \item<5-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip + + \begin{itemize} + \item $0\;\act\;x = x$\\ + \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$ + \end{itemize} + + \small + \onslide<6->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$} + \end{itemize} + + \only<4>{ + \begin{textblock}{6}(2.5,11) + \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 + This is slightly odd, since in general: + \begin{center}$\pi_1 + \pi_2 \alert{\not=} \pi_2 + \pi_1$\end{center} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-3> + \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item \underline{concrete} atoms: + \end{itemize} +*} +(*<*) +consts sort :: "atom \ string" +(*>*) + +typedef name = "{a :: atom. sort a = ''name''}" (*<*)sorry(*>*) +typedef ident = "{a :: atom. sort a = ''ident''}" (*<*)sorry(*>*) + +text_raw {* + \mbox{}\bigskip\bigskip + \begin{itemize} + \item<2-> there is an overloaded function \underline{atom}, which injects concrete + atoms into generic ones\medskip + \begin{center} + \begin{tabular}{l} + $\text{atom}(a) \fresh x$\\ + $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$ + \end{tabular} + \end{center}\bigskip\medskip + + \onslide<3-> + {I would like to have $a \fresh x$, $(a\; b)$, \ldots} + + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2>[c] + \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item the formalised version of the nominal theory is now much nicer to + work with (sorts are occasionally explicit)\bigskip + + \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip + + \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity} + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2> + \frametitle{\begin{tabular}{c}\LARGE{}Part II: General Bindings\end{tabular}} + \mbox{}\\[-6mm] + + \begin{itemize} + \item old Nominal 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 is a \alert{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)\\ + \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 (restriction)\medskip + + \item the order does not matter, but the cardinality of the binders + must be the same (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) $=$ $\varnothing$}}\\ + \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $\{$a$\}$ $\cup$ bn(as)}}\\ + \end{tabular} + + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-4> + \frametitle{\begin{tabular}{c}Ott\end{tabular}} + \mbox{}\\[-3mm] + + \begin{itemize} + \item this way of specifying binding is pretty much stolen from + Ott\onslide<2->{, \alert{\bf but} with adjustments:}\medskip + + \begin{itemize} + \item<2-> Ott allows specifications like\smallskip + \begin{center} + $t ::= t\;t\; |\;\lambda x.t$ + \end{center}\medskip + + \item<3-> whether something is bound can depend on other bound things\smallskip + \begin{center} + Foo $(\lambda x. t)\; s$ + \end{center}\medskip + \onslide<4->{this might make sense for ``raw'' terms, but not at all + for $\alpha$-equated terms} + \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 old Nominal we represented single binders as partial functions:\bigskip + + \begin{center} + \begin{tabular}{l} + Lam [$a$].$t$ $\;\dn$\\[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-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 atoms\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 atoms + \end{textblock}} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2> + \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<2->{ + \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<2->{ + \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<2->{ + \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> + \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}} + + \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]{${}_{\star}$}^{=,\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}_\star$\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)\;^\star$\\ + \end{tabular}} + \end{center} + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}One 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}\times\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'}} + \] + + + \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}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 the 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---just a matter of + another week or two) + \end{itemize} + + + \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 (POPL 2011 tutorial)\medskip + \item<4-> Thanks goes to Cezary!\\ + \only<5->{\hspace{3mm}\ldots{}and of course others $\in$ Isabelle-team!} + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +(*<*) +end +(*>*) \ No newline at end of file diff -r 530b0adbcf77 -r 118a0ca16381 Slides/document/root.beamer.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/document/root.beamer.tex Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Slides/document/root.notes.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/document/root.notes.tex Tue Jun 01 15:46:07 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 530b0adbcf77 -r 118a0ca16381 Slides/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/document/root.tex Tue Jun 01 15:46:07 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: +