# HG changeset patch # User Christian Urban # Date 1284302800 -28800 # Node ID 2f289c1f6cf15558e74ad8087c09da429b7ee0b1 # Parent 8f8652a8107fed4cc41d466eaac7cb77854bee88 tuned code diff -r 8f8652a8107f -r 2f289c1f6cf1 Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Sat Sep 11 05:56:49 2010 +0800 +++ b/Nominal-General/nominal_eqvt.ML Sun Sep 12 22:46:40 2010 +0800 @@ -34,97 +34,101 @@ val perm_cancel = @{thms permute_minus_cancel(2)} fun eqvt_rel_single_case_tac ctxt pred_names pi intro = -let - val thy = ProofContext.theory_of ctxt - val cpi = Thm.cterm_of thy (mk_minus pi) - val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE - val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} - val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} -in - eqvt_strict_tac ctxt [] pred_names THEN' - SUBPROOF (fn {prems, context as ctxt, ...} => - let - 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' ] - val tac3 = EVERY' [ rtac pi_intro_rule, - eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, - simp_tac simps2, resolve_tac prems'] - in - (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 - end) ctxt -end + let + val thy = ProofContext.theory_of ctxt + val cpi = Thm.cterm_of thy (mk_minus pi) + val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE + val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} + val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} + in + eqvt_strict_tac ctxt [] pred_names THEN' + SUBPROOF (fn {prems, context as ctxt, ...} => + let + 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' ] + val tac3 = EVERY' [ rtac pi_intro_rule, + eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, + simp_tac simps2, resolve_tac prems'] + in + (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 + end) ctxt + end fun eqvt_rel_tac ctxt pred_names pi induct intros = -let - val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros -in - EVERY' (rtac induct :: cases) -end + let + val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros + in + EVERY' (rtac induct :: cases) + end (** equivariance procedure *) -(* sets up goal and makes sure parameters - are untouched PROBLEM: this violates the - form of eqvt lemmas *) fun prepare_goal pi pred = -let - val (c, xs) = strip_comb pred; -in - HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) -end + let + val (c, xs) = strip_comb pred; + in + HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) + end (* stores thm under name.eqvt and adds [eqvt]-attribute *) + fun note_named_thm (name, thm) ctxt = -let - val thm_name = Binding.qualified_name - (Long_Name.qualify (Long_Name.base_name name) "eqvt") - val attr = Attrib.internal (K eqvt_add) - val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt -in - (thm', ctxt') -end + let + val thm_name = Binding.qualified_name + (Long_Name.qualify (Long_Name.base_name name) "eqvt") + val attr = Attrib.internal (K eqvt_add) + val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt + in + (thm', ctxt') + end fun equivariance note_flag pred_trms raw_induct intrs ctxt = -let - val is_already_eqvt = - filter (is_eqvt ctxt) pred_trms - |> map (Syntax.string_of_term ctxt) - val _ = if null is_already_eqvt then () - else error ("Already equivariant: " ^ commas is_already_eqvt) + let + val is_already_eqvt = + filter (is_eqvt ctxt) pred_trms + |> map (Syntax.string_of_term ctxt) + val _ = if null is_already_eqvt then () + else error ("Already equivariant: " ^ commas is_already_eqvt) - val pred_names = map (fst o dest_Const) pred_trms - val raw_induct' = atomize_induct ctxt raw_induct - val intrs' = map atomize_intr intrs - val (([raw_concl], [raw_pi]), ctxt') = - ctxt - |> Variable.import_terms false [concl_of raw_induct'] - ||>> Variable.variant_fixes ["p"] - val pi = Free (raw_pi, @{typ perm}) - val preds = map (fst o HOLogic.dest_imp) - (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); - val goal = HOLogic.mk_Trueprop - (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) - val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal - (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) - |> singleton (ProofContext.export ctxt' ctxt)) - val thms' = map (fn th => zero_var_indexes (th RS mp)) thms -in - if note_flag - then ctxt |> fold_map note_named_thm (pred_names ~~ thms') - else (thms', ctxt) -end + val pred_names = map (fst o dest_Const) pred_trms + val raw_induct' = atomize_induct ctxt raw_induct + val intrs' = map atomize_intr intrs + + val (([raw_concl], [raw_pi]), ctxt') = + ctxt + |> Variable.import_terms false [concl_of raw_induct'] + ||>> Variable.variant_fixes ["p"] + val pi = Free (raw_pi, @{typ perm}) + + val preds = map (fst o HOLogic.dest_imp) + (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); + + val goal = HOLogic.mk_Trueprop + (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) + + val thms = Goal.prove ctxt' [] [] goal + (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) + |> Datatype_Aux.split_conj_thm + |> ProofContext.export ctxt' ctxt + |> map (fn th => th RS mp) + |> map zero_var_indexes + in + if note_flag + then fold_map note_named_thm (pred_names ~~ thms) ctxt + else (thms, ctxt) + end fun equivariance_cmd pred_name ctxt = -let - val thy = ProofContext.theory_of ctxt - val (_, {preds, raw_induct, intrs, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) -in - equivariance true preds raw_induct intrs ctxt |> snd -end + let + val thy = ProofContext.theory_of ctxt + val (_, {preds, raw_induct, intrs, ...}) = + Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) + in + equivariance true preds raw_induct intrs ctxt |> snd + end local structure P = Parse and K = Keyword in @@ -132,6 +136,7 @@ Outer_Syntax.local_theory "equivariance" "Proves equivariance for inductive predicate involving nominal datatypes." K.thy_decl (P.xname >> equivariance_cmd); + end; end (* structure *) diff -r 8f8652a8107f -r 2f289c1f6cf1 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Sat Sep 11 05:56:49 2010 +0800 +++ b/Nominal-General/nominal_library.ML Sun Sep 12 22:46:40 2010 +0800 @@ -100,12 +100,12 @@ fun sum_case_const ty1 ty2 ty3 = Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) fun mk_sum_case trm1 trm2 = -let - val ([ty1], ty3) = strip_type (fastype_of trm1) - val ty2 = domain_type (fastype_of trm2) -in - sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 -end + let + val ([ty1], ty3) = strip_type (fastype_of trm1) + val ty2 = domain_type (fastype_of trm2) + in + sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 + end @@ -209,19 +209,19 @@ (* 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 + 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 - (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) + map (map aux) (all_dtyp_constrs_info descr) 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 @@ -230,45 +230,45 @@ (* 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 + 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_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 + 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_tac size_simps ctxt i st = -let - fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = - SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) - | mk_size_measure T = size_const T + let + fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = + SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) + | mk_size_measure T = size_const T - val ((_ $ (_ $ rel)) :: tl) = prems_of st - val measure_trm = - fastype_of rel - |> HOLogic.dest_setT - |> mk_size_measure - |> curry (op $) (Const (@{const_name measure}, dummyT)) - |> Syntax.check_term ctxt - val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral - zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals -in - (Function_Relation.relation_tac ctxt measure_trm - THEN_ALL_NEW simp_tac ss) i st -end + val ((_ $ (_ $ rel)) :: tl) = prems_of st + val measure_trm = + fastype_of rel + |> HOLogic.dest_setT + |> mk_size_measure + |> curry (op $) (Const (@{const_name measure}, dummyT)) + |> Syntax.check_term ctxt + val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral + zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals + in + (Function_Relation.relation_tac ctxt measure_trm + THEN_ALL_NEW simp_tac ss) i st + end fun prove_termination size_simps ctxt = Function.prove_termination NONE @@ -300,24 +300,24 @@ | 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 + 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 + 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 diff -r 8f8652a8107f -r 2f289c1f6cf1 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Sat Sep 11 05:56:49 2010 +0800 +++ b/Nominal-General/nominal_permeq.ML Sun Sep 12 22:46:40 2010 +0800 @@ -41,33 +41,33 @@ fun trace_enabled ctxt = Config.get ctxt trace_eqvt fun trace_msg ctxt result = -let - val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) - val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) -in - warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) -end + let + val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) + val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) + in + warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) + end fun trace_conv ctxt conv ctrm = -let - val result = conv ctrm -in - if Thm.is_reflexive result - then result - else (trace_msg ctxt result; result) -end + let + val result = conv ctrm + in + if Thm.is_reflexive result + then result + else (trace_msg ctxt result; result) + end (* this conversion always fails, but prints out the analysed term *) fun trace_info_conv ctxt ctrm = -let - val trm = term_of ctrm - val _ = case (head_of trm) of - @{const "Trueprop"} => () - | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) -in - Conv.no_conv ctrm -end + let + val trm = term_of ctrm + val _ = case (head_of trm) of + @{const "Trueprop"} => () + | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) + in + Conv.no_conv ctrm + end (* conversion for applications *) fun eqvt_apply_conv ctrm = @@ -101,39 +101,39 @@ | is_excluded _ _ = false fun progress_info_conv ctxt strict_flag excluded ctrm = -let - fun msg trm = - if is_excluded excluded trm then () else - (if strict_flag then error else warning) - ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) + let + fun msg trm = + if is_excluded excluded trm then () else + (if strict_flag then error else warning) + ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) - val _ = case (term_of ctrm) of - Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm - | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm - | _ => () -in - Conv.all_conv ctrm -end + val _ = case (term_of ctrm) of + Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm + | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm + | _ => () + in + Conv.all_conv ctrm + end (* main conversion *) fun eqvt_conv ctxt strict_flag user_thms excluded ctrm = -let - val first_conv_wrapper = - if trace_enabled ctxt - then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) - else Conv.first_conv + let + val first_conv_wrapper = + if trace_enabled ctxt + then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) + else Conv.first_conv - val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt - val post_thms = map safe_mk_equiv @{thms permute_pure} -in - first_conv_wrapper - [ Conv.rewrs_conv pre_thms, - eqvt_apply_conv, - eqvt_lambda_conv, - Conv.rewrs_conv post_thms, - progress_info_conv ctxt strict_flag excluded - ] ctrm -end + val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt + val post_thms = map safe_mk_equiv @{thms permute_pure} + in + first_conv_wrapper + [ Conv.rewrs_conv pre_thms, + eqvt_apply_conv, + eqvt_lambda_conv, + Conv.rewrs_conv post_thms, + progress_info_conv ctxt strict_flag excluded + ] ctrm + end (* the eqvt-tactics first eta-normalise goals in order to avoid problems with inductions in the diff -r 8f8652a8107f -r 2f289c1f6cf1 Nominal-General/nominal_thmdecls.ML --- a/Nominal-General/nominal_thmdecls.ML Sat Sep 11 05:56:49 2010 +0800 +++ b/Nominal-General/nominal_thmdecls.ML Sun Sep 12 22:46:40 2010 +0800 @@ -118,85 +118,85 @@ end fun eqvt_transform_eq ctxt thm = -let - val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) - handle TERM _ => error "Equivariance lemma must be an equality." - val (p, t) = dest_perm lhs - handle TERM _ => error "Equivariance lemma is not of the form p \ c... = c..." + let + val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) + handle TERM _ => error "Equivariance lemma must be an equality." + val (p, t) = dest_perm lhs + handle TERM _ => error "Equivariance lemma is not of the form p \ c... = c..." - val ps = get_perms rhs handle TERM _ => [] - val (c, c') = (head_of t, head_of rhs) - val msg = "Equivariance lemma is not of the right form " -in - if c <> c' - then error (msg ^ "(constants do not agree).") - else if is_bad_list (p :: ps) - then error (msg ^ "(permutations do not agree).") - else if not (rhs aconv (put_perm p t)) - then error (msg ^ "(arguments do not agree).") - else if is_Const t - then safe_mk_equiv thm - else - let - val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) - val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt - in - Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) - |> singleton (ProofContext.export ctxt' ctxt) - |> safe_mk_equiv - |> zero_var_indexes - end -end + val ps = get_perms rhs handle TERM _ => [] + val (c, c') = (head_of t, head_of rhs) + val msg = "Equivariance lemma is not of the right form " + in + if c <> c' + then error (msg ^ "(constants do not agree).") + else if is_bad_list (p :: ps) + then error (msg ^ "(permutations do not agree).") + else if not (rhs aconv (put_perm p t)) + then error (msg ^ "(arguments do not agree).") + else if is_Const t + then safe_mk_equiv thm + else + let + val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) + val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt + in + Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) + |> singleton (ProofContext.export ctxt' ctxt) + |> safe_mk_equiv + |> zero_var_indexes + end + end (* transforms equations into the "p o c == c"-form from R x1 ...xn ==> R (p o x1) ... (p o xn) *) fun eqvt_transform_imp_tac ctxt p p' thm = -let - val thy = ProofContext.theory_of ctxt - val cp = Thm.cterm_of thy p - val cp' = Thm.cterm_of thy (mk_minus p') - val thm' = Drule.cterm_instantiate [(cp, cp')] thm - val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} -in - EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, - rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] -end + let + val thy = ProofContext.theory_of ctxt + val cp = Thm.cterm_of thy p + val cp' = Thm.cterm_of thy (mk_minus p') + val thm' = Drule.cterm_instantiate [(cp, cp')] thm + val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} + in + EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, + rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] + end fun eqvt_transform_imp ctxt thm = -let - val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) - val (c, c') = (head_of prem, head_of concl) - val ps = get_perms concl handle TERM _ => [] - val p = try hd ps - val msg = "Equivariance lemma is not of the right form " -in - if c <> c' - then error (msg ^ "(constants do not agree).") - else if is_bad_list ps - then error (msg ^ "(permutations do not agree).") - else if not (concl aconv (put_perm (the p) prem)) - then error (msg ^ "(arguments do not agree).") - else - let - val prem' = mk_perm (the p) prem - val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) - val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt - in - Goal.prove ctxt' [] [] goal' - (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) - |> singleton (ProofContext.export ctxt' ctxt) - end -end + let + val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) + val (c, c') = (head_of prem, head_of concl) + val ps = get_perms concl handle TERM _ => [] + val p = try hd ps + val msg = "Equivariance lemma is not of the right form " + in + if c <> c' + then error (msg ^ "(constants do not agree).") + else if is_bad_list ps + then error (msg ^ "(permutations do not agree).") + else if not (concl aconv (put_perm (the p) prem)) + then error (msg ^ "(arguments do not agree).") + else + let + val prem' = mk_perm (the p) prem + val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) + val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt + in + Goal.prove ctxt' [] [] goal' + (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) + |> singleton (ProofContext.export ctxt' ctxt) + end + end fun eqvt_transform ctxt thm = - case (prop_of thm) of - @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ - (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => - eqvt_transform_eq ctxt thm - | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => - eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt - | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." + case (prop_of thm) of + @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ + (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => + eqvt_transform_eq ctxt thm + | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => + eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt + | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." (** attributes **) diff -r 8f8652a8107f -r 2f289c1f6cf1 Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Sat Sep 11 05:56:49 2010 +0800 +++ b/Nominal/Ex/ExPS8.thy Sun Sep 12 22:46:40 2010 +0800 @@ -58,15 +58,6 @@ thm fun_pats.fsupp thm fun_pats.supp - -ML {* -fun add_ss thms = - HOL_basic_ss addsimps thms - -fun symmetric thms = - map (fn thm => thm RS @{thm sym}) thms -*} - lemma "(fv_exp x = supp x) \ (fv_fnclause xa = supp xa \ fv_b_lrb xa = supp_rel alpha_b_lrb xa) \ @@ -92,7 +83,13 @@ "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and "fv_b_lrb y = supp_rel alpha_b_lrb y" -apply(induct "x::exp" and "y::fnclause" and xb and xc and xd and xe rule: fun_pats.inducts) +thm fun_pats.inducts +apply(induct rule: fun_pats.inducts(1)[where ?exp="x::exp"] + fun_pats.inducts(2)[where ?fnclause="y"] + fun_pats.inducts(3)[where ?fnclauses="xb"] + fun_pats.inducts(4)[where ?lrb="xc"] + fun_pats.inducts(5)[where ?lrbs="xd"] + fun_pats.inducts(6)[where ?pat="xe"]) thm fun_pats.inducts oops diff -r 8f8652a8107f -r 2f289c1f6cf1 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sat Sep 11 05:56:49 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Sun Sep 12 22:46:40 2010 +0800 @@ -2,6 +2,11 @@ imports "../Nominal2" begin +ML {* +Inductive.unpartition_rules +*} + + atom_decl name declare [[STEPS = 100]] diff -r 8f8652a8107f -r 2f289c1f6cf1 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Sat Sep 11 05:56:49 2010 +0800 +++ b/Nominal/nominal_dt_alpha.ML Sun Sep 12 22:46:40 2010 +0800 @@ -371,7 +371,8 @@ val true_trms = replicate (length alphas) (K @{term True}) fun apply_all x fs = map (fn f => f x) fs - val goals_rhs = + + val goals_rhs = group (props @ (alphas ~~ true_trms)) |> map snd |> map2 apply_all (args1 ~~ args2)