# HG changeset patch # User Christian Urban # Date 1261431391 -3600 # Node ID e9e205b904e243779516c3ead5fbbf4694e878b9 # Parent 37285ec4387d463cd0c0c9068cfdca6fa6889747 get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO diff -r 37285ec4387d -r e9e205b904e2 FIXME-TODO --- a/FIXME-TODO Sun Dec 20 00:53:35 2009 +0100 +++ b/FIXME-TODO Mon Dec 21 22:36:31 2009 +0100 @@ -8,11 +8,9 @@ finite sets (syntax should be \ \, look at Set.thy how syntax is been introduced) -- think about what happens if things go wrong (like - theorem cannot be lifted) / proper diagnostic - messages for the user - -- Handle theorems that include Ball/Bex +- Handle theorems that include Ball/Bex. Would it help + if we introduced separate Bex and Ball constants for + quotienting? - user should be able to give quotient_respects and preserves theorems in a more natural form. @@ -22,12 +20,15 @@ Lower Priority ============== +- Maybe a quotient_definition should already require + a proof of the respectfulness (in this way one + already excludes non-sensical definitions) + - accept partial equvalence relations -- what happens if the original theorem contains bounded - quantifiers? can such theorems be lifted? If not, would - it help if we introduced separate Bex and Ball constants - for quotienting? +- think about what happens if things go wrong (like + theorem cannot be lifted) / proper diagnostic + messages for the user - inductions from the datatype package have a strange order of quantifiers in assumptions. @@ -55,4 +56,18 @@ [QuotList, QuotOption, QuotPair...] could be automatically proven? -- Examples: Finite multiset. \ No newline at end of file +- Examples: Finite multiset. + +- The current syntax of the quotient_definition is + + "qconst :: qty" + as "rconst" + + Is it possible to have the more Isabelle-like + syntax + + qconst :: "qty" + as "rconst" + + That means "qconst :: qty" is not read as a term, but + as two entities. \ No newline at end of file diff -r 37285ec4387d -r e9e205b904e2 Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Sun Dec 20 00:53:35 2009 +0100 +++ b/Quot/Examples/FSet.thy Mon Dec 21 22:36:31 2009 +0100 @@ -1,5 +1,5 @@ theory FSet -imports "../QuotMain" List +imports "../QuotMain" "../QuotList" List begin inductive @@ -26,6 +26,61 @@ fset = "'a list" / "list_eq" by (rule equivp_list_eq) + +fun + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" +where + "intrel (x, y) (u, v) = (x + v = u + y)" + +quotient_type int = "nat \ nat" / intrel + apply(unfold equivp_def) + apply(auto simp add: mem_def expand_fun_eq) + done + + +ML {* +open Quotient_Def; +*} + +ML {* +get_fun absF @{context} (@{typ "'a list"}, + @{typ "'a fset"}) +|> Syntax.check_term @{context} +|> Syntax.string_of_term @{context} +|> writeln +*} + +term "map id" +term "abs_fset o (map id)" + +ML {* +get_fun absF @{context} (@{typ "(nat * nat) list"}, + @{typ "int fset"}) +|> Syntax.check_term @{context} +|> Syntax.string_of_term @{context} +|> writeln +*} + +term "map abs_int" +term "abs_fset o map abs_int" + + +ML {* +get_fun absF @{context} (@{typ "('a list) list"}, + @{typ "('a fset) fset"}) +|> Syntax.check_term @{context} +|> Syntax.string_of_term @{context} +|> writeln +*} + +ML {* +get_fun absF @{context} (@{typ "('a list) list \ 'a"}, + @{typ "('a fset) fset \ 'a"}) +|> Syntax.check_term @{context} +|> Syntax.string_of_term @{context} +|> writeln +*} + quotient_definition "EMPTY :: 'a fset" as @@ -52,11 +107,19 @@ as "card1" -(* text {* +quotient_definition + "fconcat :: ('a fset) fset \ 'a fset" +as + "concat" + +term concat +term fconcat + +text {* Maybe make_const_def should require a theorem that says that the particular lifted function respects the relation. With it such a definition would be impossible: - make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd -*}*) + make_const_def CARD @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} lemma card1_0: fixes a :: "'a list" @@ -213,7 +276,8 @@ done lemma "IN x (INSERT y xa) = (x = y \ IN x xa)" -by (lifting member.simps(2)) +apply (lifting member.simps(2)) +done lemma "INSERT a (INSERT a x) = INSERT a x" apply (lifting list_eq.intros(4)) diff -r 37285ec4387d -r e9e205b904e2 Quot/Examples/FSet2.thy --- a/Quot/Examples/FSet2.thy Sun Dec 20 00:53:35 2009 +0100 +++ b/Quot/Examples/FSet2.thy Mon Dec 21 22:36:31 2009 +0100 @@ -1,5 +1,5 @@ theory FSet2 -imports "../QuotMain" List +imports "../QuotMain" "../QuotList" List begin inductive diff -r 37285ec4387d -r e9e205b904e2 Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Sun Dec 20 00:53:35 2009 +0100 +++ b/Quot/Examples/FSet3.thy Mon Dec 21 22:36:31 2009 +0100 @@ -1,37 +1,342 @@ theory FSet3 -imports "../QuotMain" List +imports "../QuotMain" "../QuotList" List begin fun list_eq :: "'a list \ 'a list \ bool" (infix "\" 50) where - "list_eq xs ys = (\e. (e \ set xs) = (e \ set ys))" + "list_eq xs ys = (\x. x \ set xs \ x \ set ys)" lemma list_eq_equivp: shows "equivp list_eq" unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def by auto -quotient_type fset = "'a list" / "list_eq" - by (rule list_eq_equivp) +quotient_type + fset = "'a list" / "list_eq" +by (rule list_eq_equivp) + + +section {* empty fset, finsert and membership *} + +quotient_definition + "fempty :: 'a fset" ("{||}") +as "[]::'a list" + +quotient_definition + "finsert :: 'a \ 'a fset \ 'a fset" +as "op #" + +syntax + "@Finset" :: "args => 'a fset" ("{|(_)|}") -lemma not_nil_equiv_cons: - "\[] \ a # A" -by auto +translations + "{|x, xs|}" == "CONST finsert x {|xs|}" + "{|x|}" == "CONST finsert x {||}" + +definition + memb :: "'a \ 'a list \ bool" +where + "memb x xs \ x \ set xs" + +quotient_definition + "fin :: 'a \ 'a fset \ bool" ("_ |\| _" [50, 51] 50) +as "memb" + +abbreviation + fnotin :: "'a \ 'a fset \ bool" ("_ |\| _" [50, 51] 50) +where + "a |\| S \ \(a |\| S)" + +lemma memb_rsp[quot_respect]: + shows "(op = ===> op \ ===> op =) memb memb" +by (auto simp add: memb_def) lemma nil_rsp[quot_respect]: shows "[] \ []" - by simp +by simp lemma cons_rsp[quot_respect]: shows "(op = ===> op \ ===> op \) op # op #" - by simp +by simp + + +section {* Augmenting a set -- @{const finsert} *} + +text {* raw section *} + +lemma nil_not_cons: + shows "\[] \ x # xs" +by auto + +lemma memb_cons_iff: + shows "memb x (y # xs) = (x = y \ memb x xs)" +by (induct xs) (auto simp add: memb_def) + +lemma memb_consI1: + shows "memb x (x # xs)" +by (simp add: memb_def) + +lemma memb_consI2: + shows "memb x xs \ memb x (y # xs)" + by (simp add: memb_def) + +lemma memb_absorb: + shows "memb x xs \ (x # xs) \ xs" +by (induct xs) (auto simp add: memb_def) + +text {* lifted section *} + +lemma fempty_not_finsert[simp]: + shows "{||} \ finsert x S" +by (lifting nil_not_cons) + +lemma fin_finsert_iff[simp]: + "x |\| finsert y S = (x = y \ x |\| S)" +by (lifting memb_cons_iff) + +lemma + shows finsertI1: "x |\| finsert x S" + and finsertI2: "x |\| S \ x |\| finsert y S" + by (lifting memb_consI1, lifting memb_consI2) + +lemma finsert_absorb [simp]: + shows "x |\| S \ finsert x S = S" +by (lifting memb_absorb) + + +section {* Singletons *} + +text {* raw section *} + +lemma singleton_list_eq: + shows "[x] \ [y] \ x = y" +by auto + +text {* lifted section *} + +lemma fsingleton_eq[simp]: + shows "{|x|} = {|y|} \ x = y" +by (lifting singleton_list_eq) + + +section {* Cardinality of finite sets *} + +fun + fcard_raw :: "'a list \ nat" +where + fcard_raw_nil: "fcard_raw [] = 0" +| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))" + +quotient_definition + "fcard :: 'a fset \ nat" +as "fcard_raw" + +text {* raw section *} + +lemma fcard_raw_ge_0: + assumes a: "x \ set xs" + shows "0 < fcard_raw xs" +using a +by (induct xs) (auto simp add: memb_def) + +lemma fcard_raw_delete_one: + "fcard_raw ([x \ xs. x \ y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" +by (induct xs) (auto dest: fcard_raw_ge_0 simp add: memb_def) + +lemma fcard_raw_rsp_aux: + assumes a: "a \ b" + shows "fcard_raw a = fcard_raw b" +using a +apply(induct a arbitrary: b) +apply(auto simp add: memb_def) +apply(metis) +apply(drule_tac x="[x \ b. x \ a1]" in meta_spec) +apply(simp add: fcard_raw_delete_one) +apply(metis Suc_pred' fcard_raw_ge_0 fcard_raw_delete_one memb_def) +done + +lemma fcard_raw_rsp[quot_respect]: + "(op \ ===> op =) fcard_raw fcard_raw" + by (simp add: fcard_raw_rsp_aux) + +text {* lifted section *} + +lemma fcard_fempty [simp]: + shows "fcard {||} = 0" +by (lifting fcard_raw_nil) + +lemma fcard_finsert_if [simp]: + shows "fcard (finsert x S) = (if x |\| S then fcard S else Suc (fcard S))" +by (lifting fcard_raw_cons) + + +section {* Induction and Cases rules for finite sets *} + +lemma fset_exhaust[case_names fempty finsert, cases type: fset]: + shows "\S = {||} \ P; \x S'. S = finsert x S' \ P\ \ P" +by (lifting list.exhaust) + +lemma fset_induct[case_names fempty finsert]: + shows "\P {||}; \x S. P S \ P (finsert x S)\ \ P S" +by (lifting list.induct) -(* -lemma mem_rsp[quot_respect]: - "(op = ===> op \ ===> op =) (op mem) (op mem)" +lemma fset_induct2[case_names fempty finsert, induct type: fset]: + assumes prem1: "P {||}" + and prem2: "\x S. \x |\| S; P S\ \ P (finsert x S)" + shows "P S" +proof(induct S rule: fset_induct) + case fempty + show "P {||}" by (rule prem1) +next + case (finsert x S) + have asm: "P S" by fact + show "P (finsert x S)" + proof(cases "x |\| S") + case True + have "x |\| S" by fact + then show "P (finsert x S)" using asm by simp + next + case False + have "x |\| S" by fact + then show "P (finsert x S)" using prem2 asm by simp + qed +qed + + +section {* fmap and fset comprehension *} + +quotient_definition + "fmap :: ('a \ 'b) \ 'a fset \ 'b fset" +as + "map" + +(* PROPBLEM +quotient_definition + "fconcat :: ('a fset) fset => 'a fset" +as + "concat" + +term concat +term fconcat *) +consts + fconcat :: "('a fset) fset => 'a fset" + +text {* raw section *} + +lemma map_rsp_aux: + assumes a: "a \ b" + shows "map f a \ map f b" + using a +apply(induct a arbitrary: b) +apply(auto) +apply(metis rev_image_eqI) +done + +lemma map_rsp[quot_respect]: + shows "(op = ===> op \ ===> op \) map map" +by (auto simp add: map_rsp_aux) + + +text {* lifted section *} + +(* TBD *) + +text {* syntax for fset comprehensions (adapted from lists) *} + +nonterminals fsc_qual fsc_quals + +syntax +"_fsetcompr" :: "'a \ fsc_qual \ fsc_quals \ 'a fset" ("{|_ . __") +"_fsc_gen" :: "'a \ 'a fset \ fsc_qual" ("_ <- _") +"_fsc_test" :: "bool \ fsc_qual" ("_") +"_fsc_end" :: "fsc_quals" ("|}") +"_fsc_quals" :: "fsc_qual \ fsc_quals \ fsc_quals" (", __") +"_fsc_abs" :: "'a => 'b fset => 'b fset" + +syntax (xsymbols) +"_fsc_gen" :: "'a \ 'a fset \ fsc_qual" ("_ \ _") +syntax (HTML output) +"_fsc_gen" :: "'a \ 'a fset \ fsc_qual" ("_ \ _") + +parse_translation (advanced) {* +let + val femptyC = Syntax.const @{const_name fempty}; + val finsertC = Syntax.const @{const_name finsert}; + val fmapC = Syntax.const @{const_name fmap}; + val fconcatC = Syntax.const @{const_name fconcat}; + val IfC = Syntax.const @{const_name If}; + fun fsingl x = finsertC $ x $ femptyC; + + fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *) + let + val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT); + val e = if opti then fsingl e else e; + val case1 = Syntax.const "_case1" $ p $ e; + val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN + $ femptyC; + val cs = Syntax.const "_case2" $ case1 $ case2 + val ft = Datatype_Case.case_tr false Datatype.info_of_constr + ctxt [x, cs] + in lambda x ft end; + + fun abs_tr ctxt (p as Free(s,T)) e opti = + let val thy = ProofContext.theory_of ctxt; + val s' = Sign.intern_const thy s + in if Sign.declared_const thy s' + then (pat_tr ctxt p e opti, false) + else (lambda p e, true) + end + | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false); + + fun fsc_tr ctxt [e, Const("_fsc_test",_) $ b, qs] = + let + val res = case qs of + Const("_fsc_end",_) => fsingl e + | Const("_fsc_quals",_)$ q $ qs => fsc_tr ctxt [e, q, qs]; + in + IfC $ b $ res $ femptyC + end + + | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_end",_)] = + (case abs_tr ctxt p e true of + (f,true) => fmapC $ f $ es + | (f, false) => fconcatC $ (fmapC $ f $ es)) + + | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_quals",_) $ q $ qs] = + let + val e' = fsc_tr ctxt [e, q, qs]; + in + fconcatC $ (fmapC $ (fst (abs_tr ctxt p e' false)) $ es) + end + +in [("_fsetcompr", fsc_tr)] end +*} + +(* examles *) +term "{|(x,y,z). b|}" +term "{|x. x \ xs|}" +term "{|(x,y,z). x\xs|}" +term "{|e x y. x\xs, y\ys|}" +term "{|(x,y,z). xb|}" +term "{|(x,y,z). x\xs, x>b|}" +term "{|(x,y,z). xxs|}" +term "{|(x,y). Cons True x \ xs|}" +term "{|(x,y,z). Cons x [] \ xs|}" +term "{|(x,y,z). xb, x=d|}" +term "{|(x,y,z). xb, y\ys|}" +term "{|(x,y,z). xxs,y>b|}" +term "{|(x,y,z). xxs, y\ys|}" +term "{|(x,y,z). x\xs, x>b, yxs, x>b, y\ys|}" +term "{|(x,y,z). x\xs, y\ys,y>x|}" +term "{|(x,y,z). x\xs, y\ys,z\zs|}" + + +(* BELOW CONSTRUCTION SITE *) + lemma no_mem_nil: "(\a. a \ set A) = (A = [])" @@ -108,49 +413,9 @@ "X = [] \ (\a. a mem X \ X \ a # delete_raw X a)" by (induct X) (auto) -fun - card_raw :: "'a list \ nat" -where - card_raw_nil: "card_raw [] = 0" -| card_raw_cons: "card_raw (x # xs) = (if x \ set xs then card_raw xs else Suc (card_raw xs))" -lemma not_mem_card_raw: - fixes x :: "'a" - fixes xs :: "'a list" - shows "(\(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))" - sorry - -lemma card_raw_suc: - assumes c: "card_raw xs = Suc n" - shows "\a ys. (a \ set ys) \ xs \ (a # ys)" - using c apply(induct xs) - apply(simp) - sorry -lemma mem_card_raw_gt_0: - "a \ set A \ 0 < card_raw A" - by (induct A) (auto) -lemma card_raw_cons_gt_0: - "0 < card_raw (a # A)" - by (induct A) (auto) - -lemma card_raw_delete_raw: - "card_raw (delete_raw A a) = (if a \ set A then card_raw A - 1 else card_raw A)" -sorry - -lemma card_raw_rsp_aux: - assumes e: "a \ b" - shows "card_raw a = card_raw b" - using e sorry - -lemma card_raw_rsp[quot_respect]: - "(op \ ===> op =) card_raw card_raw" - by (simp add: card_raw_rsp_aux) - -lemma card_raw_0: - "(card_raw A = 0) = (A = [])" - by (induct A) (auto) lemma list2set_thm: shows "set [] = {}" @@ -209,26 +474,6 @@ section {* Constants on the Quotient Type *} -quotient_definition - "fempty :: 'a fset" - as "[]::'a list" - -quotient_definition - "finsert :: 'a \ 'a fset \ 'a fset" - as "op #" - -quotient_definition - "fin :: 'a \ 'a fset \ bool" ("_ \f _" [50, 51] 50) - as "\x X. x \ set X" - -abbreviation - fnotin :: "'a \ 'a fset \ bool" ("_ \f _" [50, 51] 50) -where - "a \f S \ \(a \f S)" - -quotient_definition - "fcard :: 'a fset \ nat" - as "card_raw" quotient_definition "fdelete :: 'a fset \ 'a \ 'a fset" @@ -271,20 +516,21 @@ thm mem_cons thm finite_set_raw_strong_cases -thm card_raw.simps -thm not_mem_card_raw -thm card_raw_suc +(*thm card_raw.simps*) +(*thm not_mem_card_raw*) +(*thm card_raw_suc*) lemma "fcard X = Suc n \ (\a S. a \f S & X = finsert a S)" (*by (lifting card_raw_suc)*) sorry -thm card_raw_cons_gt_0 +(*thm card_raw_cons_gt_0 thm mem_card_raw_gt_0 thm not_nil_equiv_cons +*) thm delete_raw.simps (*thm mem_delete_raw*) -thm card_raw_delete_raw +(*thm card_raw_delete_raw*) thm cons_delete_raw thm mem_cons_delete_raw thm finite_set_raw_delete_raw_cases diff -r 37285ec4387d -r e9e205b904e2 Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Sun Dec 20 00:53:35 2009 +0100 +++ b/Quot/Examples/IntEx.thy Mon Dec 21 22:36:31 2009 +0100 @@ -249,7 +249,10 @@ apply(lifting lam_tst3a) apply(rule impI) apply(rule lam_tst3a_reg) -done +apply(injection) +sorry +(* PROBLEM +done*) lemma lam_tst3b: "(\(y :: nat \ nat \ nat \ nat). y) = (\(x :: nat \ nat \ nat \ nat). x)" by auto @@ -259,7 +262,10 @@ apply(rule impI) apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) apply(simp add: id_rsp) -done +apply(injection) +sorry +(* PROBLEM +done*) term map diff -r 37285ec4387d -r e9e205b904e2 Quot/QuotList.thy --- a/Quot/QuotList.thy Sun Dec 20 00:53:35 2009 +0100 +++ b/Quot/QuotList.thy Mon Dec 21 22:36:31 2009 +0100 @@ -59,7 +59,7 @@ apply(rule list_rel_rel[OF q]) done -lemma map_id: "map id \ id" +lemma map_id[id_simps]: "map id \ id" apply (rule eq_reflection) apply (rule ext) apply (rule_tac list="x" in list.induct) diff -r 37285ec4387d -r e9e205b904e2 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Sun Dec 20 00:53:35 2009 +0100 +++ b/Quot/QuotMain.thy Mon Dec 21 22:36:31 2009 +0100 @@ -166,6 +166,9 @@ fun_map_id[THEN eq_reflection] id_apply[THEN eq_reflection] id_def[THEN eq_reflection, symmetric] + id_o[THEN eq_reflection] + o_id[THEN eq_reflection] + section {* Methods / Interface *} diff -r 37285ec4387d -r e9e205b904e2 Quot/quotient_def.ML --- a/Quot/quotient_def.ML Sun Dec 20 00:53:35 2009 +0100 +++ b/Quot/quotient_def.ML Mon Dec 21 22:36:31 2009 +0100 @@ -32,6 +32,11 @@ fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) +fun mk_compose flag (trm1, trm2) = + case flag of + absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 + | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 + fun get_fun_aux lthy s fs = let val thy = ProofContext.theory_of lthy @@ -42,7 +47,7 @@ end fun get_const flag lthy _ qty = -(* FIXME: check here that _ and qty are related *) +(* FIXME: check here that the type-constructors of _ and qty are related *) let val thy = ProofContext.theory_of lthy val qty_name = Long_Name.base_name (fst (dest_Type qty)) @@ -68,14 +73,18 @@ in get_fun_aux lthy "fun" [fs_ty1, fs_ty2] end - | (Type (s, []), Type (s', [])) => + | (Type (s, _), Type (s', [])) => if s = s' then mk_identity qty else get_const flag lthy rty qty | (Type (s, tys), Type (s', tys')) => - if s = s' - then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) - else get_const flag lthy rty qty + let + val args = map (get_fun flag lthy) (tys ~~ tys') + in + if s = s' + then get_fun_aux lthy s args + else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args) + end | (TFree x, TFree x') => if x = x' then mk_identity qty diff -r 37285ec4387d -r e9e205b904e2 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Sun Dec 20 00:53:35 2009 +0100 +++ b/Quot/quotient_tacs.ML Mon Dec 21 22:36:31 2009 +0100 @@ -389,7 +389,8 @@ let val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) in - inj_repabs_step_tac ctxt rel_refl + simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) + THEN' inj_repabs_step_tac ctxt rel_refl end fun all_inj_repabs_tac ctxt = @@ -491,7 +492,7 @@ (* *) (* 5. Test for refl *) -fun clean_tac lthy = +fun clean_tac_aux lthy = let val thy = ProofContext.theory_of lthy; val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) @@ -508,7 +509,7 @@ TRY o rtac refl] end - +fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) (* Tactic for Genralisation of Free Variables in a Goal *)