nominal2: comparison Nominal/NewParser.thy

equal deleted inserted replaced

-:09bbed4f21d6
+:9fb315392493
 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]
-*}
 ML {*
 (* for testing porposes - to exit the procedure early *)
 exception TEST of Proof.context
 fun get_STEPS ctxt = Config.get ctxt STEPS
 *}
 setup STEPS_setup
-ML {* dtyp_no_of_typ *}
+ML {*
+fun mk_conjl props =
+fold (fn a => fn b =>
+if a = @{term True} then b else
+if b = @{term True} then a else
+HOLogic.mk_conj (a, b)) (rev props) @{term True};
+*}
+ML {*
+val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
+(* Given function for buildng a goal for an input, prepares a
+one common goals for all the inputs and proves it by induction
+together *)
+ML {*
+fun prove_by_induct tys build_goal ind utac inputs ctxt =
+let
+val names = Datatype_Prop.make_tnames tys;
+val (names', ctxt') = Variable.variant_fixes names ctxt;
+val frees = map Free (names' ~~ tys);
+val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';
+val gls = flat gls_lists;
+fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
+val trm_gl_lists = map trm_gls_map frees;
+val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
+val trm_gls = map mk_conjl trm_gl_lists;
+val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
+fun tac {context,...} = (
+InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
+THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1
+val th_loc = Goal.prove ctxt'' [] [] gl tac
+val ths_loc = HOLogic.conj_elims th_loc
+val ths = Variable.export ctxt'' ctxt ths_loc
+in
+filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
+end
+*}
+ML {*
+fun build_eqvt_gl pi frees fnctn ctxt =
+let
+val typ = domain_type (fastype_of fnctn);
+val arg = the (AList.lookup (op=) frees typ);
+in
+([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt)
+end
+*}
+ML {*
+fun prove_eqvt tys ind simps funs ctxt =
+let
+val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt;
+val p = Free (p, @{typ perm})
+val simp_set = @{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'
+val tac = asm_full_simp_tac (HOL_ss addsimps simp_set)
+val ths_loc = prove_by_induct tys (build_eqvt_gl p) ind tac funs ctxt'
+val ths = Variable.export ctxt' ctxt ths_loc
+val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
+in
+(ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
+end
+*}
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
 (* definition of the raw datatypes *)
 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);
 val rel_dtinfos = List.take (dtinfos, (length dts));
-val rel_distinct = map #distinct rel_dtinfos;  (* thm list list *)
+val raw_constrs_distinct = (map #distinct rel_dtinfos);
 val induct_thm = #induct dtinfo;
 val exhaust_thms = map #exhaust dtinfos;
 val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
 val bns = raw_bn_funs ~~ bn_nos;
 if get_STEPS lthy2 > 3
 then define_raw_fvs descr sorts raw_bn_info raw_bclauses lthy3
 else raise TEST lthy3
 (* definition of raw alphas *)
-val (alpha_ts, alpha_bn_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) =
+val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
 if get_STEPS lthy > 4
 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a
 else raise TEST lthy3a
-(* HERE *)
+(* definition of alpha-distinct lemmas *)
+val (alpha_distincts, alpha_bn_distincts) =
+mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info
 (* definition of raw_alpha_eq_iff  lemmas *)
-val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) (rel_distinct ~~ alpha_ts));
-val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
-((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_bn_ts))
 val alpha_eq_iff =
 if get_STEPS lthy > 5
-then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
+then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
 else raise TEST lthy4
-val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
 (* proving equivariance lemmas for bns, fvs and alpha *)
 val _ = warning "Proving equivariance";
 val (bv_eqvt, lthy5) =
 if get_STEPS lthy > 6
 then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) raw_bn_funs lthy4
 then prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5
 else raise TEST lthy5
 val (alpha_eqvt, lthy6a) =
 if get_STEPS lthy > 8
-then Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6
+then Nominal_Eqvt.equivariance alpha_trms alpha_induct alpha_intros lthy6
 else raise TEST lthy6
 (* proving alpha equivalence *)
 val _ = warning "Proving equivalence";
-val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts, alpha_bn_ts) bn_nos;
+val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos;
-val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
+val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy6a;
 val alpha_equivp =
-if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts
+if !cheat_equivp then map (equivp_hack lthy6a) alpha_trms
-else build_equivps alpha_ts reflps alpha_induct
+else build_equivps alpha_trms reflps alpha_induct
-inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a;
+inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy6a;
 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_tys alpha_ts alpha_equivp lthy6a;
+val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms 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)) =>
 map (fn (cname, dts) =>
 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
 val _ = warning "Proving respects";
-val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
+val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8;
 val (bns_rsp_pre, lthy9) = fold_map (
 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
 resolve_tac bns_rsp_pre' 1)) bns lthy8;
 val bns_rsp = flat (map snd bns_rsp_pre);
 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
 else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1;
-val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
+val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9;
 val (fv_rsp_pre, lthy10) = fold_map
 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9;
 val fv_rsp = flat (map snd fv_rsp_pre);
 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs
 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
 else
-let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_bn_ts lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
+let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
-alpha_bn_rsp_tac) alpha_bn_ts lthy11
+alpha_bn_rsp_tac) alpha_bn_trms lthy11
 fun const_rsp_tac _ =
-let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_bn_ts lthy11a
+let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a
-in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
 const_rsp_tac) raw_consts lthy11a
 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12;
 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
-val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_ts
+val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms
-val (qalpha_bn_ts, qalphabn_defs, lthy12c) =
+val (qalpha_bn_trms, qalphabn_defs, lthy12c) =
-quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_ts) lthy12b;
+quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_trms) lthy12b;
 val _ = warning "Lifting permutations";
 val thy = Local_Theory.exit_global lthy12c;
 val perm_names = map (fn x => "permute_" ^ x) qty_names
 val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) raw_perm_simps thy;
 val lthy13 = Theory_Target.init NONE thy';
 val lthy16 = note_simp_suffix "fv" q_fv lthy15;
 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
 val lthy17 = note_simp_suffix "bn" q_bn lthy16;
 val _ = warning "Lifting eq-iff";
 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
-val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff_simp
+val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff
 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0
 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded1;
 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0
 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1
 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2
 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
-val q_dis = map (lift_thm qtys lthy18) rel_dists;
+val q_dis = map (lift_thm qtys lthy18) alpha_distincts;
 val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt);
 val (_, lthy20) = Local_Theory.note ((Binding.empty,
 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 val _ = warning "Supports";
 val thy3 = Local_Theory.exit_global lthy20;
 val _ = warning "Instantiating FS";
 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
 val lthy22 = Class.prove_instantiation_instance tac lthy21
-val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts, qalpha_bn_ts) bn_nos;
+val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos;
 val (names, supp_eq_t) = supp_eq fv_alpha_all;
 val _ = warning "Support Equations";
 fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else
 supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>

changeset 2300	9fb315392493
parent 2299	09bbed4f21d6
child 2301	8732ff59068b