# HG changeset patch # User berghofe # Date 1160756338 -7200 # Node ID 6f19e5eb3a44ae5a6e5dc6cf23dacdf0368f9bbc # Parent 9af9ceb16d584c06e47aaae498c97c3da3c0d40c Adapted to new inductive definition package. diff -r 9af9ceb16d58 -r 6f19e5eb3a44 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Fri Oct 13 18:15:18 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Fri Oct 13 18:18:58 2006 +0200 @@ -71,7 +71,7 @@ (term_frees t2) of [Free (s, T)] => absfree (s, T, t2) | _ => sys_error "indtac") - | SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2))) + | SOME (_ $ t') => Abs ("x", fastype_of t', abstract_over (t', t2))) val cert = cterm_of (Thm.sign_of_thm st); val Ps = map (cert o head_of o snd o getP) ts; val indrule' = cterm_instantiate (Ps ~~ @@ -145,6 +145,8 @@ val rev_simps = thms "rev.simps"; val app_simps = thms "op @.simps"; +val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq]; + fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy = let (* this theory is used just for parsing *) @@ -448,8 +450,8 @@ val _ = warning "representing sets"; - val rep_set_names = map (Sign.full_name thy3) (DatatypeProp.indexify_names - (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr)); + val rep_set_names = DatatypeProp.indexify_names + (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr); val big_rep_name = space_implode "_" (DatatypeProp.indexify_names (List.mapPartial (fn (i, ("Nominal.noption", _, _)) => NONE @@ -488,34 +490,37 @@ in (j + 1, j' + length Ts, case dt'' of DtRec k => list_all (map (pair "x") Us, - HOLogic.mk_Trueprop (HOLogic.mk_mem (free', - Const (List.nth (rep_set_names, k), - HOLogic.mk_setT T)))) :: prems + HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k), + T --> HOLogic.boolT) $ free')) :: prems | _ => prems, snd (foldr mk_abs_fun (j', free) Ts) :: ts) end; val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs; - val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem - (list_comb (Const (cname, map fastype_of ts ---> T), ts), - Const (s, HOLogic.mk_setT T))) + val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $ + list_comb (Const (cname, map fastype_of ts ---> T), ts)) in Logic.list_implies (prems, concl) end; - val (intr_ts, ind_consts) = - apfst List.concat (ListPair.unzip (List.mapPartial + val (intr_ts, (rep_set_names', recTs')) = + apfst List.concat (apsnd ListPair.unzip (ListPair.unzip (List.mapPartial (fn ((_, ("Nominal.noption", _, _)), _) => NONE | ((i, (_, _, constrs)), rep_set_name) => let val T = nth_dtyp i in SOME (map (make_intr rep_set_name T) constrs, - Const (rep_set_name, HOLogic.mk_setT T)) + (rep_set_name, T)) end) - (descr ~~ rep_set_names))); + (descr ~~ rep_set_names)))); + val rep_set_names'' = map (Sign.full_name thy3) rep_set_names'; val (thy4, {raw_induct = rep_induct, intrs = rep_intrs, ...}) = setmp InductivePackage.quiet_mode false - (InductivePackage.add_inductive_i false true big_rep_name false true false - ind_consts (map (fn x => (("", x), [])) intr_ts) []) thy3; + (TheoryTarget.init NONE #> + InductivePackage.add_inductive_i false big_rep_name false true false + (map (fn (s, T) => (s, SOME (T --> HOLogic.boolT), NoSyn)) + (rep_set_names' ~~ recTs')) + [] (map (fn x => (("", []), x)) intr_ts) [] #> + apfst (snd o LocalTheory.exit false)) thy3; (**** Prove that representing set is closed under permutation ****) @@ -528,16 +533,16 @@ fun mk_perm_closed name = map (fn th => standard (th RS mp)) (List.take (split_conj_thm (Goal.prove_global thy4 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map - (fn (S, x) => + (fn ((s, T), x) => let - val S = map_types (map_type_tfree - (fn (s, cs) => TFree (s, cs union cp_classes))) S; - val T = HOLogic.dest_setT (fastype_of S); + val T = map_type_tfree + (fn (s, cs) => TFree (s, cs union cp_classes)) T; + val S = Const (s, T --> HOLogic.boolT); val permT = mk_permT (Type (name, [])) - in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S), - HOLogic.mk_mem (Const ("Nominal.perm", permT --> T --> T) $ - Free ("pi", permT) $ Free (x, T), S)) - end) (ind_consts ~~ perm_indnames')))) + in HOLogic.mk_imp (S $ Free (x, T), + S $ (Const ("Nominal.perm", permT --> T --> T) $ + Free ("pi", permT) $ Free (x, T))) + end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))) (fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *) [indtac rep_induct [] 1, ALLGOALS (simp_tac (simpset_of thy4 addsimps @@ -556,10 +561,12 @@ val (typedefs, thy6) = thy5 - |> fold_map (fn ((((name, mx), tvs), c), name') => fn thy => + |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy => setmp TypedefPackage.quiet_mode true - (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE - (rtac exI 1 THEN + (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) + (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ + Const (cname, U --> HOLogic.boolT)) NONE + (rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) thy |> (fn ((_, r), thy) => let @@ -567,7 +574,6 @@ val pi = Free ("pi", permT); val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs; val T = Type (Sign.intern_type thy name, tvs'); - val Const (_, Type (_, [U])) = c in apfst (pair r o hd) (PureThy.add_defs_unchecked_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T), @@ -577,12 +583,13 @@ Free ("x", T))))), [])] thy) end)) (types_syntax ~~ tyvars ~~ - (List.take (ind_consts, length new_type_names)) ~~ new_type_names); + List.take (rep_set_names'' ~~ recTs', length new_type_names) ~~ + new_type_names); val perm_defs = map snd typedefs; - val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs; + val Abs_inverse_thms = map (collect_simp o #Abs_inverse o fst) typedefs; val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs; - val Rep_thms = map (#Rep o fst) typedefs; + val Rep_thms = map (collect_simp o #Rep o fst) typedefs; val big_name = space_implode "_" new_type_names; @@ -592,7 +599,7 @@ val _ = warning "prove that new types are in class pt_ ..."; fun pt_instance ((class, atom), perm_closed_thms) = - fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...}, + fold (fn ((((((Abs_inverse, Rep_inverse), Rep), perm_def), name), tvs), perm_closed) => fn thy => AxClass.prove_arity (Sign.intern_type thy name, @@ -604,7 +611,8 @@ [Rep RS perm_closed RS Abs_inverse]) 1, asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy (Name ("pt_" ^ Sign.base_name atom ^ "3"))]) 1]) thy) - (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms); + (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ + new_type_names ~~ tyvars ~~ perm_closed_thms); (** prove that new types are in class cp__ **) @@ -616,7 +624,7 @@ val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2; val class = Sign.intern_class thy name; val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1 - in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...}, + in fold (fn ((((((Abs_inverse, Rep), perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy => AxClass.prove_arity (Sign.intern_type thy name, @@ -630,8 +638,8 @@ cong_tac 1, rtac refl 1, rtac cp1' 1]) thy) - (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~ - perm_closed_thms2) thy + (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~ + tyvars ~~ perm_closed_thms1 ~~ perm_closed_thms2) thy end; val thy7 = fold (fn x => fn thy => thy |> @@ -697,9 +705,6 @@ val abs_names = map (fn s => Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names; - val recTs' = List.mapPartial - (fn ((_, ("Nominal.noption", _, _)), T) => NONE - | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts'); val recTs = get_rec_types descr'' sorts'; val newTs' = Library.take (length new_type_names, recTs'); val newTs = Library.take (length new_type_names, recTs); @@ -758,30 +763,21 @@ List.take (pdescr, length new_type_names) ~~ new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax); - val abs_inject_thms = map (fn tname => - PureThy.get_thm thy8 (Name ("Abs_" ^ tname ^ "_inject"))) new_type_names; - - val rep_inject_thms = map (fn tname => - PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inject"))) new_type_names; - - val rep_thms = map (fn tname => - PureThy.get_thm thy8 (Name ("Rep_" ^ tname))) new_type_names; - - val rep_inverse_thms = map (fn tname => - PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inverse"))) new_type_names; + val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs + val rep_inject_thms = map (#Rep_inject o fst) typedefs (* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *) fun prove_constr_rep_thm eqn = let val inj_thms = map (fn r => r RS iffD1) abs_inject_thms; - val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms + val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY [resolve_tac inj_thms 1, rewrite_goals_tac rewrites, rtac refl 3, resolve_tac rep_intrs 2, - REPEAT (resolve_tac rep_thms 1)]) + REPEAT (resolve_tac Rep_thms 1)]) end; val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns; @@ -790,7 +786,7 @@ fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th => let - val _ $ (_ $ (Rep $ x) $ _) = Logic.unvarify (prop_of th); + val _ $ (_ $ (Rep $ x)) = Logic.unvarify (prop_of th); val Type ("fun", [T, U]) = fastype_of Rep; val permT = mk_permT (Type (atom, [])); val pi = Free ("pi", permT); @@ -979,8 +975,8 @@ val Abs_t = Const (List.nth (abs_names, i), U --> T) - in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t, - Const (List.nth (rep_set_names, i), HOLogic.mk_setT U)) $ + in (prems @ [HOLogic.imp $ + (Const (List.nth (rep_set_names'', i), U --> HOLogic.boolT) $ Rep_t) $ (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) end; @@ -1359,17 +1355,20 @@ val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts'; val rec_fn_Ts = map (typ_subst_atomic (rec_result_Ts' ~~ rec_result_Ts)) rec_fn_Ts'; - val rec_set_Ts = map (fn (T1, T2) => rec_fn_Ts ---> HOLogic.mk_setT - (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts); + val rec_set_Ts = map (fn (T1, T2) => + rec_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts); val big_rec_name = big_name ^ "_rec_set"; - val rec_set_names = map (Sign.full_name (Theory.sign_of thy10)) - (if length descr'' = 1 then [big_rec_name] else - (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int) - (1 upto (length descr'')))); + val rec_set_names' = + if length descr'' = 1 then [big_rec_name] else + map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int) + (1 upto (length descr'')); + val rec_set_names = map (Sign.full_name (Theory.sign_of thy10)) rec_set_names'; val rec_fns = map (uncurry (mk_Free "f")) (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts))); + val rec_sets' = map (fn c => list_comb (Free c, rec_fns)) + (rec_set_names' ~~ rec_set_Ts); val rec_sets = map (fn c => list_comb (Const c, rec_fns)) (rec_set_names ~~ rec_set_Ts); @@ -1399,8 +1398,7 @@ val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~ map (fn (i, _) => List.nth (rec_result_Ts, i)) recs; val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop - (HOLogic.mk_mem (HOLogic.mk_prod (Free x, Free y), - List.nth (rec_sets, i)))) (recs ~~ frees''); + (List.nth (rec_sets', i) $ Free x $ Free y)) (recs ~~ frees''); val prems2 = map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop (Const ("Nominal.fresh", T --> fastype_of f --> HOLogic.boolT) $ @@ -1422,9 +1420,8 @@ val P = HOLogic.mk_Trueprop (p $ result) in (rec_intr_ts @ [Logic.list_implies (List.concat prems2 @ prems3 @ prems1, - HOLogic.mk_Trueprop (HOLogic.mk_mem - (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), map Free frees), - result), rec_set)))], + HOLogic.mk_Trueprop (rec_set $ + list_comb (Const (cname, Ts ---> T), map Free frees) $ result))], rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))], if null result_freshs then rec_prems' else rec_prems' @ [list_all_free (frees @ frees'', @@ -1437,12 +1434,16 @@ val (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, _) = Library.foldl (fn (x, ((((d, d'), T), p), rec_set)) => Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d')) - (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets); + (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets'); val (thy11, {intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}) = setmp InductivePackage.quiet_mode (!quiet_mode) - (InductivePackage.add_inductive_i false true big_rec_name false false false - rec_sets (map (fn x => (("", x), [])) rec_intr_ts) []) thy10; + (TheoryTarget.init NONE #> + InductivePackage.add_inductive_i false big_rec_name false false false + (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts)) + (map (apsnd SOME o dest_Free) rec_fns) + (map (fn x => (("", []), x)) rec_intr_ts) [] #> + apfst (snd o LocalTheory.exit false)) thy10; (** equivariance **) @@ -1462,8 +1463,7 @@ val x = Free ("x" ^ string_of_int i, T); val y = Free ("y" ^ string_of_int i, U) in - (HOLogic.mk_mem (HOLogic.mk_prod (x, y), R), - HOLogic.mk_mem (HOLogic.mk_prod (mk_perm [] (pi, x), mk_perm [] (pi, y)), R')) + (R $ x $ y, R' $ mk_perm [] (pi, x) $ mk_perm [] (pi, y)) end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs)); val ths = map (fn th => standard (th RS mp)) (split_conj_thm (Goal.prove_global thy11 [] [] @@ -1501,7 +1501,7 @@ val x = Free ("x" ^ string_of_int i, T); val y = Free ("y" ^ string_of_int i, U) in - HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (x, y), R), + HOLogic.mk_imp (R $ x $ y, HOLogic.mk_mem (Const ("Nominal.supp", U --> aset) $ y, finites)) end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs))))) (fn fins => (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT @@ -1543,12 +1543,9 @@ val y' = Free ("y'", U) in standard (Goal.prove (Context.init_proof thy11) [] (finite_prems @ - [HOLogic.mk_Trueprop (HOLogic.mk_mem - (HOLogic.mk_prod (x, y), R)), + [HOLogic.mk_Trueprop (R $ x $ y), HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U, - HOLogic.mk_imp (HOLogic.mk_mem - (HOLogic.mk_prod (x, y'), R), - HOLogic.mk_eq (y', y)))), + HOLogic.mk_imp (R $ x $ y', HOLogic.mk_eq (y', y)))), HOLogic.mk_Trueprop (Const ("Nominal.fresh", aT --> T --> HOLogic.boolT) $ a $ x)] @ freshs) @@ -1605,9 +1602,9 @@ val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees; val rec_unique_frees' = DatatypeProp.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts; - val rec_unique_concls = map (fn ((x as (_, T), U), R) => + val rec_unique_concls = map (fn ((x, U), R) => Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $ - Abs ("y", U, HOLogic.mk_mem (HOLogic.pair_const T U $ Free x $ Bound 0, R))) + Abs ("y", U, R $ Free x $ Bound 0)) (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets); val induct_aux_rec = Drule.cterm_instantiate @@ -1656,8 +1653,8 @@ (Goal.prove context (map fst (rec_unique_frees'' @ rec_unique_frees')) [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map (fn (((x, y), S), P) => HOLogic.mk_imp (HOLogic.mk_mem - (HOLogic.mk_prod (Free x, Free y), S), P $ (Free y))) + (map (fn (((x, y), S), P) => HOLogic.mk_imp + (S $ Free x $ Free y, P $ (Free y))) (rec_unique_frees'' ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds)))) (fn _ => rtac rec_induct 1 THEN @@ -1678,11 +1675,12 @@ (resolve_tac rec_intrs THEN_ALL_NEW atac) 1, rotate_tac ~1 1, ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac - (HOL_ss addsimps (Pair_eq :: List.concat distinct_thms))) 1] @ - (if null idxs then [] else [etac conjE 1, hyp_subst_tac 1, + (HOL_ss addsimps List.concat distinct_thms)) 1] @ + (if null idxs then [] else [hyp_subst_tac 1, SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} => let - val (_, prem) = split_last prems'; + val SOME prem = find_first (can (HOLogic.dest_eq o + HOLogic.dest_Trueprop o prop_of)) prems'; val _ $ (_ $ lhs $ rhs) = prop_of prem; val _ $ (_ $ lhs' $ rhs') = term_of concl; val rT = fastype_of lhs'; @@ -1696,7 +1694,7 @@ chop (length params div 2) (map term_of params); val params' = params1 @ params2; val rec_prems = filter (fn th => case prop_of th of - _ $ (Const ("op :", _) $ _ $ _) => true | _ => false) prems'; + _ $ (S $ _ $ _) => S mem rec_sets | _ => false) prems'; val fresh_prems = filter (fn th => case prop_of th of _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true | _ $ (Const ("Not", _) $ _) => true @@ -1777,7 +1775,7 @@ val _ = warning "step 6: (ts, pi1^-1 o pi2 o vs) in rec_set"; val rec_prems' = map (fn th => let - val _ $ (_ $ (_ $ x $ y) $ S) = prop_of th; + val _ $ (S $ x $ y) = prop_of th; val k = find_index (equal S) rec_sets; val pi = rpi1 @ pi2; fun mk_pi z = foldr (mk_perm []) z pi; @@ -1791,8 +1789,7 @@ cterm_of thy11 p)]) th; in rtac th' 1 end; val th' = Goal.prove context'' [] [] - (HOLogic.mk_Trueprop (HOLogic.mk_mem - (HOLogic.mk_prod (mk_pi x, mk_pi y), S))) + (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y)) (fn _ => EVERY (map eqvt_tac pi @ [simp_tac (HOL_ss addsimps (fresh_prems' @ freshs2' @ @@ -1829,9 +1826,9 @@ val (rec_freshs1, rec_freshs2) = ListPair.unzip (List.concat (map (fn (((rec_prem, rec_prem'), eqn), ih) => let - val _ $ (_ $ (_ $ x $ (y as Free (_, T))) $ S) = + val _ $ (S $ x $ (y as Free (_, T))) = prop_of rec_prem; - val _ $ (_ $ (_ $ _ $ y') $ _) = prop_of rec_prem'; + val _ $ (_ $ _ $ y') = prop_of rec_prem'; val k = find_index (equal S) rec_sets; val atoms = List.concat (List.mapPartial (fn ((bs, z), (bs', _)) => @@ -1941,7 +1938,7 @@ |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T, Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', - HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))) + set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)); (* prove characteristic equations for primrec combinators *) diff -r 9af9ceb16d58 -r 6f19e5eb3a44 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Oct 13 18:15:18 2006 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Oct 13 18:18:58 2006 +0200 @@ -108,24 +108,27 @@ val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))); val big_rec_name' = big_name ^ "_rec_set"; - val rec_set_names = map (Sign.full_name (Theory.sign_of thy0)) - (if length descr' = 1 then [big_rec_name'] else - (map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int) - (1 upto (length descr')))); + val rec_set_names' = + if length descr' = 1 then [big_rec_name'] else + map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int) + (1 upto (length descr')); + val rec_set_names = map (Sign.full_name (Theory.sign_of thy0)) rec_set_names'; val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used; - val rec_set_Ts = map (fn (T1, T2) => reccomb_fn_Ts ---> HOLogic.mk_setT - (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts); + val rec_set_Ts = map (fn (T1, T2) => + reccomb_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts); val rec_fns = map (uncurry (mk_Free "f")) (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts))); + val rec_sets' = map (fn c => list_comb (Free c, rec_fns)) + (rec_set_names' ~~ rec_set_Ts); val rec_sets = map (fn c => list_comb (Const c, rec_fns)) (rec_set_names ~~ rec_set_Ts); (* introduction rules for graph of primrec function *) - fun make_rec_intr T set_name ((rec_intr_ts, l), (cname, cargs)) = + fun make_rec_intr T rec_set ((rec_intr_ts, l), (cname, cargs)) = let fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) = let val free1 = mk_Free "x" U j @@ -135,9 +138,8 @@ val free2 = mk_Free "y" (Us ---> List.nth (rec_result_Ts, m)) k; val i = length Us in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all - (map (pair "x") Us, HOLogic.mk_mem (HOLogic.mk_prod - (app_bnds free1 i, app_bnds free2 i), - List.nth (rec_sets, m)))) :: prems, + (map (pair "x") Us, List.nth (rec_sets', m) $ + app_bnds free1 i $ app_bnds free2 i)) :: prems, free1::t1s, free2::t2s) end | _ => (j + 1, k, prems, free1::t1s, t2s)) @@ -146,19 +148,23 @@ val Ts = map (typ_of_dtyp descr' sorts) cargs; val (_, _, prems, t1s, t2s) = foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts) - in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem - (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s), - list_comb (List.nth (rec_fns, l), t1s @ t2s)), set_name)))], l + 1) + in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop + (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $ + list_comb (List.nth (rec_fns, l), t1s @ t2s)))], l + 1) end; val (rec_intr_ts, _) = Library.foldl (fn (x, ((d, T), set_name)) => Library.foldl (make_rec_intr T set_name) (x, #3 (snd d))) - (([], 0), descr' ~~ recTs ~~ rec_sets); + (([], 0), descr' ~~ recTs ~~ rec_sets'); val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) = setmp InductivePackage.quiet_mode (!quiet_mode) - (InductivePackage.add_inductive_i false true big_rec_name' false false true - rec_sets (map (fn x => (("", x), [])) rec_intr_ts) []) thy0; + (TheoryTarget.init NONE #> + InductivePackage.add_inductive_i false big_rec_name' false false true + (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts)) + (map (apsnd SOME o dest_Free) rec_fns) + (map (fn x => (("", []), x)) rec_intr_ts) [] #> + apfst (snd o LocalTheory.exit false)) thy0; (* prove uniqueness and termination of primrec combinators *) @@ -166,7 +172,7 @@ fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) = let - val distinct_tac = (etac Pair_inject 1) THEN + val distinct_tac = (if i < length newTs then full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1 else full_simp_tac dist_ss 1); @@ -185,7 +191,7 @@ REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1), etac elim 1, REPEAT_DETERM_N j distinct_tac, - etac Pair_inject 1, TRY (dresolve_tac inject 1), + TRY (dresolve_tac inject 1), REPEAT (etac conjE 1), hyp_subst_tac 1, REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]), TRY (hyp_subst_tac 1), @@ -203,9 +209,8 @@ let val rec_unique_ts = map (fn (((set_t, T1), T2), i) => Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $ - absfree ("y", T2, HOLogic.mk_mem (HOLogic.mk_prod - (mk_Free "x" T1 i, Free ("y", T2)), set_t))) - (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs)); + absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2))) + (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs)); val cert = cterm_of thy1 val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t)) ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts); @@ -241,7 +246,7 @@ |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T, Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', - HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))) + set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) ||> parent_path flat_names; diff -r 9af9ceb16d58 -r 6f19e5eb3a44 src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Fri Oct 13 18:15:18 2006 +0200 +++ b/src/HOL/Tools/datatype_aux.ML Fri Oct 13 18:18:58 2006 +0200 @@ -138,7 +138,7 @@ fun abstr (t1, t2) = (case t1 of NONE => let val [Free (s, T)] = add_term_frees (t2, []) in absfree (s, T, t2) end - | SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2))) + | SOME (_ $ t') => Abs ("x", fastype_of t', abstract_over (t', t2))) val cert = cterm_of (Thm.sign_of_thm st); val Ps = map (cert o head_of o snd o getP) ts; val indrule' = cterm_instantiate (Ps ~~ diff -r 9af9ceb16d58 -r 6f19e5eb3a44 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Oct 13 18:15:18 2006 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Oct 13 18:18:58 2006 +0200 @@ -27,6 +27,8 @@ val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); +val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq]; + (** theory context references **) @@ -65,10 +67,11 @@ val big_name = space_implode "_" new_type_names; val thy1 = add_path flat_names big_name thy; val big_rec_name = big_name ^ "_rep_set"; - val rep_set_names = map (Sign.full_name (Theory.sign_of thy1)) + val rep_set_names' = (if length descr' = 1 then [big_rec_name] else (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int) (1 upto (length descr')))); + val rep_set_names = map (Sign.full_name (Theory.sign_of thy1)) rep_set_names'; val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr); val leafTs' = get_nonrec_types descr' sorts; @@ -85,6 +88,8 @@ else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs; val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); val UnivT = HOLogic.mk_setT Univ_elT; + val UnivT' = Univ_elT --> HOLogic.boolT; + val Collect = Const ("Collect", UnivT' --> UnivT); val In0 = Const (In0_name, Univ_elT --> Univ_elT); val In1 = Const (In1_name, Univ_elT --> Univ_elT); @@ -149,8 +154,8 @@ val free_t = app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts) in (j + 1, list_all (map (pair "x") Ts, - HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t, - Const (List.nth (rep_set_names, k), UnivT)))) :: prems, + HOLogic.mk_Trueprop + (Free (List.nth (rep_set_names', k), UnivT') $ free_t)) :: prems, mk_lim free_t Ts :: ts) end | _ => @@ -159,32 +164,37 @@ end); val (_, prems, ts) = foldr mk_prem (1, [], []) cargs; - val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem - (mk_univ_inj ts n i, Const (s, UnivT))) + val concl = HOLogic.mk_Trueprop + (Free (s, UnivT') $ mk_univ_inj ts n i) in Logic.list_implies (prems, concl) end; - val consts = map (fn s => Const (s, UnivT)) rep_set_names; - val intr_ts = List.concat (map (fn ((_, (_, _, constrs)), rep_set_name) => map (make_intr rep_set_name (length constrs)) - ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names)); + ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names')); val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) = setmp InductivePackage.quiet_mode (!quiet_mode) - (InductivePackage.add_inductive_i false true big_rec_name false true false - consts (map (fn x => (("", x), [])) intr_ts) []) thy1; + (TheoryTarget.init NONE #> + InductivePackage.add_inductive_i false big_rec_name false true false + (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') [] + (map (fn x => (("", []), x)) intr_ts) [] #> + apfst (snd o LocalTheory.exit false)) thy1; (********************************* typedef ********************************) - val thy3 = add_path flat_names big_name (Library.foldl (fn (thy, ((((name, mx), tvs), c), name')) => - setmp TypedefPackage.quiet_mode true - (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE - (rtac exI 1 THEN - QUIET_BREADTH_FIRST (has_fewer_prems 1) - (resolve_tac rep_intrs 1))) thy |> snd) - (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ - (Library.take (length newTs, consts)) ~~ new_type_names)); + val (typedefs, thy3) = thy2 |> + parent_path flat_names |> + fold_map (fn ((((name, mx), tvs), c), name') => + setmp TypedefPackage.quiet_mode true + (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) + (Collect $ Const (c, UnivT')) NONE + (rtac exI 1 THEN rtac CollectI 1 THEN + QUIET_BREADTH_FIRST (has_fewer_prems 1) + (resolve_tac rep_intrs 1)))) + (types_syntax ~~ tyvars ~~ + (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||> + add_path flat_names big_name; (*********************** definition of constructors ***********************) @@ -257,47 +267,12 @@ val _ = message "Proving isomorphism properties ..."; - (* get axioms from theory *) - - val newT_iso_axms = map (fn s => - (get_thm thy4 (Name ("Abs_" ^ s ^ "_inverse")), - get_thm thy4 (Name ("Rep_" ^ s ^ "_inverse")), - get_thm thy4 (Name ("Rep_" ^ s)))) new_type_names; - - (*------------------------------------------------*) - (* prove additional theorems: *) - (* inj_on dt_Abs_i rep_set_i and inj dt_Rep_i *) - (*------------------------------------------------*) - - fun prove_newT_iso_inj_thm (((s, (thm1, thm2, _)), T), rep_set_name) = - let - val sg = Theory.sign_of thy4; - val RepT = T --> Univ_elT; - val Rep_name = Sign.intern_const sg ("Rep_" ^ s); - val AbsT = Univ_elT --> T; - val Abs_name = Sign.intern_const sg ("Abs_" ^ s); + val newT_iso_axms = map (fn (_, td) => + (collect_simp (#Abs_inverse td), #Rep_inverse td, + collect_simp (#Rep td))) typedefs; - val inj_Abs_thm = - Goal.prove_global sg [] [] - (HOLogic.mk_Trueprop - (Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $ - Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT))) - (fn _ => EVERY [rtac inj_on_inverseI 1, etac thm1 1]); - - val setT = HOLogic.mk_setT T - - val inj_Rep_thm = - Goal.prove_global sg [] [] - (HOLogic.mk_Trueprop - (Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $ - Const (Rep_name, RepT) $ Const ("UNIV", setT))) - (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1]); - - in (inj_Abs_thm, inj_Rep_thm) end; - - val newT_iso_inj_thms = map prove_newT_iso_inj_thm - (new_type_names ~~ newT_iso_axms ~~ newTs ~~ - Library.take (length newTs, rep_set_names)); + val newT_iso_inj_thms = map (fn (_, td) => + (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs; (********* isomorphisms between existing types and "unfolded" types *******) @@ -385,7 +360,7 @@ fun mk_funs_inv thm = let val {sign, prop, ...} = rep_thm thm; - val _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $ + val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $ (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop; val used = add_term_tfree_names (a, []); @@ -396,7 +371,7 @@ val f = Free ("f", Ts ---> U) in Goal.prove_global sign [] [] (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.list_all - (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))), + (map (pair "x") Ts, S $ app_bnds f i)), HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts, r $ (a $ app_bnds f i)), f)))) (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1]) @@ -418,14 +393,14 @@ in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $ HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $ HOLogic.mk_eq (mk_Free "x" T i, Bound 0)), - HOLogic.mk_mem (Rep_t $ mk_Free "x" T i, Const (rep_set_name, UnivT))) + Const (rep_set_name, UnivT') $ (Rep_t $ mk_Free "x" T i)) end; val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds); val rewrites = map mk_meta_eq iso_char_thms; - val inj_thms' = map (fn r => r RS injD) - (map snd newT_iso_inj_thms @ inj_thms); + val inj_thms' = map snd newT_iso_inj_thms @ + map (fn r => r RS injD) inj_thms; val inj_thm = Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY @@ -465,14 +440,15 @@ val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms ([], map #3 newT_iso_axms) (tl descr); - val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded; + val iso_inj_thms = map snd newT_iso_inj_thms @ + map (fn r => r RS injD) iso_inj_thms_unfolded; - (* prove x : dt_rep_set_i --> x : range dt_Rep_i *) + (* prove dt_rep_set_i x --> x : range dt_Rep_i *) fun mk_iso_t (((set_name, iso_name), i), T) = let val isoT = T --> Univ_elT in HOLogic.imp $ - HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const (set_name, UnivT)) $ + (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $ (if i < length newTs then Const ("True", HOLogic.boolT) else HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $ @@ -517,12 +493,12 @@ fun prove_constr_rep_thm eqn = let - val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms; + val inj_thms = map fst newT_iso_inj_thms; val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms) in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY [resolve_tac inj_thms 1, rewrite_goals_tac rewrites, - rtac refl 1, + rtac refl 3, resolve_tac rep_intrs 2, REPEAT (resolve_tac iso_elem_thms 1)]) end; @@ -559,7 +535,7 @@ fun prove_constr_inj_thm rep_thms t = let val inj_thms = Scons_inject :: (map make_elim - ((map (fn r => r RS injD) iso_inj_thms) @ + (iso_inj_thms @ [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject, Suml_inject, Sumr_inject])) in Goal.prove_global thy5 [] [] t (fn _ => EVERY @@ -601,8 +577,8 @@ else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $ Const (List.nth (all_rep_names, i), T --> Univ_elT) - in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t, - Const (List.nth (rep_set_names, i), UnivT)) $ + in (prems @ [HOLogic.imp $ + (Const (List.nth (rep_set_names, i), UnivT') $ Rep_t) $ (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) end;