# HG changeset patch # User Cezary Kaliszyk # Date 1272531548 -7200 # Node ID 9f9c4965b608e70a80167042e398383033b5dc83 # Parent 8feedc0d4ea837d015c45669ecfd18706a1af081 Include support of unknown datatypes in new fv diff -r 8feedc0d4ea8 -r 9f9c4965b608 Nominal/NewFv.thy --- a/Nominal/NewFv.thy Thu Apr 29 10:11:48 2010 +0200 +++ b/Nominal/NewFv.thy Thu Apr 29 10:59:08 2010 +0200 @@ -1,6 +1,6 @@ theory NewFv -imports "../Nominal-General/Nominal2_Atoms" - "Abs" "Perm" "Rsp" "Nominal2_FSet" +imports "../Nominal-General/Nominal2_Atoms" + "Abs" "Perm" "Nominal2_FSet" begin ML {* @@ -75,6 +75,11 @@ *} ML {* +fun mk_supp t = + Const (@{const_name supp}, fastype_of t --> @{typ "atom set"}) $ t +*} + +ML {* fun setify x = if fastype_of x = @{typ "atom list"} then @{term "set::atom list \ atom set"} $ x @@ -89,9 +94,9 @@ val x = nth args i; val dt = nth dts i; in - if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) $ x - else atoms thy x + if Datatype_Aux.is_rec_type dt + then nth fv_frees (Datatype_Aux.body_index dt) $ x + else mk_supp x end val fv_bodys = mk_union (map fv_body bodys) val bound_vars = @@ -119,9 +124,9 @@ val dt = nth dts i; in case AList.lookup (op=) args_in_bn i of - NONE => if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) $ x - else atoms thy x + NONE => if Datatype_Aux.is_rec_type dt + then nth fv_frees (Datatype_Aux.body_index dt) $ x + else mk_supp x | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x | SOME NONE => noatoms end @@ -131,9 +136,9 @@ *} ML {* -fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) = +fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bclausess (fvbn, (_, ith_dtyp, args_in_bns)) = let - fun fv_bn_constr (cname, dts) (args_in_bn, bml) = + fun fv_bn_constr (cname, dts) (args_in_bn, bclauses) = let val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; val names = Datatype_Prop.make_tnames Ts; @@ -142,16 +147,16 @@ val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn in HOLogic.mk_Trueprop (HOLogic.mk_eq - (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml))) + (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bclauses))) end; val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; in - map2 fv_bn_constr constrs (args_in_bns ~~ bmll) + map2 fv_bn_constr constrs (args_in_bns ~~ bclausess) end *} ML {* -fun fv_bns thy dt_descr sorts fv_frees bn_funs bclauses = +fun fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss = let fun mk_fvbn_free (bn, ith, _) = let @@ -161,8 +166,8 @@ end; val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs); val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees - val bmlls = map (fn (_, i, _) => nth bclauses i) bn_funs; - val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs); + val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs; + val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs); in (bn_fvbn, fvbn_names, eqs) end @@ -176,9 +181,9 @@ val x = nth args i; val dt = nth dts i; in - if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) $ x - else atoms thy x + if Datatype_Aux.is_rec_type dt + then nth fv_frees (Datatype_Aux.body_index dt) $ x + else mk_supp x end | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y @@ -186,9 +191,9 @@ *} ML {* -fun fv thy dt_descr sorts fv_frees bn_fvbn bmll (fv_free, ith_dtyp) = +fun fv thy dt_descr sorts fv_frees bn_fvbn bclausess (fv_free, ith_dtyp) = let - fun fv_constr (cname, dts) bml = + fun fv_constr (cname, dts) bclauses = let val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; val names = Datatype_Prop.make_tnames Ts; @@ -197,23 +202,15 @@ val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn in HOLogic.mk_Trueprop (HOLogic.mk_eq - (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml))) + (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bclauses))) end; val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; in - map2 fv_constr constrs bmll + map2 fv_constr constrs bclausess end *} ML {* -val by_pat_completeness_auto = - Proof.global_terminal_proof - (Method.Basic Pat_Completeness.pat_completeness, - SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) - -fun termination_by method = - Function.termination_proof NONE - #> Proof.global_terminal_proof (Method.Basic method, NONE) *} ML {* @@ -226,25 +223,31 @@ val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr; val fv_frees = map Free (fv_names ~~ fv_types); - val (bn_fvbn, fv_bn_names, fv_bn_eqs) = + val (bn_fvbn, fv_bn_names, fv_bn_eqs) = fv_bns thy dt_descr sorts fv_frees bn_funs bclauses; val fvbns = map snd bn_fvbn; val fv_nums = 0 upto (length fv_frees - 1) val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums); - + val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) - val lthy' = - lthy - |> Function.add_function all_fv_names all_fv_eqs Function_Common.default_config - |> by_pat_completeness_auto - |> Local_Theory.restore - |> termination_by (Lexicographic_Order.lexicographic_order) + fun pat_completeness_auto ctxt = + Pat_Completeness.pat_completeness_tac ctxt 1 + THEN auto_tac (clasimpset_of ctxt) + + fun prove_termination lthy = + Function.prove_termination NONE + (Lexicographic_Order.lexicographic_order_tac true lthy) lthy + + val (info, lthy') = Function.add_function all_fv_names all_fv_eqs + Function_Common.default_config pat_completeness_auto lthy + + val lthy'' = prove_termination (Local_Theory.restore lthy') in - (fv_frees @ fvbns, lthy') + ((fv_frees, fvbns), info, lthy'') end *} diff -r 8feedc0d4ea8 -r 9f9c4965b608 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Thu Apr 29 10:11:48 2010 +0200 +++ b/Nominal/NewParser.thy Thu Apr 29 10:59:08 2010 +0200 @@ -277,7 +277,7 @@ val thy = Local_Theory.exit_global lthy2; val lthy3 = Theory_Target.init NONE thy; - val (_, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; + val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; in ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) end @@ -460,11 +460,12 @@ P1 name | P2 pt pt binder - bn::"pt \ atom set" + bn::"pt \ atom set" where "bn (P1 x) = {atom x}" | "bn (P2 p1 p2) = bn p1 \ bn p2" +thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps nominal_datatype exp = EVar name