# HG changeset patch # User Christian Urban # Date 1291811845 0 # Node ID ca6b4bc7a871dbaa3692a0a4a3bc66a3ad6b984b # Parent d6fe94028a5dd93270ffa380c1cdfc6003fbaa13 kept the nested structure of constructors (belonging to one datatype) diff -r d6fe94028a5d -r ca6b4bc7a871 Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Tue Dec 07 19:16:09 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Wed Dec 08 12:37:25 2010 +0000 @@ -30,6 +30,7 @@ thm foo.perm_bn_simps thm foo.bn_finite + thm foo.distinct thm foo.induct thm foo.inducts @@ -45,12 +46,9 @@ thm foo.supp thm foo.fresh -text {* - tests by cu -*} -text {* *} + (* @@ -71,6 +69,25 @@ sorry *) +thm foo.exhaust + +ML {* +fun strip_prems_concl trm = + (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) +*} + + +ML {* + @{thms foo.exhaust} + |> map prop_of + |> map strip_prems_concl + |> map fst + |> map (map (Syntax.string_of_term @{context})) + |> map cat_lines + |> cat_lines + |> writeln +*} + lemma test6: fixes c::"'a::fs" assumes "\name. y = Var name \ P" diff -r d6fe94028a5d -r ca6b4bc7a871 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue Dec 07 19:16:09 2010 +0000 +++ b/Nominal/Nominal2.thy Wed Dec 08 12:37:25 2010 +0000 @@ -200,7 +200,7 @@ *} ML {* -fun define_raw_dts dts bn_funs bn_eqs binds lthy = +fun define_raw_dts dts bn_funs bn_eqs bclauses lthy = let val thy = Local_Theory.exit_global lthy val thy_name = Context.theory_name thy @@ -225,7 +225,7 @@ val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs - val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds + val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses val (raw_dt_full_names, thy1) = Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy @@ -258,6 +258,8 @@ then define_raw_dts dts bn_funs bn_eqs bclauses lthy else raise TEST lthy + val _ = tracing ("raw_bclauses\n" ^ cat_lines (map @{make_string} raw_bclauses)) + val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo @@ -270,7 +272,7 @@ val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names val raw_cns_info = all_dtyp_constrs_types descr sorts - val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) raw_cns_info) + val raw_constrs = map (map (fn (c, _, _, _) => c)) raw_cns_info val raw_inject_thms = flat (map #inject dtinfos) val raw_distinct_thms = flat (map #distinct dtinfos) @@ -286,7 +288,7 @@ val _ = warning "Definition of raw permutations"; val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = if get_STEPS lthy0 > 0 - then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0 + then define_raw_perms raw_full_ty_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0 else raise TEST lthy0 (* noting the raw permutations as eqvt theorems *) @@ -419,7 +421,7 @@ val raw_constrs_rsp = if get_STEPS lthy > 18 - then raw_constrs_rsp raw_constrs alpha_trms alpha_intros + then raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 else raise TEST lthy6 @@ -462,9 +464,8 @@ (* defining of quotient term-constructors, binding functions, free vars functions *) val _ = warning "Defining the quotient constants" - val qconstrs_descr = - flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) - |> map2 (fn t => fn (b, mx) => (b, t, mx)) raw_constrs + val qconstrs_descrs = + map2 (map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx))) (get_cnstrs dts) raw_constrs val qbns_descr = map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns @@ -487,12 +488,12 @@ val qperm_bn_descr = map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns - - val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8)= + val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), + lthy8) = if get_STEPS lthy > 24 then lthy7 - |> define_qconsts qtys qconstrs_descr + |> fold_map (define_qconsts qtys) qconstrs_descrs ||>> define_qconsts qtys qbns_descr ||>> define_qconsts qtys qfvs_descr ||>> define_qconsts qtys qfv_bns_descr @@ -511,7 +512,7 @@ then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 else raise TEST lthy9 - val qtrms = map #qconst qconstrs_info + val qtrms = map (map #qconst) qconstrs_infos val qbns = map #qconst qbns_info val qfvs = map #qconst qfvs_info val qfv_bns = map #qconst qfv_bns_info @@ -554,7 +555,7 @@ val _ = warning "Proving Supports Lemmas and fs-Instances" val qsupports_thms = if get_STEPS lthy > 29 - then prove_supports lthyB qperm_simps qtrms + then prove_supports lthyB qperm_simps (flat qtrms) else raise TEST lthyB (* finite supp lemmas *) @@ -573,7 +574,7 @@ val _ = warning "Proving Equality between fv and supp" val qfv_supp_thms = if get_STEPS lthy > 32 - then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs + then prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC else []