diff -r d5713db7e146 -r dd7490fdd998 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Sun Dec 19 07:50:37 2010 +0000 +++ b/Nominal/Nominal2.thy Tue Dec 21 10:28:08 2010 +0000 @@ -116,7 +116,8 @@ ML {* (* derives abs_eq theorems of the form Exists s. [as].t = [p o as].s *) -fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) = +fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns + (bclause as (BC (bmode, binders, bodies))) = case binders of [] => [] | _ => @@ -133,37 +134,85 @@ val abs = Const (abs_name, [binder_ty, body_ty] ---> Type (abs_ty, [body_ty])) val abs_lhs = abs $ binder_trm $ body_trm - val abs_rhs = abs $ mk_perm p binder_trm $ Bound 0 - val goal = HOLogic.mk_eq (abs_lhs, abs_rhs) - |> (fn t => HOLogic.mk_exists ("y", body_ty, t)) + val abs_rhs = abs $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm + val abs_rhs' = abs $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm + val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) + val abs_eq' = HOLogic.mk_eq (abs_lhs, abs_rhs') + val eq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) + + val goal = HOLogic.mk_conj (abs_eq, eq) + |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |> HOLogic.mk_Trueprop + + val goal' = HOLogic.mk_conj (abs_eq', eq) + |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) + |> HOLogic.mk_Trueprop val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset - fresh_star_set} @ @{thms finite.intros finite_fset} + fresh_star_set} @ @{thms finite.intros finite_fset} in - [Goal.prove ctxt [] [] goal - (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} - THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))] + if is_recursive_binder bclause + then + (tracing "recursive"; + [ Goal.prove ctxt [] [] goal' + (K (HEADGOAL (resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} + THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss)))) + |> Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] + ]) + else + (tracing "non-recursive"; + [ Goal.prove ctxt [] [] goal + (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} + THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss)))) + |> Nominal_Permeq.eqvt_strict_rule ctxt permute_bns [] + ]) end *} - -(* FIXME: use pure cterm functions *) ML {* -fun mk_cperm ctxt p ctrm = - mk_perm (term_of p) (term_of ctrm) - |> cterm_of (ProofContext.theory_of ctxt) +fun conj_tac tac i = + let + fun select (t, i) = + case t of + @{term "Trueprop"} $ t' => select (t', i) + | @{term "op \"} $ _ $ _ => (rtac @{thm conjI} THEN' RANGE [conj_tac tac, conj_tac tac]) i + | _ => tac i + in + SUBGOAL select i + end *} +ML {* +fun is_abs_eq thm = + let + fun is_abs trm = + case (head_of trm) of + Const (@{const_name "Abs_set"}, _) => true + | Const (@{const_name "Abs_lst"}, _) => true + | Const (@{const_name "Abs_res"}, _) => true + | _ => false + in + thm |> prop_of + |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq + |> fst + |> is_abs + end +*} + +lemma setify: + shows "xs = ys \ set xs = set ys" + by simp ML {* -fun case_tac ctxt c bn_finite_thms (prems, bclausess) thm = +fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas + (prems, bclausess) qexhaust_thm = let fun aux_tac prem bclauses = case (get_all_binders bclauses) of [] => EVERY' [rtac prem, atac] - | binders => Subgoal.FOCUS (fn {params, prems, context = ctxt, ...} => + | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => let val parms = map (term_of o snd) params val fthm = fresh_thm ctxt c parms binders bn_finite_thms @@ -172,36 +221,76 @@ val (([(_, fperm)], fprops), ctxt') = Obtain.result (K (EVERY1 [etac exE, full_simp_tac (HOL_basic_ss addsimps ss), - REPEAT o (etac conjE)])) [fthm] ctxt + REPEAT o (etac @{thm conjE})])) [fthm] ctxt - val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses) + val abs_eq_thms = flat + (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses) + + val ((_, eqs), ctxt'') = Obtain.result + (K (EVERY1 + [ REPEAT o (etac @{thm exE}), + REPEAT o (etac @{thm conjE}), + REPEAT o (dtac @{thm setify}), + full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' + + val (abs_eqs, peqs) = split_filter is_abs_eq eqs + + val fprops' = map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops + val fprops'' = map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops - val _ = tracing ("test") - (* - val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops)) - *) - (* - val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs)) - *) + val _ = tracing ("prem:\n" ^ (Syntax.string_of_term ctxt'' o prop_of) prem) + val _ = tracing ("prems:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) prems)) + val _ = tracing ("fprop':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops')) + val _ = tracing ("fprop'':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops'')) + val _ = tracing ("abseq:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) abs_eqs)) + val _ = tracing ("peqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) peqs)) + + + val tac1 = EVERY' + [ simp_tac (HOL_basic_ss addsimps peqs), + rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), + K (print_tac "before solving freshness"), + conj_tac (TRY o DETERM o resolve_tac (fprops' @ fprops'')) ] + + val tac2 = EVERY' + [ rtac (@{thm ssubst} OF prems), + rewrite_goal_tac (map safe_mk_equiv eq_iff_thms), + K (print_tac "before substituting"), + rewrite_goal_tac (map safe_mk_equiv abs_eqs), + K (print_tac "after substituting"), + conj_tac (TRY o DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)), + K (print_tac "end") + ] + + val side_thm = Goal.prove ctxt'' [] [] (term_of concl) + (fn _ => (* Skip_Proof.cheat_tac (ProofContext.theory_of ctxt'') *) + EVERY + [ rtac prem 1, + print_tac "after applying prem", + RANGE [SOLVED' tac1, SOLVED' tac2] 1, + print_tac "final" ] ) + |> singleton (ProofContext.export ctxt'' ctxt) + + val _ = tracing ("side_thm:\n" ^ (Syntax.string_of_term ctxt o prop_of) side_thm) in - (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*) - Skip_Proof.cheat_tac (ProofContext.theory_of ctxt') + rtac side_thm 1 end) ctxt in - rtac thm THEN' RANGE (map2 aux_tac prems bclausess) + rtac qexhaust_thm THEN' RANGE (map2 aux_tac prems bclausess) end *} ML {* -fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms = +fun prove_strong_exhausts lthy exhausts qtrms bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns + perm_bn_alphas = let - val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy + val ((_, exhausts'), lthy') = Variable.import true exhausts lthy val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' val c = Free (c, TFree (a, @{sort fs})) - val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *) + val (ecases, main_concls) = exhausts' (* ecases or of the form (params, prems, concl) *) |> map prop_of |> map Logic.strip_horn |> split_list @@ -215,7 +304,8 @@ val prems' = partitions prems (map length bclausesss) in EVERY1 [Goal.conjunction_tac, - RANGE (map2 (case_tac context c bn_finite_thms) (prems' ~~ bclausesss) qexhausts')] + RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) + (prems' ~~ bclausesss) exhausts')] end) end *} @@ -582,7 +672,7 @@ (* defining of quotient term-constructors, binding functions, free vars functions *) val _ = warning "Defining the quotient constants" val qconstrs_descrs = - map2 (map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx))) (get_cnstrs dts) raw_constrs + (map2 o map2) (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) (get_cnstrs dts) raw_constrs val qbns_descr = map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns @@ -734,7 +824,9 @@ then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC else [] - val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms + val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms qeq_iffs' + qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms + (* noting the theorems *) @@ -917,7 +1009,7 @@ bcs @ (flat (map_range (add bcs) n)) end in - map2 (map2 complt) args bclauses + (map2 o map2) complt args bclauses end *}