# HG changeset patch # User Christian Urban # Date 1274094054 -3600 # Node ID 871d8a5e0c6740cb7b5f29a288b531804b825925 # Parent c39d4fe31100fba43a8cbc261ace16c80bbc517e somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms diff -r c39d4fe31100 -r 871d8a5e0c67 Nominal/Ex/Test.thy --- a/Nominal/Ex/Test.thy Sun May 16 12:41:27 2010 +0100 +++ b/Nominal/Ex/Test.thy Mon May 17 12:00:54 2010 +0100 @@ -5,6 +5,8 @@ (* This file contains only the examples that are not supposed to work yet. *) +declare [[STEPS = 2]] + atom_decl name (* example 4 from Terms.thy *) @@ -12,12 +14,11 @@ defined fv and defined alpha... *) (* lists-datastructure does not work yet *) -(* nominal_datatype trm = Vr "name" | Ap "trm" "trm list" | Lm x::"name" t::"trm" bind x in t -*) + (* thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] diff -r c39d4fe31100 -r 871d8a5e0c67 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sun May 16 12:41:27 2010 +0100 +++ b/Nominal/NewParser.thy Mon May 17 12:00:54 2010 +0100 @@ -67,8 +67,9 @@ ML {* +(* exports back the results *) fun add_primrec_wrapper funs eqs lthy = - if null funs then (([], []), lthy) + if null funs then ([], [], lthy) else let val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs @@ -76,7 +77,7 @@ 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') + (map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs'', lthy') end *} @@ -162,9 +163,9 @@ 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 *) +(* strip_bn_fun takes a rhs of a bn function: this can only contain unions or + appends of elements; in case of recursive calls it retruns also the applied + bn function *) ML {* fun strip_bn_fun t = case t of @@ -226,7 +227,6 @@ end *} -ML {* add_primrec_wrapper *} ML {* fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = let @@ -252,14 +252,12 @@ (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) val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy - val ((raw_bn_funs, raw_bn_eqs), lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 + val (raw_bn_funs, raw_bn_eqs, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 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); @@ -370,22 +368,19 @@ setup STEPS_setup - ML {* fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = let - (* definition of the raw datatype and raw bn-functions *) + (* definition of the raw datatypes and raw bn-functions *) val (raw_dt_names, 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 all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) - val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; - - val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; + val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) + val {descr, sorts, ...} = dtinfo + val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr + val all_full_tnames = map (fn (_, (n, _, _)) => n) descr + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames val inject_thms = flat (map #inject dtinfos); val distinct_thms = flat (map #distinct dtinfos); @@ -395,13 +390,14 @@ val exhaust_thms = map #exhaust dtinfos; (* definitions of raw permutations *) - val ((raw_perm_def, raw_perm_simps, perms), lthy2) = - if get_STEPS lthy > 2 + val ((perms, raw_perm_defs, raw_perm_simps), lthy2) = + if get_STEPS lthy1 > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 else raise TEST lthy1 val (_, lthy2a) = Local_Theory.note ((Binding.empty, - [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; + [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_defs) lthy2; + val thy = Local_Theory.exit_global lthy2a; val thy_name = Context.theory_name thy @@ -410,7 +406,7 @@ val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; val ((fv, fvbn), fv_def, lthy3a) = - if get_STEPS lthy > 3 + if get_STEPS lthy2 > 3 then define_raw_fv descr sorts raw_bns raw_bclauses lthy3 else raise TEST lthy3 @@ -439,8 +435,8 @@ (* proving equivariance lemmas *) val _ = warning "Proving equivariance"; - val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 - val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 + val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 + val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; (* proving alpha equivalence *) @@ -454,7 +450,7 @@ 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 (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6a; + val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts_nobn alpha_equivp lthy6a; val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); val raw_consts = flat (map (fn (i, (_, _, l)) => @@ -515,7 +511,7 @@ [Rule_Cases.name constr_names q_induct]) lthy13; val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; - val q_perm = map (lift_thm qtys lthy14) raw_perm_def; + val q_perm = map (lift_thm qtys lthy14) raw_perm_defs; val lthy15 = note_simp_suffix "perm" q_perm lthy14a; val q_fv = map (lift_thm qtys lthy15) fv_def; val lthy16 = note_simp_suffix "fv" q_fv lthy15; diff -r c39d4fe31100 -r 871d8a5e0c67 Nominal/Perm.thy --- a/Nominal/Perm.thy Sun May 16 12:41:27 2010 +0100 +++ b/Nominal/Perm.thy Mon May 17 12:00:54 2010 +0100 @@ -146,17 +146,20 @@ val perms_zero_bind = Binding.name (perms_name ^ "_zero") val perms_plus_bind = Binding.name (perms_name ^ "_plus") - fun tac _ (_, simps, _) = + fun tac _ (_, _, simps) = Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) - fun morphism phi (dfs, simps, fvs) = - (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); + fun morphism phi (fvs, dfs, simps) = + (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); + + val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) in lthy' + (*|> snd o (Local_Theory.note ((Binding.empty, [eqvt_attrib]), perm_eq_thms))*) |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |> Class_Target.prove_instantiation_exit_result morphism tac - (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs) + (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') end *}