nominal2: Nominal/Ex/LetSimple2.thy@dc6007dd9c30 (annotated)

2931 aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Let
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../Nominal2"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	atom_decl name
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	nominal_datatype trm =
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	Var "name"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	\| App "trm" "trm"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	10	\| Let as::"assn" t::"trm" binds "bn as" in t
2931 aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	and assn =
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	Assn "name" "trm"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	binder
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	bn
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	where
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	"bn (Assn x t) = [atom x]"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	print_theorems
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	19
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	thm bn_raw.simps
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	thm permute_bn_raw.simps
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	thm trm_assn.perm_bn_alpha
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	thm trm_assn.permute_bn
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	24
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	thm trm_assn.fv_defs
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	thm trm_assn.eq_iff
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	thm trm_assn.bn_defs
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	thm trm_assn.bn_inducts
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	thm trm_assn.perm_simps
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	thm trm_assn.induct
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	thm trm_assn.inducts
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	thm trm_assn.distinct
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	thm trm_assn.supp
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	thm trm_assn.fresh
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	thm trm_assn.exhaust
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	thm trm_assn.strong_exhaust
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	thm trm_assn.perm_bn_simps
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	38
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	thm alpha_bn_raw.cases
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	40
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	41
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	lemmas alpha_bn_cases[consumes 1] = alpha_bn_raw.cases[quot_lifted]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	43
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	lemma alpha_bn_refl: "alpha_bn x x"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	by (induct x rule: trm_assn.inducts(2))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	(rule TrueI, auto simp add: trm_assn.eq_iff)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	lemma alpha_bn_sym: "alpha_bn x y \<Longrightarrow> alpha_bn y x"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	apply(erule alpha_bn_cases)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	apply(auto)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	51
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	sorry
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	54
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	lemma k: "A \<Longrightarrow> A \<and> A" by blast
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	56
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	by (simp add: permute_pure)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	59
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	60
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	section {* definition with helper functions *}
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	62
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	63	function
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	64	apply_assn
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	65	where
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	"apply_assn f (Assn x t) = (f t)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	67	apply(case_tac x)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	69	apply(case_tac b rule: trm_assn.exhaust(2))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	apply(blast)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	73
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	termination
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	by lexicographic_order
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	76
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	function
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	apply_assn2
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	where
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	"apply_assn2 f (Assn x t) = Assn x (f t)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	apply(case_tac x)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	apply(case_tac b rule: trm_assn.exhaust(2))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	apply(blast)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	87
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	88	termination
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	by lexicographic_order
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	90
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	lemma [eqvt]:
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	92	shows "p \<bullet> (apply_assn f as) = apply_assn (p \<bullet> f) (p \<bullet> as)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	apply(induct f as rule: apply_assn.induct)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	95	apply(perm_simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	96	apply(rule)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	97	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	98
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	99	lemma [eqvt]:
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	100	shows "p \<bullet> (apply_assn2 f as) = apply_assn2 (p \<bullet> f) (p \<bullet> as)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	101	apply(induct f as rule: apply_assn.induct)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	102	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	apply(perm_simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	104	apply(rule)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	105	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	106
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	107
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	108	nominal_primrec
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	height_trm :: "trm \<Rightarrow> nat"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	110	where
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	111	"height_trm (Var x) = 1"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	112	\| "height_trm (App l r) = max (height_trm l) (height_trm r)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	113	\| "height_trm (Let as b) = max (apply_assn height_trm as) (height_trm b)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	114	apply (simp only: eqvt_def height_trm_graph_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	115	apply (rule, perm_simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	apply(rule)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	apply(rule TrueI)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	118	apply (case_tac x rule: trm_assn.exhaust(1))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	119	apply (auto simp add: alpha_bn_refl)[3]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	120	apply (drule_tac x="assn" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	121	apply (drule_tac x="trm" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	apply(simp add: alpha_bn_refl)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	apply(simp_all)[5]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	124	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	125	apply(erule conjE)+
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	126	thm alpha_bn_cases
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	apply(erule alpha_bn_cases)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	apply (subgoal_tac "height_trm_sumC b = height_trm_sumC ba")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	130	apply simp
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	131	apply(simp add: trm_assn.bn_defs)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	132	apply(erule_tac c="()" in Abs_lst_fcb2)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	133	apply(simp_all add: pure_fresh fresh_star_def)[3]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	134	apply(simp_all add: eqvt_at_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	135	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	136
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	137
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	138	nominal_primrec
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	140	where
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	"(Var x)[y ::= s] = (if x = y then s else (Var x))"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	142	\| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	143	\| "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow>
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	144	(Let as t)[y ::= s] = Let (apply_assn2 (\<lambda>t. t[y ::=s]) as) (t[y ::= s])"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	145	apply (simp only: eqvt_def subst_trm_graph_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	146	apply (rule, perm_simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	147	apply(rule)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	148	apply(rule TrueI)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	149	apply(case_tac x)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	150	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	151	apply (rule_tac y="a" and c="(b,c)" in trm_assn.strong_exhaust(1))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	152	apply (auto simp add: alpha_bn_refl)[3]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	153	apply(simp_all)[5]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	154	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	155	apply(erule conjE)+
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	156	thm alpha_bn_cases
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	157	apply(erule alpha_bn_cases)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	158	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	159	apply(simp add: trm_assn.bn_defs)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	160	apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	161	apply(simp add: Abs_fresh_iff fresh_star_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	162	apply(simp add: fresh_star_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	163	apply(simp_all add: eqvt_at_def perm_supp_eq fresh_star_Pair)[2]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	164	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	165
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	166
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	167	section {* direct definitions --- problems *}
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	168
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	169
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	170	nominal_primrec
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	171	height_trm :: "trm \<Rightarrow> nat"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	172	and height_assn :: "assn \<Rightarrow> nat"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	173	where
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	174	"height_trm (Var x) = 1"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	175	\| "height_trm (App l r) = max (height_trm l) (height_trm r)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	176	\| "height_trm (Let as b) = max (height_assn as) (height_trm b)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	177	\| "height_assn (Assn x t) = (height_trm t)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	178	apply (simp only: eqvt_def height_trm_height_assn_graph_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	179	apply (rule, perm_simp, rule, rule TrueI)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	180	apply (case_tac x)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	181	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	182	apply (case_tac a rule: trm_assn.exhaust(1))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	183	apply (auto simp add: alpha_bn_refl)[3]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	184	apply (drule_tac x="assn" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	185	apply (drule_tac x="trm" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	186	apply(simp add: alpha_bn_refl)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	187	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	188	apply (case_tac b rule: trm_assn.exhaust(2))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	189	apply (auto)[1]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	190	apply(simp_all)[7]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	191	prefer 2
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	192	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	193	--"let case"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	194	apply (simp only: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff])
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	195	apply (simp only: meta_eq_to_obj_eq[OF height_assn_def, symmetric, unfolded fun_eq_iff])
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	196	apply (subgoal_tac "eqvt_at height_assn as")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	197	apply (subgoal_tac "eqvt_at height_assn asa")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	198	apply (subgoal_tac "eqvt_at height_trm b")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	199	apply (subgoal_tac "eqvt_at height_trm ba")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	200	apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr as)")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	201	apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr asa)")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	202	apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl b)")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	203	apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl ba)")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	204	defer
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	205	apply (simp add: eqvt_at_def height_trm_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	206	apply (simp add: eqvt_at_def height_trm_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	207	apply (simp add: eqvt_at_def height_assn_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	208	apply (simp add: eqvt_at_def height_assn_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	209	prefer 2
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	210	apply (subgoal_tac "height_assn as = height_assn asa")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	211	apply (subgoal_tac "height_trm b = height_trm ba")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	212	apply simp
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	213	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	214	apply(erule conjE)+
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	215	apply(erule alpha_bn_cases)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	216	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	217	apply(simp add: trm_assn.bn_defs)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	218	thm Abs_lst_fcb2
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	219	apply(erule_tac c="()" in Abs_lst_fcb2)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	220	apply(simp_all add: fresh_star_def pure_fresh)[3]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	221	apply(simp add: eqvt_at_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	222	apply(simp add: eqvt_at_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	223	defer
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	224	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	225	apply(frule Inl_inject)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	226	apply(subst (asm) trm_assn.eq_iff)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	227	apply(drule Inl_inject)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	228	apply(clarify)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	229	apply(erule alpha_bn_cases)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	230	apply(simp del: trm_assn.eq_iff)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	231	apply(rename_tac as s as' s' t' t x x')
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	232	apply(simp only: trm_assn.bn_defs)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	233	(* HERE *)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	234	oops
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	235
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	236
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	237	lemma ww1:
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	238	shows "finite (fv_trm t)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	239	and "finite (fv_bn as)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	240	apply(induct t and as rule: trm_assn.inducts)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	241	apply(simp_all add: trm_assn.fv_defs supp_at_base)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	242	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	243
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	244	text {* works, but only because no recursion in as *}
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	245
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	246	nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	247	frees_set :: "trm \<Rightarrow> atom set"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	248	where
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	249	"frees_set (Var x) = {atom x}"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	250	\| "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	251	\| "frees_set (Let as t) = (frees_set t) - (set (bn as)) \<union> (fv_bn as)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	252	apply(simp add: eqvt_def frees_set_graph_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	253	apply(rule, perm_simp, rule)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	254	apply(erule frees_set_graph.induct)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	255	apply(auto simp add: ww1)[3]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	256	apply(rule_tac y="x" in trm_assn.exhaust(1))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	257	apply(auto simp add: alpha_bn_refl)[3]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	258	apply(drule_tac x="assn" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	259	apply(drule_tac x="trm" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	260	apply(simp add: alpha_bn_refl)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	261	apply(simp_all)[5]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	262	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	263	apply(erule conjE)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	264	apply(erule alpha_bn_cases)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	265	apply(simp add: trm_assn.bn_defs)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	266	apply(simp add: trm_assn.fv_defs)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	267	(* apply(erule_tac c="(trm_rawa)" in Abs_lst1_fcb2) *)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	268	apply(subgoal_tac " frees_set_sumC t - {atom name} = frees_set_sumC ta - {atom namea}")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	269	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	270	apply(erule_tac c="()" in Abs_lst1_fcb2)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	271	apply(simp add: fresh_minus_atom_set)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	272	apply(simp add: fresh_star_def fresh_Unit)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	273	apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	274	apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	275	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	276
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	277	termination
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	278	by lexicographic_order
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	279
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	280	lemma test:
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	281	assumes a: "\<exists>y. f x = Inl y"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	282	shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	283	using a
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	284	apply clarify
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	285	apply(frule_tac p="p" in permute_boolI)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	286	apply(simp (no_asm_use) only: eqvts)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	287	apply(subst (asm) permute_fun_app_eq)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	288	back
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	289	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	290	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	291
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	292
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	293	nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	294	subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::trm= _]" [90, 90, 90] 90) and
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	295	subst_assn :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn" ("_ [_ ::assn= _]" [90, 90, 90] 90)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	296	where
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	297	"(Var x)[y ::trm= s] = (if x = y then s else (Var x))"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	298	\| "(App t1 t2)[y ::trm= s] = App (t1[y ::trm= s]) (t2[y ::trm= s])"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	299	\| "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> (Let as t)[y ::trm= s] = Let (ast[y ::assn= s]) (t[y ::trm= s])"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	300	\| "(Assn x t)[y ::assn= s] = Assn x (t[y ::trm= s])"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	301	apply(subgoal_tac "\<And>p x r. subst_trm_subst_assn_graph x r \<Longrightarrow> subst_trm_subst_assn_graph (p \<bullet> x) (p \<bullet> r)")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	302	apply(simp add: eqvt_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	303	apply(rule allI)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	304	apply(simp add: permute_fun_def permute_bool_def)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	305	apply(rule ext)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	306	apply(rule ext)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	307	apply(rule iffI)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	308	apply(drule_tac x="p" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	309	apply(drule_tac x="- p \<bullet> x" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	310	apply(drule_tac x="- p \<bullet> xa" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	311	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	312	apply(drule_tac x="-p" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	313	apply(drule_tac x="x" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	314	apply(drule_tac x="xa" in meta_spec)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	315	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	316	--"Eqvt One way"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	317	defer
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	318	apply(rule TrueI)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	319	apply(case_tac x)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	320	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	321	apply(case_tac a)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	322	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	323	apply(rule_tac y="aa" and c="(b, c)" in trm_assn.strong_exhaust(1))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	324	apply(blast)+
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	325	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	326	apply(case_tac b)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	327	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	328	apply(rule_tac y="a" in trm_assn.exhaust(2))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	329	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	330	apply(blast)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	331	apply(simp_all)[7]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	332	prefer 2
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	333	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	334	prefer 2
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	335	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	336	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	337	apply (simp only: meta_eq_to_obj_eq[OF subst_trm_def, symmetric, unfolded fun_eq_iff])
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	338	apply (simp only: meta_eq_to_obj_eq[OF subst_assn_def, symmetric, unfolded fun_eq_iff])
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	339	apply (subgoal_tac "eqvt_at (\<lambda>ast. subst_assn ast ya sa) ast")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	340	apply (subgoal_tac "eqvt_at (\<lambda>asta. subst_assn asta ya sa) asta")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	341	apply (subgoal_tac "eqvt_at (\<lambda>t. subst_trm t ya sa) t")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	342	apply (subgoal_tac "eqvt_at (\<lambda>ta. subst_trm ta ya sa) ta")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	343	apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inr (ast, ya, sa))")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	344	apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inr (asta, ya, sa))")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	345	apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inl (t, ya, sa))")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	346	apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inl (ta, ya, sa))")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	347	defer
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	348	defer
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	349	defer
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	350	defer
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	351	defer
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	352	defer
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	353	apply(rule conjI)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	354	apply (subgoal_tac "subst_assn ast ya sa= subst_assn asta ya sa")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	355	apply (subgoal_tac "subst_trm t ya sa = subst_trm ta ya sa")
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	356	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	357	apply(erule_tac conjE)+
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	358	apply(erule alpha_bn_cases)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	359	apply(simp add: trm_assn.bn_defs)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	360	apply(rotate_tac 7)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	361	apply(drule k)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	362	apply(erule conjE)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	363	apply(subst (asm) Abs1_eq_iff)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	364	apply(rule sort_of_atom_eq)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	365	apply(rule sort_of_atom_eq)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	366	apply(erule disjE)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	367	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	368	apply(rotate_tac 12)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	369	apply(drule sym)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	370	apply(rule sym)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	371	apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	372	apply(erule fresh_eqvt_at)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	373
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	374	thm fresh_eqvt_at
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	375	apply(simp add: Abs_fresh_iff)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	376	apply(simp add: fresh_star_def fresh_Pair)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	377	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	378	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	379
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	380
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	381
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	382	apply(simp_all add: fresh_star_def fresh_Pair_elim)[1]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	383	apply(blast)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	384	apply(simp_all)[5]
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	385	apply(simp (no_asm_use))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	386	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	387	apply(erule conjE)+
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	388	apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	389	apply(simp add: Abs_fresh_iff)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	390	apply(simp add: fresh_star_def fresh_Pair)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	391	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	392	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	393	done
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	394
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	395
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	396	end

author	Christian Urban <urbanc@in.tum.de>
	Wed, 06 Jul 2011 01:04:09 +0200
changeset 2954	dc6007dd9c30
parent 2950	0911cb7bf696
child 2960	248546bfeb16
permissions	-rw-r--r--