--- a/Attic/Quot/quotient_term.ML Wed Jun 23 09:01:45 2010 +0200
+++ b/Attic/Quot/quotient_term.ML Wed Jun 23 15:40:00 2010 +0100
@@ -224,9 +224,9 @@
val map_fun = mk_mapfun ctxt vs rty_pat
val result = list_comb (map_fun, args)
in
- if forall is_identity args
+ (*if forall is_identity args
then absrep_const flag ctxt s'
- else mk_fun_compose flag (absrep_const flag ctxt s', result)
+ else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
end
| (TFree x, TFree x') =>
if x = x'
--- a/IsaMakefile Wed Jun 23 09:01:45 2010 +0200
+++ b/IsaMakefile Wed Jun 23 15:40:00 2010 +0100
@@ -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/Nominal2_Base.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy Wed Jun 23 15:40:00 2010 +0100
@@ -385,6 +385,11 @@
unfolding permute_perm_def
by (auto simp add: swap_atom expand_perm_eq)
+lemma uminus_eqvt:
+ fixes p q::"perm"
+ shows "p \<bullet> (- q) = - (p \<bullet> q)"
+ unfolding permute_perm_def
+ by (simp add: diff_minus minus_add add_assoc)
subsection {* Permutations for functions *}
--- a/Nominal-General/Nominal2_Eqvt.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy Wed Jun 23 15:40:00 2010 +0100
@@ -295,14 +295,13 @@
shows "a \<sharp> ()"
by (simp add: fresh_def supp_unit)
-
section {* additional eqvt lemmas *}
lemmas [eqvt] =
imp_eqvt [folded induct_implies_def]
(* nominal *)
- supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt
+ supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt
(* datatypes *)
Pair_eqvt permute_list.simps
--- a/Nominal-General/nominal_eqvt.ML Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML Wed Jun 23 15:40:00 2010 +0100
@@ -10,7 +10,7 @@
val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
- val equivariance: term list -> thm -> thm list -> Proof.context -> thm list * local_theory
+ val equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory
val equivariance_cmd: string -> Proof.context -> local_theory
end
@@ -28,66 +28,6 @@
(Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
-(**
- given the theorem F[t]; proves the theorem F[f t]
-
- - F needs to be monotone
- - f returns either SOME for a term it fires on
- and NONE elsewhere
-**)
-fun map_term f t =
- (case f t of
- NONE => map_term' f t
- | x => x)
-and map_term' f (t $ u) =
- (case (map_term f t, map_term f u) of
- (NONE, NONE) => NONE
- | (SOME t'', NONE) => SOME (t'' $ u)
- | (NONE, SOME u'') => SOME (t $ u'')
- | (SOME t'', SOME u'') => SOME (t'' $ u''))
- | map_term' f (Abs (s, T, t)) =
- (case map_term f t of
- NONE => NONE
- | SOME t'' => SOME (Abs (s, T, t'')))
- | map_term' _ _ = NONE;
-
-fun map_thm_tac ctxt tac thm =
-let
- val monos = Inductive.get_monos ctxt
- val simps = HOL_basic_ss addsimps @{thms split_def}
-in
- EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
- REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
- REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
-end
-
-fun map_thm ctxt f tac thm =
-let
- val opt_goal_trm = map_term f (prop_of thm)
-in
- case opt_goal_trm of
- NONE => thm
- | SOME goal =>
- Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm)
-end
-
-(*
- inductive premises can be of the form
- R ... /\ P ...; split_conj picks out
- the part P ...
-*)
-fun transform_prem ctxt names thm =
-let
- fun split_conj names (Const ("op &", _) $ f1 $ f2) =
- (case head_of f1 of
- Const (name, _) => if member (op =) names name then SOME f2 else NONE
- | _ => NONE)
- | split_conj _ _ = NONE;
-in
- map_thm ctxt (split_conj names) (etac conjunct2 1) thm
-end
-
-
(** equivariance tactics **)
val perm_boolE = @{thm permute_boolE}
@@ -104,7 +44,7 @@
eqvt_strict_tac ctxt [] pred_names THEN'
SUBPROOF (fn {prems, context as ctxt, ...} =>
let
- val prems' = map (transform_prem ctxt pred_names) prems
+ val prems' = map (transform_prem2 ctxt pred_names) prems
val tac1 = resolve_tac prems'
val tac2 = EVERY' [ rtac pi_intro_rule,
eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]
@@ -147,7 +87,7 @@
(thm', ctxt')
end
-fun equivariance pred_trms raw_induct intrs ctxt =
+fun equivariance note_flag pred_trms raw_induct intrs ctxt =
let
val is_already_eqvt =
filter (is_eqvt ctxt) pred_trms
@@ -172,7 +112,9 @@
|> singleton (ProofContext.export ctxt' ctxt))
val thms' = map (fn th => zero_var_indexes (th RS mp)) thms
in
- ctxt |> fold_map note_named_thm (pred_names ~~ thms')
+ if note_flag
+ then ctxt |> fold_map note_named_thm (pred_names ~~ thms')
+ else (thms', ctxt)
end
fun equivariance_cmd pred_name ctxt =
@@ -181,7 +123,7 @@
val (_, {preds, raw_induct, intrs, ...}) =
Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
in
- equivariance preds raw_induct intrs ctxt |> snd
+ equivariance true preds raw_induct intrs ctxt |> snd
end
local structure P = Parse and K = Keyword in
--- a/Nominal-General/nominal_library.ML Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal-General/nominal_library.ML Wed Jun 23 15:40:00 2010 +0100
@@ -6,6 +6,10 @@
signature NOMINAL_LIBRARY =
sig
+ val last2: 'a list -> 'a * 'a
+
+ val dest_listT: typ -> typ
+
val mk_minus: term -> term
val mk_plus: term -> term -> term
@@ -20,17 +24,49 @@
val mk_atom: term -> term
val supp_ty: typ -> typ
+ val supp_const: typ -> term
val mk_supp_ty: typ -> term -> term
val mk_supp: term -> term
val mk_equiv: thm -> thm
val safe_mk_equiv: thm -> thm
+
+ val mk_diff: term * term -> term
+ val mk_append: term * term -> term
+ val mk_union: term * term -> term
+ val fold_union: term list -> term
+
+ (* datatype operations *)
+ val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
+ val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
+ val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list ->
+ (term * typ * typ list * bool list) list list
+ val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int ->
+ (term * typ * typ list * bool list) list
+ val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
+
+ (* tactics for function package *)
+ val pat_completeness_auto: Proof.context -> tactic
+ val pat_completeness_simp: thm list -> Proof.context -> tactic
+ val prove_termination: Proof.context -> Function.info * local_theory
+
+ (* transformations of premises in inductions *)
+ val transform_prem1: Proof.context -> string list -> thm -> thm
+ val transform_prem2: Proof.context -> string list -> thm -> thm
end
structure Nominal_Library: NOMINAL_LIBRARY =
struct
+fun last2 [] = raise Empty
+ | last2 [_] = raise Empty
+ | last2 [x, y] = (x,y)
+ | last2 (_ :: xs) = last2 xs
+
+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 +78,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 +86,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 +95,165 @@
fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
+(* functions that construct differences, appends and unions
+ but avoid producing empty atom sets or empty atom lists *)
+
+fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
+ | mk_diff (t1, @{term "{}::atom set"}) = t1
+ | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
+
+fun mk_append (@{term "[]::atom list"}, @{term "[]::atom list"}) = @{term "[]::atom list"}
+ | mk_append (t1, @{term "[]::atom list"}) = t1
+ | mk_append (@{term "[]::atom list"}, t2) = t2
+ | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2)
+
+fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
+ | mk_union (t1 , @{term "{}::atom set"}) = t1
+ | mk_union (@{term "{}::atom set"}, t2) = t2
+ | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)
+
+fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
+
+
+
+
+(** datatypes **)
+
+
+(* returns the type of the nth datatype *)
+fun all_dtyps descr sorts =
+ map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))
+
+fun nth_dtyp descr sorts n =
+ Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
+
+(* returns info about constructors in a datatype *)
+fun all_dtyp_constrs_info descr =
+ map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr
+
+(* returns the constants of the constructors plus the
+ corresponding type and types of arguments *)
+fun all_dtyp_constrs_types descr sorts =
+let
+ fun aux ((ty_name, vs), (cname, args)) =
+ let
+ val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
+ val ty = Type (ty_name, vs_tys)
+ val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
+ val is_rec = map Datatype_Aux.is_rec_type args
+ in
+ (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)
+ end
+in
+ map (map aux) (all_dtyp_constrs_info descr)
+end
+
+fun nth_dtyp_constrs_types descr sorts n =
+ nth (all_dtyp_constrs_types descr sorts) n
+
+
+(* generates for every datatype a name str ^ dt_name
+ plus and index for multiple occurences of a string *)
+fun prefix_dt_names descr sorts str =
+let
+ fun get_nth_name (i, _) =
+ Datatype_Aux.name_of_typ (nth_dtyp descr sorts i)
+in
+ Datatype_Prop.indexify_names
+ (map (prefix str o get_nth_name) descr)
+end
+
+
+
+(** function package tactics **)
+
+fun pat_completeness_auto lthy =
+ Pat_Completeness.pat_completeness_tac lthy 1
+ THEN auto_tac (clasimpset_of lthy)
+
+fun pat_completeness_simp simps lthy =
+let
+ val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps)
+in
+ Pat_Completeness.pat_completeness_tac lthy 1
+ THEN ALLGOALS (asm_full_simp_tac simp_set)
+end
+
+fun prove_termination lthy =
+ Function.prove_termination NONE
+ (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
+
+
+(** transformations of premises (in inductive proofs) **)
+
+(*
+ given the theorem F[t]; proves the theorem F[f t]
+
+ - F needs to be monotone
+ - f returns either SOME for a term it fires on
+ and NONE elsewhere
+*)
+fun map_term f t =
+ (case f t of
+ NONE => map_term' f t
+ | x => x)
+and map_term' f (t $ u) =
+ (case (map_term f t, map_term f u) of
+ (NONE, NONE) => NONE
+ | (SOME t'', NONE) => SOME (t'' $ u)
+ | (NONE, SOME u'') => SOME (t $ u'')
+ | (SOME t'', SOME u'') => SOME (t'' $ u''))
+ | map_term' f (Abs (s, T, t)) =
+ (case map_term f t of
+ NONE => NONE
+ | SOME t'' => SOME (Abs (s, T, t'')))
+ | map_term' _ _ = NONE;
+
+fun map_thm_tac ctxt tac thm =
+let
+ val monos = Inductive.get_monos ctxt
+ val simps = HOL_basic_ss addsimps @{thms split_def}
+in
+ EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
+ REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
+ REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
+end
+
+fun map_thm ctxt f tac thm =
+let
+ val opt_goal_trm = map_term f (prop_of thm)
+in
+ case opt_goal_trm of
+ NONE => thm
+ | SOME goal =>
+ Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm)
+end
+
+(*
+ inductive premises can be of the form
+ R ... /\ P ...; split_conj_i picks out
+ the part R or P part
+*)
+fun split_conj1 names (Const ("op &", _) $ f1 $ f2) =
+ (case head_of f1 of
+ Const (name, _) => if member (op =) names name then SOME f1 else NONE
+ | _ => NONE)
+| split_conj1 _ _ = NONE;
+
+fun split_conj2 names (Const ("op &", _) $ f1 $ f2) =
+ (case head_of f1 of
+ Const (name, _) => if member (op =) names name then SOME f2 else NONE
+ | _ => NONE)
+| split_conj2 _ _ = NONE;
+
+fun transform_prem1 ctxt names thm =
+ map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm
+
+fun transform_prem2 ctxt names thm =
+ map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm
+
+
+
end (* structure *)
open Nominal_Library;
\ No newline at end of file
--- a/Nominal-General/nominal_permeq.ML Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML Wed Jun 23 15:40:00 2010 +0100
@@ -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 Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Abs.thy Wed Jun 23 15:40:00 2010 +0100
@@ -51,6 +51,136 @@
by (case_tac [!] bs, case_tac [!] cs)
(auto simp add: le_fun_def le_bool_def alphas)
+(* equivariance *)
+lemma alpha_gen_eqvt[eqvt]:
+ shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
+ unfolding alphas
+ unfolding permute_eqvt[symmetric]
+ unfolding set_eqvt[symmetric]
+ unfolding permute_fun_app_eq[symmetric]
+ unfolding Diff_eqvt[symmetric]
+ by (auto simp add: permute_bool_def fresh_star_permute_iff)
+
+(* equivalence *)
+lemma alpha_gen_refl:
+ assumes a: "R x x"
+ shows "(bs, x) \<approx>gen R f 0 (bs, x)"
+ and "(bs, x) \<approx>res R f 0 (bs, x)"
+ and "(cs, x) \<approx>lst R f 0 (cs, x)"
+ using a
+ unfolding alphas
+ unfolding fresh_star_def
+ by (simp_all add: fresh_zero_perm)
+
+lemma alpha_gen_sym:
+ assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
+ shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
+ and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
+ and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+ unfolding alphas fresh_star_def
+ using a
+ by (auto simp add: fresh_minus_perm)
+
+lemma alpha_gen_sym_eqvt:
+ assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
+ and b: "p \<bullet> R = R"
+ shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
+ and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
+ and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+apply(auto intro!: alpha_gen_sym)
+apply(drule_tac [!] a)
+apply(rule_tac [!] p="p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel b)
+apply(assumption)
+apply(perm_simp add: permute_minus_cancel b)
+apply(assumption)
+apply(perm_simp add: permute_minus_cancel b)
+apply(assumption)
+done
+
+lemma alpha_gen_trans:
+ assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
+ shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+ and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
+ and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
+ using a
+ unfolding alphas fresh_star_def
+ by (simp_all add: fresh_plus_perm)
+
+
+lemma alpha_gen_trans_eqvt:
+ assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
+ and a: "(bs, x) \<approx>gen R f p (cs, y)"
+ and d: "q \<bullet> R = R"
+ and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
+apply(rule alpha_gen_trans)
+defer
+apply(rule a)
+apply(rule b)
+apply(drule c)
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel d)
+apply(assumption)
+apply(rotate_tac -1)
+apply(drule_tac p="q" in permute_boolI)
+apply(perm_simp add: permute_minus_cancel d)
+apply(simp add: permute_eqvt[symmetric])
+done
+
+lemma alpha_res_trans_eqvt:
+ assumes b: "(cs, y) \<approx>res R f q (ds, z)"
+ and a: "(bs, x) \<approx>res R f p (cs, y)"
+ and d: "q \<bullet> R = R"
+ and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
+apply(rule alpha_gen_trans)
+defer
+apply(rule a)
+apply(rule b)
+apply(drule c)
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel d)
+apply(assumption)
+apply(rotate_tac -1)
+apply(drule_tac p="q" in permute_boolI)
+apply(perm_simp add: permute_minus_cancel d)
+apply(simp add: permute_eqvt[symmetric])
+done
+
+lemma alpha_lst_trans_eqvt:
+ assumes b: "(cs, y) \<approx>lst R f q (ds, z)"
+ and a: "(bs, x) \<approx>lst R f p (cs, y)"
+ and d: "q \<bullet> R = R"
+ and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
+apply(rule alpha_gen_trans)
+defer
+apply(rule a)
+apply(rule b)
+apply(drule c)
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel d)
+apply(assumption)
+apply(rotate_tac -1)
+apply(drule_tac p="q" in permute_boolI)
+apply(perm_simp add: permute_minus_cancel d)
+apply(simp add: permute_eqvt[symmetric])
+done
+
+lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
+
+lemma test:
+ shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
+ and "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
+ and "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s"
+ by (simp_all add: alphas)
+
+
+section {* General Abstractions *}
+
fun
alpha_abs
where
@@ -406,7 +536,8 @@
apply(simp add: atom_image_cong)
done
-lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
+lemma swap_atom_image_fresh:
+ "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
apply (simp add: fresh_def)
apply (simp add: supp_atom_image)
apply (fold fresh_def)
@@ -448,329 +579,6 @@
R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
by (simp add: alphas)
-lemma alpha_gen_compose_sym:
- fixes pi
- assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
- using b apply -
- apply(simp add: alphas)
- apply(erule conjE)+
- apply(rule conjI)
- apply(simp add: fresh_star_def fresh_minus_perm)
- apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
- apply simp
- apply(clarify)
- apply(simp)
- apply(rule a)
- apply assumption
- done
-
-lemma alpha_res_compose_sym:
- fixes pi
- assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(ab, s) \<approx>res R f (- pi) (aa, t)"
- using b apply -
- apply(simp add: alphas)
- apply(erule conjE)+
- apply(rule conjI)
- apply(simp add: fresh_star_def fresh_minus_perm)
- apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
- apply simp
- apply(rule a)
- apply assumption
- done
-
-lemma alpha_lst_compose_sym:
- fixes pi
- assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(ab, s) \<approx>lst R f (- pi) (aa, t)"
- using b apply -
- apply(simp add: alphas)
- apply(erule conjE)+
- apply(rule conjI)
- apply(simp add: fresh_star_def fresh_minus_perm)
- apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
- apply simp
- apply(clarify)
- apply(simp)
- apply(rule a)
- apply assumption
- done
-
-lemmas alphas_compose_sym = alpha_gen_compose_sym alpha_res_compose_sym alpha_lst_compose_sym
-
-lemma alpha_gen_compose_sym2:
- assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
- (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
- and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
- and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
- shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
- using a
- apply(simp add: alphas)
- apply clarify
- apply (rule conjI)
- apply(simp add: fresh_star_def fresh_minus_perm)
- apply (rule conjI)
- apply (rotate_tac 3)
- apply (drule_tac pi="- pi" in r1)
- apply simp
- apply (rule conjI)
- apply (rotate_tac -1)
- apply (drule_tac pi="- pi" in r2)
- apply simp_all
- done
-
-lemma alpha_res_compose_sym2:
- assumes a: "(aa, t1, t2) \<approx>res (\<lambda>(x11, x12) (x21, x22).
- (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
- and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
- and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
- shows "(ab, s1, s2) \<approx>res (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
- using a
- apply(simp add: alphas)
- apply clarify
- apply (rule conjI)
- apply(simp add: fresh_star_def fresh_minus_perm)
- apply (rule conjI)
- apply (rotate_tac 3)
- apply (drule_tac pi="- pi" in r1)
- apply simp
- apply (rotate_tac -1)
- apply (drule_tac pi="- pi" in r2)
- apply simp
- done
-
-lemma alpha_lst_compose_sym2:
- assumes a: "(aa, t1, t2) \<approx>lst (\<lambda>(x11, x12) (x21, x22).
- (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
- and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
- and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
- shows "(ab, s1, s2) \<approx>lst (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
- using a
- apply(simp add: alphas)
- apply clarify
- apply (rule conjI)
- apply(simp add: fresh_star_def fresh_minus_perm)
- apply (rule conjI)
- apply (rotate_tac 3)
- apply (drule_tac pi="- pi" in r1)
- apply simp
- apply (rule conjI)
- apply (rotate_tac -1)
- apply (drule_tac pi="- pi" in r2)
- apply simp_all
- done
-
-lemmas alphas_compose_sym2 = alpha_gen_compose_sym2 alpha_res_compose_sym2 alpha_lst_compose_sym2
-
-lemma alpha_gen_compose_trans:
- fixes pi pia
- assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
- and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
- using b c apply -
- apply(simp add: alphas)
- apply(erule conjE)+
- apply(simp add: fresh_star_plus)
- apply(drule_tac x="- pia \<bullet> sa" in spec)
- apply(drule mp)
- apply(rotate_tac 5)
- apply(drule_tac pi="- pia" in a)
- apply(simp)
- apply(rotate_tac 7)
- apply(drule_tac pi="pia" in a)
- apply(simp)
- done
-
-lemma alpha_res_compose_trans:
- fixes pi pia
- assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
- and c: "(ab, ta) \<approx>res R f pia (ac, sa)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(aa, t) \<approx>res R f (pia + pi) (ac, sa)"
- using b c apply -
- apply(simp add: alphas)
- apply(erule conjE)+
- apply(simp add: fresh_star_plus)
- apply(drule_tac x="- pia \<bullet> sa" in spec)
- apply(drule mp)
- apply(drule_tac pi="- pia" in a)
- apply(simp)
- apply(rotate_tac 6)
- apply(drule_tac pi="pia" in a)
- apply(simp)
- done
-
-lemma alpha_lst_compose_trans:
- fixes pi pia
- assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
- and c: "(ab, ta) \<approx>lst R f pia (ac, sa)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(aa, t) \<approx>lst R f (pia + pi) (ac, sa)"
- using b c apply -
- apply(simp add: alphas)
- apply(erule conjE)+
- apply(simp add: fresh_star_plus)
- apply(drule_tac x="- pia \<bullet> sa" in spec)
- apply(drule mp)
- apply(rotate_tac 5)
- apply(drule_tac pi="- pia" in a)
- apply(simp)
- apply(rotate_tac 7)
- apply(drule_tac pi="pia" in a)
- apply(simp)
- done
-
-lemmas alphas_compose_trans = alpha_gen_compose_trans alpha_res_compose_trans alpha_lst_compose_trans
-
-lemma alpha_gen_compose_trans2:
- fixes pi pia
- assumes b: "(aa, (t1, t2)) \<approx>gen
- (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
- (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
- and c: "(ab, (ta1, ta2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
- pia (ac, (sa1, sa2))"
- and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
- and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
- shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
- (pia + pi) (ac, (sa1, sa2))"
- using b c apply -
- apply(simp add: alphas2)
- apply(simp add: alphas)
- apply(erule conjE)+
- apply(simp add: fresh_star_plus)
- apply(drule_tac x="- pia \<bullet> sa1" in spec)
- apply(drule mp)
- apply(rotate_tac 5)
- apply(drule_tac pi="- pia" in r1)
- apply(simp)
- apply(rotate_tac -1)
- apply(drule_tac pi="pia" in r1)
- apply(simp)
- apply(drule_tac x="- pia \<bullet> sa2" in spec)
- apply(drule mp)
- apply(rotate_tac 6)
- apply(drule_tac pi="- pia" in r2)
- apply(simp)
- apply(rotate_tac -1)
- apply(drule_tac pi="pia" in r2)
- apply(simp)
- done
-
-lemma alpha_res_compose_trans2:
- fixes pi pia
- assumes b: "(aa, (t1, t2)) \<approx>res
- (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
- (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
- and c: "(ab, (ta1, ta2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
- pia (ac, (sa1, sa2))"
- and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
- and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
- shows "(aa, (t1, t2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
- (pia + pi) (ac, (sa1, sa2))"
- using b c apply -
- apply(simp add: alphas2)
- apply(simp add: alphas)
- apply(erule conjE)+
- apply(simp add: fresh_star_plus)
- apply(drule_tac x="- pia \<bullet> sa1" in spec)
- apply(drule mp)
- apply(rotate_tac 5)
- apply(drule_tac pi="- pia" in r1)
- apply(simp)
- apply(rotate_tac -1)
- apply(drule_tac pi="pia" in r1)
- apply(simp)
- apply(drule_tac x="- pia \<bullet> sa2" in spec)
- apply(drule mp)
- apply(rotate_tac 6)
- apply(drule_tac pi="- pia" in r2)
- apply(simp)
- apply(rotate_tac -1)
- apply(drule_tac pi="pia" in r2)
- apply(simp)
- done
-
-lemma alpha_lst_compose_trans2:
- fixes pi pia
- assumes b: "(aa, (t1, t2)) \<approx>lst
- (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
- (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
- and c: "(ab, (ta1, ta2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
- pia (ac, (sa1, sa2))"
- and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
- and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
- shows "(aa, (t1, t2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
- (pia + pi) (ac, (sa1, sa2))"
- using b c apply -
- apply(simp add: alphas2)
- apply(simp add: alphas)
- apply(erule conjE)+
- apply(simp add: fresh_star_plus)
- apply(drule_tac x="- pia \<bullet> sa1" in spec)
- apply(drule mp)
- apply(rotate_tac 5)
- apply(drule_tac pi="- pia" in r1)
- apply(simp)
- apply(rotate_tac -1)
- apply(drule_tac pi="pia" in r1)
- apply(simp)
- apply(drule_tac x="- pia \<bullet> sa2" in spec)
- apply(drule mp)
- apply(rotate_tac 6)
- apply(drule_tac pi="- pia" in r2)
- apply(simp)
- apply(rotate_tac -1)
- apply(drule_tac pi="pia" in r2)
- apply(simp)
- done
-
-lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2
-
-lemma alpha_gen_refl:
- assumes a: "R x x"
- shows "(bs, x) \<approx>gen R f 0 (bs, x)"
- and "(bs, x) \<approx>res R f 0 (bs, x)"
- and "(cs, x) \<approx>lst R f 0 (cs, x)"
- using a
- unfolding alphas
- unfolding fresh_star_def
- by (simp_all add: fresh_zero_perm)
-
-lemma alpha_gen_sym:
- assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
- shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
- and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
- and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
- unfolding alphas fresh_star_def
- using a
- by (auto simp add: fresh_minus_perm)
-
-lemma alpha_gen_trans:
- assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
- shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
- and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
- and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
- using a
- unfolding alphas fresh_star_def
- by (simp_all add: fresh_plus_perm)
-
-
-lemma alpha_gen_eqvt[eqvt]:
- shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
- and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
- and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
- unfolding alphas
- unfolding permute_eqvt[symmetric]
- unfolding set_eqvt[symmetric]
- unfolding permute_fun_app_eq[symmetric]
- unfolding Diff_eqvt[symmetric]
- by (auto simp add: permute_bool_def fresh_star_permute_iff)
-
lemma alpha_gen_simpler:
assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
and fin_fv: "finite (f x)"
@@ -830,8 +638,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 +654,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 +670,6 @@
unfolding prod_fv.simps
by (perm_simp) (rule refl)
+
end
--- a/Nominal/Equivp.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Equivp.thy Wed Jun 23 15:40:00 2010 +0100
@@ -1,167 +1,7 @@
theory Equivp
-imports "NewFv" "Tacs" "Rsp"
+imports "Abs" "Perm" "Tacs" "Rsp"
begin
-ML {*
-fun build_alpha_sym_trans_gl alphas (x, y, z) =
-let
- fun build_alpha alpha =
- let
- val ty = domain_type (fastype_of alpha);
- val var = Free(x, ty);
- val var2 = Free(y, ty);
- val var3 = Free(z, ty);
- val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
- val transp = HOLogic.mk_imp (alpha $ var $ var2,
- HOLogic.mk_all (z, ty,
- HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
- in
- (symp, transp)
- end;
- val eqs = map build_alpha alphas
- val (sym_eqs, trans_eqs) = split_list eqs
- fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
-in
- (conj sym_eqs, conj trans_eqs)
-end
-*}
-
-ML {*
-fun build_alpha_refl_gl fv_alphas_lst alphas =
-let
- val (fvs_alphas, _) = split_list fv_alphas_lst;
- val (_, alpha_ts) = split_list fvs_alphas;
- val tys = map (domain_type o fastype_of) alpha_ts;
- val names = Datatype_Prop.make_tnames tys;
- val args = map Free (names ~~ tys);
- fun find_alphas ty x =
- domain_type (fastype_of x) = ty;
- fun refl_eq_arg (ty, arg) =
- let
- val rel_alphas = filter (find_alphas ty) alphas;
- in
- map (fn x => x $ arg $ arg) rel_alphas
- end;
- (* Flattening loses the induction structure *)
- val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args))
-in
- (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
-end
-*}
-
-ML {*
-fun reflp_tac induct eq_iff =
- rtac induct THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
- split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
- THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
- @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
- add_0_left supp_zero_perm Int_empty_left split_conv prod_rel.simps})
-*}
-
-ML {*
-fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
-let
- val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
- val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
-in
- HOLogic.conj_elims refl_conj
-end
-*}
-
-lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
-apply (erule exE)
-apply (rule_tac x="-pi" in exI)
-by auto
-
-ML {*
-fun symp_tac induct inj eqvt ctxt =
- rtac induct THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
- THEN_ALL_NEW
- REPEAT o etac @{thm exi_neg}
- THEN_ALL_NEW
- split_conj_tac THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
- TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW
- (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
-*}
-
-
-lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
-apply (erule exE)+
-apply (rule_tac x="pia + pi" in exI)
-by auto
-
-
-ML {*
-fun eetac rule =
- Subgoal.FOCUS_PARAMS (fn focus =>
- let
- val concl = #concl focus
- val prems = Logic.strip_imp_prems (term_of concl)
- val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
- val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
- val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
- in
- (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1
- end
- )
-*}
-
-ML {*
-fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
- rtac induct THEN_ALL_NEW
- (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
- asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
- split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
- THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
- THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
- TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW
- (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
-*}
-
-lemma transpI:
- "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
- unfolding transp_def
- by blast
-
-ML {*
-fun equivp_tac reflps symps transps =
- (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)
- simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
- THEN' rtac conjI THEN' rtac allI THEN'
- resolve_tac reflps THEN'
- rtac conjI THEN' rtac allI THEN' rtac allI THEN'
- resolve_tac symps THEN'
- rtac @{thm transpI} THEN' resolve_tac transps
-*}
-
-ML {*
-fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
-let
- val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
- val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)
- fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
- fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
- val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';
- val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';
- val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]
- val symps = HOLogic.conj_elims symp
- val transps = HOLogic.conj_elims transp
- fun equivp alpha =
- let
- val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
- val goal = @{term Trueprop} $ (equivp $ alpha)
- fun tac _ = equivp_tac reflps symps transps 1
- in
- Goal.prove ctxt [] [] goal tac
- end
-in
- map equivp alphas
-end
-*}
-
lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
by auto
@@ -194,7 +34,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 +43,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 +180,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/Classical.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Ex/Classical.thy Wed Jun 23 15:40:00 2010 +0100
@@ -4,26 +4,23 @@
(* example from my Urban's PhD *)
-(*
- alpha_trm_raw is incorrectly defined, therefore the equivalence proof
- does not go through; below the correct definition is given
-*)
-
atom_decl name
atom_decl coname
-ML {* val _ = cheat_equivp := true *}
+declare [[STEPS = 9]]
nominal_datatype trm =
Ax "name" "coname"
-| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2
-| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
-| AndL1 n::"name" t::"trm" "name" bind n in t
-| AndL2 n::"name" t::"trm" "name" bind n in t
-| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2
-| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t
+| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2
+| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
+| AndL1 n::"name" t::"trm" "name" bind n in t
+| AndL2 n::"name" t::"trm" "name" bind n in t
+| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2
+| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t
+thm alpha_trm_raw.intros[no_vars]
+(*
thm trm.fv
thm trm.eq_iff
thm trm.bn
@@ -31,44 +28,7 @@
thm trm.induct
thm trm.distinct
thm trm.fv[simplified trm.supp]
-
-(* correct alpha definition *)
-
-inductive
- alpha
-where
- "\<lbrakk>name = namea; coname = conamea\<rbrakk> \<Longrightarrow>
- alpha (Ax_raw name coname) (Ax_raw namea conamea)"
-| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a);
- \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a)\<rbrakk> \<Longrightarrow>
- alpha (Cut_raw coname1 trm_raw1 coname2 trm_raw2)
- (Cut_raw coname1a trm_raw1a coname2a trm_raw2a)"
-| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a);
- \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a);
- coname3 = coname3a\<rbrakk> \<Longrightarrow>
- alpha (AndR_raw coname1 trm_raw1 coname2 trm_raw2 coname3)
- (AndR_raw coname1a trm_raw1a coname2a trm_raw2a coname3a)"
-| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
- name2 = name2a\<rbrakk> \<Longrightarrow>
- alpha (AndL1_raw name1 trm_raw name2) (AndL1_raw name1a trm_rawa name2a)"
-| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
- name2 = name2a\<rbrakk> \<Longrightarrow>
- alpha (AndL2_raw name1 trm_raw name2) (AndL2_raw name1a trm_rawa name2a)"
-| "\<lbrakk>\<exists>pi. ({atom coname}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom conamea}, trm_raw1a);
- \<exists>pia. ({atom name1}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom name1a}, trm_raw2a);
- name2 = name2a\<rbrakk> \<Longrightarrow>
- alpha (ImpL_raw coname trm_raw1 name1 trm_raw2 name2)
- (ImpL_raw conamea trm_raw1a name1a trm_raw2a name2a)"
-| "\<lbrakk>\<exists>pi.({atom name} \<union> {atom coname1}, trm_raw) \<approx>gen alpha fv_trm_raw pi
- ({atom namea} \<union> {atom coname1a}, trm_rawa); coname2 = coname2a\<rbrakk> \<Longrightarrow>
- alpha (ImpR_raw coname1 name trm_raw coname2)
- (ImpR_raw coname1a namea trm_rawa coname2a)"
-
-thm alpha.intros
-
-equivariance alpha
-
-thm eqvts_raw
+*)
end
--- a/Nominal/Ex/CoreHaskell.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy Wed Jun 23 15:40:00 2010 +0100
@@ -2,15 +2,14 @@
imports "../NewParser"
begin
-(* core haskell *)
-
-(* at the moment it is hard coded that shallow binders
- need to use bind_set *)
+(* Core Haskell *)
atom_decl var
atom_decl cvar
atom_decl tvar
+declare [[STEPS = 14]]
+
nominal_datatype tkind =
KStar
| KFun "tkind" "tkind"
@@ -86,7 +85,6 @@
| "bv_cvs CvsNil = []"
| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
-
lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
--- a/Nominal/Ex/Ex1rec.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Ex/Ex1rec.thy Wed Jun 23 15:40:00 2010 +0100
@@ -2,10 +2,9 @@
imports "../NewParser"
begin
-atom_decl name
+declare [[STEPS = 9]]
-ML {* val _ = cheat_supp_eq := true *}
-ML {* val _ = cheat_equivp := true *}
+atom_decl name
nominal_datatype lam =
Var "name"
@@ -19,6 +18,9 @@
where
"bi (Bp x t) = {atom x}"
+
+thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros
+
thm lam_bp.fv
thm lam_bp.eq_iff[no_vars]
thm lam_bp.bn
--- a/Nominal/Ex/Ex2.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Ex/Ex2.thy Wed Jun 23 15:40:00 2010 +0100
@@ -3,6 +3,7 @@
begin
text {* example 2 *}
+declare [[STEPS = 9]]
atom_decl name
@@ -10,17 +11,23 @@
Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm" bind_set x in t
-| Let p::"pat" "trm" t::"trm" bind "f p" in t
+| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
and pat =
PN
| PS "name"
| PD "name" "name"
binder
- f::"pat \<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/LF.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Ex/LF.thy Wed Jun 23 15:40:00 2010 +0100
@@ -2,21 +2,23 @@
imports "../NewParser"
begin
+declare [[STEPS = 9]]
+
atom_decl name
atom_decl ident
nominal_datatype kind =
Type
- | KPi "ty" n::"name" k::"kind" bind_set n in k
+ | KPi "ty" n::"name" k::"kind" bind n in k
and ty =
TConst "ident"
| TApp "ty" "trm"
- | TPi "ty" n::"name" t::"ty" bind_set n in t
+ | TPi "ty" n::"name" t::"ty" bind n in t
and trm =
Const "ident"
| Var "name"
| App "trm" "trm"
- | Lam "ty" n::"name" t::"trm" bind_set n in t
+ | Lam "ty" n::"name" t::"trm" bind n in t
thm kind_ty_trm.supp
--- a/Nominal/Ex/Lambda.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Ex/Lambda.thy Wed Jun 23 15:40:00 2010 +0100
@@ -3,11 +3,12 @@
begin
atom_decl name
+declare [[STEPS = 9]]
nominal_datatype lam =
Var "name"
| App "lam" "lam"
-| Lam x::"name" l::"lam" bind_set x in l
+| Lam x::"name" l::"lam" bind x in l
thm lam.fv
thm lam.supp
--- a/Nominal/Ex/SingleLet.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy Wed Jun 23 15:40:00 2010 +0100
@@ -4,20 +4,23 @@
atom_decl name
+declare [[STEPS = 14]]
+
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
-
+| Let a::"assg" t::"trm" bind_set "bn a" in t
+| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2
+| Bar x::"name" y::"name" t::"trm" bind y x in t x y
+| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2
and assg =
- As "name" "trm"
+ As "name" x::"name" t::"trm" bind x in t
binder
bn::"assg \<Rightarrow> atom set"
where
- "bn (As x t) = {atom x}"
+ "bn (As x y t) = {atom x}"
-ML {* Inductive.the_inductive *}
thm trm_assg.fv
thm trm_assg.supp
thm trm_assg.eq_iff
@@ -27,8 +30,10 @@
thm trm_assg.inducts
thm trm_assg.distinct
ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
-(* thm trm_assg.fv[simplified trm_assg.supp(1-2)] *)
+(* TEMPORARY
+thm trm_assg.fv[simplified trm_assg.supp(1-2)]
+*)
end
--- a/Nominal/Ex/Test.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Ex/Test.thy Wed Jun 23 15:40:00 2010 +0100
@@ -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/Ex/TypeSchemes.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy Wed Jun 23 15:40:00 2010 +0100
@@ -5,6 +5,7 @@
section {*** Type Schemes ***}
atom_decl name
+declare [[STEPS = 9]]
nominal_datatype ty =
Var "name"
@@ -12,6 +13,15 @@
and tys =
All xs::"name fset" ty::"ty" bind_res xs in ty
+nominal_datatype ty2 =
+ Var2 "name"
+| Fun2 "ty2" "ty2"
+
+(* PROBLEM: this only works once the type is defined
+nominal_datatype tys2 =
+ All2 xs::"name fset" ty::"ty2" bind_res xs in ty
+*)
+
lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
--- a/Nominal/FSet.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/FSet.thy Wed Jun 23 15:40:00 2010 +0100
@@ -1410,267 +1410,6 @@
unfolding fset_to_set_trans
by (rule card_Diff_subset_Int) (fold inter_set, rule finite_fset)
-
-ML {*
-fun dest_fsetT (Type (@{type_name fset}, [T])) = T
- | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
-*}
-
-ML {*
-open Quotient_Info;
-
-exception LIFT_MATCH of string
-
-
-
-(*** Aggregate Rep/Abs Function ***)
-
-
-(* The flag RepF is for types in negative position; AbsF is for types
- in positive position. Because of this, function types need to be
- treated specially, since there the polarity changes.
-*)
-
-datatype flag = AbsF | RepF
-
-fun negF AbsF = RepF
- | negF RepF = AbsF
-
-fun is_identity (Const (@{const_name "id"}, _)) = true
- | is_identity _ = false
-
-fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
-
-fun mk_fun_compose flag (trm1, trm2) =
- case flag of
- AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
- | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
-
-fun get_mapfun ctxt s =
-let
- val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
- val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
-in
- Const (mapfun, dummyT)
-end
-
-(* makes a Free out of a TVar *)
-fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
-
-(* produces an aggregate map function for the
- rty-part of a quotient definition; abstracts
- over all variables listed in vs (these variables
- correspond to the type variables in rty)
-
- for example for: (?'a list * ?'b)
- it produces: %a b. prod_map (map a) b
-*)
-fun mk_mapfun ctxt vs rty =
-let
- val vs' = map (mk_Free) vs
-
- fun mk_mapfun_aux rty =
- case rty of
- TVar _ => mk_Free rty
- | Type (_, []) => mk_identity rty
- | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
- | _ => raise LIFT_MATCH "mk_mapfun (default)"
-in
- fold_rev Term.lambda vs' (mk_mapfun_aux rty)
-end
-
-(* looks up the (varified) rty and qty for
- a quotient definition
-*)
-fun get_rty_qty ctxt s =
-let
- val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
- val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
-in
- (#rtyp qdata, #qtyp qdata)
-end
-
-(* takes two type-environments and looks
- up in both of them the variable v, which
- must be listed in the environment
-*)
-fun double_lookup rtyenv qtyenv v =
-let
- val v' = fst (dest_TVar v)
-in
- (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
-end
-
-(* matches a type pattern with a type *)
-fun match ctxt err ty_pat ty =
-let
- val thy = ProofContext.theory_of ctxt
-in
- Sign.typ_match thy (ty_pat, ty) Vartab.empty
- handle MATCH_TYPE => err ctxt ty_pat ty
-end
-
-(* produces the rep or abs constant for a qty *)
-fun absrep_const flag ctxt qty_str =
-let
- val qty_name = Long_Name.base_name qty_str
- val qualifier = Long_Name.qualifier qty_str
-in
- case flag of
- AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
- | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
-end
-
-(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
-fun absrep_const_chk flag ctxt qty_str =
- Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
-
-fun absrep_match_err ctxt ty_pat ty =
-let
- val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
- val ty_str = Syntax.string_of_typ ctxt ty
-in
- raise LIFT_MATCH (space_implode " "
- ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
-end
-
-
-(** generation of an aggregate absrep function **)
-
-(* - In case of equal types we just return the identity.
-
- - In case of TFrees we also return the identity.
-
- - In case of function types we recurse taking
- the polarity change into account.
-
- - If the type constructors are equal, we recurse for the
- arguments and build the appropriate map function.
-
- - If the type constructors are unequal, there must be an
- instance of quotient types:
-
- - we first look up the corresponding rty_pat and qty_pat
- from the quotient definition; the arguments of qty_pat
- must be some distinct TVars
- - we then match the rty_pat with rty and qty_pat with qty;
- if matching fails the types do not correspond -> error
- - the matching produces two environments; we look up the
- assignments for the qty_pat variables and recurse on the
- assignments
- - we prefix the aggregate map function for the rty_pat,
- which is an abstraction over all type variables
- - finally we compose the result with the appropriate
- absrep function in case at least one argument produced
- a non-identity function /
- otherwise we just return the appropriate absrep
- function
-
- The composition is necessary for types like
-
- ('a list) list / ('a foo) foo
-
- The matching is necessary for types like
-
- ('a * 'a) list / 'a bar
-
- The test is necessary in order to eliminate superfluous
- identity maps.
-*)
-
-fun absrep_fun flag ctxt (rty, qty) =
- if rty = qty
- then mk_identity rty
- else
- case (rty, qty) of
- (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
- let
- val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
- val arg2 = absrep_fun flag ctxt (ty2, ty2')
- in
- list_comb (get_mapfun ctxt "fun", [arg1, arg2])
- end
- | (Type (s, tys), Type (s', tys')) =>
- if s = s'
- then
- let
- val args = map (absrep_fun flag ctxt) (tys ~~ tys')
- in
- list_comb (get_mapfun ctxt s, args)
- end
- else
- let
- val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
- val rtyenv = match ctxt absrep_match_err rty_pat rty
- val qtyenv = match ctxt absrep_match_err qty_pat qty
- val args_aux = map (double_lookup rtyenv qtyenv) vs
- val args = map (absrep_fun flag ctxt) args_aux
- val map_fun = mk_mapfun ctxt vs rty_pat
- val result = list_comb (map_fun, args)
- in
- (*if forall is_identity args
- then absrep_const flag ctxt s'
- else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
- end
- | (TFree x, TFree x') =>
- if x = x'
- then mk_identity rty
- else raise (LIFT_MATCH "absrep_fun (frees)")
- | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
- | _ => raise (LIFT_MATCH "absrep_fun (default)")
-
-
-*}
-
-ML {*
-let
-val parser = Args.context -- Scan.lift Args.name_source
-fun typ_pat (ctxt, str) =
-str |> Syntax.parse_typ ctxt
-|> ML_Syntax.print_typ
-|> ML_Syntax.atomic
-in
-ML_Antiquote.inline "typ_pat" (parser >> typ_pat)
-end
-*}
-
-ML {*
- mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
- |> Syntax.check_term @{context}
- |> fastype_of
- |> Syntax.string_of_typ @{context}
- |> tracing
-*}
-
-ML {*
- mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
- |> Syntax.check_term @{context}
- |> Syntax.string_of_term @{context}
- |> warning
-*}
-
-ML {*
- mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
- |> Syntax.check_term @{context}
-*}
-
-term prod_fun
-term map
-term fun_map
-term "op o"
-
-ML {*
- absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})
- |> Syntax.string_of_term @{context}
- |> writeln
-*}
-
-lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}"
-apply(auto simp add: mem_def)
-done
-
lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)"
apply rule
apply (rule ball_reg_right)
--- a/Nominal/Lift.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Lift.thy Wed Jun 23 15:40:00 2010 +0100
@@ -2,10 +2,9 @@
imports "../Nominal-General/Nominal2_Atoms"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Nominal2_Supp"
- "Abs" "Perm" "Equivp" "Rsp"
+ "Abs" "Perm" "Rsp"
begin
-
ML {*
fun define_quotient_types binds tys alphas equivps ctxt =
let
--- a/Nominal/NewAlpha.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/NewAlpha.thy Wed Jun 23 15:40:00 2010 +0100
@@ -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 Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/NewFv.thy Wed Jun 23 15:40:00 2010 +0100
@@ -4,38 +4,42 @@
begin
ML {*
-(* binding modes *)
+(* binding modes and binding clauses *)
-datatype bmodes =
- BEmy of int
-| BLst of ((term option * int) list) * (int list)
-| BSet of ((term option * int) list) * (int list)
-| BRes of ((term option * int) list) * (int list)
+datatype bmode = Lst | Res | Set
+
+datatype bclause =
+ BC of bmode * (term option * int) list * int list
*}
ML {*
-fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
-
-val noatoms = @{term "{} :: atom set"};
+fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
+ | mk_diff (t1, @{term "{}::atom set"}) = t1
+ | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
-fun mk_union sets =
- fold (fn a => fn b =>
- if a = noatoms then b else
- if b = noatoms then a else
- if a = b then a else
- HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
+fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
+ | mk_union (t1 , @{term "{}::atom set"}) = t1
+ | mk_union (@{term "{}::atom set"}, t2) = t2
+ | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2)
+
+fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
*}
ML {*
-fun is_atom thy ty =
- Sign.of_sort thy (ty, @{sort at_base})
+fun is_atom ctxt ty =
+ Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
-fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
+fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
| is_atom_set _ _ = false;
-fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
+fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
| is_atom_fset _ _ = false;
+fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
+ | is_atom_list _ _ = false
+*}
+
+ML {*
fun mk_atom_set t =
let
val ty = fastype_of t;
@@ -55,23 +59,6 @@
fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
end;
-fun mk_diff a b =
- if b = noatoms then a else
- if b = a then noatoms else
- HOLogic.mk_binop @{const_name minus} (a, b);
-*}
-
-ML {*
-fun is_atom_list (Type (@{type_name list}, [T])) = true
- | is_atom_list _ = false
-*}
-
-ML {*
-fun dest_listT (Type (@{type_name list}, [T])) = T
- | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
-*}
-
-ML {*
fun mk_atom_list t =
let
val ty = fastype_of t;
@@ -83,193 +70,170 @@
*}
ML {*
-fun setify thy t =
+fun setify ctxt t =
let
val ty = fastype_of t;
in
- if is_atom thy ty
- then mk_singleton_atom t
- else if is_atom_set thy ty
+ if is_atom ctxt ty
+ then HOLogic.mk_set @{typ atom} [mk_atom t]
+ else if is_atom_set ctxt ty
then mk_atom_set t
- else if is_atom_fset thy ty
+ else if is_atom_fset ctxt ty
then mk_atom_fset t
else error ("setify" ^ (PolyML.makestring (t, ty)))
end
*}
ML {*
-fun listify thy t =
+fun listify ctxt t =
let
val ty = fastype_of t;
in
- if is_atom thy ty
+ if is_atom ctxt ty
then HOLogic.mk_list @{typ atom} [mk_atom t]
- else if is_atom_list ty
+ else if is_atom_list ctxt ty
then mk_atom_set t
else error "listify"
end
*}
ML {*
-fun set x =
+fun to_set x =
if fastype_of x = @{typ "atom list"}
then @{term "set::atom list \<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)
-
- val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_bn_eqs)))
-
- fun pat_completeness_auto ctxt =
- Pat_Completeness.pat_completeness_tac ctxt 1
- THEN auto_tac (clasimpset_of ctxt)
+ fun pat_completeness_auto lthy =
+ Pat_Completeness.pat_completeness_tac lthy 1
+ THEN auto_tac (clasimpset_of lthy)
fun prove_termination lthy =
Function.prove_termination NONE
@@ -292,21 +256,8 @@
end
*}
-(**************************************************)
-datatype foo =
- C1 nat
-| C2 foo int
-(*
-ML {*
-fun mk_body descr sorts fv_ty_map dtyp =
-let
- val nth_dtyp_constr_tys descr sorts
-in
- true
-end
-*}
-*)
+
end
--- a/Nominal/NewParser.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/NewParser.thy Wed Jun 23 15:40:00 2010 +0100
@@ -2,9 +2,15 @@
imports "../Nominal-General/Nominal2_Base"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Nominal2_Supp"
- "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp" "Lift"
+ "Perm" "Tacs" "Lift" "Equivp"
begin
+(* TODO
+
+ we need to also export a cases-rule for nominal datatypes
+ size function
+*)
+
section{* Interface for nominal_datatype *}
@@ -139,7 +145,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 +160,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 +170,23 @@
appends of elements; in case of recursive calls it retruns also the applied
bn function *)
ML {*
-fun strip_bn_fun t =
- case t of
- Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
- | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
- | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
- (i, NONE) :: strip_bn_fun y
- | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
- (i, NONE) :: strip_bn_fun y
- | Const (@{const_name bot}, _) => []
- | Const (@{const_name Nil}, _) => []
- | (f as Free _) $ Bound i => [(i, SOME f)]
- | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t))
+fun strip_bn_fun lthy args t =
+let
+ fun aux t =
+ case t of
+ Const (@{const_name sup}, _) $ l $ r => aux l @ aux r
+ | Const (@{const_name append}, _) $ l $ r => aux l @ aux r
+ | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+ (find_index (equal x) args, NONE) :: aux y
+ | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+ (find_index (equal x) args, NONE) :: aux y
+ | Const (@{const_name bot}, _) => []
+ | Const (@{const_name Nil}, _) => []
+ | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)]
+ | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t))
+in
+ aux t
+end
*}
ML {*
@@ -187,23 +195,21 @@
*}
ML {*
-fun prep_bn lthy dt_names dts eqs =
+fun prep_bn_info lthy dt_names dts eqs =
let
fun aux eq =
let
val (lhs, rhs) = eq
- |> strip_qnt_body "all"
|> HOLogic.dest_Trueprop
|> HOLogic.dest_eq
val (bn_fun, [cnstr]) = strip_comb lhs
- val (_, ty) = dest_Free bn_fun
+ val (_, ty) = dest_Const bn_fun
val (ty_name, _) = dest_Type (domain_type ty)
val dt_index = find_index (fn x => x = ty_name) dt_names
- val (cnstr_head, cnstr_args) = strip_comb cnstr
- val rhs_elements = strip_bn_fun rhs
- val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
+ val (cnstr_head, cnstr_args) = strip_comb cnstr
+ val rhs_elements = strip_bn_fun lthy cnstr_args rhs
in
- (dt_index, (bn_fun, (cnstr_head, included)))
+ (dt_index, (bn_fun, (cnstr_head, rhs_elements)))
end
fun order dts i ts =
let
@@ -219,9 +225,9 @@
val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered'
val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
- val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))
+ (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*)
(*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*)
- val _ = tracing ("ordered'\n" ^ @{make_string} ordered')
+ (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*)
in
ordered'
end
@@ -254,108 +260,42 @@
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
*}
-lemma equivp_hack: "equivp x"
-sorry
ML {*
-fun equivp_hack ctxt rel =
-let
- val thy = ProofContext.theory_of ctxt
- val ty = domain_type (fastype_of rel)
- val cty = ctyp_of thy ty
- val ct = cterm_of thy rel
-in
- Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
-end
+fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy =
+ if null raw_bn_funs
+ then ([], [], [], [], lthy)
+ else
+ let
+ val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
+ Function_Common.default_config (pat_completeness_simp constr_thms) lthy
+
+ val (info, lthy2) = prove_termination (Local_Theory.restore lthy1)
+ val {fs, simps, inducts, ...} = info;
+
+ val raw_bn_induct = (the inducts)
+ val raw_bn_eqs = the simps
+
+ val raw_bn_info =
+ prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
+ in
+ (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
+ end
*}
-ML {* val cheat_equivp = Unsynchronized.ref false *}
+
+
ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
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,29 +311,33 @@
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 _ = warning "Definition of raw datatypes";
+ val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
+ if get_STEPS lthy > 0
+ then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
else raise TEST lthy
- val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names)
+ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
val {descr, sorts, ...} = dtinfo
val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr
val all_full_tnames = map (fn (_, (n, _, _)) => n) descr
- val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames
+ val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_full_tnames
val inject_thms = flat (map #inject dtinfos);
val distinct_thms = flat (map #distinct dtinfos);
+ val constr_thms = inject_thms @ distinct_thms
val rel_dtinfos = List.take (dtinfos, (length dts));
- val rel_distinct = map #distinct rel_dtinfos; (* thm list list *)
+ val raw_constrs_distinct = (map #distinct rel_dtinfos);
val induct_thm = #induct dtinfo;
val exhaust_thms = map #exhaust dtinfos;
(* definitions of raw permutations *)
- val ((perms, raw_perm_defs, raw_perm_simps), lthy2) =
- if get_STEPS lthy1 > 2
- then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
- else raise TEST lthy1
+ val _ = warning "Definition of raw permutations";
+ val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) =
+ if get_STEPS lthy0 > 1
+ then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0
+ else raise TEST lthy0
(* noting the raw permutations as eqvt theorems *)
val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
@@ -403,54 +347,112 @@
val thy_name = Context.theory_name thy
(* definition of raw fv_functions *)
+ val _ = warning "Definition of raw fv-functions";
val lthy3 = Theory_Target.init NONE thy;
- val raw_bn_funs = map (fn (f, _, _) => f) raw_bns;
- val (fv, fvbn, fv_def, lthy3a) =
- if get_STEPS lthy2 > 3
- then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3
+ val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
+ if get_STEPS lthy3 > 2
+ then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
else raise TEST lthy3
-
+
+ val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) =
+ if get_STEPS lthy3a > 3
+ then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a
+ else raise TEST lthy3a
+
(* definition of raw alphas *)
- val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
- if get_STEPS lthy > 4
- then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a
- else raise TEST lthy3a
-
- val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
+ val _ = warning "Definition of alphas";
+ val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
+ if get_STEPS lthy3b > 4
+ then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b
+ else raise TEST lthy3b
- val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
- val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
- val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
- val bns = raw_bn_funs ~~ bn_nos;
- val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
- (rel_distinct ~~ alpha_ts_nobn));
- val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
- ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
-
+ (* definition of alpha-distinct lemmas *)
+ val _ = warning "Distinct theorems";
+ val (alpha_distincts, alpha_bn_distincts) =
+ mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info
+
(* definition of raw_alpha_eq_iff lemmas *)
- val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
- val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
- val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);
+ val _ = warning "Eq-iff theorems";
+ val alpha_eq_iff =
+ if get_STEPS lthy > 5
+ then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
+ else raise TEST lthy4
+
+ (* proving equivariance lemmas for bns, fvs and alpha *)
+ val _ = warning "Proving equivariance";
+ val bn_eqvt =
+ if get_STEPS lthy > 6
+ then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4
+ else raise TEST lthy4
- (* proving equivariance lemmas *)
- val _ = warning "Proving equivariance";
- val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4
- val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5
- val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
+ (* noting the bn_eqvt lemmas in a temprorary theory *)
+ val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+ val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4)
+
+ val fv_eqvt =
+ if get_STEPS lthy > 7
+ then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs)
+ (Local_Theory.restore lthy_tmp)
+ else raise TEST lthy4
+
+ val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
+
+ val (alpha_eqvt, lthy_tmp'') =
+ if get_STEPS lthy > 8
+ then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy_tmp'
+ else raise TEST lthy4
(* proving alpha equivalence *)
- val _ = warning "Proving equivalence";
- val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
- val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
- val 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;
+ val _ = warning "Proving equivalence"
+
+ val alpha_refl_thms =
+ if get_STEPS lthy > 9
+ then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy_tmp''
+ else raise TEST lthy4
+
+ val alpha_sym_thms =
+ if get_STEPS lthy > 10
+ then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp''
+ else raise TEST lthy4
+
+ val alpha_trans_thms =
+ if get_STEPS lthy > 11
+ then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms)
+ alpha_intros alpha_induct alpha_cases lthy_tmp''
+ else raise TEST lthy4
+
+ val alpha_equivp_thms =
+ if get_STEPS lthy > 12
+ then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy_tmp''
+ else raise TEST lthy4
+
+ (* proving alpha implies alpha_bn *)
+ val _ = warning "Proving alpha implies bn"
+
+ val alpha_bn_imp_thms =
+ if get_STEPS lthy > 13
+ then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy_tmp''
+ else raise TEST lthy4
+
+ val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms))
+ val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms))
+ val _ = tracing ("alpha_refl\n" ^
+ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms))
+ val _ = tracing ("alpha_bn_imp\n" ^
+ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms))
+ val _ = tracing ("alpha_equivp\n" ^
+ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_equivp_thms))
+
+ (* old stuff *)
+ val _ =
+ if get_STEPS lthy > 14
+ then true else raise TEST 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_thms 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 +461,50 @@
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 bn_nos = map (fn (_, i, _) => i) raw_bn_info;
+ val bns = raw_bn_funs ~~ bn_nos;
+
+ 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_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
+
+ 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_thms 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 @ alpha_refl_thms @ 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 +518,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 +548,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 +648,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 +679,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 +694,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 +724,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 Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy Wed Jun 23 15:40:00 2010 +0100
@@ -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 Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Perm.thy Wed Jun 23 15:40:00 2010 +0100
@@ -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 Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/ROOT.ML Wed Jun 23 15:40:00 2010 +0100
@@ -1,5 +1,6 @@
quick_and_dirty := true;
+(*
no_document use_thys
["Ex/Lambda",
"Ex/LF",
@@ -14,6 +15,7 @@
"Ex/ExPS3",
"Ex/ExPS7",
"Ex/CoreHaskell",
- "Ex/Test",
- "Manual/Term4"
+ "Ex/Test"(*,
+ "Manual/Term4"*)
];
+*)
\ No newline at end of file
--- a/Nominal/Tacs.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Nominal/Tacs.thy Wed Jun 23 15:40:00 2010 +0100
@@ -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 Wed Jun 23 15:40:00 2010 +0100
@@ -0,0 +1,639 @@
+(* Title: nominal_dt_alpha.ML
+ Author: Cezary Kaliszyk
+ Author: Christian Urban
+
+ Definitions and proofs for the alpha-relations.
+*)
+
+signature NOMINAL_DT_ALPHA =
+sig
+ val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
+ bclause list list list -> term list -> Proof.context ->
+ term list * term list * thm list * thm list * thm * local_theory
+
+ val mk_alpha_distincts: Proof.context -> thm list -> thm list list ->
+ term list -> term list -> bn_info -> thm list * thm list
+
+ val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list
+
+ val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
+ val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
+ val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
+ val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list
+ val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
+end
+
+structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
+struct
+
+fun lookup xs x = the (AList.lookup (op=) xs x)
+fun group xs = AList.group (op=) xs
+
+(** 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 [lookup 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 (lookup 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 (lookup 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) => [lookup 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 = lookup 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
+
+
+
+(** reflexivity proof for the alphas **)
+
+val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
+
+fun cases_tac intros =
+let
+ val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
+
+ val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac
+
+ val bound_tac =
+ EVERY' [ rtac exi_zero,
+ resolve_tac @{thms alpha_gen_refl},
+ asm_full_simp_tac (HOL_ss addsimps prod_simps) ]
+in
+ REPEAT o FIRST' [rtac @{thm conjI},
+ resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]]
+end
+
+fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt =
+let
+ val arg_tys =
+ alpha_trms
+ |> map fastype_of
+ |> map domain_type
+ val arg_bn_tys =
+ alpha_bns
+ |> map fastype_of
+ |> map domain_type
+ val arg_names = Datatype_Prop.make_tnames arg_tys
+ val arg_bn_names = map (lookup (arg_tys ~~ arg_names)) arg_bn_tys
+ val args = map Free (arg_names ~~ arg_tys)
+ val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys)
+ val goal =
+ group ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms))
+ |> map (fn (ar, cnsts) => map (fn c => c $ ar $ ar) cnsts)
+ |> map (foldr1 HOLogic.mk_conj)
+ |> foldr1 HOLogic.mk_conj
+ |> HOLogic.mk_Trueprop
+in
+ Goal.prove ctxt arg_names [] goal
+ (fn {context, ...} =>
+ HEADGOAL (DETERM o (rtac raw_dt_induct) THEN_ALL_NEW cases_tac alpha_intros))
+ |> Datatype_Aux.split_conj_thm
+ |> map Datatype_Aux.split_conj_thm
+ |> flat
+end
+
+
+
+(** symmetry proof for the alphas **)
+
+val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"
+ by (erule exE, rule_tac x="-p" in exI, auto)}
+
+(* for premises that contain binders *)
+fun prem_bound_tac pred_names ctxt =
+let
+ fun trans_prem_tac pred_names ctxt =
+ SUBPROOF (fn {prems, context, ...} =>
+ let
+ val prems' = map (transform_prem1 context pred_names) prems
+ in
+ resolve_tac prems' 1
+ end) ctxt
+ val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas}
+in
+ EVERY'
+ [ etac exi_neg,
+ resolve_tac @{thms alpha_gen_sym_eqvt},
+ asm_full_simp_tac (HOL_ss addsimps prod_simps),
+ Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
+ trans_prem_tac pred_names ctxt ]
+end
+
+fun prove_sym_tac pred_names intros induct ctxt =
+let
+ val prem_eq_tac = rtac @{thm sym} THEN' atac
+ val prem_unbound_tac = atac
+
+ val prem_cases_tacs = FIRST'
+ [prem_eq_tac, prem_unbound_tac, prem_bound_tac pred_names ctxt]
+in
+ HEADGOAL (rtac induct THEN_ALL_NEW
+ (resolve_tac intros THEN_ALL_NEW prem_cases_tacs))
+end
+
+fun prep_sym_goal alpha_trm (arg1, arg2) =
+let
+ val lhs = alpha_trm $ arg1 $ arg2
+ val rhs = alpha_trm $ arg2 $ arg1
+in
+ HOLogic.mk_imp (lhs, rhs)
+end
+
+fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt =
+let
+ val alpha_names = map (fst o dest_Const) alpha_trms
+ val arg_tys =
+ alpha_trms
+ |> map fastype_of
+ |> map domain_type
+ val (arg_names1, (arg_names2, ctxt')) =
+ ctxt
+ |> Variable.variant_fixes (replicate (length arg_tys) "x")
+ ||> Variable.variant_fixes (replicate (length arg_tys) "y")
+ val args1 = map Free (arg_names1 ~~ arg_tys)
+ val args2 = map Free (arg_names2 ~~ arg_tys)
+ val goal = HOLogic.mk_Trueprop
+ (foldr1 HOLogic.mk_conj (map2 prep_sym_goal alpha_trms (args1 ~~ args2)))
+in
+ Goal.prove ctxt' [] [] goal
+ (fn {context,...} => prove_sym_tac alpha_names alpha_intros alpha_induct context)
+ |> singleton (ProofContext.export ctxt' ctxt)
+ |> Datatype_Aux.split_conj_thm
+ |> map (fn th => zero_var_indexes (th RS mp))
+end
+
+
+
+(** transitivity proof for alphas **)
+
+(* applies cases rules and resolves them with the last premise *)
+fun ecases_tac cases =
+ Subgoal.FOCUS (fn {prems, ...} =>
+ HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
+
+fun aatac pred_names =
+ SUBPROOF (fn {prems, context, ...} =>
+ HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
+
+(* instantiates exI with the permutation p + q *)
+val perm_inst_tac =
+ Subgoal.FOCUS (fn {params, ...} =>
+ let
+ val (p, q) = pairself snd (last2 params)
+ val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q]
+ val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
+ in
+ HEADGOAL (rtac exi_inst)
+ end)
+
+fun non_trivial_cases_tac pred_names intros ctxt =
+let
+ val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
+in
+ resolve_tac intros
+ THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN'
+ TRY o EVERY' (* if binders are present *)
+ [ etac @{thm exE},
+ etac @{thm exE},
+ perm_inst_tac ctxt,
+ resolve_tac @{thms alpha_trans_eqvt},
+ atac,
+ aatac pred_names ctxt,
+ Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
+ asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
+end
+
+fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt =
+let
+ fun all_cases ctxt =
+ asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms)
+ THEN' TRY o non_trivial_cases_tac pred_names intros ctxt
+in
+ HEADGOAL (rtac induct THEN_ALL_NEW
+ EVERY' [ rtac @{thm allI}, rtac @{thm impI},
+ ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ])
+end
+
+fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
+let
+ val lhs = alpha_trm $ arg1 $ arg2
+ val mid = alpha_trm $ arg2 $ (Bound 0)
+ val rhs = alpha_trm $ arg1 $ (Bound 0)
+in
+ HOLogic.mk_imp (lhs,
+ HOLogic.all_const arg_ty $ Abs ("z", arg_ty,
+ HOLogic.mk_imp (mid, rhs)))
+end
+
+val norm = @{lemma "A --> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}
+
+fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =
+let
+ val alpha_names = map (fst o dest_Const) alpha_trms
+ val arg_tys =
+ alpha_trms
+ |> map fastype_of
+ |> map domain_type
+ val (arg_names1, (arg_names2, ctxt')) =
+ ctxt
+ |> Variable.variant_fixes (replicate (length arg_tys) "x")
+ ||> Variable.variant_fixes (replicate (length arg_tys) "y")
+ val args1 = map Free (arg_names1 ~~ arg_tys)
+ val args2 = map Free (arg_names2 ~~ arg_tys)
+ val goal = HOLogic.mk_Trueprop
+ (foldr1 HOLogic.mk_conj (map2 prep_trans_goal alpha_trms (args1 ~~ args2 ~~ arg_tys)))
+in
+ Goal.prove ctxt' [] [] goal
+ (fn {context,...} =>
+ prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_induct alpha_cases context)
+ |> singleton (ProofContext.export ctxt' ctxt)
+ |> Datatype_Aux.split_conj_thm
+ |> map (fn th => zero_var_indexes (th RS norm))
+end
+
+(* proves the equivp predicate for all alphas *)
+
+val equivp_intro =
+ @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y z. R x y --> R y z --> R x z|] ==> equivp R"
+ by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)}
+
+fun raw_prove_equivp alphas refl symm trans ctxt =
+let
+ val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
+ val refl' = map atomize refl
+ val symm' = map atomize symm
+ val trans' = map atomize trans
+ fun prep_goal t =
+ HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t)
+in
+ Goal.prove_multi ctxt [] [] (map prep_goal alphas)
+ (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac equivp_intro THEN'
+ RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
+end
+
+
+(* proves that alpha_raw implies alpha_bn *)
+
+fun is_true @{term "Trueprop True"} = true
+ | is_true _ = false
+
+fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt =
+ SUBPROOF (fn {prems, context, ...} =>
+ let
+ val prems' = flat (map Datatype_Aux.split_conj_thm prems)
+ val prems'' = map (transform_prem1 context pred_names) prems'
+ in
+ HEADGOAL
+ (REPEAT_ALL_NEW
+ (FIRST' [ rtac @{thm TrueI},
+ rtac @{thm conjI},
+ resolve_tac prems',
+ resolve_tac prems'',
+ resolve_tac alpha_intros ]))
+ end) ctxt
+
+fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt =
+let
+ val alpha_names = map (fst o dest_Const) alpha_trms
+
+ val arg_tys =
+ alpha_trms
+ |> map fastype_of
+ |> map domain_type
+ val arg_bn_tys =
+ alpha_bns
+ |> map fastype_of
+ |> map domain_type
+ val (arg_names1, (arg_names2, ctxt')) =
+ ctxt
+ |> Variable.variant_fixes (replicate (length arg_tys) "x")
+ ||> Variable.variant_fixes (replicate (length arg_tys) "y")
+ val arg_bn_names1 = map (lookup (arg_tys ~~ arg_names1)) arg_bn_tys
+ val arg_bn_names2 = map (lookup (arg_tys ~~ arg_names2)) arg_bn_tys
+ val args1 = map Free (arg_names1 ~~ arg_tys)
+ val args2 = map Free (arg_names2 ~~ arg_tys)
+ val arg_bns1 = map Free (arg_bn_names1 ~~ arg_bn_tys)
+ val arg_bns2 = map Free (arg_bn_names2 ~~ arg_bn_tys)
+
+ val alpha_bn_trms = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_bns (arg_bns1 ~~ arg_bns2)
+ val true_trms = map (K @{term True}) arg_tys
+
+ val goal_rhs =
+ group ((arg_bn_tys ~~ alpha_bn_trms) @ (arg_tys ~~ true_trms))
+ |> map snd
+ |> map (foldr1 HOLogic.mk_conj)
+
+ val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_trms (args1 ~~ args2)
+ val goal_rest = map (fn t => HOLogic.mk_imp (t, @{term "True"})) alpha_bn_trms
+
+ val goal =
+ (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs) @ goal_rest
+ |> foldr1 HOLogic.mk_conj
+ |> HOLogic.mk_Trueprop
+in
+ Goal.prove ctxt' [] [] goal
+ (fn {context, ...} =>
+ HEADGOAL (DETERM o (rtac alpha_induct)
+ THEN_ALL_NEW (raw_prove_bn_imp_tac alpha_names alpha_intros context)))
+ |> singleton (ProofContext.export ctxt' ctxt)
+ |> Datatype_Aux.split_conj_thm
+ |> map (fn th => zero_var_indexes (th RS mp))
+ |> map Datatype_Aux.split_conj_thm
+ |> flat
+ |> filter_out (is_true o concl_of)
+end
+
+end (* structure *)
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML Wed Jun 23 15:40:00 2010 +0100
@@ -0,0 +1,299 @@
+(* 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 dest_fsetT (Type (@{type_name fset}, [T])) = T
+ | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+
+fun mk_atom_fset t =
+let
+ val ty = fastype_of t;
+ val atom_ty = dest_fsetT ty --> @{typ "atom"};
+ val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
+ val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
+in
+ fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+end
+
+fun mk_atom_list t =
+let
+ val ty = fastype_of t;
+ val atom_ty = dest_listT ty --> @{typ atom};
+ val map_ty = atom_ty --> ty --> @{typ "atom list"};
+in
+ Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
+end
+
+(* functions that coerces singletons, sets and fsets of concrete atoms
+ into sets of general atoms *)
+fun setify ctxt t =
+let
+ val ty = fastype_of t;
+in
+ if is_atom ctxt ty
+ then HOLogic.mk_set @{typ atom} [mk_atom t]
+ else if is_atom_set ctxt ty
+ then mk_atom_set t
+ else if is_atom_fset ctxt ty
+ then mk_atom_fset t
+ else raise TERM ("setify", [t])
+end
+
+(* functions that coerces singletons and lists of concrete atoms
+ into lists of general atoms *)
+fun listify ctxt t =
+let
+ val ty = fastype_of t;
+in
+ if is_atom ctxt ty
+ then HOLogic.mk_list @{typ atom} [mk_atom t]
+ else if is_atom_list ctxt ty
+ then mk_atom_set t
+ else raise TERM ("listify", [t])
+end
+
+(* coerces a list into a set *)
+fun to_set t =
+ if fastype_of t = @{typ "atom list"}
+ then @{term "set::atom list => atom set"} $ t
+ else t
+
+
+(** functions that construct the equations for fv and fv_bn **)
+
+fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
+let
+ fun mk_fv_body fv_map args i =
+ let
+ val arg = nth args i
+ val ty = fastype_of arg
+ in
+ case AList.lookup (op=) fv_map ty of
+ NONE => mk_supp arg
+ | SOME fv => fv $ arg
+ end
+
+ fun mk_fv_binder lthy fv_bn_map args (bn_option, i) =
+ let
+ val arg = nth args i
+ in
+ case bn_option of
+ NONE => (setify lthy arg, @{term "{}::atom set"})
+ | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
+ end
+
+ val t1 = map (mk_fv_body fv_map args) bodies
+ val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
+in
+ fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
+end
+
+(* in case of fv_bn we have to treat the case special, where an
+ "empty" binding clause is given *)
+fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
+let
+ fun mk_fv_bn_body fv_map fv_bn_map bn_args args i =
+ let
+ val arg = nth args i
+ val ty = fastype_of arg
+ in
+ case AList.lookup (op=) bn_args i of
+ NONE => (case (AList.lookup (op=) fv_map ty) of
+ NONE => mk_supp arg
+ | SOME fv => fv $ arg)
+ | SOME (NONE) => @{term "{}::atom set"}
+ | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
+ end
+in
+ case bclause of
+ BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
+ | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
+end
+
+fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses =
+let
+ val arg_names = Datatype_Prop.make_tnames arg_tys
+ val args = map Free (arg_names ~~ arg_tys)
+ val fv = the (AList.lookup (op=) fv_map ty)
+ val lhs = fv $ list_comb (constr, args)
+ val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
+ val rhs = fold_union rhs_trms
+in
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+end
+
+fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
+let
+ val arg_names = Datatype_Prop.make_tnames arg_tys
+ val args = map Free (arg_names ~~ arg_tys)
+ val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)
+ val lhs = fv_bn $ list_comb (constr, args)
+ val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
+ val rhs = fold_union rhs_trms
+in
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+end
+
+fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
+let
+ val nth_constrs_info = nth constrs_info bn_n
+ val nth_bclausess = nth bclausesss bn_n
+in
+ map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
+end
+
+fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy =
+let
+ val fv_names = prefix_dt_names descr sorts "fv_"
+ val fv_arg_tys = all_dtyps descr sorts
+ val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
+ val fv_frees = map Free (fv_names ~~ fv_tys);
+ val fv_map = fv_arg_tys ~~ fv_frees
+
+ val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
+ val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
+ val fv_bn_names = map (prefix "fv_") bn_names
+ val fv_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
+ val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
+ val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
+ val fv_bn_map = bns ~~ fv_bn_frees
+
+ val constrs_info = all_dtyp_constrs_types descr sorts
+
+ val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss
+ val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info
+
+ val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
+ val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
+
+ val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
+ Function_Common.default_config (pat_completeness_simp constr_thms) lthy
+
+ val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
+
+ val {fs, simps, inducts, ...} = info;
+
+ val morphism = ProofContext.export_morphism lthy'' lthy
+ val fs_exp = map (Morphism.term morphism) fs
+
+ val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
+ val simps_exp = map (Morphism.thm morphism) (the simps)
+ val fv_bns_inducts_exp = map (Morphism.thm morphism) (the inducts)
+in
+ (fv_frees_exp, fv_bns_exp, simps_exp, fv_bns_inducts_exp, lthy'')
+end
+
+
+(** equivarance proofs **)
+
+val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}
+
+fun subproof_tac const_names simps =
+ Subgoal.FOCUS (fn {prems, context, ...} =>
+ HEADGOAL
+ (simp_tac (HOL_basic_ss addsimps simps)
+ THEN' Nominal_Permeq.eqvt_tac context [] const_names
+ THEN' simp_tac (HOL_basic_ss addsimps (eqvt_apply_sym :: prems))))
+
+fun prove_eqvt_tac insts ind_thms const_names simps ctxt =
+ HEADGOAL
+ (Object_Logic.full_atomize_tac
+ THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))
+ THEN_ALL_NEW subproof_tac const_names simps ctxt)
+
+fun mk_eqvt_goal pi const arg =
+let
+ val lhs = mk_perm pi (const $ arg)
+ val rhs = const $ (mk_perm pi arg)
+in
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+end
+
+fun raw_prove_eqvt consts ind_thms simps ctxt =
+ if null consts then []
+ else
+ let
+ val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+ val p = Free (p, @{typ perm})
+ val arg_tys =
+ consts
+ |> map fastype_of
+ |> map domain_type
+ val (arg_names, ctxt'') =
+ Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
+ val args = map Free (arg_names ~~ arg_tys)
+ val goals = map2 (mk_eqvt_goal p) consts args
+ val insts = map (single o SOME) arg_names
+ val const_names = map (fst o dest_Const) consts
+ in
+ Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} =>
+ prove_eqvt_tac insts ind_thms const_names simps context)
+ |> ProofContext.export ctxt'' ctxt
+ end
+
+end (* structure *)
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_dt_rawperm.ML Wed Jun 23 15:40:00 2010 +0100
@@ -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 *)
+
--- a/Paper/Paper.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Paper/Paper.thy Wed Jun 23 15:40:00 2010 +0100
@@ -1,6 +1,6 @@
(*<*)
theory Paper
-imports "../Nominal/Test" "LaTeXsugar"
+imports "../Nominal/NewParser" "LaTeXsugar"
begin
consts
--- a/Paper/ROOT.ML Wed Jun 23 09:01:45 2010 +0200
+++ b/Paper/ROOT.ML Wed Jun 23 15:40:00 2010 +0100
@@ -1,3 +1,3 @@
quick_and_dirty := true;
-no_document use_thys ["LaTeXsugar"];
+no_document use_thys ["LaTeXsugar", "../Nominal/NewParser"];
use_thys ["Paper"];
\ No newline at end of file
--- a/Quotient-Paper/Paper.thy Wed Jun 23 09:01:45 2010 +0200
+++ b/Quotient-Paper/Paper.thy Wed Jun 23 15:40:00 2010 +0100
@@ -347,8 +347,8 @@
\end{isabelle}
\noindent
- In the context of quotients, the following two notions from are \cite{Homeier05}
- needed later on.
+ In the context of quotients, the following two notions from \cite{Homeier05}
+ are needed later on.
\begin{definition}[Respects]\label{def:respects}
An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
@@ -394,7 +394,8 @@
\begin{definition}[Composition of Relations]
@{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
- composition defined by @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
+ composition defined by
+ @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
@{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
\end{definition}
@@ -410,7 +411,7 @@
composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
with @{text R} being an equivalence relation, then
- @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep \<circ> rep_fset)"}
+ @{text [display, indent=10] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map Abs) (map Rep \<circ> Rep_fset)"}
\vspace{-.5mm}
*}
@@ -838,14 +839,16 @@
The second and third proof step will always succeed if the appropriate
respectfulness and preservation theorems are given. In contrast, the first
proof step can fail: a theorem given by the user does not always
- imply a regularized version and a stronger one needs to be proved. This
- is outside of the scope where the quotient package can help. An example
+ imply a regularized version and a stronger one needs to be proved. An example
for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},
- but the raw theorem only shows that particular element in the
- equivalence classes are not equal. A more general statement stipulating that
- the equivalence classes are not equal is necessary, and then leads to the
- theorem @{text "0 \<noteq> 1"}.
+ but this raw theorem only shows that particular element in the
+ equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a
+ more general statement stipulating that the equivalence classes are not
+ equal is necessary. This kind of failure is beyond the scope where the
+ quotient package can help: the user has to provide a raw theorem that
+ can be regularized automatically, or has to provide an explicit proof
+ for the first proof step.
In the following we will first define the statement of the
regularized theorem based on @{text "raw_thm"} and
@@ -923,12 +926,12 @@
\end{center}
\noindent
- where again the cases for existential quantifiers and unique existential
- quantifiers have been omitted.
+ In this definition we again omitted the cases for existential and unique existential
+ quantifiers.
In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
start with an implication. Isabelle provides \emph{mono} rules that can split up
- the implications into simpler implication subgoals. This succeeds for every
+ the implications into simpler implicational subgoals. This succeeds for every
monotone connective, except in places where the function @{text REG} inserted,
for instance, a quantifier by a bounded quantifier. In this case we have
rules of the form
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/ROOT.ML Wed Jun 23 15:40:00 2010 +0100
@@ -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 Wed Jun 23 15:40:00 2010 +0100
@@ -0,0 +1,1103 @@
+(*<*)
+theory Slides1
+imports "LaTeXsugar" "Nominal"
+begin
+
+notation (latex output)
+ set ("_") and
+ Cons ("_::/_" [66,65] 65)
+
+(*>*)
+
+
+text_raw {*
+ \renewcommand{\slidecaption}{Cambridge, 8.~June 2010}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[t]
+ \frametitle{%
+ \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
+ \\
+ \huge Nominal Isabelle 2\\[-2mm]
+ \large Or, How to Reason Conveniently\\[-5mm]
+ \large with General Bindings\\[5mm]
+ \end{tabular}}
+ \begin{center}
+ Christian Urban
+ \end{center}
+ \begin{center}
+ joint work with {\bf Cezary Kaliszyk}\\[0mm]
+ \end{center}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-2>
+ \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}}
+ \mbox{}\\[-6mm]
+
+ \begin{itemize}
+ \item the old Nominal Isabelle provided a reasoning infrastructure for single binders\medskip
+
+ \begin{center}
+ Lam [a].(Var a)
+ \end{center}\bigskip
+
+ \item<2-> but representing
+
+ \begin{center}
+ $\forall\{a_1,\ldots,a_n\}.\; T$
+ \end{center}\medskip
+
+ with single binders and reasoning about it is a \alert{\bf major} pain;
+ take my word for it!
+ \end{itemize}
+
+ \only<1>{
+ \begin{textblock}{6}(1.5,11)
+ \small
+ for example\\
+ \begin{tabular}{l@ {\hspace{2mm}}l}
+ \pgfuseshading{smallspherered} & a $\fresh$ Lam [a]. t\\
+ \pgfuseshading{smallspherered} & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\
+ \pgfuseshading{smallspherered} & Barendregt-style reasoning about bound variables\\
+ \end{tabular}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<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 \textcolor{gray}{(restriction)}\medskip
+
+ \item the order does not matter, but the cardinality of the binders
+ must be the same \textcolor{gray}{(abstraction)}\medskip
+
+ \item the order does matter \textcolor{gray}{(iterated single binders)}
+ \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) $=$ []}}\\
+ \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\
+ \end{tabular}
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-5>
+ \frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}}
+ \mbox{}\\[-3mm]
+
+ \begin{itemize}
+ \item this way of specifying binding is inspired by
+ {\bf Ott}\onslide<2->{, \alert{\bf but} we made some adjustments:}\medskip
+
+
+ \only<2>{
+ \begin{itemize}
+ \item Ott allows specifications like\smallskip
+ \begin{center}
+ $t ::= t\;t\; |\;\lambda x.t$
+ \end{center}
+ \end{itemize}}
+
+ \only<3-4>{
+ \begin{itemize}
+ \item whether something is bound can depend in Ott on other bound things\smallskip
+ \begin{center}
+ \begin{tikzpicture}
+ \node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$};
+ \node (B) at ( 1.1,1) {$s$};
+ \onslide<4>{\node (C) at (0.5,0) {$\{y, x\}$};}
+ \onslide<4>{\draw[->,red,line width=1mm] (A) -- (C);}
+ \onslide<4>{\draw[->,red,line width=1mm] (C) -- (B);}
+ \end{tikzpicture}
+ \end{center}
+ \onslide<4>{this might make sense for ``raw'' terms, but not at all
+ for $\alpha$-equated terms}
+ \end{itemize}}
+
+ \only<5>{
+ \begin{itemize}
+ \item we allow multiple ``binders'' and ``bodies''\smallskip
+ \begin{center}
+ \begin{tabular}{l}
+ \isacommand{bind} a b c \ldots \isacommand{in} x y z \ldots\\
+ \isacommand{bind\_set} a b c \ldots \isacommand{in} x y z \ldots\\
+ \isacommand{bind\_res} a b c \ldots \isacommand{in} x y z \ldots
+ \end{tabular}
+ \end{center}\bigskip\medskip
+ the reason is that with our definition of $\alpha$-equivalence\medskip
+ \begin{center}
+ \begin{tabular}{l}
+ \isacommand{bind\_res} as \isacommand{in} x y $\not\Leftrightarrow$\\
+ \hspace{8mm}\isacommand{bind\_res} as \isacommand{in} x, \isacommand{bind\_res} as \isacommand{in} y
+ \end{tabular}
+ \end{center}\medskip
+
+ same with \isacommand{bind\_set}
+ \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 the old Nominal Isabelle, we represented single binders as partial functions:\bigskip
+
+ \begin{center}
+ \begin{tabular}{l}
+ Lam [$a$].\,$t$ $\;{^\text{``}}\!\dn{}\!^{\text{''}}$\\[2mm]
+ \;\;\;\;$\lambda b.$\;$\text{if}\;a = b\;\text{then}\;t\;\text{else}$\\
+ \phantom{\;\;\;\;$\lambda b.$\;\;\;\;\;\;}$\text{if}\;b \fresh t\;
+ \text{then}\;(a\;b)\act t\;\text{else}\;\text{error}$
+ \end{tabular}
+ \end{center}
+ \end{itemize}
+
+ \begin{textblock}{10}(2,14)
+ \footnotesize $^*$ alpha-equality coincides with equality on functions
+ \end{textblock}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->
+ \frametitle{\begin{tabular}{c}New Design\end{tabular}}
+ \mbox{}\\[4mm]
+
+ \begin{center}
+ \begin{tikzpicture}
+ {\draw (0,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
+ (A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};}
+
+ {\draw (3,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
+ (B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};}
+
+ \alt<2>
+ {\draw (6,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+ (C) {\textcolor{red}{\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}}};}
+ {\draw (6,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
+ (C) {\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}};}
+
+ {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
+ (D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};}
+
+ {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
+ (E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};}
+
+ {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
+ (F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};}
+
+ \draw[->,fg!50,line width=1mm] (A) -- (B);
+ \draw[->,fg!50,line width=1mm] (B) -- (C);
+ \draw[->,fg!50,line width=1mm, line join=round, rounded corners=2mm]
+ (C) -- (8,0) -- (8,-1.5) -- (-2,-1.5) -- (-2,-3) -- (D);
+ \draw[->,fg!50,line width=1mm] (D) -- (E);
+ \draw[->,fg!50,line width=1mm] (E) -- (F);
+ \end{tikzpicture}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-8>
+ \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-6>{${}_{\text{set}}$}%
+ \only<7>{${}_{\text{\alert{list}}}$}%
+ \only<8>{${}_{\text{\alert{res}}}$}}%
+ \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$
+ \end{tabular}\bigskip
+ \end{itemize}
+
+ \only<1>{
+ \begin{textblock}{8}(3,8.5)
+ \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}
+ \pgfuseshading{smallspherered} & $as$ is a set of names\ldots the binders\\
+ \pgfuseshading{smallspherered} & $x$ is the body (might be a tuple)\\
+ \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<5->{$\;\;\;\wedge$} & \onslide<5->{$(\pi \act x)\;R\;y$}\\[1mm]
+ & \onslide<6-7>{$\;\;\;\wedge$} & \onslide<6-7>{$\pi \act as = bs$}\\
+ \end{tabular}
+ \end{textblock}}
+
+ \only<7>{
+ \begin{textblock}{7}(3,13.8)
+ \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names
+ \end{textblock}}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-3>
+ \frametitle{\begin{tabular}{c}Examples\end{tabular}}
+ \mbox{}\\[-3mm]
+
+ \begin{itemize}
+ \item lets look at ``type-schemes'':\medskip\medskip
+
+ \begin{center}
+ $(as, x) \approx\!\makebox[0mm][l]{${}_{\text{set}}$}\only<1>{{}^{R,\text{fv}}}\only<2->{{}^{\alert{=},\alert{\text{fv}}}} (bs, y)$
+ \end{center}\medskip
+
+ \onslide<2->{
+ \begin{center}
+ \begin{tabular}{l}
+ $\text{fv}(x) = \{x\}$\\[1mm]
+ $\text{fv}(T_1 \rightarrow T_2) = \text{fv}(T_1) \cup \text{fv}(T_2)$\\
+ \end{tabular}
+ \end{center}}
+ \end{itemize}
+
+
+ \only<3->{
+ \begin{textblock}{4}(0.3,12)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\tiny\color{darkgray}
+ \begin{minipage}{3.4cm}\raggedright
+ \begin{tabular}{r@ {\hspace{1mm}}l}
+ \multicolumn{2}{@ {}l}{res:}\\
+ $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\
+ $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\
+ $\wedge$ & $\pi \cdot x = y$\\
+ \\
+ \end{tabular}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+ \only<3->{
+ \begin{textblock}{4}(5.2,12)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\tiny\color{darkgray}
+ \begin{minipage}{3.4cm}\raggedright
+ \begin{tabular}{r@ {\hspace{1mm}}l}
+ \multicolumn{2}{@ {}l}{set:}\\
+ $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\
+ $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\
+ $\wedge$ & $\pi \cdot x = y$\\
+ $\wedge$ & $\pi \cdot as = bs$\\
+ \end{tabular}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+ \only<3->{
+ \begin{textblock}{4}(10.2,12)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\tiny\color{darkgray}
+ \begin{minipage}{3.4cm}\raggedright
+ \begin{tabular}{r@ {\hspace{1mm}}l}
+ \multicolumn{2}{@ {}l}{list:}\\
+ $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\
+ $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\
+ $\wedge$ & $\pi \cdot x = y$\\
+ $\wedge$ & $\pi \cdot as = bs$\\
+ \end{tabular}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<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-2>
+ \frametitle{\begin{tabular}{c}Examples\end{tabular}}
+ \mbox{}\\[-3mm]
+
+ \begin{center}
+ \only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$}
+ \end{center}
+
+ \begin{itemize}
+ \item $\approx_{\text{res}}$, $\not\approx_{\text{set}}$,
+ $\not\approx_{\text{list}}$
+ \end{itemize}
+
+
+ \only<1->{
+ \begin{textblock}{4}(0.3,12)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\tiny\color{darkgray}
+ \begin{minipage}{3.4cm}\raggedright
+ \begin{tabular}{r@ {\hspace{1mm}}l}
+ \multicolumn{2}{@ {}l}{res:}\\
+ $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\
+ $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\
+ $\wedge$ & $\pi \cdot x = y$\\
+ \\
+ \end{tabular}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+ \only<1->{
+ \begin{textblock}{4}(5.2,12)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\tiny\color{darkgray}
+ \begin{minipage}{3.4cm}\raggedright
+ \begin{tabular}{r@ {\hspace{1mm}}l}
+ \multicolumn{2}{@ {}l}{set:}\\
+ $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\
+ $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\
+ $\wedge$ & $\pi \cdot x = y$\\
+ $\wedge$ & $\pi \cdot as = bs$\\
+ \end{tabular}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+ \only<1->{
+ \begin{textblock}{4}(10.2,12)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\tiny\color{darkgray}
+ \begin{minipage}{3.4cm}\raggedright
+ \begin{tabular}{r@ {\hspace{1mm}}l}
+ \multicolumn{2}{@ {}l}{list:}\\
+ $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\
+ $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\
+ $\wedge$ & $\pi \cdot x = y$\\
+ $\wedge$ & $\pi \cdot as = bs$\\
+ \end{tabular}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \only<2>{
+ \begin{textblock}{6}(2.5,4)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=5mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\normalsize
+ \begin{minipage}{8cm}\raggedright
+ \begin{itemize}
+ \item \color{darkgray}$\alpha$-equivalences coincide when a single name is
+ abstracted
+ \item \color{darkgray}in that case they are equivalent to ``old-fashioned'' definitions of $\alpha$
+ \end{itemize}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<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]{${}_{{}*{}}$}^{=,\text{supp}} (bs, y)$\medskip
+ \item they are equivalence relations\medskip
+ \item we can therefore use the quotient package to introduce the
+ types $\beta\;\text{abs}_*$\bigskip
+ \begin{center}
+ \only<1>{$[as].\,x$}
+ \only<2>{$\text{supp}([as].x) = \text{supp}(x) - as$}
+ \only<3>{%
+ \begin{tabular}{r@ {\hspace{1mm}}l}
+ \multicolumn{2}{@ {\hspace{-7mm}}l}{$[as]. x \alert{=} [bs].y\;\;\;\text{if\!f}$}\\[2mm]
+ $\exists \pi.$ & $\text{supp}(x) - as = \text{supp}(y) - bs$\\
+ $\wedge$ & $\text{supp}(x) - as \fresh^* \pi$\\
+ $\wedge$ & $\pi \act x = y $\\
+ $(\wedge$ & $\pi \act as = bs)\;^*$\\
+ \end{tabular}}
+ \end{center}
+ \end{itemize}
+
+ \only<1->{
+ \begin{textblock}{8}(12,3.8)
+ \footnotesize $^*$ set, res, list
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>
+ \frametitle{\begin{tabular}{c}A Problem\end{tabular}}
+ \mbox{}\\[-3mm]
+
+ \begin{center}
+ $\text{let}\;x_1=t_1 \ldots x_n=t_n\;\text{in}\;s$
+ \end{center}
+
+ \begin{itemize}
+ \item we cannot represent this as\medskip
+ \begin{center}
+ $\text{let}\;[x_1,\ldots,x_n]\alert{.}s\;\;[t_1,\ldots,t_n]$
+ \end{center}\bigskip
+
+ because\medskip
+ \begin{center}
+ $\text{let}\;[x].s\;\;[t_1,t_2]$
+ \end{center}
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<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}\cup\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'}}
+ \]\bigskip
+
+
+ \onslide<1->{\small{}bn-function $\Rightarrow$ \alert{deep binders}}
+ \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}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}
+ \mbox{}\\[6mm]
+
+ \begin{center}
+ LetRec as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t \alert{as}\\
+ \end{center}
+
+
+ \[\mbox{}\hspace{-4mm}
+ \infer[\text{LetRec-}\!\approx_\alpha]
+ {\text{LetRec}\;as\;t \approx_\alpha \text{LetRec}\;as'\;t'}
+ {(\text{bn}(as), (t, as)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
+ ^{R,fv} (\text{bn}(as'), (t', as'))}
+ \]\bigskip
+
+ \onslide<1->{\alert{deep recursive binders}}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->
+ \frametitle{\begin{tabular}{c}Restrictions\end{tabular}}
+ \mbox{}\\[-6mm]
+
+ Our restrictions on binding specifications:
+
+ \begin{itemize}
+ \item a body can only occur once in a list of binding clauses\medskip
+ \item you can only have one binding function for a deep binder\medskip
+ \item binding functions can return: the empty set, singletons, unions (similarly for lists)
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<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 our quotient package to introduce the type(s)
+ of $\alpha$-equated terms
+
+ \[
+ \infer
+ {\text{Lam}\;x\;t \alert{=} \text{Lam}\;x'\;t'}
+ {\only<1>{([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
+ ^{=,\text{supp}} ([x'], t')}%
+ \only<2>{[x].t = [x'].t'}}
+ \]
+
+
+ \item the properties for support are implied by the properties of $[\_].\_$
+ \item we can derive strong induction principles (almost automatic---matter of time)
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[t]
+ \frametitle{\begin{tabular}{c}Runtime is Acceptable\end{tabular}}
+ \mbox{}\\[-7mm]\mbox{}
+
+ \footnotesize
+ \begin{center}
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
+ (A) {\begin{minipage}{0.8cm}bind.\\spec.\end{minipage}};
+
+ \draw (2,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
+ (B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}};
+
+ \draw (4,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
+ (C) {\begin{minipage}{0.8cm}$\alpha$-\\equiv.\end{minipage}};
+
+ \draw (0,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
+ (D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}};
+
+ \draw (2,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
+ (E) {\begin{minipage}{0.8cm}lift\\thms\end{minipage}};
+
+ \draw (4,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
+ (F) {\begin{minipage}{0.8cm}add.\\thms\end{minipage}};
+
+ \draw[->,fg!50,line width=1mm] (A) -- (B);
+ \draw[->,fg!50,line width=1mm] (B) -- (C);
+ \draw[->,fg!50,line width=1mm, line join=round, rounded corners=2mm]
+ (C) -- (5,0) -- (5,-1) -- (-1,-1) -- (-1,-2) -- (D);
+ \draw[->,fg!50,line width=1mm] (D) -- (E);
+ \draw[->,fg!50,line width=1mm] (E) -- (F);
+ \end{tikzpicture}
+ \end{center}
+
+ \begin{itemize}
+ \item Core Haskell: 11 types, 49 term-constructors, 7 binding functions
+ \begin{center}
+ $\sim$ 1 min
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->
+ \frametitle{\begin{tabular}{c}Interesting Phenomenon\end{tabular}}
+ \mbox{}\\[-6mm]
+
+ \small
+ \mbox{}\hspace{20mm}
+ \begin{tabular}{ll}
+ \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
+ \hspace{5mm}\phantom{$|$} Var name\\
+ \hspace{5mm}$|$ App trm trm\\
+ \hspace{5mm}$|$ Lam x::name t::trm
+ & \isacommand{bind} x \isacommand{in} t\\
+ \hspace{5mm}$|$ Let as::assn t::trm
+ & \isacommand{bind} bn(as) \isacommand{in} t\\
+ \multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+ \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
+ \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
+ \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\
+ \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
+ \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
+ \end{tabular}\bigskip\medskip
+
+ we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots
+
+ \only<1->{
+ \begin{textblock}{8}(0.2,7.3)
+ \alert{\begin{tabular}{p{2.6cm}}
+ \raggedright\footnotesize{}Should a ``naked'' assn be quotient?
+ \end{tabular}\hspace{-3mm}
+ $\begin{cases}
+ \mbox{} \\ \mbox{}
+ \end{cases}$}
+ \end{textblock}}
+ \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
+ (Barendregt's variable convention is unsound in general,
+ found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{\begin{tabular}{c}Questions?\end{tabular}}
+ \mbox{}\\[-6mm]
+
+ \begin{center}
+ \alert{\huge{Thanks!}}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-2>[c]
+ \frametitle{\begin{tabular}{c}Examples\end{tabular}}
+ \mbox{}\\[-6mm]
+
+ \begin{center}
+ $(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, a \rightarrow b)$
+ $(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, b \rightarrow a)$
+ \end{center}
+
+ \begin{center}
+ $(\{a,b\}, (a \rightarrow b, a \rightarrow b))$\\
+ \hspace{17mm}$\not\approx_\alpha (\{a, b\}, (a \rightarrow b, b \rightarrow a))$
+ \end{center}
+
+ \onslide<2->
+ {1.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$,
+ \isacommand{bind\_set} as \isacommand{in} $\tau_2$\medskip
+
+ 2.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$ $\tau_2$
+ }
+
+ \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 Wed Jun 23 15:40:00 2010 +0100
@@ -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 Wed Jun 23 15:40:00 2010 +0100
@@ -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 Wed Jun 23 15:40:00 2010 +0100
@@ -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:
+