nominal2: Nominal/Ex/Foo1.thy@3b6a70e73006 (annotated)

2494 11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Foo1
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../Nominal2"
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	(*
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	Contrived example that has more than one
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	binding function for a datatype
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	*)
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	atom_decl name
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	11
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	nominal_datatype foo: trm =
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	Var "name"
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	\| App "trm" "trm"
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	\| Lam x::"name" t::"trm" bind x in t
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	\| Let1 a::"assg" t::"trm" bind "bn1 a" in t
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	\| Let2 a::"assg" t::"trm" bind "bn2 a" in t
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	\| Let3 a::"assg" t::"trm" bind "bn3 a" in t
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	and assg =
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	As "name" "name" "trm"
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	binder
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	bn1::"assg \<Rightarrow> atom list" and
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	bn2::"assg \<Rightarrow> atom list" and
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	bn3::"assg \<Rightarrow> atom list"
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	where
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	"bn1 (As x y t) = [atom x]"
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	\| "bn2 (As x y t) = [atom y]"
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	\| "bn3 (As x y t) = [atom x, atom y]"
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	thm foo.distinct
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	thm foo.induct
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	thm foo.inducts
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	thm foo.exhaust
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	thm foo.fv_defs
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	thm foo.bn_defs
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	thm foo.perm_simps
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	thm foo.eq_iff
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	thm foo.fv_bn_eqvt
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	thm foo.size_eqvt
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	thm foo.supports
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	thm foo.fsupp
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	thm foo.supp
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	thm foo.fresh
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	44
2500 3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	45	primrec
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	46	permute_bn1_raw
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	47	where
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	48	"permute_bn1_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	49
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	50	primrec
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	51	permute_bn2_raw
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	52	where
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	53	"permute_bn2_raw p (As_raw x y t) = As_raw x (p \<bullet> y) t"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	54
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	55	primrec
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	56	permute_bn3_raw
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	57	where
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	58	"permute_bn3_raw p (As_raw x y t) = As_raw (p \<bullet> x) (p \<bullet> y) t"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	59
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	60	quotient_definition
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	61	"permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	62	is
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	63	"permute_bn1_raw"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	64
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	65	quotient_definition
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	66	"permute_bn2 :: perm \<Rightarrow> assg \<Rightarrow> assg"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	67	is
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	68	"permute_bn2_raw"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	69
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	70	quotient_definition
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	71	"permute_bn3 :: perm \<Rightarrow> assg \<Rightarrow> assg"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	72	is
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	73	"permute_bn3_raw"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	74
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	75	lemma [quot_respect]:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	76	shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	77	apply simp
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	78	apply clarify
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	79	apply (erule alpha_assg_raw.cases)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	80	apply simp_all
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	81	apply (rule foo.raw_alpha)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	82	apply simp_all
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	83	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	84
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	85	lemma [quot_respect]:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	86	shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	87	apply simp
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	88	apply clarify
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	89	apply (erule alpha_assg_raw.cases)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	90	apply simp_all
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	91	apply (rule foo.raw_alpha)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	92	apply simp_all
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	93	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	94
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	95	lemma [quot_respect]:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	96	shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	97	apply simp
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	98	apply clarify
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	99	apply (erule alpha_assg_raw.cases)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	100	apply simp_all
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	101	apply (rule foo.raw_alpha)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	102	apply simp_all
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	103	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	104
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	105	lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	106	lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	107	lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	108
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	109	lemma uu1:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	110	shows "alpha_bn1 as (permute_bn1 p as)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	111	apply(induct as rule: foo.inducts(2))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	112	apply(auto)[6]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	113	apply(simp add: permute_bn1)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	114	apply(simp add: foo.eq_iff)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	115	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	116
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	117	lemma uu2:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	118	shows "alpha_bn2 as (permute_bn2 p as)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	119	apply(induct as rule: foo.inducts(2))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	120	apply(auto)[6]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	121	apply(simp add: permute_bn2)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	122	apply(simp add: foo.eq_iff)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	123	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	124
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	125	lemma uu3:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	126	shows "alpha_bn3 as (permute_bn3 p as)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	127	apply(induct as rule: foo.inducts(2))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	128	apply(auto)[6]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	129	apply(simp add: permute_bn3)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	130	apply(simp add: foo.eq_iff)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	131	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	132
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	133	lemma tt1:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	134	shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	135	apply(induct as rule: foo.inducts(2))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	136	apply(auto)[6]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	137	apply(simp add: permute_bn1 foo.bn_defs)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	138	apply(simp add: atom_eqvt)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	139	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	140
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	141	lemma tt2:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	142	shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	143	apply(induct as rule: foo.inducts(2))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	144	apply(auto)[6]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	145	apply(simp add: permute_bn2 foo.bn_defs)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	146	apply(simp add: atom_eqvt)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	147	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	148
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	149	lemma tt3:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	150	shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	151	apply(induct as rule: foo.inducts(2))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	152	apply(auto)[6]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	153	apply(simp add: permute_bn3 foo.bn_defs)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	154	apply(simp add: atom_eqvt)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	155	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	156
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	157
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	158	lemma strong_exhaust1:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	159	fixes c::"'a::fs"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	160	assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	161	and "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	162	and "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	163	and "\<And>assn trm ca. \<lbrakk>set (bn1 assn) \<sharp>* ca; c = ca; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	164	and "\<And>assn trm ca. \<lbrakk>set (bn2 assn) \<sharp>* ca; c = ca; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	165	and "\<And>assn trm ca. \<lbrakk>set (bn3 assn) \<sharp>* ca; c = ca; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	166	shows "P"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	167	apply(rule_tac y="y" in foo.exhaust(1))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	168	apply(rule assms(1))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	169	apply(auto)[2]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	170	apply(rule assms(2))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	171	apply(auto)[2]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	172	apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	173	apply(erule exE)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	174	apply(erule conjE)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	175	apply(rule assms(3))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	176	apply(perm_simp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	177	apply(assumption)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	178	apply(rule refl)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	179	apply(drule supp_perm_eq[symmetric])
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	180	apply(simp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	181	apply(rule at_set_avoiding2)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	182	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	183	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	184	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	185	apply(simp add: foo.fresh fresh_star_def)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	186	apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn1 assg))) \<sharp>* c \<and> supp ([bn1 assg]lst.trm) \<sharp>* q")
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	187	apply(erule exE)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	188	apply(erule conjE)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	189	apply(rule assms(4))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	190	apply(simp add: set_eqvt)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	191	apply(simp add: tt1)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	192	apply(rule refl)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	193	apply(simp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	194	apply(simp add: foo.eq_iff)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	195	apply(drule supp_perm_eq[symmetric])
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	196	apply(simp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	197	apply(simp add: tt1 uu1)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	198	apply(rule at_set_avoiding2)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	199	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	200	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	201	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	202	apply(simp add: Abs_fresh_star)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	203	apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	204	apply(erule exE)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	205	apply(erule conjE)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	206	apply(rule assms(5))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	207	apply(simp add: set_eqvt)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	208	apply(simp add: tt2)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	209	apply(rule refl)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	210	apply(simp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	211	apply(simp add: foo.eq_iff)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	212	apply(drule supp_perm_eq[symmetric])
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	213	apply(simp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	214	apply(simp add: tt2 uu2)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	215	apply(rule at_set_avoiding2)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	216	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	217	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	218	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	219	apply(simp add: Abs_fresh_star)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	220	apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn3 assg))) \<sharp>* c \<and> supp ([bn3 assg]lst.trm) \<sharp>* q")
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	221	apply(erule exE)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	222	apply(erule conjE)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	223	apply(rule assms(6))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	224	apply(simp add: set_eqvt)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	225	apply(simp add: tt3)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	226	apply(rule refl)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	227	apply(simp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	228	apply(simp add: foo.eq_iff)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	229	apply(drule supp_perm_eq[symmetric])
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	230	apply(simp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	231	apply(simp add: tt3 uu3)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	232	apply(rule at_set_avoiding2)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	233	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	234	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	235	apply(simp add: finite_supp)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	236	apply(simp add: Abs_fresh_star)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	237	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	238
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	239	thm foo.exhaust
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	240
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	241	lemma strong_exhaust2:
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	242	assumes "\<And>x y t ca. \<lbrakk>c = ca; as = As x y t\<rbrakk> \<Longrightarrow> P"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	243	shows "P"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	244	apply(rule_tac y="as" in foo.exhaust(2))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	245	apply(rule assms(1))
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	246	apply(auto)[2]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	247	done
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	248
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	249
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	250	lemma
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	251	fixes t::trm
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	252	and as::assg
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	253	and c::"'a::fs"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	254	assumes a1: "\<And>x c. P1 c (Var x)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	255	and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	256	and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	257	and a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	258	and a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	259	and a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	260	and a7: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	261	shows "P1 c t" "P2 c as"
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	262	using assms
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	263	apply(induction_schema)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	264	apply(rule_tac y="t" in strong_exhaust1)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	265	apply(blast)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	266	apply(blast)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	267	apply(blast)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	268	apply(blast)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	269	apply(blast)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	270	apply(blast)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	271	apply(rule_tac as="as" in strong_exhaust2)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	272	apply(blast)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	273	apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	274	apply(auto)[1]
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	275	apply(simp_all add: foo.size)
3b6a70e73006 worked example Foo1 with induct_schema Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	276	done
2494 11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	277
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	278	end
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	279
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	280
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: diff changeset	281

author	Christian Urban <urbanc@in.tum.de>
	Wed, 29 Sep 2010 09:47:26 -0400
changeset 2500	3b6a70e73006
parent 2494	11133eb76f61
child 2503	cc5d23547341
permissions	-rw-r--r--