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

2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2966 diff changeset	1	theory LetSimple2
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	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
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	5
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	6	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	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	8	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	9	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	10	\| 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	11	\| 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	12	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	13	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	14	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	15	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	16	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	17	"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	18
aaef9dec5e1d side-by-side tests of lets with 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	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	20
aaef9dec5e1d side-by-side tests of lets with 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 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 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	23	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	24	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	25
aaef9dec5e1d side-by-side tests of lets with 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.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	27	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	28	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	29	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	30	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	31	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	32	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	33	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	34	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	35	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	36	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	37	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	38	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	39
aaef9dec5e1d side-by-side tests of lets with 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	thm alpha_bn_raw.cases
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	41	thm trm_assn.alpha_refl
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	42	thm trm_assn.alpha_sym
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	43	thm trm_assn.alpha_trans
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	44
aaef9dec5e1d side-by-side tests of lets with 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	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	46
aaef9dec5e1d side-by-side tests of lets with 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_refl: "alpha_bn x x"
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	48	by(rule trm_assn.alpha_refl)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	49
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	50	lemma alpha_bn_sym: "alpha_bn x y \<Longrightarrow> alpha_bn y x"
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	51	by (rule trm_assn.alpha_sym)
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	52
aaef9dec5e1d side-by-side tests of lets with 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	lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z"
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	54	using trm_assn.alpha_trans by metis
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	55
2970 374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	56	lemma fv_bn_finite[simp]:
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	57	"finite (fv_bn as)"
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	58	apply(case_tac as rule: trm_assn.exhaust(2))
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	59	apply(simp add: trm_assn.supp finite_supp)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	60	done
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	61
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	62
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	63	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	64
aaef9dec5e1d side-by-side tests of lets with 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
aaef9dec5e1d side-by-side tests of lets with 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
aaef9dec5e1d side-by-side tests of lets with 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	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	68
aaef9dec5e1d side-by-side tests of lets with 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	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	70	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	71	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	72	"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	73	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	74	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	75	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	76	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	77	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	78	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	79
aaef9dec5e1d side-by-side tests of lets with 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	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	81	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	82
aaef9dec5e1d side-by-side tests of lets with 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	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	84	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	85	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	86	"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	87	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	88	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	89	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	90	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	91	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	92	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	93
aaef9dec5e1d side-by-side tests of lets with 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	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	95	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	96
aaef9dec5e1d side-by-side tests of lets with 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	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	98	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	99	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	100	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	101	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	102	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	103	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	104
aaef9dec5e1d side-by-side tests of lets with 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	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	106	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	107	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	108	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	109	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	110	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	111	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	112
aaef9dec5e1d side-by-side tests of lets with 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
aaef9dec5e1d side-by-side tests of lets with 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	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	115	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	116	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	117	"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	118	\| "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	119	\| "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	120	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	121	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	122	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	123	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	124	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	125	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	126	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	127	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	128	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	129	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	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(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	132	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	133	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	134	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	135	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	136	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	137	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	138	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	139	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	140	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	141
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	142	(* assn-function prevents automatic discharge
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	143	termination by lexicographic_order
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	144	*)
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	145
aaef9dec5e1d side-by-side tests of lets with 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	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	147	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	148	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	149	"(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	150	\| "(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	151	\| "(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	152	(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	153	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	154	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	155	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	156	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	157	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	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 (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	160	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	161	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	162	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	163	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	164	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	165	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	166	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	167	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	168	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	169	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	170	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	171	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	172
aaef9dec5e1d side-by-side tests of lets with 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
aaef9dec5e1d side-by-side tests of lets with 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	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	175
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	176	lemma cheat: "P" sorry
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	177
2977 a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	178	definition
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	179	"eqvt_at_bn f as \<equiv> \<forall>p. (p \<bullet> (f as)) = f (permute_bn p as)"
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	180
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	181	definition
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	182	"alpha_bn_preserve f as \<equiv> \<forall>p. f as = f (permute_bn p as)"
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	183
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	184	lemma
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	185	fixes as::"assn"
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	186	assumes "eqvt_at f as"
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	187	shows "eqvt_at_bn f as"
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	188	using assms
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	189	unfolding eqvt_at_bn_def
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	190	apply(rule_tac allI)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	191	apply(drule k)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	192	apply(erule conjE)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	193	apply(subst (asm) eqvt_at_def)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	194	apply(simp)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	195
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	196	oops
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	197
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	198
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	199
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	200	nominal_primrec
2977 a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	201	<<<<<<< variant A
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	202	(invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True \| Inr x2 \<Rightarrow> alpha_bn_preserve (height_assn2::assn \<Rightarrow> nat) x2")
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	203	>>>>>>> variant B
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	204	####### Ancestor
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	205	(invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True \| Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y")
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	206	======= end
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	207	height_trm2 :: "trm \<Rightarrow> nat"
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	208	and height_assn2 :: "assn \<Rightarrow> nat"
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	209	where
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	210	"height_trm2 (Var x) = 1"
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	211	\| "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)"
2970 374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	212	\| "set (bn as) \<sharp>* fv_bn as \<Longrightarrow> height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)"
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	213	\| "height_assn2 (Assn x t) = (height_trm2 t)"
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	214	thm height_trm2_height_assn2_graph.intros[no_vars]
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	215	thm height_trm2_height_assn2_graph_def
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	216	apply (simp only: eqvt_def height_trm2_height_assn2_graph_def)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	217	apply (rule, perm_simp, rule)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	218	-- "invariant"
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	219	apply(simp)
2977 a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	220	<<<<<<< variant A
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	221	apply(simp)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	222	apply(simp)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	223	apply(simp)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	224	apply(simp add: alpha_bn_preserve_def)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	225	apply(simp add: height_assn2_def)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	226	apply(simp add: trm_assn.perm_bn_simps)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	227	apply(rule allI)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	228	thm height_trm2_height_assn2_graph.intros[no_vars]
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	229	thm height_trm2_height_assn2_sumC_def
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	230	apply(rule cheat)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	231	apply -
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	232	>>>>>>> variant B
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	233	####### Ancestor
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	234	apply(simp)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	235	apply(simp)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	236	apply(simp)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	237	apply(rule cheat)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	238	apply -
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	239	======= end
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	240	--"completeness"
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	241	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	242	apply(simp)
2970 374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	243	apply (rule_tac y="a" and c="a" in trm_assn.strong_exhaust(1))
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	244	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	245	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	246	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	247	apply(simp add: alpha_bn_refl)
2970 374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	248	apply(rotate_tac 3)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	249	apply(drule meta_mp)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	250	apply(simp add: fresh_star_def trm_assn.fresh)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	251	apply(simp add: fresh_def)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	252	apply(subst supp_finite_atom_set)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	253	apply(simp)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	254	apply(simp)
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	255	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	256	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	257	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	258	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	259	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	260	apply(simp)
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	261	prefer 2
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	262	apply(simp)
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	263	--"let case"
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	264	apply (simp only: meta_eq_to_obj_eq[OF height_trm2_def, symmetric, unfolded fun_eq_iff])
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	265	apply (simp only: meta_eq_to_obj_eq[OF height_assn2_def, symmetric, unfolded fun_eq_iff])
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	266	apply (subgoal_tac "eqvt_at height_assn2 as")
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	267	apply (subgoal_tac "eqvt_at height_assn2 asa")
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	268	apply (subgoal_tac "eqvt_at height_trm2 b")
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	269	apply (subgoal_tac "eqvt_at height_trm2 ba")
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	270	apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inr as)")
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	271	apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inr asa)")
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	272	apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inl b)")
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	273	apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inl ba)")
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	274	defer
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	275	apply (simp add: eqvt_at_def height_trm2_def)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	276	apply (simp add: eqvt_at_def height_trm2_def)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	277	apply (simp add: eqvt_at_def height_assn2_def)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	278	apply (simp add: eqvt_at_def height_assn2_def)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	279	apply (subgoal_tac "height_assn2 as = height_assn2 asa")
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	280	apply (subgoal_tac "height_trm2 b = height_trm2 ba")
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	281	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	282	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	283	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	284	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	285	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	286	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	287	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	288	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	289	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	290	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	291	apply(drule Inl_inject)
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	292	apply(simp (no_asm_use))
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	293	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	294	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	295	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	296	apply(simp only: trm_assn.bn_defs)
2977 a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	297	<<<<<<< variant A
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	298	apply(erule_tac c="()" in Abs_lst1_fcb2')
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	299	apply(simp_all add: fresh_star_def pure_fresh)[3]
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	300	apply(simp add: eqvt_at_bn_def)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	301	apply(simp add: trm_assn.perm_bn_simps)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	302	apply(simp add: eqvt_at_bn_def)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	303	apply(simp add: trm_assn.perm_bn_simps)
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	304	done
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	305
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	306	>>>>>>> variant B
2970 374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	307	apply(erule_tac c="(trm_rawa)" in Abs_lst1_fcb2')
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	308	apply(simp_all add: fresh_star_def pure_fresh)[2]
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	309	apply(simp add: trm_assn.supp)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	310	apply(simp add: fresh_def)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	311	apply(subst (asm) supp_finite_atom_set)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	312	apply(simp add: finite_supp)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	313	apply(subst (asm) supp_finite_atom_set)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	314	apply(simp add: finite_supp)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	315	apply(simp)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	316	apply(simp add: eqvt_at_def perm_supp_eq)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	317	apply(simp add: eqvt_at_def perm_supp_eq)
374e2f90140c direct definition of height using bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	318	done
2977 a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	319	####### Ancestor
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	320	apply(erule_tac c="()" in Abs_lst1_fcb2')
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	321	apply(simp_all add: fresh_star_def pure_fresh)[3]
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	322
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	323	oops
a4b6e997a7c6 merged Christian Urban <urbanc@in.tum.de> parents: 2971 diff changeset	324	======= end
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	325
2971 d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	326	termination by lexicographic_order
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	327
aaef9dec5e1d side-by-side tests of lets with 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	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	329	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	330	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	331	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	332	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	333	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	334
aaef9dec5e1d side-by-side tests of lets with 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	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	336
aaef9dec5e1d side-by-side tests of lets with 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	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	338	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	339	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	340	"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	341	\| "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	342	\| "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	343	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	344	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	345	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	346	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	347	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	348	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	349	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	350	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	351	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	352	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	353	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	354	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	355	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	356	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	357	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	358	(* 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	359	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	360	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	361	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	362	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	363	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	364	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	365	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	366	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	367
aaef9dec5e1d side-by-side tests of lets with 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	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	369	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	370
aaef9dec5e1d side-by-side tests of lets with 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	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	372	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	373	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	374	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	375	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	376	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	377	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	378	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	379	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	380	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	381	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	382
aaef9dec5e1d side-by-side tests of lets with 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
aaef9dec5e1d side-by-side tests of lets with 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	nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	385	subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::trm2= _]" [90, 90, 90] 90) and
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	386	subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn" ("_ [_ ::assn2= _]" [90, 90, 90] 90)
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	387	where
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	388	"(Var x)[y ::trm2= s] = (if x = y then s else (Var x))"
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	389	\| "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])"
2971 d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	390	\| "(set (bn as)) \<sharp>* (y, s, fv_bn as) \<Longrightarrow> (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])"
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	391	\| "(Assn x t)[y ::assn2= s] = Assn x (t[y ::trm2= s])"
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	392	apply(subgoal_tac "\<And>p x r. subst_trm2_subst_assn2_graph x r \<Longrightarrow> subst_trm2_subst_assn2_graph (p \<bullet> x) (p \<bullet> r)")
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	393	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	394	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	395	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	396	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	397	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	398	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	399	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	400	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	401	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	402	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	403	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	404	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	405	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	406	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	407	--"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	408	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	409	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	410	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	411	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	412	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	413	apply(simp)
2971 d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	414	apply(rule_tac y="aa" and c="(b, c, aa)" in trm_assn.strong_exhaust(1))
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	415	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	416	apply(simp)
2971 d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	417	apply(drule_tac x="assn" in meta_spec)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	418	apply(drule_tac x="b" in meta_spec)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	419	apply(drule_tac x="c" in meta_spec)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	420	apply(drule_tac x="trm" in meta_spec)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	421	apply(simp add: trm_assn.alpha_refl)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	422	apply(rotate_tac 5)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	423	apply(drule meta_mp)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	424	apply(simp add: fresh_star_Pair)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	425	apply(simp add: fresh_star_def trm_assn.fresh)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	426	apply(simp add: fresh_def)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	427	apply(subst supp_finite_atom_set)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	428	apply(simp)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	429	apply(simp)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	430	apply(simp)
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	431	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	432	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	433	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	434	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	435	apply(blast)
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	436	--"compatibility"
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	437	apply(all_trivials)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	438	apply(simp)
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	439	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	440	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	441	apply(simp)
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	442	apply(drule Inl_inject)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	443	apply(rule arg_cong)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	444	back
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	445	apply (simp only: meta_eq_to_obj_eq[OF subst_trm2_def, symmetric, unfolded fun_eq_iff])
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	446	apply (simp only: meta_eq_to_obj_eq[OF subst_assn2_def, symmetric, unfolded fun_eq_iff])
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	447	apply (subgoal_tac "eqvt_at (\<lambda>ast. subst_assn2 ast ya sa) ast")
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	448	apply (subgoal_tac "eqvt_at (\<lambda>asta. subst_assn2 asta ya sa) asta")
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	449	apply (subgoal_tac "eqvt_at (\<lambda>t. subst_trm2 t ya sa) t")
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	450	apply (subgoal_tac "eqvt_at (\<lambda>ta. subst_trm2 ta ya sa) ta")
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	451	apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (ast, y, s))")
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	452	apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (asta, ya, sa))")
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	453	apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (t, y, s))")
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	454	apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (ta, ya, sa))")
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	455	apply(simp)
2971 d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	456	(* HERE *)
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	457	apply (subgoal_tac "subst_assn2 ast y s= subst_assn2 asta ya sa")
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	458	apply (subgoal_tac "subst_trm2 t y s = subst_trm2 ta ya sa")
d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	459	apply(simp)
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	460	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	461	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	462	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	463	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	464	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	465	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	466	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	467
2971 d629240f0f63 some tuning Christian Urban <urbanc@in.tum.de> parents: 2970 diff changeset	468
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	469	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	470	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	471	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	472	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	473	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	474
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	475
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	476
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	477	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	478	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	479	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	480	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	481	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	482	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	483	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	484	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	485	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	486	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	487	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	488	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	489
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	490
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	491	end

author	Christian Urban <urbanc@in.tum.de>
	Tue, 19 Jul 2011 09:40:46 +0100
changeset 2978	967c55907ce1
parent 2977	a4b6e997a7c6
child 3235	5ebd327ffb96
permissions	-rw-r--r--