# HG changeset patch # User Christian Urban # Date 1282749402 -28800 # Node ID 3772bb3bd7ce43a0b0c118ccb42e6be5b2de148a # Parent 92dc6cfa3a95d4592107343fd9302db3ca430ee5 cleaning of unused files and code diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/Abs.thy --- 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: - "\a \ atom ` (fn :: ('a :: at_base set)); b \ atom ` fn\ \ (a \ b) \ 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 \ (\p. (bs, x) \gen (op =) supp p (cs, y))" and "Abs_res bs x = Abs_res cs y \ (\p. (bs, x) \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) \gen (\(x1, y1) (x2, y2). R1 x1 x2 \ R2 y1 y2) (\(a, b). f1 a \ f2 b) pi (cs, y1, y2) = - (f1 x1 \ f2 x2 - bs = f1 y1 \ f2 y2 - cs \ (f1 x1 \ f2 x2 - bs) \* pi \ R1 (pi \ x1) y1 \ R2 (pi \ x2) y2 - \ pi \ bs = cs)" - "(bs, x1, x2) \res (\(x1, y1) (x2, y2). R1 x1 x2 \ R2 y1 y2) (\(a, b). f1 a \ f2 b) pi (cs, y1, y2) = - (f1 x1 \ f2 x2 - bs = f1 y1 \ f2 y2 - cs \ (f1 x1 \ f2 x2 - bs) \* pi \ R1 (pi \ x1) y1 \ R2 (pi \ x2) y2)" - "(bsl, x1, x2) \lst (\(x1, y1) (x2, y2). R1 x1 x2 \ R2 y1 y2) (\(a, b). f1 a \ f2 b) pi (csl, y1, y2) = - (f1 x1 \ f2 x2 - set bsl = f1 y1 \ f2 y2 - set csl \ (f1 x1 \ f2 x2 - set bsl) \* pi \ R1 (pi \ x1) y1 \ R2 (pi \ x2) y2 - \ pi \ bsl = csl)" -by (simp_all add: alphas) - -lemma alphas3: - "(bsl, x1, x2, x3) \lst (\(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \ R2 y1 y2 \ R3 z1 z2) (\(a, b, c). f1 a \ (f2 b \ f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \ (f2 x2 \ f3 x3) - set bsl = f1 y1 \ (f2 y2 \ f3 y3) - set csl \ - (f1 x1 \ (f2 x2 \ f3 x3) - set bsl) \* pi \ - R1 (pi \ x1) y1 \ R2 (pi \ x2) y2 \ R3 (pi \ x3) y3 \ pi \ bsl = csl)" -by (simp add: alphas) +*) end diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/Abs_equiv.thy --- 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) \ (a = b \ x = y) \ (a \ b \ x = (a \ b) \ y \ a \ y)" - -notation - alpha1 ("_ \abs1 _") - -fun - alpha2 -where - "alpha2 (a, x) (b, y) \ (\c. c \ (a,b,x,y) \ ((c \ a) \ x) = ((c \ b) \ y))" - -notation - alpha2 ("_ \abs2 _") - -lemma alpha_old_new: - assumes a: "(a, x) \abs1 (b, y)" "sort_of a = sort_of b" - shows "({a}, x) \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 \ b)" in exI) -apply(simp add: alpha_gen) -apply(simp add: fresh_def) -apply(rule conjI) -apply(rule_tac ?p1="(a \ 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 \ 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 \ b) \ {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: "\a b. \sort_of a = sort_of b; a \ b\ \ P (a \ b)" - assumes plus: "\p1 p2. \supp p1 \ supp p2 = {}; P p1; P p2\ \ P (p1 + p2)" - shows "P p" -using fin -apply(induct F\"supp p" arbitrary: p rule: finite_induct) -oops - -lemma ii: - assumes "\x \ A. p \ x = x" - shows "p \ 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)) \gen (\(x1,x2) (y1,y2). x1=y1 \ x2=y2) (\(x,y). supp x \ supp y) p (cs, (y1, y2)) - \ ((bs, x1) \gen (op=) supp p (cs, y1) \ (bs, x2) \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 \ S1" "x \ S2" - shows "S1 = S2" -using assms -apply (metis insert_Diff_single insert_absorb) -done - -lemma kk: - assumes a: "p \ x = y" - shows "\a \ supp x. (p \ a) \ 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 \ supp x" "b \ supp x" "a \ b" "sort_of a = sort_of b" - shows "((a \ b) \ x) \ 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 \ b)" in permute_boolI) -apply(simp add: mem_eqvt supp_eqvt) -done - -lemma alpha_abs_sym: - assumes a: "({a}, x) \abs ({b}, y)" - shows "({b}, y) \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) \abs ({a2}, x2)" - assumes b: "({a2}, x2) \abs ({a3}, x3)" - shows "({a1}, x1) \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) \abs ({a}, y)" - shows "(a, x) \abs1 (a, y)" -using a -apply(simp) -apply(erule exE) -apply(simp add: alpha_gen) -apply(erule conjE)+ -apply(case_tac "a \ supp x") -apply(simp) -apply(subgoal_tac "supp x \* p") -apply(drule supp_perm_eq) -apply(simp) -apply(simp) -apply(simp) -apply(case_tac "a \ 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 \ p") -apply(subgoal_tac "supp y \* 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 \ a) \ p)") -apply(simp add: fresh_def supp_perm) -apply(simp add: fresh_star_def) -done - -lemma alpha_unequal: - assumes a: "({a}, x) \abs ({b}, y)" "sort_of a = sort_of b" "a \ b" - shows "(a, x) \abs1 (b, y)" -using a -apply - -apply(subgoal_tac "a \ supp x - {a}") -apply(subgoal_tac "b \ 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 \ b)" in permute_boolE) -apply(simp add: fresh_eqvt) -apply(simp add: fresh_def) -done - -lemma alpha_new_old: - assumes a: "({a}, x) \abs ({b}, y)" "sort_of a = sort_of b" - shows "(a, x) \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 diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/NewAlpha.thy --- 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 diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/NewParser.thy --- 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 \ C2 y ...) (Proof by cases; simp) - -Tacs.thy/build_rel_inj - 6) prove alpha_eq_iff (C1 x = C2 y \ P x y ...) - (left-to-right by intro rule, right-to-left by cases; simp) -Equivp.thy/prove_eqvt - 7) prove bn_eqvt (common induction on the raw datatype) - 8) prove fv_eqvt (common induction on the raw datatype with help of above) -Rsp.thy/build_alpha_eqvts - 9) prove alpha_eqvt and alpha_bn_eqvt - (common alpha-induction, unfolding alpha_gen, permute of #* and =) -Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps - 10) prove that alpha and alpha_bn are equivalence relations - (common induction and application of 'compose' lemmas) -Lift.thy/define_quotient_types - 11) define quotient types -Rsp.thy/build_fvbv_rsps - 12) prove bn respects (common induction and simp with alpha_gen) -Rsp.thy/prove_const_rsp - 13) prove fv respects (common induction and simp with alpha_gen) - 14) prove permute respects (unfolds to alpha_eqvt) -Rsp.thy/prove_alpha_bn_rsp - 15) prove alpha_bn respects - (alpha_induct then cases then sym and trans of the relations) -Rsp.thy/prove_alpha_alphabn - 16) show that alpha implies alpha_bn (by unduction, needed in following step) -Rsp.thy/prove_const_rsp - 17) prove respects for all datatype constructors - (unfold eq_iff and alpha_gen; introduce zero permutations; simp) -Perm.thy/quotient_lift_consts_export - 18) define lifted constructors, fv, bn, alpha_bn, permutations -Perm.thy/define_lifted_perms - 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass -Lift.thy/lift_thm - 20) lift permutation simplifications - 21) lift induction - 22) lift fv - 23) lift bn - 24) lift eq_iff - 25) lift alpha_distincts - 26) lift fv and bn eqvts -Equivp.thy/prove_supports - 27) prove that union of arguments supports constructors -Equivp.thy/prove_fs - 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) -Equivp.thy/supp_eq - 29) prove supp = fv -*} - - - end diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/Perm.thy --- 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 diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/Rsp.thy --- 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 \ r a b \ r a c = r b c" - unfolding equivp_reflp_symp_transp symp_def transp_def - by blast - -lemma equivp_rspr: - "equivp r \ r a b \ 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 \"]}) 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: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q p) \ \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 diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/Tacs.thy --- 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 - diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/Unused.thy --- 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: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (pi \ p)) \ \pi. Q pi" -apply (erule exE) -apply (rule_tac x="pi \ 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' \ R y y' \ 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; -*} diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/nominal_dt_alpha.ML --- 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