# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1293013921 0 # Node ID d17fadc20507240506e1c52721fd4c7c49ba6750 # Parent e44551d067e6dfd1a585bfab2a3c0c96b77d0ee4 corrected premises of strong exhausts theorems diff -r e44551d067e6 -r d17fadc20507 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Wed Dec 22 09:13:25 2010 +0000 +++ b/Nominal/Ex/Let.thy Wed Dec 22 10:32:01 2010 +0000 @@ -30,39 +30,6 @@ thm trm_assn.exhaust thm trm_assn.strong_exhaust -lemma strong_exhaust1: - fixes c::"'a::fs" - assumes "\<And>name. y = Var name \<Longrightarrow> P" - and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" - and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" - and "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P" - shows "P" -apply(rule_tac y="y" in trm_assn.strong_exhaust(1)) -apply(rule assms(1)) -apply(assumption) -apply(rule assms(2)) -apply(assumption) -apply(rule assms(3)) -apply(assumption) -apply(assumption) -apply(rule assms(4)) -apply(assumption) -apply(assumption) -sorry - - -lemma strong_exhaust2: - assumes "as = ANil \<Longrightarrow> P" - and "\<And>x t assn. \<lbrakk>as = ACons x t assn\<rbrakk> \<Longrightarrow> P" - shows "P" -apply(rule_tac y="as" in trm_assn.exhaust(2)) -apply(rule assms(1)) -apply(assumption) -apply(rule assms(2)) -apply(assumption)+ -done - - lemma fixes t::trm and as::assn @@ -76,12 +43,12 @@ shows "P1 c t" "P2 c as" using assms apply(induction_schema) -apply(rule_tac y="t" in strong_exhaust1) +apply(rule_tac y="t" in trm_assn.strong_exhaust(1)) apply(blast) apply(blast) apply(blast) apply(blast) -apply(rule_tac as="as" in strong_exhaust2) +apply(rule_tac ya="as" in trm_assn.strong_exhaust(2)) apply(blast) apply(blast) apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))") diff -r e44551d067e6 -r d17fadc20507 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Wed Dec 22 09:13:25 2010 +0000 +++ b/Nominal/Nominal2.thy Wed Dec 22 10:32:01 2010 +0000 @@ -296,18 +296,17 @@ |> split_list |>> (map o map) strip_params_prems_concl - val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss) + val premss = ((map2 o map2) (process_ecase lthy'' c) ecases bclausesss) + in - Goal.prove_multi lthy'' [] prems main_concls - (fn {prems:thm list, context} => - let - val prems' = partitions prems (map length bclausesss) - in - EVERY1 [Goal.conjunction_tac, - RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) - (prems' ~~ bclausesss) exhausts')] - end) - |> ProofContext.export lthy'' lthy + map2 (fn (prems, bclausess) => fn (exh, concl) => + Goal.prove lthy'' [] prems concl + (fn {prems: thm list, context} => + HEADGOAL (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas + (prems, bclausess) exh) + ) + ) (premss ~~ bclausesss) (exhausts' ~~ main_concls) + |> ProofContext.export lthy'' lthy end *} diff -r e44551d067e6 -r d17fadc20507 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Wed Dec 22 09:13:25 2010 +0000 +++ b/Nominal/ROOT.ML Wed Dec 22 10:32:01 2010 +0000 @@ -24,6 +24,6 @@ "Ex/TypeVarsTest", (*"Ex/Foo1", "Ex/Foo2",*) - "Ex/CoreHaskell" + "Ex/CoreHaskell", "Ex/CoreHaskell2" ];