# HG changeset patch # User Christian Urban # Date 1293065166 0 # Node ID d1bdc281be2b25dbcfdba33983aae82a4ffa52ff # Parent 478c5648e73fa7826bde1855b3302f79d5ffc4c7 moved all strong_exhaust code to nominal_dt_quot; tuned examples diff -r 478c5648e73f -r d1bdc281be2b Nominal/Ex/Foo1.thy --- a/Nominal/Ex/Foo1.thy Thu Dec 23 00:22:41 2010 +0000 +++ b/Nominal/Ex/Foo1.thy Thu Dec 23 00:46:06 2010 +0000 @@ -44,6 +44,7 @@ thm foo.induct thm foo.inducts thm foo.exhaust +thm foo.strong_exhaust thm foo.fv_defs thm foo.bn_defs thm foo.perm_simps @@ -56,62 +57,6 @@ thm foo.fresh thm foo.bn_finite -lemma strong_exhaust1: - fixes c::"'a::fs" - assumes "\name. y = Var name \ P" - and "\trm1 trm2. y = App trm1 trm2 \ P" - and "\name trm. {atom name} \* c \ y = Lam name trm \ P" - and "\(c::'a::fs) assn trm. set (bn1 assn) \* c \ y = Let1 assn trm \ P" - and "\(c::'a::fs) assn trm. set (bn2 assn) \* c \ y = Let2 assn trm \ P" - and "\(c::'a::fs) assn trm. set (bn3 assn) \* c \ y = Let3 assn trm \ P" - and "\(c::'a::fs) assn' trm. (bn4 assn') \* c \ y = Let4 assn' trm \ P" - shows "P" -oops - - -lemma strong_exhaust2: - fixes c::"'a::fs" - assumes "\name. y = Var name \ P" - and "\trm1 trm2. y = App trm1 trm2 \ P" - and "\name trm. \{atom name} \* c; y = Lam name trm\ \ P" - and "\assn trm. \set (bn1 assn) \* c; y = Let1 assn trm\ \ P" - and "\assn trm. \set (bn2 assn) \* c; y = Let2 assn trm\ \ P" - and "\assn trm. \set (bn3 assn) \* c; y = Let3 assn trm\ \ P" - and "\assn' trm. \(bn4 assn') \* c; y = Let4 assn' trm\ \ P" - shows "P" -oops - -lemma strong_exhaust1: - fixes c::"'a::fs" - assumes "\name. y = Var name \ P" - and "\trm1 trm2. y = App trm1 trm2 \ P" - and "\name trm. \{atom name} \* c; y = Lam name trm\ \ P" - and "\assn trm. \set (bn1 assn) \* c; y = Let1 assn trm\ \ P" - and "\assn trm. \set (bn2 assn) \* c; y = Let2 assn trm\ \ P" - and "\assn trm. \set (bn3 assn) \* c; y = Let3 assn trm\ \ P" - and "\assn' trm. \(bn4 assn') \* c; y = Let4 assn' trm\ \ P" - shows "P" -oops - -lemma strong_exhaust2: - assumes "\x y t. as = As x y t \ P" - shows "P" -apply(rule_tac y="as" in foo.exhaust(2)) -apply(rule assms(1)) -apply(assumption) -done - -lemma strong_exhaust3: - assumes "as' = BNil \ P" - and "\a as. as' = BAs a as \ P" - shows "P" -apply(rule_tac y="as'" in foo.exhaust(3)) -apply(rule assms(1)) -apply(assumption) -apply(rule assms(2)) -apply(assumption) -done - lemma fixes t::trm and as::assg @@ -128,20 +73,17 @@ and a9: "\c. P3 c (BNil)" and a10: "\c a as. \d. P3 d as \ P3 c (BAs a as)" shows "P1 c t" "P2 c as" "P3 c as'" -oops -(* using assms apply(induction_schema) -apply(rule_tac y="t" and c="c" in strong_exhaust1) +apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1)) apply(simp_all)[7] -apply(rule_tac as="as" in strong_exhaust2) -apply(simp) -apply(rule_tac as'="as'" in strong_exhaust3) +apply(rule_tac ya="as"in foo.strong_exhaust(2)) +apply(simp_all)[1] +apply(rule_tac yb="as'" in foo.strong_exhaust(3)) apply(simp_all)[2] -apply(relation "measure (sum_case (size o snd) (sum_case (\y. size (snd y)) (\z. size (snd z))))") +apply(relation "measure (sum_case (size o snd) (sum_case (size o snd) (size o snd)))") apply(simp_all add: foo.size) done -*) end diff -r 478c5648e73f -r d1bdc281be2b Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Thu Dec 23 00:22:41 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Thu Dec 23 00:46:06 2010 +0000 @@ -24,10 +24,6 @@ "bn (As x y t a) = [atom x] @ bn a" | "bn (As_Nil) = []" - - - - thm foo.bn_defs thm foo.permute_bn thm foo.perm_bn_alpha @@ -39,6 +35,7 @@ thm foo.induct thm foo.inducts thm foo.exhaust +thm foo.strong_exhaust thm foo.fv_defs thm foo.bn_defs thm foo.perm_simps @@ -50,308 +47,6 @@ thm foo.supp thm foo.fresh -lemma at_set_avoiding5: - assumes "finite xs" - and "finite (supp c)" - shows "\p. (p \ xs) \* c \ supp p = xs \ p \ xs" -using assms -apply(erule_tac c="c" in at_set_avoiding) -apply(auto) -done - - -lemma Abs_rename_lst3: - fixes x::"'a::fs" - assumes a: "(p \ (set bs)) \* (bs, x)" - shows "\q. [bs]lst. x = [p \ bs]lst. (q \ x) \ p \ bs = q \ bs" -proof - - from a have "p \ (set bs) \ (set bs) = {}" using at_fresh_star_inter - by (simp add: fresh_star_Pair fresh_star_set) - with list_renaming_perm - obtain q where *: "q \ bs = p \ bs" and **: "supp q \ set bs \ (p \ set bs)" by metis - have "[bs]lst. x = q \ ([bs]lst. x)" - apply(rule perm_supp_eq[symmetric]) - using a ** - unfolding fresh_star_Pair - unfolding Abs_fresh_star_iff - unfolding fresh_star_def - by auto - also have "\ = [q \ bs]lst. (q \ x)" by simp - also have "\ = [p \ bs]lst. (q \ x)" using * by simp - finally have "[bs]lst. x = [p \ bs]lst. (q \ x)" . - then show "\q. [bs]lst. x = [p \ bs]lst. (q \ x) \ p \ bs = q \ bs" - using * ** by metis -qed - - -lemma - fixes c::"'a::fs" - assumes a: "\assg1 trm1 assg2 trm2. \((set (bn assg1)) \ (set (bn assg2))) \* c; y = Let1 assg1 trm1 assg2 trm2\ \ P" - shows "y = Let1 assg1 trm1 assg2 trm2 \ P" -apply - -apply(subgoal_tac "\p. (p \ ((set (bn assg1)) \ (set (bn assg2)))) \* (c, bn assg1, bn assg2, trm1, trm2) \ - supp p = (set (bn assg1)) \ (set (bn assg2)) \ (p \ ((set (bn assg1)) \ (set (bn assg2))))") -defer -apply(rule at_set_avoiding5) -apply(simp add: foo.bn_finite) -apply(simp add: supp_Pair finite_supp) -apply(erule exE) -apply(perm_simp add: foo.permute_bn) -apply(simp add: fresh_star_Pair) -apply(erule conjE)+ -thm Abs_rename_lst -apply(insert Abs_rename_lst)[1] -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="bn assg1" in meta_spec) -apply(drule_tac x="trm1" in meta_spec) -apply(insert Abs_rename_lst)[1] -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="bn assg2" in meta_spec) -apply(drule_tac x="trm2" in meta_spec) -apply(drule meta_mp) -apply(perm_simp add: foo.permute_bn) -apply(simp add: fresh_star_Pair fresh_star_Un) -apply(drule meta_mp) -apply(perm_simp add: foo.permute_bn) -apply(simp add: fresh_star_Pair fresh_star_Un) -apply(erule exE)+ -apply(rule a) -apply(assumption) -apply(simp only: foo.eq_iff) -apply(perm_simp add: foo.permute_bn) -apply(rule conjI) -apply(rule refl) -apply(rule conjI) -apply(rule foo.perm_bn_alpha) -apply(rule conjI) -apply(perm_simp add: foo.permute_bn) -apply(rule refl) -apply(rule foo.perm_bn_alpha) -done - -lemma - fixes c::"'a::fs" - assumes a: "\assg1 trm1 assg2 trm2. \((set (bn assg1)) \ (set (bn assg2))) \* c; y = Let1 assg1 trm1 assg2 trm2\ \ P" - shows "y = Let1 assg1 trm1 assg2 trm2 \ P" -apply - -apply(subgoal_tac "\p. (p \ ((set (bn assg1)) \ (set (bn assg2)))) \* (c, bn assg1, bn assg2, trm1, trm2) \ - supp p = (set (bn assg1)) \ (set (bn assg2)) \ (p \ ((set (bn assg1)) \ (set (bn assg2))))") -defer -apply(rule at_set_avoiding5) -apply(simp add: foo.bn_finite) -apply(simp add: supp_Pair finite_supp) -apply(erule exE) -apply(perm_simp add: foo.permute_bn) -apply(simp add: fresh_star_Pair) -apply(erule conjE)+ -apply(insert Abs_rename_lst3)[1] -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="bn assg1" in meta_spec) -apply(drule_tac x="trm1" in meta_spec) -apply(insert Abs_rename_lst3)[1] -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="bn assg2" in meta_spec) -apply(drule_tac x="trm2" in meta_spec) -apply(drule meta_mp) -apply(perm_simp add: foo.permute_bn) -apply(simp add: fresh_star_Pair fresh_star_Un) -apply(drule meta_mp) -apply(perm_simp add: foo.permute_bn) -apply(simp add: fresh_star_Pair fresh_star_Un) -apply(erule exE)+ -apply(erule conjE)+ -apply(simp add: foo.permute_bn) -apply(rule a) -apply(assumption) -apply(clarify) -apply(simp (no_asm) only: foo.eq_iff) -apply(rule conjI) -apply(assumption) -apply(rule conjI) -apply(rule foo.perm_bn_alpha) -apply(rule conjI) -apply(assumption) -apply(rule foo.perm_bn_alpha) -done - - -lemma - fixes c::"'a::fs" - assumes a: "\assg1 trm1 assg2 trm2. \((set (bn assg1)) \ (set (bn assg2))) \* c; y = Let1 assg1 trm1 assg2 trm2\ \ P" - shows "y = Let1 assg1 trm1 assg2 trm2 \ P" -apply - -apply(subgoal_tac "\p. (p \ ((set (bn assg1)) \ (set (bn assg2)))) \* (c, bn assg1, bn assg2, trm1, trm2) \ - supp p = (set (bn assg1)) \ (set (bn assg2)) \ (p \ ((set (bn assg1)) \ (set (bn assg2))))") -defer -apply(rule at_set_avoiding5) -apply(simp add: foo.bn_finite) -apply(simp add: supp_Pair finite_supp) -apply(erule exE) -apply(simp add: fresh_star_Pair) -apply(erule conjE)+ -apply(simp (no_asm_use) only: foo.permute_bn set_eqvt union_eqvt) -apply(rule a) -apply(assumption) -apply(clarify) -apply(simp (no_asm) only: foo.eq_iff) -apply(rule conjI) -apply(rule trans) -apply(rule_tac p="p" in supp_perm_eq[symmetric]) -apply(rule fresh_star_supp_conv) -apply(simp (no_asm_use) add: fresh_star_def) -apply(simp (no_asm_use) add: Abs_fresh_iff)[1] -apply(rule ballI) -apply(auto simp add: fresh_Pair)[1] -apply(simp (no_asm_use) only: permute_Abs) -apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt) -apply(simp) -apply(rule at_set_avoiding5) -apply(simp add: multi_recs.bn_finite) -apply(simp add: supp_Pair finite_supp) -apply(rule finite_sets_supp) -apply(simp add: multi_recs.bn_finite) -done - - - -lemma test6: - fixes c::"'a::fs" - assumes "\name. y = Var name \ P" - and "\trm1 trm2. y = App trm1 trm2 \ P" - and "\name trm. \{atom name} \* c; y = Lam name trm\ \ P" - and "\a1 trm1 a2 trm2. \((set (bn a1)) \ (set (bn a2))) \* c; y = Let1 a1 trm1 a2 trm2\ \ P" - and "\x1 x2 trm1 trm2. {atom x1, atom x2} \* c \ y = Let2 x1 x2 trm1 trm2 \ P" - shows "P" -apply(rule_tac y="y" in foo.exhaust(1)) -apply(rule assms(1)) -apply(assumption) -apply(rule assms(2)) -apply(assumption) -(* lam case *) -apply(subgoal_tac "\p. (p \ {atom name}) \* (c, name, trm)") -apply(erule exE) -apply(insert Abs_rename_lst)[1] -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="[atom name]" in meta_spec) -apply(drule_tac x="trm" in meta_spec) -apply(simp only: fresh_star_Pair set.simps) -apply(drule meta_mp) -apply(simp add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base) -apply(erule exE) -apply(rule assms(3)) -apply(perm_simp) -apply(erule conjE)+ -apply(assumption) -apply(clarify) -apply(simp (no_asm) add: foo.eq_iff) -apply(perm_simp) -apply(assumption) -apply(rule at_set_avoiding1) -apply(simp) -apply(simp add: finite_supp) -(* let1 case *) -apply(subgoal_tac "\p. (p \ ((set (bn assg1)) \ (set (bn assg2)))) \* (c, bn assg1, bn assg2, trm1, trm2)") -apply(erule exE) -apply(perm_simp add: foo.permute_bn) -apply(simp add: fresh_star_Pair) -apply(erule conjE)+ -apply(insert Abs_rename_lst)[1] -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="bn assg1" in meta_spec) -apply(drule_tac x="trm1" in meta_spec) -apply(insert Abs_rename_lst)[1] -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="bn assg2" in meta_spec) -apply(drule_tac x="trm2" in meta_spec) -apply(drule meta_mp) -apply(perm_simp add: foo.permute_bn) -apply(simp add: fresh_star_Pair fresh_star_Un) -apply(drule meta_mp) -apply(perm_simp add: foo.permute_bn) -apply(simp add: fresh_star_Pair fresh_star_Un) -apply(erule exE)+ -apply(rule assms(4)) -apply(assumption) -apply(simp add: foo.eq_iff refl) -apply(rule conjI) -apply(perm_simp add: foo.permute_bn) -apply(rule refl) -apply(rule conjI) -apply(rule foo.perm_bn_alpha) -apply(rule conjI) -apply(perm_simp add: foo.permute_bn) -apply(rule refl) -apply(rule foo.perm_bn_alpha) -apply(rule at_set_avoiding1) -apply(simp) -apply(simp add: finite_supp) -(* let2 case *) -apply(subgoal_tac "\p. (p \ ({atom name1} \ {atom name2})) \* (c, atom name1, atom name2, trm1, trm2)") -apply(erule exE) -apply(rule assms(5)) -apply(simp only:) -apply(simp only: foo.eq_iff) -apply(insert Abs_rename_list)[1] -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec) -apply(drule_tac x="trm1" in meta_spec) -apply(insert Abs_rename_list)[1] -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="[atom name2]" in meta_spec) -apply(drule_tac x="trm2" in meta_spec) -apply(drule meta_mp) -apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp) -apply(auto)[1] -apply(perm_simp) -apply(auto simp add: fresh_star_def)[1] -apply(perm_simp) -apply(auto simp add: fresh_star_def)[1] -apply(perm_simp) -apply(auto simp add: fresh_star_def)[1] -apply(drule meta_mp) -apply(perm_simp) -apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1] -apply(erule exE)+ -apply(rule exI)+ -apply(perm_simp add: foo.permute_bn) -apply(rule conjI) -prefer 2 -apply(rule conjI) -apply(assumption) -apply(assumption) -apply(simp add: fresh_star_Pair) -apply(simp add: fresh_star_def) -apply(rule at_set_avoiding1) -apply(simp) -apply(simp add: finite_supp) -done - -lemma test5: - fixes c::"'a::fs" - assumes "\name. y = Var name \ P" - and "\trm1 trm2. y = App trm1 trm2 \ P" - and "\name trm. \{atom name} \* c; y = Lam name trm\ \ P" - and "\a1 trm1 a2 trm2. \((set (bn a1)) \ (set (bn a2))) \* c; y = Let1 a1 trm1 a2 trm2\ \ P" - and "\x1 x2 trm1 trm2. \{atom x1, atom x2} \* c; y = Let2 x1 x2 trm1 trm2\ \ P" - shows "P" -apply(rule_tac y="y" in test6) -apply(erule exE)+ -apply(rule assms(1)) -apply(assumption) -apply(erule exE)+ -apply(rule assms(2)) -apply(assumption) -apply(rule assms(3)) -apply(auto)[2] -apply(erule exE)+ -apply(rule assms(4)) -apply(auto)[2] -apply(erule exE)+ -apply(rule assms(5)) -apply(auto)[2] -done - - lemma strong_induct: fixes c :: "'a :: fs" and assg :: assg and trm :: trm @@ -362,15 +57,15 @@ \((set (bn a1)) \ (set (bn a2))) \* c; \d. P2 c a1; \d. P1 d t1; \d. P2 d a2; \d. P1 d t2\ \ P1 c (Let1 a1 t1 a2 t2)" and a4: "\n1 n2 t1 t2 c. - \{atom n1, atom n2} \* c; \d. P1 d t1; \d. P1 d t2\ \ P1 c (Let2 n1 n2 t1 t2)" + \({atom n1} \ {atom n2}) \* c; \d. P1 d t1; \d. P1 d t2\ \ P1 c (Let2 n1 n2 t1 t2)" and a5: "\c. P2 c As_Nil" and a6: "\name1 name2 trm assg c. \\d. P1 d trm; \d. P2 d assg\ \ P2 c (As name1 name2 trm assg)" shows "P1 c trm" "P2 c assg" using assms apply(induction_schema) - apply(rule_tac y="trm" and c="c" in test5) + apply(rule_tac y="trm" and c="c" in foo.strong_exhaust(1)) apply(simp_all)[5] - apply(rule_tac y="assg" in foo.exhaust(2)) + apply(rule_tac ya="assg" in foo.strong_exhaust(2)) apply(simp_all)[2] apply(relation "measure (sum_case (size o snd) (size o snd))") apply(simp_all add: foo.size) diff -r 478c5648e73f -r d1bdc281be2b Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Thu Dec 23 00:22:41 2010 +0000 +++ b/Nominal/Nominal2.thy Thu Dec 23 00:46:06 2010 +0000 @@ -16,250 +16,6 @@ use "nominal_dt_quot.ML" ML {* open Nominal_Dt_Quot *} -text {* TEST *} - - -ML {* -(* adds a freshness condition to the assumptions *) -fun mk_ecase_prems lthy c (params, prems, concl) bclauses = - let - val tys = map snd params - val binders = get_all_binders bclauses - - fun prep_binder (opt, i) = - let - val t = Bound (length tys - i - 1) - in - case opt of - NONE => setify_ty lthy (nth tys i) t - | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) - end - - val prems' = - case binders of - [] => prems (* case: no binders *) - | _ => binders (* case: binders *) - |> map prep_binder - |> fold_union_env tys - |> (fn t => mk_fresh_star t c) - |> (fn t => HOLogic.mk_Trueprop t :: prems) - in - mk_full_horn params prems' concl - end -*} - - -ML {* -(* derives the freshness theorem that there exists a p, such that - (p o as) #* (c, t1,\, tn) *) -fun fresh_thm ctxt c parms binders bn_finite_thms = - let - fun prep_binder (opt, i) = - case opt of - NONE => setify ctxt (nth parms i) - | SOME bn => to_set (bn $ (nth parms i)) - - fun prep_binder2 (opt, i) = - case opt of - NONE => atomify ctxt (nth parms i) - | SOME bn => bn $ (nth parms i) - - val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders)) - val lhs = binders - |> map prep_binder - |> fold_union - |> mk_perm (Bound 0) - - val goal = mk_fresh_star lhs rhs - |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t)) - |> HOLogic.mk_Trueprop - - val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} - @ @{thms finite.intros finite_Un finite_set finite_fset} - in - Goal.prove ctxt [] [] goal - (K (HEADGOAL (rtac @{thm at_set_avoiding1} - THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) - end -*} - -ML {* -fun abs_const bmode ty = - let - val (const_name, binder_ty, abs_ty) = - case bmode of - Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst}) - | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set}) - | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res}) - in - Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty])) - end - -fun mk_abs bmode trm1 trm2 = - abs_const bmode (fastype_of trm2) $ trm1 $ trm2 - -fun is_abs_eq thm = - let - fun is_abs trm = - case (head_of trm) of - Const (@{const_name "Abs_set"}, _) => true - | Const (@{const_name "Abs_lst"}, _) => true - | Const (@{const_name "Abs_res"}, _) => true - | _ => false - in - thm |> prop_of - |> HOLogic.dest_Trueprop - |> HOLogic.dest_eq - |> fst - |> is_abs - end -*} - - - -ML {* -(* derives an abs_eq theorem of the form - - Exists q. [as].x = [p o as].(q o x) for non-recursive binders - Exists q. [as].x = [q o as].(q o x) for recursive binders -*) -fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns - (bclause as (BC (bmode, binders, bodies))) = - case binders of - [] => [] - | _ => - let - val rec_flag = is_recursive_binder bclause - val binder_trm = comb_binders ctxt bmode parms binders - val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) - - val abs_lhs = mk_abs bmode binder_trm body_trm - val abs_rhs = - if rec_flag - then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm) - else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm) - - val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) - val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) - - val goal = HOLogic.mk_conj (abs_eq, peq) - |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) - |> HOLogic.mk_Trueprop - - val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} - @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset - fresh_star_set} @ @{thms finite.intros finite_fset} - - val tac1 = - if rec_flag - then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} - else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} - - val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] - in - [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) - |> (if rec_flag - then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] - else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ] - end -*} - - - -lemma setify: - shows "xs = ys \ set xs = set ys" - by simp - -ML {* -fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas - prems bclausess qexhaust_thm = - let - fun aux_tac prem bclauses = - case (get_all_binders bclauses) of - [] => EVERY' [rtac prem, atac] - | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => - let - val parms = map (term_of o snd) params - val fthm = fresh_thm ctxt c parms binders bn_finite_thms - - val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} - val (([(_, fperm)], fprops), ctxt') = Obtain.result - (K (EVERY1 [etac exE, - full_simp_tac (HOL_basic_ss addsimps ss), - REPEAT o (etac @{thm conjE})])) [fthm] ctxt - - val abs_eq_thms = flat - (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses) - - val ((_, eqs), ctxt'') = Obtain.result - (K (EVERY1 - [ REPEAT o (etac @{thm exE}), - REPEAT o (etac @{thm conjE}), - REPEAT o (dtac @{thm setify}), - full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' - - val (abs_eqs, peqs) = split_filter is_abs_eq eqs - - val fprops' = - map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops - @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops - - (* for freshness conditions *) - val tac1 = SOLVED' (EVERY' - [ simp_tac (HOL_basic_ss addsimps peqs), - rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), - conj_tac (DETERM o resolve_tac fprops') ]) - - (* for equalities between constructors *) - val tac2 = SOLVED' (EVERY' - [ rtac (@{thm ssubst} OF prems), - rewrite_goal_tac (map safe_mk_equiv eq_iff_thms), - rewrite_goal_tac (map safe_mk_equiv abs_eqs), - conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) - - (* proves goal "P" *) - val side_thm = Goal.prove ctxt'' [] [] (term_of concl) - (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ])) - |> singleton (ProofContext.export ctxt'' ctxt) - in - rtac side_thm 1 - end) ctxt - in - EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)] - end -*} - -ML {* -fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns - perm_bn_alphas = - let - val ((_, exhausts'), lthy') = Variable.import true exhausts lthy - - val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' - val c = Free (c, TFree (a, @{sort fs})) - - val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *) - |> map prop_of - |> map Logic.strip_horn - |> split_list - - val ecases' = (map o map) strip_full_horn ecases - - val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss - - fun tac bclausess exhaust {prems, context} = - case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas - prems bclausess exhaust - - fun prove prems bclausess exhaust concl = - Goal.prove lthy'' [] prems concl (tac bclausess exhaust) - in - map4 prove premss bclausesss exhausts' main_concls - |> ProofContext.export lthy'' lthy - end -*} - - ML {* val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) diff -r 478c5648e73f -r d1bdc281be2b Nominal/ROOT.ML --- a/Nominal/ROOT.ML Thu Dec 23 00:22:41 2010 +0000 +++ b/Nominal/ROOT.ML Thu Dec 23 00:46:06 2010 +0000 @@ -22,8 +22,8 @@ "Ex/SystemFOmega", "Ex/TypeSchemes", "Ex/TypeVarsTest", - (*"Ex/Foo1", - "Ex/Foo2",*) + "Ex/Foo1", + "Ex/Foo2", "Ex/CoreHaskell", "Ex/CoreHaskell2" ]; diff -r 478c5648e73f -r d1bdc281be2b Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Thu Dec 23 00:22:41 2010 +0000 +++ b/Nominal/nominal_dt_quot.ML Thu Dec 23 00:46:06 2010 +0000 @@ -3,7 +3,7 @@ Author: Cezary Kaliszyk Performing quotient constructions, lifting theorems and - deriving support propoerties for the quotient types. + deriving support properties for the quotient types. *) signature NOMINAL_DT_QUOT = @@ -38,6 +38,10 @@ val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> Proof.context -> thm list + + val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> + thm list -> thm list -> thm list -> thm list -> thm list + end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = @@ -373,5 +377,236 @@ |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) end + +(** proves strong exhauts theorems **) + + +(* fixme: move into nominal_library *) +fun abs_const bmode ty = + let + val (const_name, binder_ty, abs_ty) = + case bmode of + Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst}) + | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set}) + | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res}) + in + Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty])) + end + +fun mk_abs bmode trm1 trm2 = + abs_const bmode (fastype_of trm2) $ trm1 $ trm2 + +fun is_abs_eq thm = + let + fun is_abs trm = + case (head_of trm) of + Const (@{const_name "Abs_set"}, _) => true + | Const (@{const_name "Abs_lst"}, _) => true + | Const (@{const_name "Abs_res"}, _) => true + | _ => false + in + thm |> prop_of + |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq + |> fst + |> is_abs + end + + +(* adds a freshness condition to the assumptions *) +fun mk_ecase_prems lthy c (params, prems, concl) bclauses = + let + val tys = map snd params + val binders = get_all_binders bclauses + + fun prep_binder (opt, i) = + let + val t = Bound (length tys - i - 1) + in + case opt of + NONE => setify_ty lthy (nth tys i) t + | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) + end + + val prems' = + case binders of + [] => prems (* case: no binders *) + | _ => binders (* case: binders *) + |> map prep_binder + |> fold_union_env tys + |> (fn t => mk_fresh_star t c) + |> (fn t => HOLogic.mk_Trueprop t :: prems) + in + mk_full_horn params prems' concl + end + + +(* derives the freshness theorem that there exists a p, such that + (p o as) #* (c, t1,..., tn) *) +fun fresh_thm ctxt c parms binders bn_finite_thms = + let + fun prep_binder (opt, i) = + case opt of + NONE => setify ctxt (nth parms i) + | SOME bn => to_set (bn $ (nth parms i)) + + fun prep_binder2 (opt, i) = + case opt of + NONE => atomify ctxt (nth parms i) + | SOME bn => bn $ (nth parms i) + + val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders)) + val lhs = binders + |> map prep_binder + |> fold_union + |> mk_perm (Bound 0) + + val goal = mk_fresh_star lhs rhs + |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t)) + |> HOLogic.mk_Trueprop + + val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} + @ @{thms finite.intros finite_Un finite_set finite_fset} + in + Goal.prove ctxt [] [] goal + (K (HEADGOAL (rtac @{thm at_set_avoiding1} + THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) + end + + +(* derives an abs_eq theorem of the form + + Exists q. [as].x = [p o as].(q o x) for non-recursive binders + Exists q. [as].x = [q o as].(q o x) for recursive binders +*) +fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns + (bclause as (BC (bmode, binders, bodies))) = + case binders of + [] => [] + | _ => + let + val rec_flag = is_recursive_binder bclause + val binder_trm = comb_binders ctxt bmode parms binders + val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) + + val abs_lhs = mk_abs bmode binder_trm body_trm + val abs_rhs = + if rec_flag + then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm) + else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm) + + val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) + val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) + + val goal = HOLogic.mk_conj (abs_eq, peq) + |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) + |> HOLogic.mk_Trueprop + + val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} + @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset + fresh_star_set} @ @{thms finite.intros finite_fset} + + val tac1 = + if rec_flag + then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} + else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} + + val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] + in + [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) + |> (if rec_flag + then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] + else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ] + end + + +val setify = @{lemma "xs = ys ==> set xs = set ys" by simp} + +fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas + prems bclausess qexhaust_thm = + let + fun aux_tac prem bclauses = + case (get_all_binders bclauses) of + [] => EVERY' [rtac prem, atac] + | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => + let + val parms = map (term_of o snd) params + val fthm = fresh_thm ctxt c parms binders bn_finite_thms + + val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} + val (([(_, fperm)], fprops), ctxt') = Obtain.result + (K (EVERY1 [etac exE, + full_simp_tac (HOL_basic_ss addsimps ss), + REPEAT o (etac @{thm conjE})])) [fthm] ctxt + + val abs_eq_thms = flat + (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses) + + val ((_, eqs), ctxt'') = Obtain.result + (K (EVERY1 + [ REPEAT o (etac @{thm exE}), + REPEAT o (etac @{thm conjE}), + REPEAT o (dtac setify), + full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' + + val (abs_eqs, peqs) = split_filter is_abs_eq eqs + + val fprops' = + map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops + @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops + + (* for freshness conditions *) + val tac1 = SOLVED' (EVERY' + [ simp_tac (HOL_basic_ss addsimps peqs), + rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), + conj_tac (DETERM o resolve_tac fprops') ]) + + (* for equalities between constructors *) + val tac2 = SOLVED' (EVERY' + [ rtac (@{thm ssubst} OF prems), + rewrite_goal_tac (map safe_mk_equiv eq_iff_thms), + rewrite_goal_tac (map safe_mk_equiv abs_eqs), + conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) + + (* proves goal "P" *) + val side_thm = Goal.prove ctxt'' [] [] (term_of concl) + (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ])) + |> singleton (ProofContext.export ctxt'' ctxt) + in + rtac side_thm 1 + end) ctxt + in + EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)] + end + + +fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns + perm_bn_alphas = + let + val ((_, exhausts'), lthy') = Variable.import true exhausts lthy + + val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' + val c = Free (c, TFree (a, @{sort fs})) + + val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *) + |> map prop_of + |> map Logic.strip_horn + |> split_list + + val ecases' = (map o map) strip_full_horn ecases + + val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss + + fun tac bclausess exhaust {prems, context} = + case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas + prems bclausess exhaust + + fun prove prems bclausess exhaust concl = + Goal.prove lthy'' [] prems concl (tac bclausess exhaust) + in + map4 prove premss bclausesss exhausts' main_concls + |> ProofContext.export lthy'' lthy + end + end (* structure *)