isabelle-cookbook: CookBook/comp_simproc.ML@b11653b11bd3 (annotated)

0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	1
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	fun dest_relcomp (t as (Const (@{const_name "Collect"}, _) $ Abs (_, pT, ex_exp))) =
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	let
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	val (T1, T2) = HOLogic.dest_prodT pT
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	val qs = Term.strip_qnt_vars "Ex" ex_exp
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	val bod = Term.strip_qnt_body "Ex" ex_exp
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	7
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	val (l, r, cond) = case bod of
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	Const ("op &", _)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	$ (Const ("op =", _) $ Bound idx
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	$ (Const ("Pair", _) $ l $ r))
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	$ cond
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	=> if idx = length qs then (l, r, cond)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	else raise TERM ("dest_relcomp", [t])
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	\| _ => raise TERM ("dest_relcomp", [t])
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	in
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	(T1, T2, qs, l, r, cond)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	end
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	\| dest_relcomp t = raise TERM ("dest_relcomp", [t])
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	fun mk_pair_compr (T1, T2, qs, l, r, cond) =
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	let
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	val pT = HOLogic.mk_prodT (T1, T2)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	val peq = HOLogic.eq_const pT $ Bound (length qs) $ (HOLogic.pair_const T1 T2 $ l $ r)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	val bod = HOLogic.mk_conj (peq, cond)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	in
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	HOLogic.Collect_const pT $
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	Abs ("uu_", pT, fold_rev (fn (a,T) => fn b => HOLogic.exists_const T $ Abs(a, T, b)) qs bod)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	end
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	30
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	fun join_compr c1 c2 : term =
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	let
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	val (T1, T2, qs1, l1, r1, cond1) = dest_relcomp c1
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	val (T2, T3, qs2, l2, r2, cond2) = dest_relcomp c2
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	35
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	val lift = incr_boundvars (length qs2)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	val cond = HOLogic.mk_conj (HOLogic.eq_const T2 $ lift r1 $ l2,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	HOLogic.mk_conj (lift cond1, cond2))
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	in
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	mk_pair_compr
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	(T1, T3, qs1 @ qs2, lift l1, r2, cond)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	end
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	43
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	val compr_compose_tac'=
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	EVERY1 (map (curry op o DETERM)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	[rtac @{thm set_ext},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	rtac @{thm iffI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	etac @{thm rel_compE},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	etac @{thm CollectE},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	etac @{thm CollectE},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	51	single_hyp_subst_tac 0,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	(fn i => REPEAT_DETERM (etac @{thm exE} i)),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	K (print_tac "A"),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	etac @{thm conjE},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	K (print_tac "B"),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	etac @{thm conjE},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	K (print_tac "B'"),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	etac @{thm Pair_inject},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	K (print_tac "C"),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	60	rotate_tac 1,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	K (print_tac "D"),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	etac @{thm Pair_inject},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	63	K (print_tac "E"),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	64	single_hyp_subst_tac 2,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	65	single_hyp_subst_tac 3,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	single_hyp_subst_tac 3,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	67	rtac @{thm CollectI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	(fn i => REPEAT_DETERM (rtac @{thm exI} i)),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	69	rtac @{thm conjI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	rtac @{thm refl},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	rtac @{thm conjI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	assume_tac,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	rtac @{thm conjI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	assume_tac,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	assume_tac,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	etac @{thm CollectE},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	(fn i => REPEAT (etac @{thm exE} i)),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	etac @{thm conjE},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	single_hyp_subst_tac 0,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	etac @{thm conjE},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	etac @{thm conjE},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	rtac @{thm rel_compI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	rtac @{thm CollectI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	(fn i => REPEAT (rtac @{thm exI} i)),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	rtac @{thm conjI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	rtac @{thm refl},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	assume_tac,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	88	rtac @{thm CollectI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	(fn i => REPEAT (rtac @{thm exI} i)),
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	90	rtac @{thm conjI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	stac @{thm Pair_eq},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	92	rtac @{thm conjI},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	assume_tac,
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	rtac @{thm refl},
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	95	assume_tac])
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	96
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	97
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	98	fun compose_simproc _ ss ct : thm option =
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	99	let
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	100	val thy = theory_of_cterm ct
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	101	val sCt as (_ $ s $ t) = term_of ct
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	102	val T = fastype_of sCt
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	val g : term = Logic.mk_equals (sCt, join_compr t s)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	104	(* val _ = Output.tracing (Syntax.string_of_term (Simplifier.the_context ss) g)*)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	105	in
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	106	SOME (Goal.prove_internal [] (cterm_of thy g)
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	107	(K (rtac @{thm eq_reflection} 1
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	108	THEN compr_compose_tac')))
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	end
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	110	handle TERM _ => NONE
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	111

author	Christian Urban <urbanc@in.tum.de>
	Mon, 20 Oct 2008 06:22:11 +0000
changeset 41	b11653b11bd3
parent 0	02503850a8cf
permissions	-rw-r--r--