--- a/Nominal/Nominal2.thy Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Nominal2.thy Thu Dec 16 08:42:48 2010 +0000
@@ -6,6 +6,7 @@
("nominal_dt_quot.ML")
begin
+
use "nominal_dt_rawfuns.ML"
ML {* open Nominal_Dt_RawFuns *}
@@ -50,9 +51,10 @@
ML {*
-fun process_ecase lthy c (params, prems, concl) binders =
+fun process_ecase lthy c (params, prems, concl) bclauses =
let
val tys = map snd params
+ val binders = get_all_binders bclauses
fun prep_binder (opt, i) =
let
@@ -77,15 +79,21 @@
end
*}
+
ML {*
-fun fresh_thm ctxt c params binders bn_finite_thms =
+fun fresh_thm ctxt c parms binders bn_finite_thms =
let
fun prep_binder (opt, i) =
case opt of
- NONE => setify ctxt (nth params i)
- | SOME bn => to_set (bn $ (nth params i))
+ NONE => setify ctxt (nth parms i)
+ | SOME bn => to_set (bn $ (nth parms i))
- val rhs = HOLogic.mk_tuple (c :: params)
+ fun prep_binder2 (opt, i) =
+ case opt of
+ NONE => atomify ctxt (nth parms i)
+ | SOME bn => bn $ (nth parms i)
+
+ val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))
val lhs = binders
|> map prep_binder
|> fold_union
@@ -94,33 +102,99 @@
val goal = mk_fresh_star lhs rhs
|> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))
|> HOLogic.mk_Trueprop
- val ss = @{thms finite.emptyI finite.insertI finite_supp supp_Pair finite_Un finite_fset finite_set}
- @ bn_finite_thms
+
+ val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp}
+ @ @{thms finite.intros finite_Un finite_set finite_fset}
in
Goal.prove ctxt [] [] goal
(K (HEADGOAL (rtac @{thm at_set_avoiding1}
THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
end
+
+fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) =
+ case binders of
+ [] => []
+ | binders =>
+ let
+ val binder_trm = Nominal_Dt_Alpha.comb_binders ctxt bmode parms binders
+ val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
+ val body_ty = fastype_of body_trm
+
+ val (abs_name, binder_ty, abs_ty) =
+ case bmode of
+ Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})
+ | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set})
+ | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res})
+
+ 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))
+ |> 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}
+ 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))))]
+ end
+*}
+
+ML {*
+fun partitions [] [] = []
+ | partitions xs (i :: js) =
+ let
+ val (head, tail) = chop i xs
+ in
+ head :: partitions tail js
+ end
+*}
+
+
+ML {*
+fun mk_cperm ctxt p ctrm =
+ mk_perm (term_of p) (term_of ctrm)
+ |> cterm_of (ProofContext.theory_of ctxt)
+*}
+
+
+ML {*
+fun case_tac ctxt c bn_finite_thms (prems, bclausess) 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, ...} =>
+ let
+ val parms = map (term_of o snd) params
+ val fthm = fresh_thm ctxt c parms binders bn_finite_thms
+
+ val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
+ val (([(_, fperm)], fprops), ctxt') = Obtain.result
+ (K (EVERY1 [etac exE,
+ full_simp_tac (HOL_basic_ss addsimps ss),
+ REPEAT o (etac conjE)])) [fthm] ctxt
+ (*
+ val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops))
+ *)
+ val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses)
+ (*
+ val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs))
+ *)
+ in
+ (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*)
+ Skip_Proof.cheat_tac (ProofContext.theory_of ctxt')
+ end) ctxt
+ in
+ rtac thm THEN' RANGE (map2 aux_tac prems bclausess)
+ end
*}
ML {*
-fun case_tac ctxt c bn_finite_thms binderss thm =
- let
- fun aux_tac (binders : (term option * int) list)=
- Subgoal.FOCUS (fn {params, context, ...} =>
- let
- val prms = map (term_of o snd) params
- val fthm = fresh_thm ctxt c prms binders bn_finite_thms
- val _ = tracing ("params" ^ @{make_string} params)
- val _ = tracing ("binders" ^ @{make_string} binders)
- in
- Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)
- end) ctxt
- in
- rtac thm THEN' RANGE (map aux_tac binderss)
- end
-
fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms =
let
val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy
@@ -128,22 +202,22 @@
val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
val c = Free (c, TFree (a, @{sort fs}))
- val binderss = map (map get_all_binders) bclausesss
-
val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *)
|> map prop_of
|> map Logic.strip_horn
|> split_list
|>> map (map strip_params_prems_concl)
- val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat binderss)
-
- val _ = tracing ("binderss: " ^ @{make_string} binderss)
+ val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss)
in
Goal.prove_multi lthy'' [] prems main_concls
- (fn {prems, context} =>
- EVERY1 [Goal.conjunction_tac,
- RANGE (map2 (case_tac context c bn_finite_thms) binderss qexhausts')])
+ (fn {prems:thm list, context} =>
+ let
+ val prems' = partitions prems (map length bclausesss)
+ in
+ EVERY1 [Goal.conjunction_tac,
+ RANGE (map2 (case_tac context c bn_finite_thms) (prems' ~~ bclausesss) qexhausts')]
+ end)
end
*}
@@ -323,7 +397,7 @@
val raw_induct_thm = #induct dtinfo
val raw_induct_thms = #inducts dtinfo
val raw_exhaust_thms = map #exhaust dtinfos
- val raw_size_trms = map size_const raw_tys
+ val raw_size_trms = map HOLogic.size_const raw_tys
val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
|> `(fn thms => (length thms) div 2)
|> uncurry drop