nominal2: Nominal-General/nominal_permeq.ML@2f289c1f6cf1 (annotated)

1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	1	(* Title: nominal_permeq.ML
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	2	Author: Christian Urban
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	3	Author: Brian Huffman
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	*)
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	signature NOMINAL_PERMEQ =
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	sig
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	8	val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	9	val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	10
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	11	val perm_simp_meth: thm list * string list -> Proof.context -> Method.method
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	12	val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	13	val args_parser: (thm list * string list) context_parser
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	14
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	15	val trace_eqvt: bool Config.T
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	16	val setup: theory -> theory
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	end;
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	19	(*
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	20
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	21	- eqvt_tac and eqvt_strict_tac take a list of theorems
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	22	which are first tried to simplify permutations
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	23
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	24	the string list contains constants that should not be
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	25	analysed (for example there is no raw eqvt-lemma for
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	26	the constant The); therefore it should not be analysed
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	27
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	28	- setting [[trace_eqvt = true]] switches on tracing
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	29	information
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	30
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	*)
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	32
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	structure Nominal_Permeq: NOMINAL_PERMEQ =
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	struct
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	35
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	36	open Nominal_ThmDecls;
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	37
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	38	(* tracing infrastructure *)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	39	val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	40
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	41	fun trace_enabled ctxt = Config.get ctxt trace_eqvt
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	42
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	43	fun trace_msg ctxt result =
2477 2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	44	let
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	45	val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	46	val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	47	in
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	48	warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	49	end
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	50
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	51	fun trace_conv ctxt conv ctrm =
2477 2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	52	let
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	53	val result = conv ctrm
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	54	in
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	55	if Thm.is_reflexive result
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	56	then result
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	57	else (trace_msg ctxt result; result)
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	58	end
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	59
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	60	(* this conversion always fails, but prints
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	61	out the analysed term *)
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	62	fun trace_info_conv ctxt ctrm =
2477 2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	63	let
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	64	val trm = term_of ctrm
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	65	val _ = case (head_of trm) of
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	66	@{const "Trueprop"} => ()
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	67	\| _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm)
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	68	in
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	69	Conv.no_conv ctrm
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	70	end
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	71
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	72	(* conversion for applications *)
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	73	fun eqvt_apply_conv ctrm =
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	74	case (term_of ctrm) of
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	75	Const (@{const_name "permute"}, _) $ _ $ (_ $ _) =>
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	76	let
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	77	val (perm, t) = Thm.dest_comb ctrm
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	val (_, p) = Thm.dest_comb perm
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	val (f, x) = Thm.dest_comb t
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	val a = ctyp_of_term x;
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	val b = ctyp_of_term t;
2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	val ty_insts = map SOME [b, a]
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	83	val term_insts = map SOME [p, f, x]
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	in
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	85	Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	end
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	87	\| _ => Conv.no_conv ctrm
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	88
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	89	(* conversion for lambdas *)
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	90	fun eqvt_lambda_conv ctrm =
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	91	case (term_of ctrm) of
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	92	Const (@{const_name "permute"}, _) $ _ $ (Abs _) =>
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	93	Conv.rewr_conv @{thm eqvt_lambda} ctrm
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	94	\| _ => Conv.no_conv ctrm
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	95
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	96
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	97	(* conversion that raises an error or prints a warning message,
6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	98	if a permutation on a constant or application cannot be analysed *)
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	99
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	100	fun is_excluded excluded (Const (a, _)) = member (op=) excluded a
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	101	\| is_excluded _ _ = false
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	102
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	103	fun progress_info_conv ctxt strict_flag excluded ctrm =
2477 2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	104	let
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	105	fun msg trm =
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	106	if is_excluded excluded trm then () else
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	107	(if strict_flag then error else warning)
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	108	("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	109
2477 2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	110	val _ = case (term_of ctrm) of
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	111	Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	112	\| Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	113	\| _ => ()
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	114	in
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	115	Conv.all_conv ctrm
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	116	end
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	117
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	118	(* main conversion *)
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	119	fun eqvt_conv ctxt strict_flag user_thms excluded ctrm =
2477 2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	120	let
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	121	val first_conv_wrapper =
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	122	if trace_enabled ctxt
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	123	then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	124	else Conv.first_conv
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	125
2477 2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	126	val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	127	val post_thms = map safe_mk_equiv @{thms permute_pure}
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	128	in
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	129	first_conv_wrapper
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	130	[ Conv.rewrs_conv pre_thms,
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	131	eqvt_apply_conv,
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	132	eqvt_lambda_conv,
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	133	Conv.rewrs_conv post_thms,
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	134	progress_info_conv ctxt strict_flag excluded
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	135	] ctrm
2f289c1f6cf1 tuned code Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	136	end
1037 2845e736dc1a added a first eqvt_tac which pushes permutations inside terms Christian Urban <urbanc@in.tum.de> parents: diff changeset	137
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	138	(* the eqvt-tactics first eta-normalise goals in
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	139	order to avoid problems with inductions in the
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	140	equivaraince command. *)
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	141
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	142	(* raises an error if some permutations cannot be eliminated *)
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	143	fun eqvt_strict_tac ctxt user_thms excluded =
2150 6297629f024c updated to new Isabelle (More_Conv -> Conv) Christian Urban <urbanc@in.tum.de> parents: 2127 diff changeset	144	CONVERSION (Conv.top_conv
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	145	(fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	146
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	147	(* prints a warning message if some permutations cannot be eliminated *)
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	148	fun eqvt_tac ctxt user_thms excluded =
2150 6297629f024c updated to new Isabelle (More_Conv -> Conv) Christian Urban <urbanc@in.tum.de> parents: 2127 diff changeset	149	CONVERSION (Conv.top_conv
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2069 diff changeset	150	(fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	151
1801 6d2a39db3862 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	152	(* setup of the configuration value *)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	153	val setup =
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	154	trace_eqvt_setup
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	155
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	156
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	157	( methods )
2291 20ee31bc34d5 proper parser for "exclude:" Christian Urban <urbanc@in.tum.de> parents: 2150 diff changeset	158	fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan
20ee31bc34d5 proper parser for "exclude:" Christian Urban <urbanc@in.tum.de> parents: 2150 diff changeset	159
20ee31bc34d5 proper parser for "exclude:" Christian Urban <urbanc@in.tum.de> parents: 2150 diff changeset	160	val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) \|--
20ee31bc34d5 proper parser for "exclude:" Christian Urban <urbanc@in.tum.de> parents: 2150 diff changeset	161	Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) [];
20ee31bc34d5 proper parser for "exclude:" Christian Urban <urbanc@in.tum.de> parents: 2150 diff changeset	162
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	163	val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) \|--
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	164	(Scan.repeat (Args.const true))) []
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	165
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	166	val args_parser = add_thms_parser -- exclude_consts_parser
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	167
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	168	fun perm_simp_meth (thms, consts) ctxt =
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	169	SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	170
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	171	fun perm_strict_simp_meth (thms, consts) ctxt =
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	172	SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))
51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	173
2069 2b6ba4d4e19a Fixes for new isabelle Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2064 diff changeset	174	end; (* structure *)

author	Christian Urban <urbanc@in.tum.de>
	Sun, 12 Sep 2010 22:46:40 +0800
changeset 2477	2f289c1f6cf1
parent 2301	8732ff59068b
permissions	-rw-r--r--