--- a/Nominal/Ex/Lambda.thy Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/Ex/Lambda.thy Tue Jul 19 01:40:36 2011 +0100
@@ -46,13 +46,10 @@
termination (eqvt) by lexicographic_order
ML {*
-Item_Net.content;
-Nominal_Function_Common.get_function
+Item_Net.content (Nominal_Function_Common.get_function @{context})
*}
-ML {*
-Item_Net.content (Nominal_Function_Common.get_function @{context})
-*}
+thm is_app_def
lemma [eqvt]:
@@ -165,6 +162,11 @@
apply(rule refl)
done
+thm inl_eqvt
+thm var_pos_def
+
+thm fun_eq_iff
+
termination (eqvt) by lexicographic_order
lemma var_pos1:
--- a/Nominal/Ex/LetRec.thy Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/Ex/LetRec.thy Tue Jul 19 01:40:36 2011 +0100
@@ -59,6 +59,16 @@
apply (simp add: permute_fun_def)
done
+ML {*
+let
+ val [t1, t2] = Item_Net.content (Nominal_Function_Common.get_function @{context})
+in
+ (#eqvts (snd t1),
+ #eqvts (snd t2))
+end
+*}
+
+
thm height_trm_def height_bp_def
termination (eqvt) by lexicographic_order
--- a/Nominal/nominal_function.ML Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/nominal_function.ML Tue Jul 19 01:40:36 2011 +0100
@@ -156,9 +156,6 @@
termination, domintros, cases, eqvts, ...} =
cont (Thm.close_derivation proof)
- val _ = tracing ("final psimps:\n" ^ cat_lines (map @{make_string} psimps))
- val _ = tracing ("final eqvts:\n" ^ cat_lines (map @{make_string} eqvts))
-
val fnames = map (fst o fst) fixes
fun qualify n = Binding.name n
|> Binding.qualify true defname
@@ -184,8 +181,6 @@
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
- val _ = tracing ("final final psimps:\n" ^ cat_lines (map @{make_string} psimps'))
-
val _ =
if not is_external then ()
else Specification.print_consts lthy (K false) (map fst fixes)
--- a/Nominal/nominal_function_common.ML Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/nominal_function_common.ML Tue Jul 19 01:40:36 2011 +0100
@@ -58,7 +58,7 @@
fs = map term fs, R = term R, psimps = fact psimps,
pinducts = fact pinducts, simps = Option.map fact simps,
inducts = Option.map fact inducts, termination = thm termination,
- defname = name defname, is_partial=is_partial, eqvts = (*fact*) eqvts }
+ defname = name defname, is_partial=is_partial, eqvts = fact eqvts }
end
structure NominalFunctionData = Generic_Data
--- a/Nominal/nominal_function_core.ML Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/nominal_function_core.ML Tue Jul 19 01:40:36 2011 +0100
@@ -1053,16 +1053,15 @@
let
val newthy = theory_of_thm provedgoal (*FIXME*)
- val (graph_is_function, complete_thm) =
+ val ((graph_is_function, complete_thm), graph_is_eqvt) =
provedgoal
- |> fst o Conjunction.elim
- |> fst o Conjunction.elim
|> Conjunction.elim
- |> apfst (Thm.forall_elim_vars 0)
+ |>> fst o Conjunction.elim
+ |>> Conjunction.elim
+ |>> apfst (Thm.forall_elim_vars 0)
val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
-
- val f_eqvt = graph_is_function RS (G_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
+ val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
val psimps = PROFILE "Proving simplification rules"
(mk_psimps newthy globals R xclauses values f_iff) graph_is_function
--- a/Nominal/nominal_mutual.ML Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/nominal_mutual.ML Tue Jul 19 01:40:36 2011 +0100
@@ -38,7 +38,6 @@
fvar : string * typ,
cargTs: typ list,
f_def: term,
-
f: term option,
f_defthm : thm option}
@@ -184,14 +183,13 @@
import (export : thm -> thm) sum_psimp_eq =
let
val (MutualPart {f=SOME f, ...}) = get_part fname parts
-
+
val psimp = import sum_psimp_eq
val (simp, restore_cond) =
case cprems_of psimp of
[] => (psimp, I)
| [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
| _ => raise General.Fail "Too many conditions"
-
in
Goal.prove ctxt [] []
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
@@ -202,6 +200,31 @@
|> export
end
+fun mk_meqvts ctxt eqvt_thm f_defs =
+ let
+ val ctrm1 = eqvt_thm
+ |> cprop_of
+ |> snd o Thm.dest_implies
+ |> Thm.dest_arg
+ |> Thm.dest_arg1
+ |> Thm.dest_arg
+
+ fun resolve f_def =
+ let
+ val ctrm2 = f_def
+ |> cprop_of
+ |> Thm.dest_equals_lhs
+ in
+ eqvt_thm
+ |> Thm.instantiate (Thm.match (ctrm1, ctrm2))
+ |> simplify (HOL_basic_ss addsimps (@{thm Pair_eqvt} :: @{thms permute_sum.simps}))
+ |> Local_Defs.unfold ctxt [f_def]
+ end
+ in
+ map resolve f_defs
+ end
+
+
fun mk_applied_form ctxt caTs thm =
let
val thy = ProofContext.theory_of ctxt
@@ -256,14 +279,7 @@
let
val result = inner_cont proof
val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
- termination, domintros, eqvts,...} = result
-
- (*
- val _ = tracing ("premutual induct:\n" ^ @{make_string} simple_pinduct)
- val _ = tracing ("premutual termination:\n" ^ @{make_string} termination)
- val _ = tracing ("premutual psimps:\n" ^ cat_lines (map @{make_string} psimps))
- val _ = tracing ("premutual eqvts:\n" ^ cat_lines (map @{make_string} eqvts))
- *)
+ termination, domintros, eqvts=[eqvt],...} = result
val (all_f_defs, fs) =
map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -282,17 +298,12 @@
val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
val mtermination = full_simplify rew_ss termination
val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
-
- (*
- val _ = tracing ("postmutual psimps:\n" ^ cat_lines (map @{make_string} mpsimps))
- val _ = tracing ("postmutual induct:\n" ^ cat_lines (map @{make_string} minducts))
- val _ = tracing ("postmutual termination:\n" ^ @{make_string} mtermination)
- *)
- in
+ val meqvts = mk_meqvts lthy eqvt all_f_defs
+ in
NominalFunctionResult { fs=fs, G=G, R=R,
psimps=mpsimps, simple_pinducts=minducts,
cases=cases, termination=mtermination,
- domintros=mdomintros, eqvts=eqvts }
+ domintros=mdomintros, eqvts=meqvts }
end
(* nominal *)