nominal2: Nominal/Ex/LetRec.thy@3e82c1ced5e4 (annotated)

2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	1	theory LetRec
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2438 diff changeset	2	imports "../Nominal2"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
2311 4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	5	atom_decl name
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	6
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	7	nominal_datatype let_rec:
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	8	trm =
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	9	Var "name"
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	10	\| App "trm" "trm"
abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	11	\| Lam x::"name" t::"trm" bind (set) x in t
abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	12	\| Let_Rec bp::"bp" t::"trm" bind (set) "bn bp" in bp t
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	13	and bp =
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	14	Bp "name" "trm"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	binder
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	16	bn::"bp \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	where
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	18	"bn (Bp x t) = {atom x}"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	20	thm let_rec.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	21	thm let_rec.induct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	22	thm let_rec.exhaust
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	23	thm let_rec.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	24	thm let_rec.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	25	thm let_rec.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	26	thm let_rec.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	27	thm let_rec.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	28	thm let_rec.size_eqvt
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2067 diff changeset	29
2877 3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	30	lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	31	by (simp add: permute_pure)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	32
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	33	nominal_primrec
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	34	height_trm :: "trm \<Rightarrow> nat"
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	35	and height_bp :: "bp \<Rightarrow> nat"
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	36	where
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	37	"height_trm (Var x) = 1"
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	38	\| "height_trm (App l r) = max (height_trm l) (height_trm r)"
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	39	\| "height_trm (Lam v b) = 1 + (height_trm b)"
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	40	\| "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)"
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	41	\| "height_bp (Bp v t) = height_trm t"
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	42	apply (simp only: eqvt_def height_trm_height_bp_graph_def)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	43	apply (rule, perm_simp, rule, rule TrueI)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	44	apply auto
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	45	apply (case_tac x)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	46	apply (case_tac a rule: let_rec.exhaust(1))
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	47	apply auto
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	48	apply (case_tac b rule: let_rec.exhaust(2))
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	49	apply blast
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	50	apply (erule Abs_set_fcb)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	51	apply (simp_all add: pure_fresh)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	52	apply (simp add: eqvt_at_def)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	53	apply (simp add: Abs_eq_iff2)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	54	apply (simp add: alphas)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	55	apply clarify
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	56	apply (rule trans)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	57	apply(rule_tac p="p" in supp_perm_eq[symmetric])
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	58	apply (simp add: pure_supp fresh_star_def)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	59	apply (simp only: eqvts)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	60	apply (simp add: eqvt_at_def)
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	61	done
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	62
3e82c1ced5e4 function for let-rec Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2454 diff changeset	63	termination by lexicographic_order
2067 ace7775cbd04 Experiments with equivariance. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2056 diff changeset	64
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	65	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	66
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	67
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	68

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Mon, 20 Jun 2011 20:09:30 +0900
changeset 2877	3e82c1ced5e4
parent 2454	9ffee4eb1ae1
child 2950	0911cb7bf696
permissions	-rw-r--r--