--- 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
--- 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
--- 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
--- 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))) []
--- 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 \<union> fvy y)"
+definition
+ prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 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 \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
+lemma [mono]:
+ shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+ unfolding prod_alpha_def
by auto
lemma [eqvt]:
- shows "p \<bullet> prod_rel A B x y = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+ shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> 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
--- 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
--- 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 \<Rightarrow> atom list"
+ f::"pat \<Rightarrow> 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 \<noteq> atom b \<Longrightarrow> Let (PD a a) x y \<noteq> Let (PD a b) x y"
- by (simp add: trm_pat.eq_iff alphas)
-
-lemma lets_overlap2:
- "atom a \<notin> supp y \<Longrightarrow> atom b \<notin> supp y \<Longrightarrow> 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\<leftrightarrow>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
--- 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
--- 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]
--- 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
--- 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 \<Rightarrow> atom list \<Rightarrow> 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
*}
--- 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 \<Rightarrow> 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
--- 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 \<notsimeq> C2 y ...) (Proof by cases; simp)
-
-Tacs.thy/build_rel_inj
- 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> 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 \<Rightarrow> atom set"
-where
- "bn (P1 x) = {atom x}"
-| "bn (P2 p1 p2) = bn p1 \<union> 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 \<notsimeq> C2 y ...) (Proof by cases; simp)
-and pat =
- PVar name
-| PUnit
-| PPair pat pat
-
-binder
- b_lrbs :: "lrbs \<Rightarrow> atom list" and
- b_pat :: "pat \<Rightarrow> atom set" and
- b_fnclauses :: "fnclauses \<Rightarrow> atom list" and
- b_fnclause :: "fnclause \<Rightarrow> atom list" and
- b_lrb :: "lrb \<Rightarrow> 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 \<union> 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 \<leftrightarrow> 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
+*}
--- 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 \<bullet> {} = {}"
+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 \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
+lemma permute_fset[simp]:
fixes S::"('a::pt) fset"
shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
by (lifting permute_list.simps)
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
+ML {* @{term "{}"} ; @{term "{||}"} *}
+
+declare permute_fset[eqvt]
+
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
+
lemma fmap_eqvt[eqvt]:
shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
by (lifting map_eqvt)
@@ -119,4 +142,8 @@
apply auto
done
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
end
--- 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
--- 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"*)
];
--- 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
--- /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 *)
+
--- /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 *)
+
--- /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 *)
+
--- /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
--- /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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \begin{frame}<1>
+ \frametitle{\begin{tabular}{c}Problems\end{tabular}}
+ \mbox{}\\[-3mm]
+
+ \begin{itemize}
+ \item @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip
+
+ \item @{text "supp _ :: \<beta> \<Rightarrow> \<alpha> 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<presentation>{
+ \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 \<Rightarrow> 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<presentation>{
+ \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<presentation>{
+ \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 \<Rightarrow> 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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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
--- /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:
+
--- /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:
+
--- /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<presentation>{
+\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<article>{
+\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:
+