# HG changeset patch # User Christian Urban # Date 1267542288 -3600 # Node ID da44ef9a7df22e60a5aad5016226dd14387720d5 # Parent b0eae8c933147f6b63d2e2bebee9a31a6890d354# Parent b7463e5e7d871664f0cfe35a03784f5c35daa9f2 merged diff -r b0eae8c93314 -r da44ef9a7df2 Nominal/Fv.thy --- a/Nominal/Fv.thy Tue Mar 02 16:03:19 2010 +0100 +++ b/Nominal/Fv.thy Tue Mar 02 16:04:48 2010 +0100 @@ -443,4 +443,13 @@ 1 *}) done*) +ML {* +fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free" + | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic" + | dtyp_no_of_typ dts (Type (tname, Ts)) = + case try (find_index (curry op = tname o fst)) dts of + NONE => error "dtyp_no_of_typ: Illegal recursion" + | SOME i => i +*} + end diff -r b0eae8c93314 -r da44ef9a7df2 Nominal/LFex.thy --- a/Nominal/LFex.thy Tue Mar 02 16:03:19 2010 +0100 +++ b/Nominal/LFex.thy Tue Mar 02 16:04:48 2010 +0100 @@ -45,11 +45,10 @@ done lemma alpha_eqvt: - "t1 \ki s1 \ (pi \ t1) \ki (pi \ s1)" - "t2 \ty s2 \ (pi \ t2) \ty (pi \ s2)" - "t3 \tr s3 \ (pi \ t3) \tr (pi \ s3)" -apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts) -apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) + "(t1 \ki s1 \ (p \ t1) \ki (p \ s1)) \ + (t2 \ty s2 \ (p \ t2) \ty (p \ s2)) \ + (t3 \tr s3 \ (p \ t3) \tr (p \ s3))" +apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct) apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) apply (erule alpha_gen_compose_eqvt) apply (simp_all add: rfv_eqvt eqvts atom_eqvt) diff -r b0eae8c93314 -r da44ef9a7df2 Nominal/Lift.thy --- a/Nominal/Lift.thy Tue Mar 02 16:03:19 2010 +0100 +++ b/Nominal/Lift.thy Tue Mar 02 16:04:48 2010 +0100 @@ -82,7 +82,6 @@ val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos val typs = List.take (all_typs, number) val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; -val full_tnames = List.take (all_full_tnames, number); val induct = #induct info; val inducts = #inducts info; val infos = map (Datatype.the_info thy1) all_full_tnames; @@ -106,10 +105,7 @@ val morphism = ProofContext.export_morphism lthy2 lthy1 val fv_ts = map (Morphism.term morphism) fv_ts_loc val alpha_ts = map (Morphism.term morphism) alpha_ts_loc -fun build_bv_eqvt (t, n) = - build_eqvts Binding.empty [t] [nth perms n] - (bv_simps @ raw_perm_def) (nth inducts n) -val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2; +val (bv_eqvts, lthy3) = fold_map (build_bv_eqvt perms (bv_simps @ raw_perm_def) inducts) bvs lthy2; val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4; val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc; diff -r b0eae8c93314 -r da44ef9a7df2 Nominal/Parser.thy --- a/Nominal/Parser.thy Tue Mar 02 16:03:19 2010 +0100 +++ b/Nominal/Parser.thy Tue Mar 02 16:04:48 2010 +0100 @@ -1,5 +1,5 @@ theory Parser -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" "Rsp" begin atom_decl name @@ -215,13 +215,30 @@ val (((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_binds), lthy2) = raw_nominal_decls dts bn_funs bn_eqs binds lthy val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); + val descr = #descr dtinfo; + val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; + val inject = flat (map #inject dtinfos); + val distinct = flat (map #distinct dtinfos); + val inducts = #inducts dtinfo; val ((raw_perm_def, raw_perm_simps, perms), lthy3) = Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; 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 lthy3; + val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); + val _ = tracing (PolyML.makestring dts_names); + val bn_tys = map (domain_type o fastype_of) raw_bn_funs; + val _ = tracing (PolyML.makestring bn_tys); + val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; + val _ = tracing (PolyML.makestring bn_nos); + val bns = raw_bn_funs ~~ bn_nos; + val alpha_intros = #intrs alpha; + val alpha_cases = #elims alpha + val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4 + val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; in - ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) + ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5) end *} diff -r b0eae8c93314 -r da44ef9a7df2 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Tue Mar 02 16:03:19 2010 +0100 +++ b/Nominal/Rsp.thy Tue Mar 02 16:04:48 2010 +0100 @@ -175,4 +175,9 @@ end *} +ML {* +fun build_bv_eqvt perms simps inducts (t, n) = + build_eqvts Binding.empty [t] [nth perms n] simps (nth inducts n) +*} + end diff -r b0eae8c93314 -r da44ef9a7df2 Nominal/Test.thy --- a/Nominal/Test.thy Tue Mar 02 16:03:19 2010 +0100 +++ b/Nominal/Test.thy Tue Mar 02 16:04:48 2010 +0100 @@ -24,7 +24,7 @@ thm permute_lam_raw_permute_bp_raw.simps thm alpha_lam_raw_alpha_bp_raw.intros thm fv_lam_raw_fv_bp_raw.simps - +thm eqvts print_theorems