nominal2: Nominal/Ex/Lambda.thy@331873ebc5cd (annotated)

1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	1	theory Lambda
2424 621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	2	imports "../NewParser"
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	6	declare [[STEPS = 20]]
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	8	class s1
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	9	class s2
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	10
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	11	nominal_datatype lambda:
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	12	('a, 'b) lam =
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: 1797 diff changeset	13	Var "name"
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	14	\| App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	15	\| Lam x::"name" l::"('a, 'b) lam" bind x in l
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	16
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	17	term Var_raw
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	18	term Var
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	19	term App_raw
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	20	term App
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	21	thm Var_def App_def Lam_def
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	22	term abs_lam
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	23
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	24	thm distinct
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	25	thm lam_raw.inducts
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	26	thm lam_raw.exhaust
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	27	thm fv_defs
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	28	thm bn_defs
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	29	thm perm_simps
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	30	thm perm_laws
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	31	thm lam_raw.size
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	32	thm eq_iff
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	33	thm eq_iff_simps
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	34	thm fv_eqvt
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	35	thm bn_eqvt
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	36	thm size_eqvt
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	37
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	38	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	39	val qtys = [@{typ "('a::{s1, fs}, 'b::{s2,fs}) lam"}]
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	40	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	41
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	42	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	43	val thm_a = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	44	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	45
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	46	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	47	val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.induct}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	48	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	49
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	50	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	51	val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.exhaust}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	52	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	53
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	54	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	55	val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	56	*}
2425 715ab84065a0 nominal_datatypes with type variables do not work Christian Urban <urbanc@in.tum.de> parents: 2424 diff changeset	57
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	58	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	59	val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	60	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	61
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	62	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	63	val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	64	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	65
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	66	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	67	val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	68	prod.cases}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	69	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	70
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	71	(* HERE *)
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	72
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	73	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	74	val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	75	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	76
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	77	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	78	val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff_simps}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	79	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	80
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	81
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	82	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	83	val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	84	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	85
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	86	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	87	val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	88	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	89
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	90	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	91	val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	92	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	93
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	94	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	95	val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	96	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	97
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	98
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	99
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	100	ML {*
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	101	space_explode "_raw" "bla_raw2_foo_raw3.0"
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	102	*}
331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	103
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	104
2424 621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	105
621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	106	thm eq_iff
621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	107
1845 b7423c6b5564 deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell Christian Urban <urbanc@in.tum.de> parents: 1835 diff changeset	108	thm lam.fv
b7423c6b5564 deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell Christian Urban <urbanc@in.tum.de> parents: 1835 diff changeset	109	thm lam.supp
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: 1797 diff changeset	110	lemmas supp_fn' = lam.fv[simplified lam.supp]
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: 1797 diff changeset	111
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	112	declare lam.perm[eqvt]
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	113
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2041 diff changeset	114
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: 1797 diff changeset	115	section {* Strong Induction Principles*}
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	116
2041 3842464ee03b Move 2 more to NewParser Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1954 diff changeset	117	(*
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	118	Old way of establishing strong induction
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	119	principles by chosing a fresh name.
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	120	*)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	121	lemma
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	122	fixes c::"'a::fs"
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: 1797 diff changeset	123	assumes a1: "\<And>name c. P c (Var name)"
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: 1797 diff changeset	124	and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
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: 1797 diff changeset	125	and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
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: 1797 diff changeset	126	shows "P c lam"
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	127	proof -
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: 1797 diff changeset	128	have "\<And>p. P c (p \<bullet> lam)"
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: 1797 diff changeset	129	apply(induct lam arbitrary: c rule: lam.induct)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	130	apply(perm_simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	131	apply(rule a1)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	132	apply(perm_simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	133	apply(rule a2)
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	134	apply(assumption)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	135	apply(assumption)
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: 1797 diff changeset	136	apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))")
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	137	defer
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	138	apply(simp add: fresh_def)
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: 1797 diff changeset	139	apply(rule_tac X="supp (c, Lam (p \<bullet> name) (p \<bullet> lam))" in obtain_at_base)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	140	apply(simp add: supp_Pair finite_supp)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	141	apply(blast)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	142	apply(erule exE)
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: 1797 diff changeset	143	apply(rule_tac t="p \<bullet> Lam name lam" and
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: 1797 diff changeset	144	s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lam name lam" in subst)
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: 1797 diff changeset	145	apply(simp del: lam.perm)
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: 1797 diff changeset	146	apply(subst lam.perm)
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: 1797 diff changeset	147	apply(subst (2) lam.perm)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	148	apply(rule flip_fresh_fresh)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	149	apply(simp add: fresh_def)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	150	apply(simp only: supp_fn')
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	151	apply(simp)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	152	apply(simp add: fresh_Pair)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	153	apply(simp)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	154	apply(rule a3)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	155	apply(simp add: fresh_Pair)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	156	apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	157	apply(simp)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	158	done
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: 1797 diff changeset	159	then have "P c (0 \<bullet> lam)" by blast
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: 1797 diff changeset	160	then show "P c lam" by simp
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	161	qed
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	162
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	163	(*
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	164	New way of establishing strong induction
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	165	principles by using a appropriate permutation.
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	166	*)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	167	lemma
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	168	fixes c::"'a::fs"
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: 1797 diff changeset	169	assumes a1: "\<And>name c. P c (Var name)"
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: 1797 diff changeset	170	and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
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: 1797 diff changeset	171	and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
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: 1797 diff changeset	172	shows "P c lam"
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	173	proof -
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: 1797 diff changeset	174	have "\<And>p. P c (p \<bullet> lam)"
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: 1797 diff changeset	175	apply(induct lam arbitrary: c rule: lam.induct)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	176	apply(perm_simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	177	apply(rule a1)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	178	apply(perm_simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	179	apply(rule a2)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	180	apply(assumption)
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	181	apply(assumption)
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: 1797 diff changeset	182	apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q")
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	183	apply(erule exE)
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: 1797 diff changeset	184	apply(rule_tac t="p \<bullet> Lam name lam" and
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: 1797 diff changeset	185	s="q \<bullet> p \<bullet> Lam name lam" in subst)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	186	defer
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	187	apply(simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	188	apply(rule a3)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	189	apply(simp add: eqvts fresh_star_def)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	190	apply(drule_tac x="q + p" in meta_spec)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	191	apply(simp)
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	192	apply(rule at_set_avoiding2)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	193	apply(simp add: finite_supp)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	194	apply(simp add: finite_supp)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	195	apply(simp add: finite_supp)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	196	apply(perm_simp)
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	197	apply(simp add: fresh_star_def fresh_def supp_fn')
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	198	apply(rule supp_perm_eq)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	199	apply(simp)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	200	done
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: 1797 diff changeset	201	then have "P c (0 \<bullet> lam)" by blast
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: 1797 diff changeset	202	then show "P c lam" by simp
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	203	qed
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	204
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	205	section {* Typing *}
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	206
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	207	nominal_datatype ty =
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	208	TVar string
1810 894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	209	\| TFun ty ty
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	210
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	211	notation
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	212	TFun ("_ \<rightarrow> _")
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	213
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	214	declare ty.perm[eqvt]
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	215
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	216	inductive
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	217	valid :: "(name \<times> ty) list \<Rightarrow> bool"
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	218	where
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	219	"valid []"
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	220	\| "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	221
1828 f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	222	inductive
f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	223	typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	224	where
f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	225	t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	226	\| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
1828 f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	227	\| t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	228
1831 16653e702d89 first working version of the automatic equivariance procedure Christian Urban <urbanc@in.tum.de> parents: 1828 diff changeset	229	equivariance valid
16653e702d89 first working version of the automatic equivariance procedure Christian Urban <urbanc@in.tum.de> parents: 1828 diff changeset	230	equivariance typing
1816 56cebe7f8e24 some small tunings (incompleted work in Lambda.thy) Christian Urban <urbanc@in.tum.de> parents: 1814 diff changeset	231
1831 16653e702d89 first working version of the automatic equivariance procedure Christian Urban <urbanc@in.tum.de> parents: 1828 diff changeset	232	thm valid.eqvt
16653e702d89 first working version of the automatic equivariance procedure Christian Urban <urbanc@in.tum.de> parents: 1828 diff changeset	233	thm typing.eqvt
1811 ae176476b525 implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1810 diff changeset	234	thm eqvts
ae176476b525 implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1810 diff changeset	235	thm eqvts_raw
ae176476b525 implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1810 diff changeset	236
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	237	thm typing.induct[of "\<Gamma>" "t" "T", no_vars]
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	238
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	239	lemma
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	240	fixes c::"'a::fs"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	241	assumes a: "\<Gamma> \<turnstile> t : T"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	242	and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	243	and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk>
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	244	\<Longrightarrow> P c \<Gamma> (App t1 t2) T2"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	245	and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>atom x \<sharp> c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk>
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	246	\<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	247	shows "P c \<Gamma> t T"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	248	proof -
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	249	from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	250	proof (induct)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	251	case (t_Var \<Gamma> x T p c)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	252	then show ?case
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	253	apply -
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	254	apply(perm_strict_simp)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	255	apply(rule a1)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	256	apply(drule_tac p="p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	257	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	258	apply(assumption)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	259	apply(rotate_tac 1)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	260	apply(drule_tac p="p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	261	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	262	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	263	done
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	264	next
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	265	case (t_App \<Gamma> t1 T1 T2 t2 p c)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	266	then show ?case
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	267	apply -
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	268	apply(perm_strict_simp)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	269	apply(rule a2)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	270	apply(drule_tac p="p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	271	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	272	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	273	apply(assumption)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	274	apply(rotate_tac 2)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	275	apply(drule_tac p="p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	276	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	277	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	278	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	279	done
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	280	next
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	281	case (t_Lam x \<Gamma> T1 t T2 p c)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	282	then show ?case
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	283	apply -
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	284	apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and>
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	285	supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	286	apply(erule exE)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	287	apply(rule_tac t="p \<bullet> \<Gamma>" and s="(q + p) \<bullet> \<Gamma>" in subst)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	288	apply(simp only: permute_plus)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	289	apply(rule supp_perm_eq)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	290	apply(simp add: supp_Pair fresh_star_union)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	291	apply(rule_tac t="p \<bullet> Lam x t" and s="(q + p) \<bullet> Lam x t" in subst)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	292	apply(simp only: permute_plus)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	293	apply(rule supp_perm_eq)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	294	apply(simp add: supp_Pair fresh_star_union)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	295	apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	296	apply(simp only: permute_plus)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	297	apply(rule supp_perm_eq)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	298	apply(simp add: supp_Pair fresh_star_union)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	299	apply(simp (no_asm) only: eqvts)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	300	apply(rule a3)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	301	apply(simp only: eqvts permute_plus)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	302	apply(simp add: fresh_star_def)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	303	apply(drule_tac p="q + p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	304	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	305	apply(assumption)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	306	apply(rotate_tac 1)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	307	apply(drule_tac p="q + p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	308	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	309	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	310	apply(drule_tac x="d" in meta_spec)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	311	apply(drule_tac x="q + p" in meta_spec)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	312	apply(perm_strict_simp add: permute_minus_cancel)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	313	apply(assumption)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	314	apply(rule at_set_avoiding2)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	315	apply(simp add: finite_supp)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	316	apply(simp add: finite_supp)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	317	apply(simp add: finite_supp)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	318	apply(rule_tac p="-p" in permute_boolE)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	319	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	320	(* supplied by the user *)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	321	apply(simp add: fresh_star_prod)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	322	apply(simp add: fresh_star_def)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	323	sorry
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	324	qed
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	325	then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" .
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	326	then show "P c \<Gamma> t T" by simp
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	327	qed
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	328
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	329
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	330
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	331
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	332
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	333
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	334
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	335	inductive
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	336	tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	337	for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	338	where
1835 636de31888a6 tuned and removed dead code Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	339	aa: "tt r a a"
636de31888a6 tuned and removed dead code Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	340	\| bb: "tt r a b ==> tt r a c"
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	341
1835 636de31888a6 tuned and removed dead code Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	342	(* PROBLEM: derived eqvt-theorem does not conform with [eqvt]
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	343	equivariance tt
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	344	*)
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	345
1810 894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	346
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	347	inductive
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	348	alpha_lam_raw'
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	349	where
1861 226b797868dc some tuning of eqvt-infrastructure Christian Urban <urbanc@in.tum.de> parents: 1845 diff changeset	350	a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
226b797868dc some tuning of eqvt-infrastructure Christian Urban <urbanc@in.tum.de> parents: 1845 diff changeset	351	\| a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
1810 894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	352	alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
1865 b71b838b0a75 Finished proof in Lambda.thy Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1863 diff changeset	353	\| a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
1810 894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	354	alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	355
1866 6d4e4bf9bce6 automatic proofs for equivariance of alphas Christian Urban <urbanc@in.tum.de> parents: 1865 diff changeset	356	equivariance alpha_lam_raw'
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	357
1861 226b797868dc some tuning of eqvt-infrastructure Christian Urban <urbanc@in.tum.de> parents: 1845 diff changeset	358	thm eqvts_raw
226b797868dc some tuning of eqvt-infrastructure Christian Urban <urbanc@in.tum.de> parents: 1845 diff changeset	359
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: 1797 diff changeset	360	section {* size function *}
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: 1797 diff changeset	361
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: 1797 diff changeset	362	lemma size_eqvt_raw:
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: 1797 diff changeset	363	fixes t::"lam_raw"
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: 1797 diff changeset	364	shows "size (pi \<bullet> t) = size 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: 1797 diff changeset	365	apply (induct rule: lam_raw.inducts)
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: 1797 diff changeset	366	apply simp_all
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: 1797 diff changeset	367	done
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: 1797 diff changeset	368
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: 1797 diff changeset	369	instantiation lam :: size
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: 1797 diff changeset	370	begin
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: 1797 diff changeset	371
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: 1797 diff changeset	372	quotient_definition
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: 1797 diff changeset	373	"size_lam :: lam \<Rightarrow> nat"
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: 1797 diff changeset	374	is
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: 1797 diff changeset	375	"size :: lam_raw \<Rightarrow> nat"
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: 1797 diff changeset	376
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: 1797 diff changeset	377	lemma size_rsp:
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: 1797 diff changeset	378	"alpha_lam_raw x y \<Longrightarrow> size x = size y"
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: 1797 diff changeset	379	apply (induct rule: alpha_lam_raw.inducts)
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: 1797 diff changeset	380	apply (simp_all only: lam_raw.size)
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: 1797 diff changeset	381	apply (simp_all only: alphas)
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: 1797 diff changeset	382	apply clarify
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: 1797 diff changeset	383	apply (simp_all only: size_eqvt_raw)
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: 1797 diff changeset	384	done
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: 1797 diff changeset	385
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: 1797 diff changeset	386	lemma [quot_respect]:
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: 1797 diff changeset	387	"(alpha_lam_raw ===> op =) size size"
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: 1797 diff changeset	388	by (simp_all add: size_rsp)
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: 1797 diff changeset	389
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: 1797 diff changeset	390	lemma [quot_preserve]:
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: 1797 diff changeset	391	"(rep_lam ---> id) size = size"
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: 1797 diff changeset	392	by (simp_all add: size_lam_def)
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: 1797 diff changeset	393
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: 1797 diff changeset	394	instance
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: 1797 diff changeset	395	by default
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: 1797 diff changeset	396
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: 1797 diff changeset	397	end
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: 1797 diff changeset	398
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: 1797 diff changeset	399	lemmas size_lam[simp] =
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: 1797 diff changeset	400	lam_raw.size(4)[quot_lifted]
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: 1797 diff changeset	401	lam_raw.size(5)[quot_lifted]
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: 1797 diff changeset	402	lam_raw.size(6)[quot_lifted]
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: 1797 diff changeset	403
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: 1797 diff changeset	404	(* is this needed? *)
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: 1797 diff changeset	405	lemma [measure_function]:
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: 1797 diff changeset	406	"is_measure (size::lam\<Rightarrow>nat)"
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: 1797 diff changeset	407	by (rule is_measure_trivial)
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: 1797 diff changeset	408
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: 1797 diff changeset	409	section {* Matching *}
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: 1797 diff changeset	410
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: 1797 diff changeset	411	definition
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: 1797 diff changeset	412	MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
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: 1797 diff changeset	413	where
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: 1797 diff changeset	414	"MATCH M d x \<equiv> if (\<exists>!r. \<exists>q. M q = (True, x, r)) then (THE r. \<exists>q. M q = (True, x, r)) else d"
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: 1797 diff changeset	415
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: 1797 diff changeset	416	(*
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: 1797 diff changeset	417	lemma MATCH_eqvt:
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: 1797 diff changeset	418	shows "p \<bullet> (MATCH M d x) = MATCH (p \<bullet> M) (p \<bullet> d) (p \<bullet> x)"
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: 1797 diff changeset	419	unfolding MATCH_def
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: 1797 diff changeset	420	apply(perm_simp the_eqvt)
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: 1797 diff changeset	421	apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
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: 1797 diff changeset	422	apply(simp)
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: 1797 diff changeset	423	thm eqvts_raw
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: 1797 diff changeset	424	apply(subst if_eqvt)
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: 1797 diff changeset	425	apply(subst ex1_eqvt)
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: 1797 diff changeset	426	apply(subst permute_fun_def)
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: 1797 diff changeset	427	apply(subst ex_eqvt)
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: 1797 diff changeset	428	apply(subst permute_fun_def)
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: 1797 diff changeset	429	apply(subst eq_eqvt)
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: 1797 diff changeset	430	apply(subst permute_fun_app_eq[where f="M"])
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: 1797 diff changeset	431	apply(simp only: permute_minus_cancel)
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: 1797 diff changeset	432	apply(subst permute_prod.simps)
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: 1797 diff changeset	433	apply(subst permute_prod.simps)
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: 1797 diff changeset	434	apply(simp only: permute_minus_cancel)
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: 1797 diff changeset	435	apply(simp only: permute_bool_def)
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: 1797 diff changeset	436	apply(simp)
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: 1797 diff changeset	437	apply(subst ex1_eqvt)
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: 1797 diff changeset	438	apply(subst permute_fun_def)
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: 1797 diff changeset	439	apply(subst ex_eqvt)
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: 1797 diff changeset	440	apply(subst permute_fun_def)
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: 1797 diff changeset	441	apply(subst eq_eqvt)
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: 1797 diff changeset	442
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: 1797 diff changeset	443	apply(simp only: eqvts)
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: 1797 diff changeset	444	apply(simp)
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: 1797 diff changeset	445	apply(subgoal_tac "(p \<bullet> (\<exists>!r. \<exists>q. M q = (True, x, r))) = (\<exists>!r. \<exists>q. (p \<bullet> M) q = (True, p \<bullet> x, r))")
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: 1797 diff changeset	446	apply(drule sym)
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: 1797 diff changeset	447	apply(simp)
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: 1797 diff changeset	448	apply(rule impI)
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: 1797 diff changeset	449	apply(simp add: perm_bool)
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: 1797 diff changeset	450	apply(rule trans)
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: 1797 diff changeset	451	apply(rule pt_the_eqvt[OF pta at])
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: 1797 diff changeset	452	apply(assumption)
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: 1797 diff changeset	453	apply(simp add: pt_ex_eqvt[OF pt at])
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: 1797 diff changeset	454	apply(simp add: pt_eq_eqvt[OF ptb at])
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: 1797 diff changeset	455	apply(rule cheat)
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: 1797 diff changeset	456	apply(rule trans)
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: 1797 diff changeset	457	apply(rule pt_ex1_eqvt)
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: 1797 diff changeset	458	apply(rule pta)
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: 1797 diff changeset	459	apply(rule at)
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: 1797 diff changeset	460	apply(simp add: pt_ex_eqvt[OF pt at])
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: 1797 diff changeset	461	apply(simp add: pt_eq_eqvt[OF ptb at])
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: 1797 diff changeset	462	apply(subst pt_pi_rev[OF pta at])
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: 1797 diff changeset	463	apply(subst pt_fun_app_eq[OF pt at])
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: 1797 diff changeset	464	apply(subst pt_pi_rev[OF pt at])
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: 1797 diff changeset	465	apply(simp)
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: 1797 diff changeset	466	done
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: 1797 diff changeset	467
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: 1797 diff changeset	468	lemma MATCH_cng:
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: 1797 diff changeset	469	assumes a: "M1 = M2" "d1 = d2"
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: 1797 diff changeset	470	shows "MATCH M1 d1 x = MATCH M2 d2 x"
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: 1797 diff changeset	471	using a by simp
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: 1797 diff changeset	472
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: 1797 diff changeset	473	lemma MATCH_eq:
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: 1797 diff changeset	474	assumes a: "t = l x" "G x" "\<And>x'. t = l x' \<Longrightarrow> G x' \<Longrightarrow> r x' = r x"
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: 1797 diff changeset	475	shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = r x"
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: 1797 diff changeset	476	using a
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: 1797 diff changeset	477	unfolding MATCH_def
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: 1797 diff changeset	478	apply(subst if_P)
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: 1797 diff changeset	479	apply(rule_tac a="r x" in ex1I)
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: 1797 diff changeset	480	apply(rule_tac x="x" in exI)
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: 1797 diff changeset	481	apply(blast)
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: 1797 diff changeset	482	apply(erule exE)
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: 1797 diff changeset	483	apply(drule_tac x="q" in meta_spec)
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: 1797 diff changeset	484	apply(auto)[1]
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: 1797 diff changeset	485	apply(rule the_equality)
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: 1797 diff changeset	486	apply(blast)
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: 1797 diff changeset	487	apply(erule exE)
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: 1797 diff changeset	488	apply(drule_tac x="q" in meta_spec)
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: 1797 diff changeset	489	apply(auto)[1]
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: 1797 diff changeset	490	done
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: 1797 diff changeset	491
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: 1797 diff changeset	492	lemma MATCH_eq2:
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: 1797 diff changeset	493	assumes a: "t = l x1 x2" "G x1 x2" "\<And>x1' x2'. t = l x1' x2' \<Longrightarrow> G x1' x2' \<Longrightarrow> r x1' x2' = r x1 x2"
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: 1797 diff changeset	494	shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = r x1 x2"
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: 1797 diff changeset	495	sorry
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: 1797 diff changeset	496
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: 1797 diff changeset	497	lemma MATCH_neq:
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: 1797 diff changeset	498	assumes a: "\<And>x. t = l x \<Longrightarrow> G x \<Longrightarrow> 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: 1797 diff changeset	499	shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = d"
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: 1797 diff changeset	500	using a
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: 1797 diff changeset	501	unfolding MATCH_def
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: 1797 diff changeset	502	apply(subst if_not_P)
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: 1797 diff changeset	503	apply(blast)
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: 1797 diff changeset	504	apply(rule refl)
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: 1797 diff changeset	505	done
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: 1797 diff changeset	506
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: 1797 diff changeset	507	lemma MATCH_neq2:
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: 1797 diff changeset	508	assumes a: "\<And>x1 x2. t = l x1 x2 \<Longrightarrow> G x1 x2 \<Longrightarrow> 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: 1797 diff changeset	509	shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = d"
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: 1797 diff changeset	510	using a
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: 1797 diff changeset	511	unfolding MATCH_def
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: 1797 diff changeset	512	apply(subst if_not_P)
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: 1797 diff changeset	513	apply(auto)
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: 1797 diff changeset	514	done
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: 1797 diff changeset	515	*)
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: 1797 diff changeset	516
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	517	ML {*
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	518	fun mk_avoids ctxt params name set =
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	519	let
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	520	val (_, ctxt') = ProofContext.add_fixes
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	521	(map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	522	fun mk s =
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	523	let
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	524	val t = Syntax.read_term ctxt' s;
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	525	val t' = list_abs_free (params, t) \|>
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	526	funpow (length params) (fn Abs (_, _, t) => t)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	527	in (t', HOLogic.dest_setT (fastype_of t)) end
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	528	handle TERM _ =>
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	529	error ("Expression " ^ quote s ^ " to be avoided in case " ^
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	530	quote name ^ " is not a set type");
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	531	fun add_set p [] = [p]
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	532	\| add_set (t, T) ((u, U) :: ps) =
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	533	if T = U then
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	534	let val S = HOLogic.mk_setT T
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	535	in (Const (@{const_name sup}, S --> S --> S) $ u $ t, T) :: ps
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	536	end
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	537	else (u, U) :: add_set (t, T) ps
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	538	in
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	539	(mk #> add_set) set
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	540	end;
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	541	*}
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	542
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	543
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	544	ML {*
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	545	writeln (commas (map (Syntax.string_of_term @{context} o fst)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	546	(mk_avoids @{context} [] "t_Var" "{x}" [])))
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	547	*}
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	548
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	549
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	550	ML {*
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	551
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	552	fun prove_strong_ind (pred_name, avoids) ctxt =
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	553	Proof.theorem NONE (K I) [] ctxt
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	554
2169 61a89e41c55b Renamings. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2162 diff changeset	555	local structure P = Parse and K = Keyword in
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	556
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	557	val _ =
2169 61a89e41c55b Renamings. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2162 diff changeset	558	Outer_Syntax.local_theory_to_proof "nominal_inductive"
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	559	"proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	560	(P.xname -- (Scan.optional (P.$$$ "avoids" \|-- P.enum1 "\|" (P.name --
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	561	(P.$$$ ":" \|-- P.and_list1 P.term))) []) >> prove_strong_ind)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	562
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	563	end;
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	564
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	565	*}
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	566
1950 7de54c9f81ac eliminated command so that all compiles Christian Urban <urbanc@in.tum.de> parents: 1949 diff changeset	567	(*
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	568	nominal_inductive typing
1950 7de54c9f81ac eliminated command so that all compiles Christian Urban <urbanc@in.tum.de> parents: 1949 diff changeset	569	*)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	570
2157 a1d27083e688 subst experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	571	(* Substitution *)
2159 ce00205e07ab Single variable substitution Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2158 diff changeset	572
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	573	primrec match_Var_raw where
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	574	"match_Var_raw (Var_raw x) = Some x"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	575	\| "match_Var_raw (App_raw x y) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	576	\| "match_Var_raw (Lam_raw n t) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	577
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	578	quotient_definition
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	579	"match_Var :: lam \<Rightarrow> name option"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	580	is match_Var_raw
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	581
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	582	lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	583	apply rule
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	584	apply (induct_tac a b rule: alpha_lam_raw.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	585	apply simp_all
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	586	done
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	587
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	588	lemmas match_Var_simps = match_Var_raw.simps[quot_lifted]
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	589
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	590	primrec match_App_raw where
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	591	"match_App_raw (Var_raw x) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	592	\| "match_App_raw (App_raw x y) = Some (x, y)"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	593	\| "match_App_raw (Lam_raw n t) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	594
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	595	quotient_definition
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	596	"match_App :: lam \<Rightarrow> (lam \<times> lam) option"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	597	is match_App_raw
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	598
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	599	lemma [quot_respect]:
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	600	"(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	601	apply (intro fun_relI)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	602	apply (induct_tac a b rule: alpha_lam_raw.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	603	apply simp_all
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	604	done
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	605
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	606	lemmas match_App_simps = match_App_raw.simps[quot_lifted]
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	607
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	608	definition new where
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	609	"new (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)"
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	610
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	611	definition
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	612	"match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	613	(let z = new (S, t) in Some (z, THE s. t = Lam z s)) else None)"
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	614
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	615	lemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)"
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	616	apply auto
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	617	apply (simp only: lam.eq_iff alphas)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	618	apply clarify
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	619	apply (simp add: eqvts)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	620	sorry
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	621
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	622	lemma match_Lam_simps:
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	623	"match_Lam S (Var n) = None"
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	624	"match_Lam S (App l r) = None"
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	625	"z = new (S, (Lam z s)) \<Longrightarrow> match_Lam S (Lam z s) = Some (z, s)"
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	626	apply (simp_all add: match_Lam_def)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	627	apply (simp add: lam_half_inj)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	628	apply auto
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	629	done
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	630
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	631	(*
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	632	lemma match_Lam_simps2:
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	633	"atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)"
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	634	apply (rule_tac t="Lam n s"
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	635	and s="Lam (new (S, (Lam n s))) ((n \<leftrightarrow> (new (S, (Lam n s)))) \<bullet> s)" in subst)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	636	defer
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	637	apply (subst match_Lam_simps(3))
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	638	defer
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	639	apply simp
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	640	*)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	641
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	642	(*primrec match_Lam_raw where
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	643	"match_Lam_raw (S :: atom set) (Var_raw x) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	644	\| "match_Lam_raw S (App_raw x y) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	645	\| "match_Lam_raw S (Lam_raw n t) = (let z = new (S \<union> (fv_lam_raw t - {atom n})) in Some (z, (n \<leftrightarrow> z) \<bullet> t))"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	646
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	647	quotient_definition
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	648	"match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	649	is match_Lam_raw
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	650
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	651	lemma swap_fresh:
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	652	assumes a: "fv_lam_raw t \<sharp>* p"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	653	shows "alpha_lam_raw (p \<bullet> t) t"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	654	using a apply (induct t)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	655	apply (simp add: supp_at_base fresh_star_def)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	656	apply (rule alpha_lam_raw.intros)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	657	apply (metis Rep_name_inverse atom_eqvt atom_name_def fresh_perm)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	658	apply (simp)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	659	apply (simp only: fresh_star_union)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	660	apply clarify
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	661	apply (rule alpha_lam_raw.intros)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	662	apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	663	apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	664	apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	665	apply (rule alpha_lam_raw.intros)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	666	sorry
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	667
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	668	lemma [quot_respect]:
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	669	"(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	670	proof (intro fun_relI, clarify)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	671	fix S t s
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	672	assume a: "alpha_lam_raw t s"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	673	show "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S t) (match_Lam_raw S s)"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	674	using a proof (induct t s rule: alpha_lam_raw.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	675	case goal1 show ?case by simp
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	676	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	677	case goal2 show ?case by simp
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	678	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	679	case (goal3 x t y s)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	680	then obtain p where "({atom x}, t) \<approx>gen (\<lambda>x1 x2. alpha_lam_raw x1 x2 \<and>
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	681	option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S x1)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	682	(match_Lam_raw S x2)) fv_lam_raw p ({atom y}, s)" ..
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	683	then have
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	684	c: "fv_lam_raw t - {atom x} = fv_lam_raw s - {atom y}" and
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	685	d: "(fv_lam_raw t - {atom x}) \<sharp>* p" and
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	686	e: "alpha_lam_raw (p \<bullet> t) s" and
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	687	f: "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S (p \<bullet> t)) (match_Lam_raw S s)" and
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	688	g: "p \<bullet> {atom x} = {atom y}" unfolding alphas(1) by - (elim conjE, assumption)+
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	689	let ?z = "new (S \<union> (fv_lam_raw t - {atom x}))"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	690	have h: "?z = new (S \<union> (fv_lam_raw s - {atom y}))" using c by simp
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	691	show ?case
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	692	unfolding match_Lam_raw.simps Let_def option_rel.simps prod_rel.simps split_conv
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	693	proof
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	694	show "?z = new (S \<union> (fv_lam_raw s - {atom y}))" by (fact h)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	695	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	696	have "atom y \<sharp> p" sorry
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	697	have "fv_lam_raw t \<sharp>* ((x \<leftrightarrow> y) \<bullet> p)" sorry
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	698	then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" using swap_fresh by auto
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	699	then have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	700	have "alpha_lam_raw t ((x \<leftrightarrow> y) \<bullet> s)" sorry
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	701	then have "alpha_lam_raw ((x \<leftrightarrow> ?z) \<bullet> t) ((y \<leftrightarrow> ?z) \<bullet> s)" using eqvts(15) sorry
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	702	then show "alpha_lam_raw ((x \<leftrightarrow> new (S \<union> (fv_lam_raw t - {atom x}))) \<bullet> t)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	703	((y \<leftrightarrow> new (S \<union> (fv_lam_raw s - {atom y}))) \<bullet> s)" unfolding h .
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	704	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	705	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	706	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	707
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	708	lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted]
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	709	*)
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	710
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	711	lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	712	by (induct x rule: lam.induct) (simp_all add: match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	713
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	714	lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	715	apply (induct x rule: lam.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	716	apply (simp_all add: match_Lam_simps)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	717	apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S")
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	718	apply (simp add: match_Lam_def)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	719	apply (subgoal_tac "\<exists>n s. Lam name lam = Lam n s")
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	720	prefer 2
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	721	apply auto[1]
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	722	apply (simp add: Let_def)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	723	apply (thin_tac "\<exists>n s. Lam name lam = Lam n s")
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	724	apply clarify
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	725	apply (rule conjI)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	726	apply (rule_tac t="THE s. Lam name lam = Lam (new (S, Lam name lam)) s" and
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	727	s="(name \<leftrightarrow> (new (S, Lam name lam))) \<bullet> lam" in subst)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	728	defer
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	729	apply (simp add: lam.eq_iff)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	730	apply (rule_tac x="(name \<leftrightarrow> (new (S, Lam name lam)))" in exI)
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	731	apply (simp add: alphas)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	732	apply (simp add: eqvts)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	733	apply (rule conjI)
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	734	sorry
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	735
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	736	function subst where
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	737	"subst v s t = (
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	738	case match_Var t of Some n \<Rightarrow> if n = v then s else Var n \| None \<Rightarrow>
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	739	case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) \| None \<Rightarrow>
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	740	case match_Lam (v,s) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) \| None \<Rightarrow> undefined)"
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	741	by pat_completeness auto
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	742
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	743	termination apply (relation "measure (\<lambda>(_, _, t). size t)")
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	744	apply auto[1]
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	745	apply (case_tac a) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	746	apply (frule lam_some) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	747	apply (case_tac a) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	748	apply (frule app_some) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	749	apply (case_tac a) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	750	apply (frule app_some) apply simp
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	751	done
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	752
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	753	lemmas lam_exhaust = lam_raw.exhaust[quot_lifted]
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	754
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	755	lemma subst_eqvt:
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	756	"p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	757	proof (induct v s t rule: subst.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	758	case (1 v s t)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	759	show ?case proof (cases t rule: lam_exhaust)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	760	fix n
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	761	assume "t = Var n"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	762	then show ?thesis by (simp add: match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	763	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	764	fix l r
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	765	assume "t = App l r"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	766	then show ?thesis
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	767	apply (simp only:)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	768	apply (subst subst.simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	769	apply (subst match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	770	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	771	apply (subst match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	772	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	773	apply (simp only: prod.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	774	apply (simp only: lam.perm)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	775	apply (subst (3) subst.simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	776	apply (subst match_Var_simps)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	777	apply (simp only: option.cases)
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	778	apply (subst match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	779	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	780	apply (simp only: prod.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	781	apply (subst 1(2)[of "(l, r)" "l" "r"])
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	782	apply (simp add: match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	783	apply (simp add: match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	784	apply (rule refl)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	785	apply (subst 1(3)[of "(l, r)" "l" "r"])
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	786	apply (simp add: match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	787	apply (simp add: match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	788	apply (rule refl)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	789	apply (rule refl)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	790	done
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	791	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	792	fix n t'
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	793	assume "t = Lam n t'"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	794	then show ?thesis
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	795	apply (simp only: )
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	796	apply (simp only: lam.perm)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	797	apply (subst subst.simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	798	apply (subst match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	799	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	800	apply (subst match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	801	apply (simp only: option.cases)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	802	apply (rule_tac t="Lam n t'" and s="Lam (new ((v, s), Lam n t')) ((n \<leftrightarrow> new ((v, s), Lam n t')) \<bullet> t')" in subst)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	803	defer
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	804	apply (subst match_Lam_simps)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	805	defer
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	806	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	807	apply (simp only: prod.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	808	apply (subst (2) subst.simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	809	apply (subst match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	810	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	811	apply (subst match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	812	apply (simp only: option.cases)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	813	apply (rule_tac t="Lam (p \<bullet> n) (p \<bullet> t')" and s="Lam (new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) (((p \<bullet> n) \<leftrightarrow> new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) \<bullet> t')" in subst)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	814	defer
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	815	apply (subst match_Lam_simps)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	816	defer
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	817	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	818	apply (simp only: prod.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	819	apply (simp only: lam.perm)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	820	thm 1(1)
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	821	sorry
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	822	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	823	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	824
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	825	lemma subst_proper_eqs:
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	826	"subst y s (Var x) = (if x = y then s else (Var x))"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	827	"subst y s (App l r) = App (subst y s l) (subst y s r)"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	828	"atom x \<sharp> (t, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	829	apply (subst subst.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	830	apply (simp only: match_Var_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	831	apply (simp only: option.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	832	apply (subst subst.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	833	apply (simp only: match_App_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	834	apply (simp only: option.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	835	apply (simp only: prod.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	836	apply (simp only: match_Var_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	837	apply (simp only: option.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	838	apply (subst subst.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	839	apply (simp only: match_Var_simps)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	840	apply (simp only: option.simps)
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	841	apply (simp only: match_App_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	842	apply (simp only: option.simps)
2173 477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	843	apply (rule_tac t="Lam x t" and s="Lam (new ((y, s), Lam x t)) ((x \<leftrightarrow> new ((y, s), Lam x t)) \<bullet> t)" in subst)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	844	defer
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	845	apply (subst match_Lam_simps)
477293d841e8 Match_Lam defined on Quotient Level. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2172 diff changeset	846	defer
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	847	apply (simp only: option.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	848	apply (simp only: prod.simps)
2157 a1d27083e688 subst experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	849	sorry
a1d27083e688 subst experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	850
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	851	end
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	852
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	853
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	854

author	Christian Urban <urbanc@in.tum.de>
	Wed, 25 Aug 2010 09:02:06 +0800
changeset 2431	331873ebc5cd
parent 2425	715ab84065a0
child 2432	7aa18bae6983
permissions	-rw-r--r--