--- 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 \<and>"} $ _ $ _ => (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 \<Longrightarrow> 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
*}