nominal2: Nominal/Manual/Term4.thy@0dc61c2966da (annotated)

1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Term4
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	2	imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove"
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	section {* lam with indirect list recursion *}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	datatype rtrm4 =
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	rVr4 "name"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	\| rAp4 "rtrm4" "rtrm4 list"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	\| rLm4 "name" "rtrm4" --"bind (name) in (trm)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	thm rtrm4.recs
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	(* there cannot be a clause for lists, as *)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	(* permutations are already defined in Nominal (also functions, options, and so on) *)
1277 6eacf60ce41d Permutation and FV_Alpha interface change. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1270 diff changeset	19	setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}
1862 310b7b768adf Lifting in Term4. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1856 diff changeset	20	print_theorems
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	(* "repairing" of the permute function *)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	lemma repaired:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	fixes ts::"rtrm4 list"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	shows "permute_rtrm4_list p ts = p \<bullet> ts"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	apply(induct ts)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	apply(simp_all)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28	done
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	thm permute_rtrm4_permute_rtrm4_list.simps
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	31	lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
1862 310b7b768adf Lifting in Term4. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1856 diff changeset	32
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33
1852 13bc3f41ad8d Updating in Term4. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1848 diff changeset	34	local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")
13bc3f41ad8d Updating in Term4. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1848 diff changeset	35	[[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *}
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36	print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37
1318 cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	38	lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4"
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	39	apply (rule ext)+
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	40	apply (induct_tac x xa rule: list_induct2')
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	41	apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros)
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	42	apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	43	apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	44	apply rule
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	45	apply (erule alpha_rtrm4_list.cases)
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	46	apply simp_all
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	47	apply (rule alpha_rtrm4_alpha_rtrm4_list.intros)
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	48	apply simp_all
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	49	done
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	50
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	51	ML {* @{term "\<Union>a"} *}
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	52
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	53	lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	54	apply (rule ext)
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	55	apply (induct_tac x)
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	56	apply simp_all
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	57	done
1318 cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	58
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	59	notation
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60	alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	61	alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
1318 cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	62	thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	63
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	64	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	65	thm alpha4_inj
1318 cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	66
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	67	lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3]
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	68
1853 0120da30673e fv_eqvt in term4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1852 diff changeset	69	local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
0120da30673e fv_eqvt in term4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1852 diff changeset	70	thm eqvts(1-2)
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	71
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	72	local_setup {*
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	73	(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	74	build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} ctxt 1) ctxt) ctxt))
1318 cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	75	*}
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	76	thm alpha4_eqvt
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	77	lemmas alpha4_eqvt_fixed = alpha4_eqvt[simplified fix2 fix3]
1318 cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	78
1854 8442d81496d5 alpha4_eqvt and alpha4_reflp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1853 diff changeset	79	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	80	build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}
1854 8442d81496d5 alpha4_eqvt and alpha4_reflp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1853 diff changeset	81	thm alpha4_reflp
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	82	lemmas alpha4_reflp_fixed = alpha4_reflp[simplified fix2 fix3]
1854 8442d81496d5 alpha4_eqvt and alpha4_reflp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1853 diff changeset	83
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	84	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	85	(build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	86	lemmas alpha4_equivp_fixed = alpha4_equivp[simplified fix2 fix3]
1318 cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	87
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	88	quotient_type
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	89	trm4 = rtrm4 / alpha_rtrm4
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	90	by (simp_all add: alpha4_equivp)
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	91
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	92	local_setup {*
cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	93	(fn ctxt => ctxt
1855 0a306922ace7 alpha4_equivp and constant lifting. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1854 diff changeset	94	\|> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4}))
1856 c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	95	\|> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4}))
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	96	\|> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4}))
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	97	\|> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4})))
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	98	*}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	99	print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	100
1856 c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	101
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	102	lemma fv_rtrm4_rsp:
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	103	"xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya"
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	104	"x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y"
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	105	apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts)
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	106	apply (simp_all add: alpha_gen)
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	107	done
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	108
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	109	local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}]
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	110	(fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *}
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	111	print_theorems
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	112
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	113	local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}]
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	114	(fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	115	local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}]
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	116	(fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	117
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	118	lemma [quot_respect]:
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	119	"(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	120	by (simp add: alpha4_inj_fixed)
1856 c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	121
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	122	local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	123	[@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]
c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	124	(fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	125
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	126	setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_plus} *}
1862 310b7b768adf Lifting in Term4. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1856 diff changeset	127	print_theorems
1318 cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	128
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	129	(* Instead of permute for trm4_list we may need the following 2 lemmas: *)
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	130	lemma [quot_preserve]: "(id ---> map rep_trm4 ---> map abs_trm4) permute = permute"
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	131	apply (simp add: expand_fun_eq)
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	132	apply clarify
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	133	apply (rename_tac "pi" x)
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	134	apply (induct_tac x)
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	135	apply simp
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	136	apply simp
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	137	apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified])
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	138	done
1856 c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	139
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	140	lemma [quot_respect]: "(op = ===> list_rel alpha_rtrm4 ===> list_rel alpha_rtrm4) permute permute"
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	141	apply simp
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	142	apply (rule allI)+
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	143	apply (induct_tac xa y rule: list_induct2')
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	144	apply simp_all
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	145	apply clarify
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	146	apply (erule alpha4_eqvt)
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	147	done
1856 c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	148
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	149	ML {*
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	150	map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed}
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	151	*}
1318 cce1b6d1b761 Some tests around Term4. Not sure how to fix the generated fv function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1300 diff changeset	152
1856 c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	153	ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	154
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	155	ML {*
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	156	map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4_fv_rtrm4_list.simps[simplified fix3]}
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	157	*}
1856 c8e406f64db0 More on Manual/Trm4 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1855 diff changeset	158
1906 0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	159	ML {*
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	160	val liftd =
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	161	map (Local_Defs.unfold @{context} @{thms id_simps}) (
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	162	map (Local_Defs.fold @{context} @{thms alphas}) (
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	163	map (lift_thm [@{typ trm4}] @{context}) @{thms alpha4_inj_fixed[unfolded alphas]}
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	164	)
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	165	)
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	166	*}
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	167
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	168	ML {*
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	169	map (lift_thm [@{typ trm4}] @{context})
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	170	(flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	171	*}
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	172
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	173	ML {*
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	174	map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fix3]}
0dc61c2966da All lifted in Term4. Requires new isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1862 diff changeset	175	*}
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	176
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	177	end

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 20 Apr 2010 17:25:31 +0200
changeset 1906	0dc61c2966da
parent 1862	310b7b768adf
child 2060	04a881bf49e4
permissions	-rw-r--r--