# HG changeset patch # User Cezary Kaliszyk # Date 1266571598 -3600 # Node ID 2f4ce88c2c96830a4d22a8eb1b4751b44fe96bf6 # Parent 4efbaba9d7544c7de3f3a15df37910b57e253a03# Parent 6f3b751356382948739fb56cb700b6233095ddd5 merge diff -r 4efbaba9d754 -r 2f4ce88c2c96 Quot/Nominal/Abs.thy --- a/Quot/Nominal/Abs.thy Fri Feb 19 10:17:35 2010 +0100 +++ b/Quot/Nominal/Abs.thy Fri Feb 19 10:26:38 2010 +0100 @@ -427,6 +427,35 @@ shows "P p" sorry +lemma tt1: + assumes a: "finite (supp p)" + shows "(supp x) \* p \ p \ x = x" +using a +unfolding fresh_star_def fresh_def +apply(induct F\"supp p" arbitrary: p rule: finite.induct) +apply(simp add: supp_perm) +defer +apply(case_tac "a \ A") +apply(simp add: insert_absorb) +apply(subgoal_tac "A = supp p - {a}") +prefer 2 +apply(blast) +apply(case_tac "p \ a = a") +apply(simp add: supp_perm) +apply(drule_tac x="p + (((- p) \ a) \ a)" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(rule subset_antisym) +apply(rule subsetI) +apply(simp) +apply(simp add: supp_perm) +apply(case_tac "xa = p \ a") +apply(simp) +apply(case_tac "p \ a = (- p) \ a") +apply(simp) +defer +apply(simp) +oops lemma tt: "(supp x) \* p \ p \ x = x" diff -r 4efbaba9d754 -r 2f4ce88c2c96 Quot/Nominal/Terms.thy diff -r 4efbaba9d754 -r 2f4ce88c2c96 Quot/Nominal/Test.thy --- a/Quot/Nominal/Test.thy Fri Feb 19 10:17:35 2010 +0100 +++ b/Quot/Nominal/Test.thy Fri Feb 19 10:26:38 2010 +0100 @@ -5,145 +5,171 @@ atom_decl name -(* test for how to add datatypes *) +(* tests *) +ML {* +Datatype.datatype_cmd; +Datatype.add_datatype Datatype.default_config; + +Primrec.add_primrec_cmd; +Primrec.add_primrec; +Primrec.add_primrec_simple; +*} + +section {* test for setting up a primrec on the ML-level *} + +datatype simple = Foo + +local_setup {* +Primrec.add_primrec [(@{binding "Bar"}, SOME @{typ "simple \ nat"}, NoSyn)] + [(Attrib.empty_binding, HOLogic.mk_Trueprop @{term "Bar Foo = Suc 0"})] #> snd +*} +thm Bar.simps + +lemma "Bar Foo = XXX" +apply(simp) +oops + +section {* test for setting up a datatype on the ML-level *} setup {* -Datatype.datatype_cmd +Datatype.add_datatype Datatype.default_config ["foo"] [([], @{binding "foo"}, NoSyn, - [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, ["foo"], NoSyn)]) - ] + [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, [Type ("Test.foo", [])], NoSyn)]) + ] #> snd +*} + +ML {* + PolyML.makestring (#descr (Datatype.the_info @{theory} "Test.foo")) *} thm foo.recs thm foo.induct +(* adds "_raw" to the end of constants and types *) +ML {* +fun raw_str [] s = s + | raw_str (s'::ss) s = (if s = s' then s ^ "_str" else raw_str ss s) -ML{* -fun filtered_input str = - filter OuterLex.is_proper (OuterSyntax.scan Position.none str) +val raw_strs = map raw_str + +fun raw_typ ty_strs (Type (a, Ts)) = Type (raw_str ty_strs a, map (raw_typ ty_strs) Ts) + | raw_typ ty_strs T = T -fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input +fun raw_term trm_strs ty_strs (Const (a, T)) = Const (raw_str trm_strs a, raw_typ ty_strs T) + | raw_term trm_strs ty_strs (Abs (a, T, t)) = Abs (a, T, raw_term trm_strs ty_strs t) + | raw_term trm_strs ty_strs (t $ u) = (raw_term trm_strs ty_strs t) $ (raw_term trm_strs ty_strs u) + +fun raw_binding bn = Binding.suffix_name "_raw" bn *} -(* type plus possible annotation *) -ML {* -val anno_typ = - (Scan.option (OuterParse.name --| OuterParse.$$$ "::")) -- OuterParse.typ +section{* Interface for nominal_datatype *} + +text {* + +Nominal-Datatype-part: + +1st Arg: string list + ^^^^^^^^^^^ + strings of the types to be defined + +2nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + type(s) to be defined constructors list + (ty args, name, syn) (name, typs, syn) + +Binder-Function-part: + +3rd Arg: (binding * typ option * mixfix) list + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + binding function(s) + to be defined + (name, type, syn) + +4th Arg: (attrib * term) list + ^^^^^^^^^^^^^^^^^^^ + the equations of the binding functions + (Trueprop equations) + *} +ML {* Datatype.add_datatype *} + ML {* -parse (Scan.repeat anno_typ) (filtered_input "x::string bool") +fun raw_definitions dt_names dts bn_funs bn_eqs lthy = +let + val conf = Datatype.default_config + val bn_funs' = map (fn (bn, ty) => (raw_binding bn, ty, NoSyn)) bn_funs + val bn_eqs' = map (pair Attrib.empty_binding) bn_eqs +in + lthy + |> (Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts)) + ||>> Primrec.add_primrec bn_funs' bn_eqs' +end *} -ML {* OuterParse.enum "," ; OuterParse.and_list1 *} +ML {* @{binding "zero"} *} + +local_setup {* +raw_definitions + ["foo'"] + [([], @{binding "foo'"}, NoSyn, + [(@{binding "zero'"}, [], NoSyn),(@{binding "suc'"}, [Type ("Test.foo'", [])], NoSyn)])] + [(@{binding "Bar'"}, SOME @{typ "simple \ nat"})] + [HOLogic.mk_Trueprop @{term "Bar'_raw Foo = Suc 0"}] + #> snd +*} + +typ foo' +thm Bar'.simps + +text {*****************************************************} +ML {* +(* nominal datatype parser *) +local + structure P = OuterParse +in + +val _ = OuterKeyword.keyword "bind" +val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ (* binding specification *) -ML {* -datatype bind = B of string * string | BS of string * string - -val _ = OuterKeyword.keyword "bind" -val _ = OuterKeyword.keyword "bindset" - -val bind_parse_aux = - (OuterParse.$$$ "bind" >> (K B)) - || (OuterParse.$$$ "bindset" >> (K BS)) - (* should use and_list *) val bind_parser = - OuterParse.enum "," - ((bind_parse_aux -- OuterParse.term) -- - (OuterParse.$$$ "in" |-- OuterParse.name) >> (fn ((bind, s1), s2) => bind (s1,s2))) -*} + P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name)) (* datatype parser *) -ML {* val dt_parser = - OuterParse.type_args -- OuterParse.binding -- OuterParse.opt_infix -- - (OuterParse.$$$ "=" |-- OuterParse.enum1 "|" - (OuterParse.binding -- (Scan.repeat anno_typ) -- bind_parser -- OuterParse.opt_mixfix)) -*} + P.type_args -- P.binding -- P.opt_infix -- + (P.$$$ "=" |-- P.enum1 "|" (P.binding -- (Scan.repeat anno_typ) -- bind_parser -- P.opt_mixfix)) (* function equation parser *) -ML {* val fun_parser = - Scan.optional - ((OuterParse.$$$ "binder") |-- OuterParse.fixes -- SpecParse.where_alt_specs) ([],[]) + Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) + +(* main parser *) +val parser = + P.and_list1 dt_parser -- fun_parser + +end *} -(* main parser *) -ML {* -val parser = - OuterParse.and_list1 dt_parser -- fun_parser -*} (* printing stuff *) ML {* fun print_str_option NONE = "NONE" | print_str_option (SOME s) = (s:bstring) -*} -ML {* fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty -*} -ML {* -fun print_bind (B (s1, s2)) = "bind " ^ s1 ^ " in " ^ s2 - | print_bind (BS (s1, s2)) = "bindset " ^ s1 ^ " in " ^ s2 -*} +fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2 -ML {* fun print_constr lthy (((name, anno_tys), bds), syn) = (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ " " ^ (commas (map print_bind bds)) ^ " " ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) -*} -(* TODO: replace with the proper thing *) -ML {* -fun is_atom ty = ty = "Test.name" -*} - -ML {* -fun fv_bds s bds set = - case bds of - [] => set - | B (s1, s2) :: tl => - if s2 = s then - fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) - else fv_bds s tl set - | BS (s1, s2) :: tl => - (* TODO: This is just a copy *) - if s2 = s then - fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) - else fv_bds s tl set -*} - -(* TODO: After variant_frees, check that the new names correspond to the ones given by user - so that 'bind' is matched with variables correctly *) -ML {* -fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) = -let - fun prepare_name (NONE, ty) = ("", ty) - | prepare_name (SOME n, ty) = (n, ty); - val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); - val var_strs = map (Syntax.string_of_term lthy) vars; - fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = - if is_atom tyS then HOLogic.mk_set ty [t] else - if (Long_Name.base_name tyS) mem dt_names then - fv_bds s bds (Free ("rfv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else - HOLogic.mk_set @{typ name} [] - val fv_eq = - if null vars then HOLogic.mk_set @{typ name} [] - else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) - val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq) -in - prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str -end -*} - -ML {* -fun single_dt lthy (((s2, s3), syn), constrs) = +fun print_single_dt lthy (((s2, s3), syn), constrs) = ["constructor declaration"] @ ["type arguments: "] @ s2 @ ["datatype name: ", Binding.name_of s3] @@ -151,57 +177,30 @@ @ ["constructors: "] @ (map (print_constr lthy) constrs) |> separate "\n" |> implode -*} -ML {* -fun fv_dt lthy dt_names (((s2, s3), syn), constrs) = - map (fv_constr lthy ("rfv_" ^ Binding.name_of s3) dt_names) constrs - |> separate "\n" - |> implode -*} - -ML {* fun single_fun_eq lthy (at, s) = +fun print_single_fun_eq lthy (at, s) = ["function equations: ", (Syntax.string_of_term lthy s)] |> separate "\n" |> implode -*} -ML {* fun single_fun_fix (b, _, _) = +fun print_single_fun_fix lthy (b, _, _) = ["functions: ", Binding.name_of b] |> separate "\n" |> implode -*} -ML {* fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3 -*} -ML {* fun print_dts (dts, (funs, feqs)) lthy = let - val _ = warning (implode (separate "\n" (map (single_dt lthy) dts))); - val _ = warning (implode (separate "\n" (map single_fun_fix funs))); - val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs))); + val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts))); + val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs))); + val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs))); in () end *} ML {* -fun fv_dts (dts, (funs, feqs)) lthy = -let - val _ = warning (implode (separate "\n" (map (fv_dt lthy (map dt_name dts)) dts))); -in - lthy -end -*} - -ML {* -parser; -Datatype.datatype_cmd; -*} - -ML {* fun transp_ty_arg (anno, ty) = ty fun transp_constr (((constr_name, ty_args), bind), mx) = @@ -225,35 +224,39 @@ fun fn_defn [] [] lthy = lthy | fn_defn funs feqs lthy = Function_Fun.add_fun Function_Common.default_config funs feqs false lthy -*} -ML {* fun fn_defn_cmd [] [] lthy = lthy | fn_defn_cmd funs feqs lthy = Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy *} ML {* -fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = +fun parse_fun lthy (b, NONE, m) = (b, NONE, m) + | parse_fun lthy (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m) + +fun parse_feq lthy (b, t) = (b, Syntax.read_prop lthy t); + +fun parse_anno_ty lthy (anno, ty) = (anno, Syntax.read_typ lthy ty); + +fun parse_constr lthy (((constr_name, ty_args), bind), mx) = + (((constr_name, map (parse_anno_ty lthy) ty_args), bind), mx); + +fun parse_dt lthy (((ty_args, ty_name), mx), constrs) = + (((ty_args, ty_name), mx), map (parse_constr lthy) constrs); +*} + +ML {* +fun nominal_datatype2_cmd (dt_strs, (fun_strs, feq_strs)) thy = let - val thy' = dt_defn (map transp_dt dts) thy + val thy' = dt_defn (map transp_dt dt_strs) thy val lthy = Theory_Target.init NONE thy' - val lthy' = fn_defn_cmd funs feqs lthy - fun parse_fun (b, NONE, m) = (b, NONE, m) - | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy' ty), m); - val funs = map parse_fun funs - fun parse_feq (b, t) = (b, Syntax.read_prop lthy' t); - val feqs = map parse_feq feqs - fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy' ty); - fun parse_constr (((constr_name, ty_args), bind), mx) = - (((constr_name, map parse_anno_ty ty_args), bind), mx); - fun parse_dt (((ty_args, ty_name), mx), constrs) = - (((ty_args, ty_name), mx), map parse_constr constrs); - val dts = map parse_dt dts - val _ = print_dts (dts, (funs, feqs)) lthy + val lthy' = fn_defn_cmd fun_strs feq_strs lthy + val funs = map (parse_fun lthy') fun_strs + val feqs = map (parse_feq lthy') feq_strs + val dts = map (parse_dt lthy') dt_strs + val _ = print_dts (dts, (funs, feqs)) lthy' in - fv_dts (dts, (funs, feqs)) lthy -|> Local_Theory.exit_global + Local_Theory.exit_global lthy' end *} @@ -284,7 +287,7 @@ nominal_datatype trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bindset x in t +| Lam x::"name" t::"trm" bind x in t | Let p::"pat" "trm" t::"trm" bind "f p" in t and pat = PN @@ -300,7 +303,7 @@ nominal_datatype trm2 = Var2 "name" | App2 "trm2" "trm2" -| Lam2 x::"name" t::"trm2" bindset x in t +| Lam2 x::"name" t::"trm2" bind x in t | Let2 p::"pat2" "trm2" t::"trm2" bind "f2 p" in t and pat2 = PN2 @@ -319,7 +322,7 @@ | Fun "ty" "ty" nominal_datatype tyS = - All xs::"name list" ty::"ty" bindset xs in ty + All xs::"name list" ty::"ty" bind xs in ty