# HG changeset patch # User berghofe # Date 1201170414 -3600 # Node ID 6ebe26bfed18a947d42de23b87da1dcfd67e4660 # Parent a3067f6f08a2548f67afe09f58e4ba6859ec3d31 Reimplemented proof of strong induction theorem. diff -r a3067f6f08a2 -r 6ebe26bfed18 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Thu Jan 24 11:23:11 2008 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Thu Jan 24 11:26:54 2008 +0100 @@ -122,21 +122,6 @@ (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg in (Ts @ [T], add_typ_tfrees (T, sorts)) end; -fun mk_subgoal i f st = - let - val cg = List.nth (cprems_of st, i - 1); - val g = term_of cg; - val revcut_rl' = Thm.lift_rule cg revcut_rl; - val v = head_of (Logic.strip_assums_concl (hd (prems_of revcut_rl'))); - val ps = Logic.strip_params g; - val cert = cterm_of (Thm.theory_of_thm st); - in - compose_tac (false, - Thm.instantiate ([], [(cert v, cert (list_abs (ps, - f (rev ps) (Logic.strip_assums_hyp g) (Logic.strip_assums_concl g))))]) - revcut_rl', 2) i st - end; - (** simplification procedure for sorting permutations **) val dj_cp = thm "dj_cp"; @@ -186,6 +171,9 @@ val supp_def = thm "supp_def"; val rev_simps = thms "rev.simps"; val app_simps = thms "append.simps"; +val at_fin_set_supp = thm "at_fin_set_supp"; +val at_fin_set_fresh = thm "at_fin_set_fresh"; +val abs_fun_eq1 = thm "abs_fun_eq1"; val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq]; @@ -204,7 +192,7 @@ end; fun mk_not_sym ths = maps (fn th => case prop_of th of - _ $ (Const ("Not", _) $ _) => [th, th RS not_sym] + _ $ (Const ("Not", _) $ (Const ("op =", _) $ _ $ _)) => [th, th RS not_sym] | _ => [th]) ths; fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT); @@ -585,6 +573,8 @@ val _ = warning "proving closure under permutation..."; + val abs_perm = PureThy.get_thms thy4 (Name "abs_perm"); + val perm_indnames' = List.mapPartial (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x) (perm_indnames ~~ descr); @@ -605,7 +595,7 @@ (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 - (symmetric perm_fun_def :: PureThy.get_thms thy4 (Name ("abs_perm"))))), + (symmetric perm_fun_def :: abs_perm))), ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW (asm_full_simp_tac (simpset_of thy4 addsimps [perm_fun_def])))])), length new_type_names)); @@ -885,8 +875,6 @@ (** prove equations for permutation functions **) - val abs_perm = PureThy.get_thms thy8 (Name "abs_perm"); (* FIXME *) - val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) => let val T = nth_dtyp' i in List.concat (map (fn (atom, perm_closed_thms) => @@ -1220,153 +1208,156 @@ (Free (tname, T)))) (descr'' ~~ recTs ~~ tnames))); - fun mk_ind_perm i k p l vs j = - let - val n = length vs; - val Ts = map snd vs; - val T = List.nth (Ts, i - j); - val pT = NominalAtoms.mk_permT T - in - Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $ - (HOLogic.pair_const T T $ Bound (l - j) $ fold_rev (mk_perm Ts) - (map (mk_ind_perm i k p l vs) (j - 1 downto 0) @ - map Bound (n - k - 1 downto n - k - p)) - (Bound (i - j))) $ - Const ("List.list.Nil", pT) - end; + val fin_set_supp = map (fn Type (s, _) => + PureThy.get_thm thy9 (Name ("at_" ^ Sign.base_name s ^ "_inst")) RS + at_fin_set_supp) dt_atomTs; + val fin_set_fresh = map (fn Type (s, _) => + PureThy.get_thm thy9 (Name ("at_" ^ Sign.base_name s ^ "_inst")) RS + at_fin_set_fresh) dt_atomTs; + val pt1_atoms = map (fn Type (s, _) => + PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "1"))) dt_atomTs; + val pt2_atoms = map (fn Type (s, _) => + PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "2")) RS sym) dt_atomTs; + val exists_fresh' = PureThy.get_thms thy9 (Name "exists_fresh'"); + val fs_atoms = PureThy.get_thms thy9 (Name "fin_supp"); + val abs_supp = PureThy.get_thms thy9 (Name "abs_supp"); + val perm_fresh_fresh = PureThy.get_thms thy9 (Name "perm_fresh_fresh"); + val calc_atm = PureThy.get_thms thy9 (Name "calc_atm"); + val fresh_atm = PureThy.get_thms thy9 (Name "fresh_atm"); + val fresh_left = PureThy.get_thms thy9 (Name "fresh_left"); + val perm_swap = PureThy.get_thms thy9 (Name "perm_swap"); - fun mk_fresh i i' j k p l is vs _ _ = + fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) = let - val n = length vs; - val Ts = map snd vs; - val T = List.nth (Ts, n - i - 1 - j); - val f = the (AList.lookup op = fresh_fs T); - val U = List.nth (Ts, n - i' - 1); - val S = HOLogic.mk_setT T; - val prms' = map Bound (n - k downto n - k - p + 1); - val prms = map (mk_ind_perm (n - i) k p (n - l) (("a", T) :: vs)) - (j - 1 downto 0) @ prms'; - val bs = rev (List.mapPartial - (fn ((_, T'), i) => if T = T' then SOME (Bound i) else NONE) - (List.take (vs, n - k - p - 1) ~~ (1 upto n - k - p - 1))); - val ts = map (fn i => - Const ("Nominal.supp", List.nth (Ts, n - i - 1) --> S) $ - fold_rev (mk_perm (T :: Ts)) prms' (Bound (n - i))) is + val p = foldr1 HOLogic.mk_prod (ts @ freshs1); + val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop + (HOLogic.exists_const T $ Abs ("x", T, + fresh_const T (fastype_of p) $ + Bound 0 $ p))) + (fn _ => EVERY + [resolve_tac exists_fresh' 1, + simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @ + fin_set_supp @ ths)) 1]); + val (([cx], ths), ctxt') = Obtain.result + (fn _ => EVERY + [etac exE 1, + full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1, + REPEAT (etac conjE 1)]) + [ex] ctxt + in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end; + + fun fresh_fresh_inst thy a b = + let + val T = fastype_of a; + val SOME th = find_first (fn th => case prop_of th of + _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T + | _ => false) perm_fresh_fresh in - HOLogic.mk_Trueprop (Const ("Ex", (T --> HOLogic.boolT) --> HOLogic.boolT) $ - Abs ("a", T, HOLogic.Not $ - (Const ("op :", T --> S --> HOLogic.boolT) $ Bound 0 $ - (foldr (fn (t, u) => Const ("insert", T --> S --> S) $ t $ u) - (foldl (fn (t, u) => Const ("op Un", S --> S --> S) $ u $ t) - (f $ Bound (n - k - p)) - (Const ("Nominal.supp", U --> S) $ - fold_rev (mk_perm (T :: Ts)) prms (Bound (n - i')) :: ts)) - (fold_rev (mk_perm (T :: Ts)) prms (Bound (n - i - j)) :: bs))))) + Drule.instantiate' [] + [SOME (cterm_of thy a), NONE, SOME (cterm_of thy b)] th end; - fun mk_fresh_constr is p vs _ concl = - let - val n = length vs; - val Ts = map snd vs; - val _ $ (_ $ _ $ t) = concl; - val c = head_of t; - val T = body_type (fastype_of c); - val k = foldr op + 0 (map (fn (_, i) => i + 1) is); - val ps = map Bound (n - k - 1 downto n - k - p); - val (_, _, ts, us) = foldl (fn ((_, i), (m, n, ts, us)) => - (m - i - 1, n - i, - ts @ map Bound (n downto n - i + 1) @ [fold_rev (mk_perm Ts) - (map (mk_ind_perm m k p n vs) (i - 1 downto 0) @ ps) - (Bound (m - i))], - us @ map (fn j => fold_rev (mk_perm Ts) ps (Bound j)) (m downto m - i))) - (n - 1, n - k - p - 2, [], []) is - in - HOLogic.mk_Trueprop (HOLogic.eq_const T $ list_comb (c, ts) $ list_comb (c, us)) - end; - - val abs_fun_finite_supp = PureThy.get_thm thy9 (Name "abs_fun_finite_supp"); - - val at_finite_select = PureThy.get_thm thy9 (Name "at_finite_select"); - - val induct_aux_lemmas = List.concat (map (fn Type (s, _) => - [PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "_inst")), - PureThy.get_thm thy9 (Name ("fs_" ^ Sign.base_name s ^ "1")), - PureThy.get_thm thy9 (Name ("at_" ^ Sign.base_name s ^ "_inst"))]) dt_atomTs); - - val induct_aux_lemmas' = map (fn Type (s, _) => - PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "2")) RS sym) dt_atomTs; - - val fresh_aux = PureThy.get_thms thy9 (Name "fresh_aux"); - (********************************************************************** The subgoals occurring in the proof of induct_aux have the following parameters: - x_1 ... x_k p_1 ... p_m z b_1 ... b_n + x_1 ... x_k p_1 ... p_m z where x_i : constructor arguments (introduced by weak induction rule) p_i : permutations (one for each atom type in the data type) z : freshness context - b_i : newly introduced names for binders (sufficiently fresh) ***********************************************************************) val _ = warning "proving strong induction theorem ..."; - val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' - (fn prems => EVERY - ([mk_subgoal 1 (K (K (K aux_ind_concl))), - indtac dt_induct tnames 1] @ - List.concat (map (fn ((_, (_, _, constrs)), (_, constrs')) => - List.concat (map (fn ((cname, cargs), is) => - [simp_tac (HOL_basic_ss addsimps List.concat perm_simps') 1, - REPEAT (rtac allI 1)] @ - List.concat (map - (fn ((_, 0), _) => [] - | ((i, j), k) => List.concat (map (fn j' => + val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' (fn prems => + let + val (prems1, prems2) = chop (length dt_atomTs) prems; + val ind_ss2 = HOL_ss addsimps + finite_Diff :: abs_fresh @ abs_supp @ fs_atoms; + val ind_ss1 = ind_ss2 addsimps fresh_left @ calc_atm @ + fresh_atm @ rev_simps @ app_simps; + val ind_ss3 = HOL_ss addsimps abs_fun_eq1 :: + abs_perm @ calc_atm @ perm_swap; + val ind_ss4 = HOL_basic_ss addsimps fresh_left @ prems1 @ + fin_set_fresh @ calc_atm; + val ind_ss5 = HOL_basic_ss addsimps pt1_atoms; + val ind_ss6 = HOL_basic_ss addsimps flat perm_simps'; + val th = Goal.prove (ProofContext.init thy9) [] [] aux_ind_concl + (fn {context = context1, ...} => + EVERY (indtac dt_induct tnames 1 :: + maps (fn ((_, (_, _, constrs)), (_, constrs')) => + map (fn ((cname, cargs), is) => + REPEAT (rtac allI 1) THEN + SUBPROOF (fn {prems = iprems, params, concl, + context = context2, ...} => let - val DtType (tname, _) = List.nth (cargs, i + j'); - val atom = Sign.base_name tname + val concl' = term_of concl; + val _ $ (_ $ _ $ u) = concl'; + val U = fastype_of u; + val (xs, params') = + chop (length cargs) (map term_of params); + val Ts = map fastype_of xs; + val cnstr = Const (cname, Ts ---> U); + val (pis, z) = split_last params'; + val mk_pi = fold_rev (mk_perm []) pis; + val xs' = partition_cargs is xs; + val xs'' = map (fn (ts, u) => (map mk_pi ts, mk_pi u)) xs'; + val ts = maps (fn (ts, u) => ts @ [u]) xs''; + val (freshs1, freshs2, context3) = fold (fn t => + let val T = fastype_of t + in obtain_fresh_name' prems1 + (the (AList.lookup op = fresh_fs T) $ z :: ts) T + end) (maps fst xs') ([], [], context2); + val freshs1' = unflat (map fst xs') freshs1; + val freshs2' = map (Simplifier.simplify ind_ss4) + (mk_not_sym freshs2); + val ind_ss1' = ind_ss1 addsimps freshs2'; + val ind_ss3' = ind_ss3 addsimps freshs2'; + val rename_eq = + if forall (null o fst) xs' then [] + else [Goal.prove context3 [] [] + (HOLogic.mk_Trueprop (HOLogic.mk_eq + (list_comb (cnstr, ts), + list_comb (cnstr, maps (fn ((bs, t), cs) => + cs @ [fold_rev (mk_perm []) (map perm_of_pair + (bs ~~ cs)) t]) (xs'' ~~ freshs1'))))) + (fn _ => EVERY + (simp_tac (HOL_ss addsimps flat inject_thms) 1 :: + REPEAT (FIRSTGOAL (rtac conjI)) :: + maps (fn ((bs, t), cs) => + if null bs then [] + else rtac sym 1 :: maps (fn (b, c) => + [rtac trans 1, rtac sym 1, + rtac (fresh_fresh_inst thy9 b c) 1, + simp_tac ind_ss1' 1, + simp_tac ind_ss2 1, + simp_tac ind_ss3' 1]) (bs ~~ cs)) + (xs'' ~~ freshs1')))]; + val th = Goal.prove context3 [] [] concl' (fn _ => EVERY + [simp_tac (ind_ss6 addsimps rename_eq) 1, + cut_facts_tac iprems 1, + (resolve_tac prems THEN_ALL_NEW + SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of + _ $ (Const ("Nominal.fresh", _) $ _ $ _) => + simp_tac ind_ss1' i + | _ $ (Const ("Not", _) $ _) => + resolve_tac freshs2' i + | _ => asm_simp_tac (HOL_basic_ss addsimps + pt2_atoms addsimprocs [perm_simproc]) i)) 1]) + val final = ProofContext.export context3 context2 [th] in - [mk_subgoal 1 (mk_fresh i (i + j) j' - (length cargs) (length dt_atomTs) - (length cargs + length dt_atomTs + 1 + i - k) - (List.mapPartial (fn (i', j) => - if i = i' then NONE else SOME (i' + j)) is)), - rtac at_finite_select 1, - rtac (PureThy.get_thm thy9 (Name ("at_" ^ atom ^ "_inst"))) 1, - asm_full_simp_tac (simpset_of thy9 addsimps - [PureThy.get_thm thy9 (Name ("fs_" ^ atom ^ "1"))]) 1, - resolve_tac prems 1, - etac exE 1, - asm_full_simp_tac (simpset_of thy9 addsimps - [symmetric fresh_def]) 1] - end) (0 upto j - 1))) (is ~~ (0 upto length is - 1))) @ - (if exists (not o equal 0 o snd) is then - [mk_subgoal 1 (mk_fresh_constr is (length dt_atomTs)), - asm_full_simp_tac (simpset_of thy9 addsimps - (List.concat inject_thms @ - alpha @ abs_perm @ abs_fresh @ [abs_fun_finite_supp] @ - induct_aux_lemmas)) 1, - dtac sym 1, - asm_full_simp_tac (simpset_of thy9) 1, - REPEAT (etac conjE 1)] - else - []) @ - [(resolve_tac prems THEN_ALL_NEW - (atac ORELSE' - SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of - _ $ (Const ("Nominal.fresh", _) $ _ $ _) => - asm_simp_tac (simpset_of thy9 addsimps fresh_aux) i - | _ => - asm_simp_tac (simpset_of thy9 - addsimps induct_aux_lemmas' - addsimprocs [perm_simproc]) i))) 1]) - (constrs ~~ constrs'))) (descr'' ~~ ndescr)) @ - [REPEAT (eresolve_tac [conjE, allE_Nil] 1), - REPEAT (etac allE 1), - REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac (simpset_of thy9) 1)])); + resolve_tac final 1 + end) context1 1) (constrs ~~ constrs')) (descr'' ~~ ndescr))) + in + EVERY + [cut_facts_tac [th] 1, + REPEAT (eresolve_tac [conjE, allE_Nil] 1), + REPEAT (etac allE 1), + REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)] + end); val induct_aux' = Thm.instantiate ([], map (fn (s, T) => @@ -1382,7 +1373,7 @@ val induct = Goal.prove_global thy9 [] ind_prems ind_concl (fn prems => EVERY [rtac induct_aux' 1, - REPEAT (resolve_tac induct_aux_lemmas 1), + REPEAT (resolve_tac fs_atoms 1), REPEAT ((resolve_tac prems THEN_ALL_NEW (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)]) @@ -1569,9 +1560,6 @@ (** freshness **) - val perm_fresh_fresh = PureThy.get_thms thy11 (Name "perm_fresh_fresh"); - val perm_swap = PureThy.get_thms thy11 (Name "perm_swap"); - val finite_premss = map (fn aT => map (fn (f, T) => HOLogic.mk_Trueprop (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $ @@ -1636,13 +1624,6 @@ (** uniqueness **) - val exists_fresh' = PureThy.get_thms thy11 (Name "exists_fresh'"); - val fs_atoms = map (fn Type (s, _) => PureThy.get_thm thy11 - (Name ("fs_" ^ Sign.base_name s ^ "1"))) dt_atomTs; - val fresh_atm = PureThy.get_thms thy11 (Name "fresh_atm"); - val calc_atm = PureThy.get_thms thy11 (Name "calc_atm"); - val fresh_left = PureThy.get_thms thy11 (Name "fresh_left"); - val fun_tuple = foldr1 HOLogic.mk_prod (rec_ctxt :: rec_fns); val fun_tupleT = fastype_of fun_tuple; val rec_unique_frees =