# HG changeset patch # User Christian Urban # Date 1280090541 -7200 # Node ID e8b9c0ebf5dd2c2279f314bdf81d231359a1851d # Parent fd85f49216547fa50628c285496c5ecf76b757a7 added paper by james; some minor cleaning diff -r fd85f4921654 -r e8b9c0ebf5dd Literature/cheney05icfp.pdf Binary file Literature/cheney05icfp.pdf has changed diff -r fd85f4921654 -r e8b9c0ebf5dd Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Fri Jul 23 16:42:47 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Sun Jul 25 22:42:21 2010 +0200 @@ -34,18 +34,19 @@ and "alpha_assg_raw x2 y2 \ alpha_bn_raw x2 y2" and "alpha_bn_raw x3 y3 \ True" apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) -apply(simp_all) +apply(rule TrueI)+ apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(assumption) -done +sorry lemma a2: shows "alpha_trm_raw x1 y1 \ fv_trm_raw x1 = fv_trm_raw y1" and "alpha_assg_raw x2 y2 \ fv_assg_raw x2 = fv_assg_raw y2 \ bn_raw x2 = bn_raw y2" and "alpha_bn_raw x3 y3 \ fv_bn_raw x3 = fv_bn_raw y3" apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) -apply(simp_all add: alphas a1 prod_alpha_def) -apply(auto) +apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) +apply(simp_all only: alphas prod_alpha_def) +apply(auto)[1] +apply(auto simp add: prod_alpha_def) done lemma [quot_respect]: diff -r fd85f4921654 -r e8b9c0ebf5dd Nominal/Parser.thy --- a/Nominal/Parser.thy Fri Jul 23 16:42:47 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,706 +0,0 @@ -theory NewParser -imports "../Nominal-General/Nominal2_Base" - "../Nominal-General/Nominal2_Eqvt" - "../Nominal-General/Nominal2_Supp" - "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp" "Lift" -begin - -section{* Interface for nominal_datatype *} - - -ML {* -(* nominal datatype parser *) -local - structure P = OuterParse; - structure S = Scan - - fun triple1 ((x, y), z) = (x, y, z) - fun triple2 (x, (y, z)) = (x, y, z) - fun tuple ((x, y, z), u) = (x, y, z, u) - fun tswap (((x, y), z), u) = (x, y, u, z) -in - -val _ = OuterKeyword.keyword "bind" -val _ = OuterKeyword.keyword "bind_set" -val _ = OuterKeyword.keyword "bind_res" - -val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ - -val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res" - -val bind_clauses = - P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) - -val cnstr_parser = - P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap - -(* datatype parser *) -val dt_parser = - (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- - (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple - -(* binding function parser *) -val bnfun_parser = - S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], []) - -(* main parser *) -val main_parser = - P.and_list1 dt_parser -- bnfun_parser >> triple2 - -end -*} - -ML {* -fun get_cnstrs dts = - map (fn (_, _, _, constrs) => constrs) dts - -fun get_typed_cnstrs dts = - flat (map (fn (_, bn, _, constrs) => - (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) - -fun get_cnstr_strs dts = - map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) - -fun get_bn_fun_strs bn_funs = - map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs -*} - - -ML {* -fun add_primrec_wrapper funs eqs lthy = - if null funs then (([], []), lthy) - else - let - val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs - val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs - val ((funs'', eqs''), lthy') = Primrec.add_primrec funs' eqs' lthy - val phi = ProofContext.export_morphism lthy' lthy - in - ((map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs''), lthy') - end -*} - -ML {* -fun add_datatype_wrapper dt_names dts = -let - val conf = Datatype.default_config -in - Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts) -end -*} - - -text {* Infrastructure for adding "_raw" to types and terms *} - -ML {* -fun add_raw s = s ^ "_raw" -fun add_raws ss = map add_raw ss -fun raw_bind bn = Binding.suffix_name "_raw" bn - -fun replace_str ss s = - case (AList.lookup (op=) ss s) of - SOME s' => s' - | NONE => s - -fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) - | replace_typ ty_ss T = T - -fun raw_dts ty_ss dts = -let - fun raw_dts_aux1 (bind, tys, mx) = - (raw_bind bind, map (replace_typ ty_ss) tys, mx) - - fun raw_dts_aux2 (ty_args, bind, mx, constrs) = - (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) -in - map raw_dts_aux2 dts -end - -fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) - | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T) - | replace_aterm trm_ss trm = trm - -fun replace_term trm_ss ty_ss trm = - trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) -*} - -ML {* -fun rawify_dts dt_names dts dts_env = -let - val raw_dts = raw_dts dts_env dts - val raw_dt_names = add_raws dt_names -in - (raw_dt_names, raw_dts) -end -*} - -ML {* -fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = -let - val bn_funs' = map (fn (bn, ty, mx) => - (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs - - val bn_eqs' = map (fn (attr, trm) => - (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs -in - (bn_funs', bn_eqs') -end -*} - -ML {* -fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses = -let - fun rawify_bnds bnds = - map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds - - fun rawify_bclause (BEmy n) = BEmy n - | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys) - | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys) - | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys) -in - map (map (map rawify_bclause)) bclauses -end -*} - -(* strip_bn_fun takes a bn function defined by the user as a union or - append of elements and returns those elements together with bn functions - applied *) -ML {* -fun strip_bn_fun t = - case t of - Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r - | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r - | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => - (i, NONE) :: strip_bn_fun y - | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => - (i, NONE) :: strip_bn_fun y - | Const (@{const_name bot}, _) => [] - | Const (@{const_name Nil}, _) => [] - | (f as Free _) $ Bound i => [(i, SOME f)] - | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t)) -*} - -ML {* -fun find [] _ = error ("cannot find element") - | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y -*} - -ML {* -fun prep_bn lthy dt_names dts eqs = -let - fun aux eq = - let - val (lhs, rhs) = eq - |> strip_qnt_body "all" - |> HOLogic.dest_Trueprop - |> HOLogic.dest_eq - val (bn_fun, [cnstr]) = strip_comb lhs - val (_, ty) = dest_Free bn_fun - val (ty_name, _) = dest_Type (domain_type ty) - val dt_index = find_index (fn x => x = ty_name) dt_names - val (cnstr_head, cnstr_args) = strip_comb cnstr - val rhs_elements = strip_bn_fun rhs - val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements - in - (dt_index, (bn_fun, (cnstr_head, included))) - end - fun aux2 eq = - let - val (lhs, rhs) = eq - |> strip_qnt_body "all" - |> HOLogic.dest_Trueprop - |> HOLogic.dest_eq - val (bn_fun, [cnstr]) = strip_comb lhs - val (_, ty) = dest_Free bn_fun - val (ty_name, _) = dest_Type (domain_type ty) - val dt_index = find_index (fn x => x = ty_name) dt_names - val (cnstr_head, cnstr_args) = strip_comb cnstr - val rhs_elements = strip_bn_fun rhs - val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements - in - (bn_fun, dt_index, (cnstr_head, included)) - end - fun order dts i ts = - let - val dt = nth dts i - val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) - val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts - in - map (find ts') cts - end - - val unordered = AList.group (op=) (map aux eqs) - val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered - val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' - val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) - - val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) - val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs)) - val _ = tracing ("ordered'\n" ^ @{make_string} ordered') -in - ordered' -end -*} - - -ML {* -fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = -let - val thy = ProofContext.theory_of lthy - val thy_name = Context.theory_name thy - - val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts - val dt_full_names = map (Long_Name.qualify thy_name) dt_names - val dt_full_names' = add_raws dt_full_names - val dts_env = dt_full_names ~~ dt_full_names' - - val cnstrs = get_cnstr_strs dts - val cnstrs_ty = get_typed_cnstrs dts - val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs - val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name - (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty - val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' - - val bn_fun_strs = get_bn_fun_strs bn_funs - val bn_fun_strs' = add_raws bn_fun_strs - val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' - val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) - (bn_fun_strs ~~ bn_fun_strs') - - 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_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs) -in - lthy - |> add_datatype_wrapper raw_dt_names raw_dts - ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs - ||>> pair raw_bclauses - ||>> pair raw_bns -end -*} - -lemma equivp_hack: "equivp x" -sorry -ML {* -fun equivp_hack ctxt rel = -let - val thy = ProofContext.theory_of ctxt - val ty = domain_type (fastype_of rel) - val cty = ctyp_of thy ty - val ct = cterm_of thy rel -in - Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} -end -*} - -ML {* val cheat_equivp = Unsynchronized.ref false *} -ML {* val cheat_fv_rsp = Unsynchronized.ref false *} -ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} -ML {* val cheat_supp_eq = Unsynchronized.ref false *} - -ML {* -fun remove_loop t = - let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end - handle TERM _ => @{thm eqTrueI} OF [t] -*} - -text {* - nominal_datatype2 does the following things in order: - -Parser.thy/raw_nominal_decls - 1) define the raw datatype - 2) define the raw binding functions - -Perm.thy/define_raw_perms - 3) define permutations of the raw datatype and show that the raw type is - in the pt typeclass - -Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha - 4) define fv and fv_bn - 5) define alpha and alpha_bn - -Perm.thy/distinct_rel - 6) prove alpha_distincts (C1 x \ C2 y ...) (Proof by cases; simp) - -Tacs.thy/build_rel_inj - 6) prove alpha_eq_iff (C1 x = C2 y \ P x y ...) - (left-to-right by intro rule, right-to-left by cases; simp) -Equivp.thy/prove_eqvt - 7) prove bn_eqvt (common induction on the raw datatype) - 8) prove fv_eqvt (common induction on the raw datatype with help of above) -Rsp.thy/build_alpha_eqvts - 9) prove alpha_eqvt and alpha_bn_eqvt - (common alpha-induction, unfolding alpha_gen, permute of #* and =) -Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps - 10) prove that alpha and alpha_bn are equivalence relations - (common induction and application of 'compose' lemmas) -Lift.thy/define_quotient_types - 11) define quotient types -Rsp.thy/build_fvbv_rsps - 12) prove bn respects (common induction and simp with alpha_gen) -Rsp.thy/prove_const_rsp - 13) prove fv respects (common induction and simp with alpha_gen) - 14) prove permute respects (unfolds to alpha_eqvt) -Rsp.thy/prove_alpha_bn_rsp - 15) prove alpha_bn respects - (alpha_induct then cases then sym and trans of the relations) -Rsp.thy/prove_alpha_alphabn - 16) show that alpha implies alpha_bn (by unduction, needed in following step) -Rsp.thy/prove_const_rsp - 17) prove respects for all datatype constructors - (unfold eq_iff and alpha_gen; introduce zero permutations; simp) -Perm.thy/quotient_lift_consts_export - 18) define lifted constructors, fv, bn, alpha_bn, permutations -Perm.thy/define_lifted_perms - 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass -Lift.thy/lift_thm - 20) lift permutation simplifications - 21) lift induction - 22) lift fv - 23) lift bn - 24) lift eq_iff - 25) lift alpha_distincts - 26) lift fv and bn eqvts -Equivp.thy/prove_supports - 27) prove that union of arguments supports constructors -Equivp.thy/prove_fs - 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) -Equivp.thy/supp_eq - 29) prove supp = fv -*} - -ML {* -(* for testing porposes - to exit the procedure early *) -exception TEST of Proof.context - -val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 10); - -fun get_STEPS ctxt = Config.get ctxt STEPS -*} - -setup STEPS_setup - - -ML {* -fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = -let - (* definition of the raw datatype and raw bn-functions *) - val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) = - if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy - else raise TEST lthy - - val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); - val {descr, sorts, ...} = dtinfo; - val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; - - val induct_thm = #induct dtinfo; - - (* definitions of raw permutations *) - val ((raw_perm_def, raw_perm_simps, perms), lthy2) = - if get_STEPS lthy > 2 - then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 - else raise TEST lthy1 - - (* definition of raw fv_functions *) - val morphism_2_0 = ProofContext.export_morphism lthy2 lthy - fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); - val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; - - val thy = Local_Theory.exit_global lthy2; - val thy_name = Context.theory_name thy - - val lthy3 = Theory_Target.init NONE thy; - val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; - - val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) - val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) - - val ((fv, fvbn), fv_def, lthy3a) = - if get_STEPS lthy > 3 - then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 - else raise TEST lthy3 - -in - (0, lthy3a) -end handle TEST ctxt => (0, ctxt) -*} - -section {* Preparing and parsing of the specification *} - -ML {* -(* parsing the datatypes and declaring *) -(* constructors in the local theory *) -fun prepare_dts dt_strs lthy = -let - val thy = ProofContext.theory_of lthy - - fun mk_type full_tname tvrs = - Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs) - - fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) = - let - val tys = map (Syntax.read_typ lthy o snd) anno_tys - val ty = mk_type full_tname tvs - in - ((cname, tys ---> ty, mx), (cname, tys, mx)) - end - - fun prep_dt (tvs, tname, mx, cnstrs) = - let - val full_tname = Sign.full_name thy tname - val (cnstrs', cnstrs'') = - split_list (map (prep_cnstr full_tname tvs) cnstrs) - in - (cnstrs', (tvs, tname, mx, cnstrs'')) - end - - val (cnstrs, dts) = split_list (map prep_dt dt_strs) -in - lthy - |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs)) - |> pair dts -end -*} - -ML {* -(* parsing the binding function specification and *) -(* declaring the functions in the local theory *) -fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy = -let - val ((bn_funs, bn_eqs), _) = - Specification.read_spec bn_fun_strs bn_eq_strs lthy - - fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) - - val bn_funs' = map prep_bn_fun bn_funs -in - lthy - |> Local_Theory.theory (Sign.add_consts_i bn_funs') - |> pair (bn_funs', bn_eqs) -end -*} - -text {* associates every SOME with the index in the list; drops NONEs *} -ML {* -fun indexify xs = -let - fun mapp _ [] = [] - | mapp i (NONE :: xs) = mapp (i + 1) xs - | mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs -in - mapp 0 xs -end - -fun index_lookup xs x = - case AList.lookup (op=) xs x of - SOME x => x - | NONE => error ("Cannot find " ^ x ^ " as argument annotation."); -*} - -ML {* -fun prepare_bclauses dt_strs lthy = -let - val annos_bclauses = - get_cnstrs dt_strs - |> map (map (fn (_, antys, _, bns) => (map fst antys, bns))) - - fun prep_binder env bn_str = - case (Syntax.read_term lthy bn_str) of - Free (x, _) => (NONE, index_lookup env x) - | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) - | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") - - fun prep_body env bn_str = index_lookup env bn_str - - fun prep_mode "bind" = BLst - | prep_mode "bind_set" = BSet - | prep_mode "bind_res" = BRes - - fun prep_bclause env (mode, binders, bodies) = - let - val binders' = map (prep_binder env) binders - val bodies' = map (prep_body env) bodies - in - prep_mode mode (binders', bodies') - end - - fun prep_bclauses (annos, bclause_strs) = - let - val env = indexify annos (* for every label, associate the index *) - in - map (prep_bclause env) bclause_strs - end -in - map (map prep_bclauses) annos_bclauses -end -*} - -text {* - adds an empty binding clause for every argument - that is not already part of a binding clause -*} - -ML {* -fun included i bcs = -let - fun incl (BEmy j) = i = j - | incl (BLst (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) - | incl (BSet (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) - | incl (BRes (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) -in - exists incl bcs -end -*} - -ML {* -fun complete dt_strs bclauses = -let - val args = - get_cnstrs dt_strs - |> map (map (fn (_, antys, _, _) => length antys)) - - fun complt n bcs = - let - fun add bcs i = (if included i bcs then [] else [BEmy i]) - in - bcs @ (flat (map_range (add bcs) n)) - end -in - map2 (map2 complt) args bclauses -end -*} - -ML {* -fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = -let - fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) - val lthy0 = - Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy - val (dts, lthy1) = prepare_dts dt_strs lthy0 - val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 - val bclauses = prepare_bclauses dt_strs lthy2 - val bclauses' = complete dt_strs bclauses -in - nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd -end - - -(* Command Keyword *) - -val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl - (main_parser >> nominal_datatype2_cmd) -*} - -(* -atom_decl name - -nominal_datatype lam = - Var name -| App lam lam -| Lam x::name t::lam bind_set x in t -| Let p::pt t::lam bind_set "bn p" in t -and pt = - P1 name -| P2 pt pt -binder - bn::"pt \ atom set" -where - "bn (P1 x) = {atom x}" -| "bn (P2 p1 p2) = bn p1 \ bn p2" - -find_theorems Var_raw - - - -thm lam_pt.bn -thm lam_pt.fv[simplified lam_pt.supp(1-2)] -thm lam_pt.eq_iff -thm lam_pt.induct -thm lam_pt.perm - -nominal_datatype exp = - EVar name -| EUnit -| EPair q1::exp q2::exp -| ELetRec l::lrbs e::exp bind "b_lrbs l" in e l - -and fnclause = - K x::name p::pat f::exp bind_res "b_pat p" in f - -and fnclauses = - S fnclause -| ORs fnclause fnclauses - -and lrb = - Clause fnclauses - -and lrbs = - Single lrb -| More lrb lrbs - -and pat = - PVar name -| PUnit -| PPair pat pat - -binder - b_lrbs :: "lrbs \ atom list" and - b_pat :: "pat \ atom set" and - b_fnclauses :: "fnclauses \ atom list" and - b_fnclause :: "fnclause \ atom list" and - b_lrb :: "lrb \ atom list" - -where - "b_lrbs (Single l) = b_lrb l" -| "b_lrbs (More l ls) = append (b_lrb l) (b_lrbs ls)" -| "b_pat (PVar x) = {atom x}" -| "b_pat (PUnit) = {}" -| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" -| "b_fnclauses (S fc) = (b_fnclause fc)" -| "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)" -| "b_lrb (Clause fcs) = (b_fnclauses fcs)" -| "b_fnclause (K x pat exp) = [atom x]" - -thm exp_fnclause_fnclauses_lrb_lrbs_pat.bn -thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv -thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff -thm exp_fnclause_fnclauses_lrb_lrbs_pat.induct -thm exp_fnclause_fnclauses_lrb_lrbs_pat.perm - -nominal_datatype ty = - Vr "name" -| Fn "ty" "ty" -and tys = - Al xs::"name fset" t::"ty" bind_res xs in t - -thm ty_tys.fv[simplified ty_tys.supp] -thm ty_tys.eq_iff - -*) - -(* some further tests *) - -(* -nominal_datatype ty2 = - Vr2 "name" -| Fn2 "ty2" "ty2" - -nominal_datatype tys2 = - All2 xs::"name fset" ty::"ty2" bind_res xs in ty - -nominal_datatype lam2 = - Var2 "name" -| App2 "lam2" "lam2 list" -| Lam2 x::"name" t::"lam2" bind x in t -*) - - - -end - - - diff -r fd85f4921654 -r e8b9c0ebf5dd Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Fri Jul 23 16:42:47 2010 +0200 +++ b/Pearl-jv/Paper.thy Sun Jul 25 22:42:21 2010 +0200 @@ -353,7 +353,7 @@ @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} @{thm plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2", THEN eq_reflection]} \hspace{4mm} @{thm uminus_perm_def[where p="\", THEN eq_reflection]} \hspace{4mm} - @{thm diff_def[where x="\\<^isub>1" and y="\\<^isub>2"]} + @{thm diff_def[where a="\\<^isub>1" and b="\\<^isub>2"]} \end{tabular} \end{isabelle} diff -r fd85f4921654 -r e8b9c0ebf5dd README --- a/README Fri Jul 23 16:42:47 2010 +0200 +++ b/README Sun Jul 25 22:42:21 2010 +0200 @@ -15,6 +15,9 @@ Nominal/Ex ... examples for new implementation -Paper ... submitted to ICFP +Paper ... submitted to POPL -Pearl ... paper accepted at ITP \ No newline at end of file +Pearl ... accepted at ITP +Pearl-jv ... journal version + +Quotient-Paper .. submitted to APLAS \ No newline at end of file