# HG changeset patch # User Christian Urban # Date 1268320335 -3600 # Node ID 7e28654a760a118b6557f38397cf93e0721e4677 # Parent d59f851926c5509ba1e22d7c6e474c00cb9af916# Parent a26cb19375e83b35c07ca1c50eb9be83531f0a3e merged diff -r d59f851926c5 -r 7e28654a760a Nominal/Fv.thy --- a/Nominal/Fv.thy Thu Mar 11 15:10:07 2010 +0100 +++ b/Nominal/Fv.thy Thu Mar 11 16:12:15 2010 +0100 @@ -174,7 +174,7 @@ in if arg_no mem args_in_bn then (if is_rec_type dt then - (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: not good") + (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.") else @{term "{} :: atom set"}) else if is_atom thy ty then mk_single_atom x else if is_atom_set thy ty then mk_atoms x else @@ -384,7 +384,7 @@ val fv_names_all = fv_names_fst @ fv_bn_names; val add_binds = map (fn x => (Attrib.empty_binding, x)) (* Function_Fun.add_fun Function_Common.default_config ... true *) - val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all) +(* val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*) val (fvs, lthy') = (Primrec.add_primrec (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) val (fvs2, lthy'') = @@ -696,4 +696,14 @@ | SOME i => i *} +ML {* +fun rename_vars fnctn thm = +let + val vars = Term.add_vars (prop_of thm) [] + val nvars = map (Var o ((apfst o apfst) fnctn)) vars +in + Thm.certify_instantiate ([], (vars ~~ nvars)) thm end +*} + +end diff -r d59f851926c5 -r 7e28654a760a Nominal/Parser.thy --- a/Nominal/Parser.thy Thu Mar 11 15:10:07 2010 +0100 +++ b/Nominal/Parser.thy Thu Mar 11 16:12:15 2010 +0100 @@ -253,7 +253,13 @@ end *} -ML {* add_primrec_wrapper *} +ML {* +fun un_raw name = unprefix "_raw" name handle Fail _ => name +fun add_under names = hd names :: (map (prefix "_") (tl names)) +fun un_raws name = implode (map un_raw (add_under (space_explode "_" name))) +val un_raw_names = rename_vars un_raws +fun lift_thm ctxt thm = un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))) +*} lemma equivp_hack: "equivp x" sorry @@ -269,8 +275,13 @@ end *} -ML {* val restricted_nominal=ref 0 *} -ML {* val cheat_alpha_eqvt = ref true *} +(* These 2 are critical, we don't know how to do it in term5 *) +ML {* val cheat_fv_rsp = ref true *} +ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) + +(* Fixes for these 2 are known *) +ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) +ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) ML {* fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = @@ -302,9 +313,13 @@ val raw_binds_flat = map (map flat) raw_binds; val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; val alpha_ts_loc = #preds alpha + val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms) val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; + val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms) + val fv_ts_nobn = List.take (fv_ts, length perms) val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; + val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts val alpha_induct_loc = #induct alpha val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc]; val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct @@ -321,27 +336,24 @@ fun alpha_eqvt_tac' _ = if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 - val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4; + val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4; val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc; -in -if !restricted_nominal = 0 then - ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) -else -let - val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; - val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms - ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; + val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; + val fv_eqvt_tac = + if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) + else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 + val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5; val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; - val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc - val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc - inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6; + val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc_nobn +(* val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc + inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*) val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; val qty_full_names = map (Long_Name.qualify thy_name) qty_names val lthy7 = define_quotient_type - (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts)) + (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) (ALLGOALS (resolve_tac alpha_equivp)) lthy6; val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); val raw_consts = @@ -351,56 +363,55 @@ typ_of_dtyp descr sorts (DtRec i))) l) descr); val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; val (consts, const_defs) = split_list consts_defs; -in -if !restricted_nominal = 1 then - ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8) -else -let val (bns_rsp_pre, lthy9) = fold_map ( fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; val bns_rsp = flat (map snd bns_rsp_pre); - val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts - (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy9; - val (const_rsps, lthy11) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] - (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1)) raw_consts lthy10 - val (perms_rsp, lthy12) = prove_const_rsp Binding.empty perms - (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy11; - val qfv_names = map (fn x => "fv_" ^ x) qty_names + fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy + else fvbv_rsp_tac alpha_induct fv_def 1; + val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9 + val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms + (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; + fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy + else constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1 + val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] + const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 + val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; - val thy = Local_Theory.exit_global lthy12b; + val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn + val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; + val thy = Local_Theory.exit_global lthy12c; val perm_names = map (fn x => "permute_" ^ x) qty_names val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; val lthy13 = Theory_Target.init NONE thy'; val q_name = space_implode "_" qty_names; - val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct)); + val q_induct = lift_thm lthy13 induct; val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; - val q_perm = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy14, th))) raw_perm_def; + val q_perm = map (lift_thm lthy14) raw_perm_def; val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; - val q_fv = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy15, th))) fv_def; + val q_fv = map (lift_thm lthy15) fv_def; val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; - val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs; + val q_bn = map (lift_thm lthy16) raw_bn_eqs; val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj - val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded; + val q_inj_pre = map (lift_thm lthy17) inj_unfolded; val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) - val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists; + val q_dis = map (lift_thm lthy18) rel_dists; val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; - val q_eqvt = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy19, th))) raw_fv_bv_eqvt; + val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; in ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20) end -end -end *} + ML {* (* parsing the datatypes and declaring *) (* constructors in the local theory *) diff -r d59f851926c5 -r 7e28654a760a Nominal/Rsp.thy --- a/Nominal/Rsp.thy Thu Mar 11 15:10:07 2010 +0100 +++ b/Nominal/Rsp.thy Thu Mar 11 16:12:15 2010 +0100 @@ -87,13 +87,18 @@ *} ML {* + fun all_eqvts ctxt = + Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt + val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) +*} + +ML {* fun constr_rsp_tac inj rsp equivps = let val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps in REPEAT o rtac impI THEN' - simp_tac (HOL_ss addsimps inj) THEN' - (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW + simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW (asm_simp_tac HOL_ss THEN_ALL_NEW ( rtac @{thm exI[of _ "0 :: perm"]} THEN' asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ @@ -120,20 +125,28 @@ *) ML {* -fun build_eqvts bind funs perms simps induct ctxt = +fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct +*} + +ML {* +fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW + (asm_full_simp_tac (HOL_ss addsimps + (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 +*} + +ML {* +fun build_eqvts bind funs tac ctxt = let val pi = Free ("p", @{typ perm}); val types = map (domain_type o fastype_of) funs; - val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); + val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types); val args = map Free (indnames ~~ types); val perm_at = @{term "permute :: perm \ atom set \ atom set"} - fun eqvtc (fnctn, (arg, perm)) = - HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg))) - val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) - fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps - (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 - val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac + fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg) + fun eqvtc (fnctn, arg) = + HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) + val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args))) + val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames) val thms = HOLogic.conj_elims thm in Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt @@ -145,14 +158,6 @@ apply (rule_tac x="pi \ pia" in exI) by auto -ML {* -fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct -*} -ML {* - fun all_eqvts ctxt = - Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt - val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) -*} ML {* fun mk_minimal_ss ctxt = @@ -195,8 +200,8 @@ *} ML {* -fun build_bv_eqvt perms simps inducts (t, n) = - build_eqvts Binding.empty [t] [nth perms n] simps (nth inducts n) +fun build_bv_eqvt simps inducts (t, n) ctxt = + build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt *} end diff -r d59f851926c5 -r 7e28654a760a Nominal/Term5.thy --- a/Nominal/Term5.thy Thu Mar 11 15:10:07 2010 +0100 +++ b/Nominal/Term5.thy Thu Mar 11 16:12:15 2010 +0100 @@ -48,25 +48,32 @@ done lemma alpha5_eqvt: - "xa \5 y \ (x \ xa) \5 (x \ y)" - "xb \l ya \ (x \ xb) \l (x \ ya)" - "alpha_rbv5 a b c \ alpha_rbv5 (x \ a) (x \ b) (x \ c)" -apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) -apply (simp_all add: alpha5_inj permute_eqvt[symmetric]) -apply (erule exE) -apply (rule_tac x="x \ pi" in exI) -apply (erule conjE)+ -apply (rule conjI) -apply (erule alpha_gen_compose_eqvt) -apply (simp_all add: eqvts) -apply (simp add: permute_eqvt[symmetric]) -apply (subst eqvts[symmetric]) -apply (simp add: eqvts) + "(xa \5 y \ (p \ xa) \5 (p \ y)) \ + (xb \l ya \ (p \ xb) \l (p \ ya)) \ + (alpha_rbv5 a b c \ alpha_rbv5 (p \ a) (p \ b) (p \ c))" +apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) done +lemma alpha5_reflp: +"y \5 y \ (x \l x \ alpha_rbv5 0 x x)" +apply (rule rtrm5_rlts.induct) +apply (simp_all add: alpha5_inj) +apply (rule_tac x="0::perm" in exI) +apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) +done + +lemma alpha5_symp: +"(a \5 b \ a \5 b) \ +(x \l y \ y \l x) \ +(alpha_rbv5 p x y \ alpha_rbv5 (-p) y x)" +apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) +apply (simp_all add: alpha5_inj) +sorry + lemma alpha5_equivp: "equivp alpha_rtrm5" "equivp alpha_rlts" + "equivp (alpha_rbv5 p)" sorry quotient_type diff -r d59f851926c5 -r 7e28654a760a Nominal/Test.thy --- a/Nominal/Test.thy Thu Mar 11 15:10:07 2010 +0100 +++ b/Nominal/Test.thy Thu Mar 11 16:12:15 2010 +0100 @@ -15,21 +15,18 @@ where "bi (BP x t) = {atom x}" +thm lam_bp_fv +thm lam_bp_inject +thm lam_bp_bn +thm lam_bp_perm +thm lam_bp_induct +thm lam_bp_distinct + (* compat should be compat (BP x t) pi (BP x' t') \ alpha_trm t t' \ pi o x = x' *) -typ lam_raw -term VAR_raw -term APP_raw -term LET_raw -term Test.BP_raw -thm bi_raw.simps -thm permute_lam_raw_permute_bp_raw.simps -thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars] -thm fv_lam_raw_fv_bp_raw.simps[no_vars] - text {* example 2 *} nominal_datatype trm' = @@ -48,6 +45,12 @@ | "f (PD x y) = {atom x, atom y}" | "f (PS x) = {atom x}" +thm trm'_pat'_fv +thm trm'_pat'_inject +thm trm'_pat'_bn +thm trm'_pat'_perm +thm trm'_pat'_induct +thm trm'_pat'_distinct (* compat should be compat (PN) pi (PN) == True @@ -55,16 +58,6 @@ compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' *) - -thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars] -thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] -thm f_raw.simps -(*thm trm'_pat'_induct -thm trm'_pat'_perm -thm trm'_pat'_fv -thm trm'_pat'_bn -thm trm'_pat'_inject*) - nominal_datatype trm0 = Var0 "name" | App0 "trm0" "trm0" @@ -81,20 +74,28 @@ | "f0 (PS0 x) = {atom x}" | "f0 (PD0 p1 p2) = (f0 p1) \ (f0 p2)" -thm f0_raw.simps -(*thm trm0_pat0_induct +thm trm0_pat0_fv +thm trm0_pat0_inject +thm trm0_pat0_bn thm trm0_pat0_perm -thm trm0_pat0_fv -thm trm0_pat0_bn*) +thm trm0_pat0_induct +thm trm0_pat0_distinct text {* example type schemes *} nominal_datatype t = - Var "name" -| Fun "t" "t" + VarTS "name" +| FunTS "t" "t" and tyS = All xs::"name set" ty::"t" bind xs in ty +thm t_tyS_fv +thm t_tyS_inject +thm t_tyS_bn +thm t_tyS_perm +thm t_tyS_induct +thm t_tyS_distinct + (* example 1 from Terms.thy *) nominal_datatype trm1 = @@ -113,8 +114,12 @@ | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \ (bv1 bp2)" | "bv1 (BV1 x) = {atom x}" - -thm bv1_raw.simps +thm trm1_bp1_fv +thm trm1_bp1_inject +thm trm1_bp1_bn +thm trm1_bp1_perm +thm trm1_bp1_induct +thm trm1_bp1_distinct text {* example 3 from Terms.thy *} @@ -132,6 +137,12 @@ "bv3 ANil = {}" | "bv3 (ACons x t as) = {atom x} \ (bv3 as)" +thm trm3_rassigns3_fv +thm trm3_rassigns3_inject +thm trm3_rassigns3_bn +thm trm3_rassigns3_perm +thm trm3_rassigns3_induct +thm trm3_rassigns3_distinct (* compat should be compat (ANil) pi (PNil) \ TRue @@ -153,6 +164,13 @@ "bv5 Lnil = {}" | "bv5 (Lcons n t ltl) = {atom n} \ (bv5 ltl)" +thm trm5_lts_fv +thm trm5_lts_inject +thm trm5_lts_bn +thm trm5_lts_perm +thm trm5_lts_induct +thm trm5_lts_distinct + (* example from my PHD *) atom_decl coname @@ -166,9 +184,12 @@ | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t -thm alpha_phd_raw.intros[no_vars] -thm fv_phd_raw.simps[no_vars] - +thm phd_fv +thm phd_inject +thm phd_bn +thm phd_perm +thm phd_induct +thm phd_distinct (* example form Leroy 96 about modules; OTT *) @@ -223,8 +244,15 @@ | "Cbinders (SStru x S) = {atom x}" | "Cbinders (SVal v T) = {atom v}" +thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv +thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject +thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn +thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm +thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct +thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct (* example 3 from Peter Sewell's bestiary *) + nominal_datatype exp = VarP "name" | AppP "exp" "exp" @@ -240,7 +268,13 @@ "bp' (PVar x) = {atom x}" | "bp' (PUnit) = {}" | "bp' (PPair p1 p2) = bp' p1 \ bp' p2" -thm alpha_exp_raw_alpha_pat3_raw_alpha_bp'_raw.intros + +thm exp_pat3_fv +thm exp_pat3_inject +thm exp_pat3_bn +thm exp_pat3_perm +thm exp_pat3_induct +thm exp_pat3_distinct (* example 6 from Peter Sewell's bestiary *) nominal_datatype exp6 = @@ -257,7 +291,13 @@ "bp6 (PVar' x) = {atom x}" | "bp6 (PUnit') = {}" | "bp6 (PPair' p1 p2) = bp6 p1 \ bp6 p2" -thm alpha_exp6_raw_alpha_pat6_raw_alpha_bp6_raw.intros + +thm exp6_pat6_fv +thm exp6_pat6_inject +thm exp6_pat6_bn +thm exp6_pat6_perm +thm exp6_pat6_induct +thm exp6_pat6_distinct (* THE REST ARE NOT SUPPOSED TO WORK YET *)