--- 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 *)
--- 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
--- 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
--- 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 \<bullet> 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 \<bullet> 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 **)
--- 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) \<and>
(fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and>
@@ -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
--- 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]]
--- 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)