--- a/Nominal/Abs.thy Wed Aug 25 22:55:42 2010 +0800
+++ b/Nominal/Abs.thy Wed Aug 25 23:16:42 2010 +0800
@@ -560,29 +560,9 @@
by (perm_simp) (rule refl)
-
-
-section {* BELOW is stuff that may or may not be needed *}
+(* Below seems to be not needed *)
-lemma supp_atom_image:
- fixes as::"'a::at_base set"
- shows "supp (atom ` as) = supp as"
-apply(simp add: supp_def)
-apply(simp add: image_eqvt)
-apply(simp add: eqvts_raw)
-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"
- apply (simp add: fresh_def)
- apply (simp add: supp_atom_image)
- apply (fold fresh_def)
- apply (simp add: swap_fresh_fresh)
- done
-
-(* TODO: The following lemmas can be moved somewhere... *)
-
+(*
lemma Abs_eq_iff:
shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
@@ -598,23 +578,7 @@
and q2: "Quotient R2 Abs2 Rep2"
shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
-
-lemma alphas2:
- "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
- (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
- \<and> pi \<bullet> bs = cs)"
- "(bs, x1, x2) \<approx>res (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
- (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)"
- "(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) =
- (f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
- \<and> pi \<bullet> bsl = csl)"
-by (simp_all add: alphas)
-
-lemma alphas3:
- "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and>
- (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
- 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)
+*)
end
--- a/Nominal/Abs_equiv.thy Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,244 +0,0 @@
-theory Abs_equiv
-imports Abs
-begin
-
-(*
- below is a construction site for showing that in the
- single-binder case, the old and new alpha equivalence
- coincide
-*)
-
-fun
- alpha1
-where
- "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
-
-notation
- alpha1 ("_ \<approx>abs1 _")
-
-fun
- alpha2
-where
- "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))"
-
-notation
- alpha2 ("_ \<approx>abs2 _")
-
-lemma alpha_old_new:
- assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
- shows "({a}, x) \<approx>abs ({b}, y)"
-using a
-apply(simp)
-apply(erule disjE)
-apply(simp)
-apply(rule exI)
-apply(rule alpha_gen_refl)
-apply(simp)
-apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
-apply(simp add: alpha_gen)
-apply(simp add: fresh_def)
-apply(rule conjI)
-apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1])
-apply(rule trans)
-apply(simp add: Diff_eqvt supp_eqvt)
-apply(subst swap_set_not_in)
-back
-apply(simp)
-apply(simp)
-apply(simp add: permute_set_eq)
-apply(rule conjI)
-apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: permute_self)
-apply(simp add: Diff_eqvt supp_eqvt)
-apply(simp add: permute_set_eq)
-apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
-apply(simp add: fresh_star_def fresh_def)
-apply(blast)
-apply(simp add: supp_swap)
-apply(simp add: eqvts)
-done
-
-
-lemma perm_induct_test:
- fixes P :: "perm => bool"
- assumes fin: "finite (supp p)"
- assumes zero: "P 0"
- assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
- assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
- shows "P p"
-using fin
-apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)
-oops
-
-lemma ii:
- assumes "\<forall>x \<in> A. p \<bullet> x = x"
- shows "p \<bullet> A = A"
-using assms
-apply(auto)
-apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff)
-apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure)
-done
-
-
-
-lemma alpha_abs_Pair:
- shows "(bs, (x1, x2)) \<approx>gen (\<lambda>(x1,x2) (y1,y2). x1=y1 \<and> x2=y2) (\<lambda>(x,y). supp x \<union> supp y) p (cs, (y1, y2))
- \<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))"
- apply(simp add: alpha_gen)
- apply(simp add: fresh_star_def)
- apply(simp add: ball_Un Un_Diff)
- apply(rule iffI)
- apply(simp)
- defer
- apply(simp)
- apply(rule conjI)
- apply(clarify)
- apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
- apply(rule sym)
- apply(rule ii)
- apply(simp add: fresh_def supp_perm)
- apply(clarify)
- apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
- apply(simp add: fresh_def supp_perm)
- apply(rule sym)
- apply(rule ii)
- apply(simp)
- done
-
-
-lemma yy:
- assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
- shows "S1 = S2"
-using assms
-apply (metis insert_Diff_single insert_absorb)
-done
-
-lemma kk:
- assumes a: "p \<bullet> x = y"
- shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
-using a
-apply(auto)
-apply(rule_tac p="- p" in permute_boolE)
-apply(simp add: mem_eqvt supp_eqvt)
-done
-
-lemma ww:
- assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b"
- shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x"
-apply(subgoal_tac "(supp x) supports x")
-apply(simp add: supports_def)
-using assms
-apply -
-apply(drule_tac x="a" in spec)
-defer
-apply(rule supp_supports)
-apply(auto)
-apply(rotate_tac 1)
-apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)
-apply(simp add: mem_eqvt supp_eqvt)
-done
-
-lemma alpha_abs_sym:
- assumes a: "({a}, x) \<approx>abs ({b}, y)"
- shows "({b}, y) \<approx>abs ({a}, x)"
-using a
-apply(simp)
-apply(erule exE)
-apply(rule_tac x="- p" in exI)
-apply(simp add: alpha_gen)
-apply(simp add: fresh_star_def fresh_minus_perm)
-apply (metis permute_minus_cancel(2))
-done
-
-lemma alpha_abs_trans:
- assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)"
- assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)"
- shows "({a1}, x1) \<approx>abs ({a3}, x3)"
-using a b
-apply(simp)
-apply(erule exE)+
-apply(rule_tac x="pa + p" in exI)
-apply(simp add: alpha_gen)
-apply(simp add: fresh_star_def fresh_plus_perm)
-done
-
-lemma alpha_equal:
- assumes a: "({a}, x) \<approx>abs ({a}, y)"
- shows "(a, x) \<approx>abs1 (a, y)"
-using a
-apply(simp)
-apply(erule exE)
-apply(simp add: alpha_gen)
-apply(erule conjE)+
-apply(case_tac "a \<notin> supp x")
-apply(simp)
-apply(subgoal_tac "supp x \<sharp>* p")
-apply(drule supp_perm_eq)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(case_tac "a \<notin> supp y")
-apply(simp)
-apply(drule supp_perm_eq)
-apply(clarify)
-apply(simp (no_asm_use))
-apply(simp)
-apply(simp)
-apply(drule yy)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(case_tac "a \<sharp> p")
-apply(subgoal_tac "supp y \<sharp>* p")
-apply(drule supp_perm_eq)
-apply(clarify)
-apply(simp (no_asm_use))
-apply(metis)
-apply(auto simp add: fresh_star_def)[1]
-apply(frule_tac kk)
-apply(drule_tac x="a" in bspec)
-apply(simp)
-apply(simp add: fresh_def)
-apply(simp add: supp_perm)
-apply(subgoal_tac "((p \<bullet> a) \<sharp> p)")
-apply(simp add: fresh_def supp_perm)
-apply(simp add: fresh_star_def)
-done
-
-lemma alpha_unequal:
- assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b"
- shows "(a, x) \<approx>abs1 (b, y)"
-using a
-apply -
-apply(subgoal_tac "a \<notin> supp x - {a}")
-apply(subgoal_tac "b \<notin> supp x - {a}")
-defer
-apply(simp add: alpha_gen)
-apply(simp)
-apply(drule_tac abs_swap1)
-apply(assumption)
-apply(simp only: insert_eqvt empty_eqvt swap_atom_simps)
-apply(simp only: abs_eq_iff)
-apply(drule alphas_abs_sym)
-apply(rotate_tac 4)
-apply(drule_tac alpha_abs_trans)
-apply(assumption)
-apply(drule alpha_equal)
-apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)
-apply(simp add: fresh_eqvt)
-apply(simp add: fresh_def)
-done
-
-lemma alpha_new_old:
- assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b"
- shows "(a, x) \<approx>abs1 (b, y)"
-using a
-apply(case_tac "a=b")
-apply(simp only: alpha_equal)
-apply(drule alpha_unequal)
-apply(simp)
-apply(simp)
-apply(simp)
-done
-
-end
\ No newline at end of file
--- a/Nominal/NewAlpha.thy Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,229 +0,0 @@
-theory NewAlpha
-imports "Abs" "Perm"
-begin
-
-ML {*
-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_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 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 (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
- 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 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 mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
-let
- fun mk_frees i =
- let
- val arg = nth args i
- val arg' = nth args' i
- val ty = fastype_of arg
- in
- if nth is_rec i
- then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg'
- else HOLogic.mk_eq (arg, arg')
- end
- fun mk_alpha_fv i =
- let
- val ty = fastype_of (nth args i)
- in
- case AList.lookup (op=) alpha_map ty of
- NONE => (HOLogic.eq_const ty, supp_const ty)
- | SOME (alpha, fv) => (alpha, fv)
- end
-
-in
- case bclause of
- BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies
- | BC (bmode, binders, bodies) =>
- let
- val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
- val comp_fv = foldl1 mk_prod_fv fvs
- val comp_alpha = foldl1 mk_prod_alpha alphas
- val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
- val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
- val comp_binders = mk_binders lthy bmode args binders
- val comp_binders' = mk_binders lthy bmode args' binders
- val alpha_prem =
- mk_alpha_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 mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
-let
- val arg_names = Datatype_Prop.make_tnames arg_tys
- val arg_names' = Name.variant_list arg_names arg_names
- val args = map Free (arg_names ~~ arg_tys)
- val args' = map Free (arg_names' ~~ arg_tys)
- val alpha = fst (the (AList.lookup (op=) alpha_map ty))
- val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
- val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
-in
- Library.foldr Logic.mk_implies (flat prems, concl)
-end
-*}
-
-ML {*
-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 mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
-let
- val arg_names = Datatype_Prop.make_tnames arg_tys
- val arg_names' = Name.variant_list arg_names arg_names
- val args = map Free (arg_names ~~ arg_tys)
- val args' = map Free (arg_names' ~~ arg_tys)
- val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm)
- val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
- val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
-in
- Library.foldr Logic.mk_implies (flat prems, concl)
-end
-*}
-
-ML {*
-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
-*}
-
-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 (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 = map2 (fn s => fn ty => ((Binding.name s, 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 = true, fork_mono = false}
- all_alpha_names [] all_alpha_intros [] lthy
-
- 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 phi = ProofContext.export_morphism lthy' lthy;
-
- 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_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
-end
-*}
-
-end
--- a/Nominal/NewParser.thy Wed Aug 25 22:55:42 2010 +0800
+++ b/Nominal/NewParser.thy Wed Aug 25 23:16:42 2010 +0800
@@ -1,10 +1,28 @@
theory NewParser
-imports "../Nominal-General/Nominal2_Base"
- "../Nominal-General/Nominal2_Eqvt"
- "../Nominal-General/Nominal2_Supp"
- "Perm" "Tacs" "Equivp"
+imports
+ "../Nominal-General/Nominal2_Base"
+ "../Nominal-General/Nominal2_Eqvt"
+ "../Nominal-General/Nominal2_Supp"
+ "Nominal2_FSet"
+ "Abs"
+uses ("nominal_dt_rawperm.ML")
+ ("nominal_dt_rawfuns.ML")
+ ("nominal_dt_alpha.ML")
+ ("nominal_dt_quot.ML")
begin
+use "nominal_dt_rawperm.ML"
+ML {* open Nominal_Dt_RawPerm *}
+
+use "nominal_dt_rawfuns.ML"
+ML {* open Nominal_Dt_RawFuns *}
+
+use "nominal_dt_alpha.ML"
+ML {* open Nominal_Dt_Alpha *}
+
+use "nominal_dt_quot.ML"
+ML {* open Nominal_Dt_Quot *}
+
section{* Interface for nominal_datatype *}
@@ -517,115 +535,8 @@
if get_STEPS lthy > 21
then true else raise TEST lthy9'
- (* old stuff *)
-
- val thy = ProofContext.theory_of lthy9'
- val thy_name = Context.theory_name thy
- val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-
- val _ = warning "Proving respects";
-
- val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
- val bns = raw_bns ~~ bn_nos;
-
- val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy9';
- 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 lthy9';
- val bns_rsp = flat (map snd bns_rsp_pre);
-
- fun fv_rsp_tac _ = fvbv_rsp_tac alpha_induct raw_fv_defs lthy9' 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) (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 raw_perm_funs
- (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
- fun alpha_bn_rsp_tac _ = let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms raw_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_bn_trms lthy11
- fun const_rsp_tac _ =
- 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_constrs lthy11a
- val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
- val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns)
- val (qfv_info, lthy12a) = define_qconsts qtys dd lthy12;
- val qfv_ts = map #qconst qfv_info
- val qfv_defs = map #def qfv_info
- 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 dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns
- val (qbn_info, lthy12b) = define_qconsts qtys dd lthy12a;
- val qbn_ts = map #qconst qbn_info
- val qbn_defs = map #def qbn_info
- val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms
- val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms
- val (qalpha_info, lthy12c) = define_qconsts qtys dd lthy12b;
- val qalpha_bn_trms = map #qconst qalpha_info
- val qalphabn_defs = map #def qalpha_info
-
- val _ = warning "Lifting permutations";
- val perm_names = map (fn x => "permute_" ^ x) qty_names
- val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
- val lthy13 = define_qperms qtys qty_full_names [] dd raw_perm_laws lthy12c
-
- val q_name = space_implode "_" qty_names;
- fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
- val _ = warning "Lifting induction";
- val constr_names = map (Long_Name.base_name o fst o dest_Const) [];
- val q_induct = Rule_Cases.name constr_names (the_single (fst (lift_thms qtys [] [raw_induct_thm] lthy13)));
- fun note_suffix s th ctxt =
- snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
- fun note_simp_suffix s th ctxt =
- snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
- 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 raw_fvs)) q_induct
- val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
- val q_perm = fst (lift_thms qtys [] raw_perm_simps lthy14);
- val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
- val q_fv = fst (lift_thms qtys [] raw_fv_defs lthy15);
- val lthy16 = note_simp_suffix "fv" q_fv lthy15;
- val q_bn = fst (lift_thms qtys [] raw_bn_defs lthy16);
- 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
- val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0
- val q_eq_iff_pre0 = fst (lift_thms qtys [] eq_iff_unfolded1 lthy17);
- 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 = fst (lift_thms qtys [] alpha_distincts lthy18);
- val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
- val q_eqvt = fst (lift_thms qtys [] (raw_bn_eqvt @ raw_fv_eqvt) lthy19);
- val (_, lthy20) = Local_Theory.note ((Binding.empty,
- [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
- val _ = warning "Supports";
- val supports = map (prove_supports lthy20 q_perm) [];
- val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys);
- val thy3 = Local_Theory.exit_global lthy20;
- val _ = warning "Instantiating FS";
- val lthy21 = Class.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_trms, qalpha_bn_trms) bn_nos;
- val (names, supp_eq_t) = supp_eq fv_alpha_all;
- val _ = warning "Support Equations";
- fun supp_eq_tac' _ = supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
- val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>
- let val _ = warning ("Support eqs failed") in [] end;
- val lthy23 = note_suffix "supp" q_supp lthy22;
in
- (0, lthy23)
+ (0, lthy9')
end handle TEST ctxt => (0, ctxt)
*}
@@ -855,73 +766,6 @@
*}
-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
-*}
-
-
-
end
--- a/Nominal/Perm.thy Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-theory Perm
-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")
- ("nominal_dt_quot.ML")
-begin
-
-use "nominal_dt_rawperm.ML"
-ML {* open Nominal_Dt_RawPerm *}
-
-use "nominal_dt_rawfuns.ML"
-ML {* open Nominal_Dt_RawFuns *}
-
-use "nominal_dt_alpha.ML"
-ML {* open Nominal_Dt_Alpha *}
-
-use "nominal_dt_quot.ML"
-ML {* open Nominal_Dt_Quot *}
-
-
-end
--- a/Nominal/Rsp.thy Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,224 +0,0 @@
-theory Rsp
-imports Abs Tacs
-begin
-
-ML {*
-fun const_rsp qtys lthy const =
-let
- val nty = Quotient_Term.derive_qtyp lthy qtys (fastype_of const)
- val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
-in
- HOLogic.mk_Trueprop (rel $ const $ const)
-end
-*}
-
-(* Replaces bounds by frees and meta implications by implications *)
-ML {*
-fun prepare_goal trm =
-let
- val vars = strip_all_vars trm
- val fs = rev (map Free vars)
- val (fixes, no_alls) = ((map fst vars), subst_bounds (fs, (strip_all_body trm)))
- val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems no_alls)
- val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl no_alls)
-in
- (fixes, fold (curry HOLogic.mk_imp) prems concl)
-end
-*}
-
-ML {*
-fun get_rsp_goal thy trm =
-let
- val goalstate = Goal.init (cterm_of thy trm);
- val tac = REPEAT o rtac @{thm fun_relI};
-in
- case (SINGLE (tac 1) goalstate) of
- NONE => error "rsp_goal failed"
- | SOME th => prepare_goal (term_of (cprem_of th 1))
-end
-*}
-
-ML {*
-fun prove_const_rsp qtys bind consts tac ctxt =
-let
- val rsp_goals = map (const_rsp qtys ctxt) consts
- val thy = ProofContext.theory_of ctxt
- val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals)
- val fixed' = distinct (op =) (flat fixed)
- val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)
- val user_thm = Goal.prove ctxt fixed' [] user_goal tac
- val user_thms = map repeat_mp (HOLogic.conj_elims user_thm)
- fun tac _ = (REPEAT o rtac @{thm fun_relI} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1
- val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals
-in
- ctxt
-|> snd o Local_Theory.note
- ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms)
-|> Local_Theory.note ((bind, []), user_thms)
-end
-*}
-
-ML {*
-fun fvbv_rsp_tac induct fvbv_simps ctxt =
- rtac induct THEN_ALL_NEW
- (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps (@{thms prod_fv.simps prod_rel.simps set.simps append.simps alphas} @ fvbv_simps)) THEN_ALL_NEW
- REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
- TRY o blast_tac (claset_of ctxt)
-*}
-
-ML {*
-fun sym_eqvts ctxt = maps (fn x => [sym OF [x]] handle _ => []) (Nominal_ThmDecls.get_eqvts_thms ctxt)
-fun all_eqvts ctxt =
- Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
-*}
-
-ML {*
-fun constr_rsp_tac inj rsp =
- REPEAT o rtac impI THEN'
- simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW
- (asm_simp_tac HOL_ss THEN_ALL_NEW (
- REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps (rsp @
- @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left prod_rel.simps prod_fv.simps}))
- ))
-*}
-
-ML {*
-fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =
-let
- val (fvs_alphas, ls) = split_list fv_alphas_lst;
- val (fv_ts, alpha_ts) = split_list fvs_alphas;
- val tys = map (domain_type o fastype_of) alpha_ts;
- val names = Datatype_Prop.make_tnames tys;
- val names2 = Name.variant_list names names;
- val args = map Free (names ~~ tys);
- val args2 = map Free (names2 ~~ tys);
- fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2));
- fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) =
- HOLogic.mk_imp (
- (alpha $ arg $ arg2),
- (foldr1 HOLogic.mk_conj
- (HOLogic.mk_eq (fv $ arg, fv $ arg2) ::
- (map (mk_fv_rsp arg arg2) l))));
- val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls);
- fun mk_fv_rsp_bn arg arg2 (fv, alpha) =
- HOLogic.mk_imp (
- (alpha $ arg $ arg2),
- HOLogic.mk_eq ((fv $ arg), (fv $ arg2)));
- fun fv_rsp_arg_bn ((arg, arg2), l) =
- map (mk_fv_rsp_bn arg arg2) l;
- val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls));
- val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas;
- val atys = map (domain_type o fastype_of) add_alphas;
- val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys);
- val aargs = map Free (anames ~~ atys);
- val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True}))
- add_alphas aargs;
- val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs));
- val th = Goal.prove ctxt (names @ names2) [] eq tac;
- val ths = HOLogic.conj_elims th;
- val (ths_nobn, ths_bn) = chop (length ls) ths;
- fun project (th, l) =
- Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th))
- val ths_nobn_pr = map project (ths_nobn ~~ ls);
-in
- (flat ths_nobn_pr @ ths_bn)
-end
-*}
-
-(** alpha_bn_rsp **)
-
-lemma equivp_rspl:
- "equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"
- unfolding equivp_reflp_symp_transp symp_def transp_def
- by blast
-
-lemma equivp_rspr:
- "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b"
- unfolding equivp_reflp_symp_transp symp_def transp_def
- by blast
-
-ML {*
-fun alpha_bn_rsp_tac simps res exhausts a ctxt =
- rtac allI THEN_ALL_NEW
- case_rules_tac ctxt a exhausts THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) THEN_ALL_NEW
- TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
- TRY o eresolve_tac res THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps simps)
-*}
-
-
-ML {*
-fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt =
-let
- val ty = domain_type (fastype_of alpha_bn);
- val (l, r) = the (AList.lookup (op=) alphas ty);
-in
- ([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)),
- HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt)
-end
-*}
-
-ML {*
-fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt =
-let
- val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt;
- val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
- val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
- val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind
- (alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt
-in
- Variable.export ctxt' ctxt ths_loc
-end
-*}
-
-ML {*
-fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt =
-let
- val ty = domain_type (fastype_of alpha_bn);
- val (l, r) = the (AList.lookup (op=) alphas ty);
-in
- ([alpha_bn $ l $ r], ctxt)
-end
-*}
-
-lemma exi_same: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q p) \<Longrightarrow> \<exists>pi. Q pi"
- by auto
-
-ML {*
-fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt =
- prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind
- (fn _ => asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas})
- THEN_ALL_NEW split_conj_tac THEN_ALL_NEW (TRY o etac @{thm exi_same})
- THEN_ALL_NEW asm_full_simp_tac HOL_ss) alpha_bns ctxt
-*}
-
-ML {*
-fun build_rsp_gl alphas fnctn ctxt =
-let
- val typ = domain_type (fastype_of fnctn);
- val (argl, argr) = the (AList.lookup (op=) alphas typ);
-in
- ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)
-end
-*}
-
-ML {*
-fun fvbv_rsp_tac' simps ctxt =
- asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ simps)) THEN_ALL_NEW
- REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
- TRY o blast_tac (claset_of ctxt)
-*}
-
-ML {*
-fun build_fvbv_rsps alphas ind simps fnctns ctxt =
- prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
-*}
-
-end
--- a/Nominal/Tacs.thy Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,103 +0,0 @@
-theory Tacs
-imports Main
-begin
-
-(* General not-nominal/quotient functionality useful for proving *)
-
-(* A version of case_rule_tac that takes more exhaust rules *)
-ML {*
-fun case_rules_tac ctxt0 s rules i st =
-let
- val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
- val ty = fastype_of (ProofContext.read_term_schematic ctxt s)
- fun exhaust_ty thm = fastype_of (hd (Induct.vars_of (Thm.term_of (Thm.cprem_of thm 1))));
- val ty_rules = filter (fn x => exhaust_ty x = ty) rules;
-in
- InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i st
-end
-*}
-
-ML {*
-fun mk_conjl props =
- fold (fn a => fn b =>
- if a = @{term True} then b else
- if b = @{term True} then a else
- HOLogic.mk_conj (a, b)) (rev props) @{term True};
-*}
-
-ML {*
-val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
-*}
-
-
-ML {*
-fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =
-let
- val tys = map (domain_type o fastype_of) alphas;
- val names = Datatype_Prop.make_tnames tys;
- val (namesl, ctxt') = Variable.variant_fixes names ctxt;
- val (namesr, ctxt'') = Variable.variant_fixes names ctxt';
- val freesl = map Free (namesl ~~ tys);
- val freesr = map Free (namesr ~~ tys);
- val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) 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 freesl;
- val trm_gls = map mk_conjl trm_gl_lists;
- val pgls = map
- (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl))
- ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))
- val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);
- fun tac {context,...} = (rtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
- TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 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 repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm
-*}
-
-(* Introduces an implication and immediately eliminates it by cases *)
-ML {*
-fun imp_elim_tac case_rules =
- Subgoal.FOCUS (fn {concl, context, ...} =>
- case term_of concl of
- _ $ (_ $ asm $ _) =>
- let
- fun filter_fn case_rule = (
- case Logic.strip_assums_hyp (prop_of case_rule) of
- ((_ $ asmc) :: _) =>
- let
- val thy = ProofContext.theory_of context
- in
- Pattern.matches thy (asmc, asm)
- end
- | _ => false)
- val matching_rules = filter filter_fn case_rules
- in
- (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
- end
- | _ => no_tac)
-*}
-
-ML {*
-fun is_ex (Const ("Ex", _) $ Abs _) = true
- | is_ex _ = false;
-*}
-
-ML {*
-fun dtyp_no_of_typ _ (TFree (_, _)) = error "dtyp_no_of_typ: Illegal free"
- | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"
- | dtyp_no_of_typ dts (Type (tname, _)) =
- case try (find_index (curry op = tname o fst)) dts of
- NONE => error "dtyp_no_of_typ: Illegal recursion"
- | SOME i => i
-*}
-
-end
-
--- a/Nominal/Unused.thy Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
-apply (erule exE)
-apply (rule_tac x="pi \<bullet> pia" in exI)
-by auto
-
-ML {*
-fun alpha_eqvt_tac induct simps ctxt =
- rtac induct THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
- REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps
- @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW
- (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
- @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
- THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
-*}
-
-ML {*
-fun build_alpha_eqvt alpha names =
-let
- val pi = Free ("p", @{typ perm});
- val (tys, _) = strip_type (fastype_of alpha)
- val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
- val args = map Free (indnames ~~ tys);
- val perm_args = map (fn x => mk_perm pi x) args
-in
- (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
-end
-*}
-
-ML {*
-fun build_alpha_eqvts funs tac ctxt =
-let
- val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
- val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
- val thm = Goal.prove ctxt names [] gl tac
-in
- map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
-end
-*}
-
-(* Given [fv1, fv2, fv3]
- produces %(x, y, z). fv1 x u fv2 y u fv3 z *)
-ML {*
-fun mk_compound_fv fvs =
-let
- val nos = (length fvs - 1) downto 0;
- val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);
- val fvs_union = mk_union fvs_applied;
- val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);
- fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
-in
- fold fold_fun tys (Abs ("", tyh, fvs_union))
-end;
-*}
-
-(* Given [R1, R2, R3]
- produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
-ML {*
-fun mk_compound_alpha Rs =
-let
- val nos = (length Rs - 1) downto 0;
- val nos2 = (2 * length Rs - 1) downto length Rs;
- val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no)
- (Rs ~~ (nos2 ~~ nos));
- val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied;
- val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);
- fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
- val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))
-in
- fold fold_fun tys (Abs ("", tyh, abs_rhs))
-end;
-*}
--- a/Nominal/nominal_dt_alpha.ML Wed Aug 25 22:55:42 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML Wed Aug 25 23:16:42 2010 +0800
@@ -291,7 +291,7 @@
fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =
let
(* proper import of type-variables does not work,
- since ther are replaced by new variables, messing
+ since then they are replaced by new variables, messing
up the ty_term assoc list *)
val distinct_thms' = map Thm.legacy_freezeT distinct_thms
val ty_trm_assoc = alpha_tys ~~ alpha_trms