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

2931 aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Let
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../Nominal2"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	5	(*
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	6	ML {*
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	7	val lemma =
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	8	Term_XML.Encode.term #>
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	9	YXML.string_of_body #>
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	10	translate_string (fn c => if ord c < 10 then "\\00" ^ string_of_int (ord c) else c) #>
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	11	quote #> prefix "lemma " #>
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	12	Markup.markup Markup.sendback #> writeln
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	13	*}
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	14
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	15	ML {* lemma @{prop "x == x"} *}
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	16	*)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	17
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	18	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	19
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	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	21	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	22	\| 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	23	\| 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	24	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	25	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	26	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	27	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	28	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	29	"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	30
aaef9dec5e1d side-by-side tests of lets with 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	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	32
aaef9dec5e1d side-by-side tests of lets with 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 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	34	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	35	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	36	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	37
aaef9dec5e1d side-by-side tests of lets with 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.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	39	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	40	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	41	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	42	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	43	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	44	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	45	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	46	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	47	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	48	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	49	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	50	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	51
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	thm alpha_bn_raw.cases
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	53	thm trm_assn.alpha_refl
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	54	thm trm_assn.alpha_sym
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	55	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	56
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	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	58
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	lemma alpha_bn_refl: "alpha_bn x x"
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	60	by(rule trm_assn.alpha_refl)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	61
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	62	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	63	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	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	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	66	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	67
aaef9dec5e1d side-by-side tests of lets with 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	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	69
aaef9dec5e1d side-by-side tests of lets with 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	lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	by (simp add: permute_pure)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	72
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	73
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	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	75
aaef9dec5e1d side-by-side tests of lets with 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	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	77	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	78	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	79	"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	80	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	81	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	82	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	83	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	84	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	85	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	86
aaef9dec5e1d side-by-side tests of lets with 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	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	88	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	89
aaef9dec5e1d side-by-side tests of lets with 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	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	91	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	92	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	93	"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	94	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	95	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	96	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	97	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	98	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	99	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	100
aaef9dec5e1d side-by-side tests of lets with 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	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	102	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	103
aaef9dec5e1d side-by-side tests of lets with 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	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	105	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	106	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	107	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	108	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	109	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	110	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	111
aaef9dec5e1d side-by-side tests of lets with 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	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	113	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	114	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	115	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	116	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	117	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	118	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	119
aaef9dec5e1d side-by-side tests of lets with 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
aaef9dec5e1d side-by-side tests of lets with 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	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	122	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	123	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	124	"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	125	\| "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	126	\| "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	127	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	128	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	129	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	130	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	131	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	132	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	133	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	134	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	135	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	136	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	137	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	138	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	139	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	140	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	141	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	142	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	143	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	144	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	145	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	146	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	147	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	148
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	149	(* assn-function prevents automatic discharge
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	150	termination by lexicographic_order
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	151	*)
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	152
aaef9dec5e1d side-by-side tests of lets with 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	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	154	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	155	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	156	"(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	157	\| "(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	158	\| "(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	159	(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	160	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	161	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	162	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	163	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	164	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	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 (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	167	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	168	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	169	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	170	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	171	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	172	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	173	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	174	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	175	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	176	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	177	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	178	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	179
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	180
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	181	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	182
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	183	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	184
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	185	nominal_primrec
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	186	(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")
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	187	height_trm2 :: "trm \<Rightarrow> nat"
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	188	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	189	where
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	190	"height_trm2 (Var x) = 1"
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	191	\| "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)"
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	192	\| "height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)"
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	193	\| "height_assn2 (Assn x t) = (height_trm2 t)"
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	194	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	195	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	196	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	197	apply (rule, perm_simp, rule)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	198	apply(erule height_trm2_height_assn2_graph.induct)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	199	-- "invariant"
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	200	apply(simp)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	201	apply(simp)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	202	apply(simp)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	203	apply(simp)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	204	apply(rule cheat)
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	205	apply -
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	206	--"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	207	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	208	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	209	apply (case_tac a rule: trm_assn.exhaust(1))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	210	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	211	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	212	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	213	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	214	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	215	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	216	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	217	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	218	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	219	apply(simp)
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	220	prefer 2
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	221	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	222	--"let case"
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	223	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	224	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	225	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	226	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	227	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	228	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	229	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	230	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	231	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	232	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	233	defer
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	234	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	235	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	236	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	237	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	238	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	239	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	240	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	241	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	242	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	243	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	244	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	245	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	246	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	247	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	248	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	249	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	250	apply(drule Inl_inject)
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	251	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	252	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	253	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	254	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	255	apply(simp only: trm_assn.bn_defs)
2960 248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	256	apply(erule_tac c="()" in Abs_lst1_fcb2')
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	257	apply(simp_all add: fresh_star_def pure_fresh)[3]
248546bfeb16 some more experiments with let and bns Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	258
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	259	oops
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	260
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	261
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	262	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	263	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	264	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	265	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	266	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	267	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	268
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	269	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	270
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	271	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	272	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	273	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	274	"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	275	\| "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	276	\| "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	277	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	278	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	279	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	280	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	281	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	282	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	283	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	284	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	285	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	286	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	287	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	288	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	289	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	290	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	291	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	292	(* 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	293	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	294	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	295	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	296	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	297	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	298	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	299	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	300	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	301
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	302	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	303	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	304
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	305	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	306	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	307	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	308	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	309	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	310	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	311	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	312	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	313	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	314	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	315	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	316
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	317
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	318	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	319	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	320	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	321	where
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	322	"(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	323	\| "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])"
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	324	\| "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])"
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	325	\| "(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	326	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	327	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	328	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	329	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	330	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	331	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	332	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	333	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	334	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	335	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	336	apply(simp)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	337	apply(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	338	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	339	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	340	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	341	--"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	342	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	343	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	344	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	345	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	346	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	347	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	348	apply(rule_tac y="aa" and c="(b, c)" in trm_assn.strong_exhaust(1))
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	349	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	350	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	351	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	352	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	353	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	354	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	355	apply(blast)
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	356	--"compatibility"
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	357	apply(all_trivials)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	358	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	359	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	360	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	361	apply(simp)
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	362	thm Inl_inject
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	363	apply(drule Inl_inject)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	364	apply(rule arg_cong)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	365	back
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	366	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	367	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	368	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	369	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	370	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	371	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	372	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	373	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	374	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	375	apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (ta, ya, sa))")
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	376	defer
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	377	apply(simp add: Abs_eq_iff alphas)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	378	apply(clarify)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	379	apply(rule eqvt_at_perm)
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	380	apply(simp)
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	381	apply(simp add: subst_trm2_def)
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	382	apply(simp add: eqvt_at_def)
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	383	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	384	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	385	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	386	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	387	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	388	apply(rule conjI)
2966 fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	389	apply (subgoal_tac "subst_assn2 ast ya sa= subst_assn2 asta ya sa")
fa37c2a33812 slight tuning Christian Urban <urbanc@in.tum.de> parents: 2960 diff changeset	390	apply (subgoal_tac "subst_trm2 t ya sa = subst_trm2 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	391	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	392	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	393	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	394	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	395	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	396	apply(drule k)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	397	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	398	apply(subst (asm) Abs1_eq_iff)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	399	apply(rule sort_of_atom_eq)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	400	apply(rule sort_of_atom_eq)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	401	apply(erule disjE)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	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(rotate_tac 12)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	404	apply(drule sym)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	405	apply(rule sym)
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	406	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	407	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	408
aaef9dec5e1d side-by-side tests of lets with 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	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	410	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	411	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	412	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	413	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	414
aaef9dec5e1d side-by-side tests of lets with 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
aaef9dec5e1d side-by-side tests of lets with 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
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	417	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	418	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	419	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	420	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	421	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	422	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	423	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	424	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	425	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	426	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	427	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	428	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	429
aaef9dec5e1d side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function Christian Urban <urbanc@in.tum.de> parents: diff changeset	430
aaef9dec5e1d side-by-side tests of lets with 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	end

author	Christian Urban <urbanc@in.tum.de>
	Wed, 13 Jul 2011 09:47:58 +0100
changeset 2966	fa37c2a33812
parent 2960	248546bfeb16
child 2968	ddb69d9f45d0
permissions	-rw-r--r--