# HG changeset patch # User Christian Urban # Date 1400514346 -3600 # Node ID e2da10806a346867a6fd70ea253ce0ffa4d7ab0d # Parent 5ebd327ffb96d118e923d20540020d236216b971 changed nominal_primrec to nominal_function and termination to nominal_termination diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/AuxNoFCB.thy --- a/Nominal/Ex/AuxNoFCB.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/AuxNoFCB.thy Mon May 19 16:45:46 2014 +0100 @@ -15,7 +15,7 @@ apply (rule, perm_simp, rule, rule) by pat_completeness auto -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order nominal_function lam2_rec where "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs" @@ -74,7 +74,7 @@ apply simp done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma lam_rec2_cong[fundef_cong]: "(\s1 s2 s3 s4. l = App s1 s2 \ l2 = App s3 s4 \ faa s1 s2 s3 s4 = faa' s1 s2 s3 s4) \ @@ -106,7 +106,7 @@ apply (rule, perm_simp, rule, rule) by pat_completeness auto -termination (eqvt) +nominal_termination (eqvt) by (relation "measure (\(l, r, xs). size l + size r)") simp_all lemma aux_simps[simp]: @@ -233,7 +233,7 @@ apply (simp add: flip_fresh_fresh flip_eqvt) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma var_eq_swapequal: "atom ab \ xs \ swapequal (Var ab) (Var ab) xs" apply (induct xs) diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/Beta.thy --- a/Nominal/Ex/Beta.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/Beta.thy Mon May 19 16:45:46 2014 +0100 @@ -34,7 +34,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma forget: diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/CPS/CPS1_Plotkin.thy --- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Mon May 19 16:45:46 2014 +0100 @@ -63,7 +63,7 @@ apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff) by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+ -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim] @@ -89,7 +89,7 @@ apply (simp add: Abs1_eq_iff CPS.eqvt) by blast -termination (eqvt) +nominal_termination (eqvt) by (relation "measure size") (simp_all) lemma convert_supp[simp]: @@ -143,7 +143,7 @@ apply(simp_all add: flip_fresh_fresh) done -termination (eqvt) +nominal_termination (eqvt) by (relation "measure (\(t, _). size t)") (simp_all) section{* lemma related to Kapply *} diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/CPS/CPS2_DanvyNielsen.thy --- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Mon May 19 16:45:46 2014 +0100 @@ -32,7 +32,7 @@ apply (simp add: flip_fresh_fresh) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order nominal_function ccomp :: "cpsctxt => cpsctxt => cpsctxt" @@ -57,7 +57,7 @@ apply (simp add: flip_fresh_fresh) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order nominal_function CPSv :: "lt => lt" diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/CPS/Lt.thy --- a/Nominal/Ex/CPS/Lt.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/CPS/Lt.thy Mon May 19 16:45:46 2014 +0100 @@ -33,7 +33,7 @@ apply(simp add: perm_supp_eq fresh_star_Pair) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma forget[simp]: shows "atom x \ M \ M[x ::= s] = M" @@ -54,7 +54,7 @@ by (auto) (erule lt.exhaust, auto) -termination (eqvt) +nominal_termination (eqvt) by (relation "measure size") (simp_all) inductive diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/CR.thy --- a/Nominal/Ex/CR.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/CR.thy Mon May 19 16:45:46 2014 +0100 @@ -30,7 +30,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma forget: diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/Classical.thy Mon May 19 16:45:46 2014 +0100 @@ -249,7 +249,7 @@ apply(blast) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order nominal_function @@ -443,7 +443,7 @@ apply(blast) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order thm crename.eqvt nrename.eqvt diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/Lambda.thy Mon May 19 16:45:46 2014 +0100 @@ -86,7 +86,7 @@ apply(all_trivials) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order thm is_app_def thm is_app.eqvt @@ -106,7 +106,7 @@ apply(simp_all) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order nominal_function rand :: "lam \ lam option" @@ -121,7 +121,7 @@ apply(simp_all) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order nominal_function is_eta_nf :: "lam \ bool" @@ -142,7 +142,7 @@ apply(simp add: eqvt_at_def conj_eqvt) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order nominal_datatype path = Left | Right | In @@ -181,7 +181,7 @@ apply(simp add: perm_supp_eq) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma var_pos1: assumes "atom y \ supp t" @@ -227,7 +227,7 @@ apply(simp add: fresh_star_Pair perm_supp_eq) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order section {* free name function *} @@ -252,7 +252,7 @@ apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order text {* a small test lemma *} lemma shows "supp t = set (frees_lst t)" @@ -280,7 +280,7 @@ apply(simp add: Diff_eqvt eqvt_at_def) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma "frees_set t = supp t" @@ -303,7 +303,7 @@ apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order thm height.simps @@ -338,7 +338,7 @@ apply(simp add: fresh_star_Pair perm_supp_eq) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order thm subst.eqvt @@ -530,7 +530,7 @@ apply(simp add: fresh_star_Pair perm_supp_eq) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order @@ -557,7 +557,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order @@ -591,7 +591,7 @@ apply(simp add: fresh_star_Pair perm_supp_eq) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order section {* De Bruijn Terms *} @@ -649,7 +649,7 @@ apply(simp add: fresh_star_Pair perm_supp_eq) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma transdb_eqvt[eqvt]: @@ -722,7 +722,7 @@ (* a small test -termination (eqvt) sorry +nominal_termination (eqvt) sorry lemma assumes "x \ y" @@ -774,7 +774,7 @@ apply (simp add: eqvt_def permute_fun_app_eq) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/LetRec.thy --- a/Nominal/Ex/LetRec.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/LetRec.thy Mon May 19 16:45:46 2014 +0100 @@ -61,7 +61,7 @@ apply(simp add: eqvt_at_def) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order thm height_trm_height_bp.eqvt diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/LetRecFunNo.thy --- a/Nominal/Ex/LetRecFunNo.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/LetRecFunNo.thy Mon May 19 16:45:46 2014 +0100 @@ -53,7 +53,7 @@ apply clarify apply metis done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order nominal_function substarec :: "(name \ trm \ assn \ assn) \ assn \ assn" where "substarec fac ANil = ANil" @@ -64,7 +64,7 @@ apply (rule_tac y="b" in trm_assn.exhaust(2)) apply auto done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma [fundef_cong]: "(\t1 t2. t = App t1 t2 \ fa t1 t2 = fa' t1 t2) \ diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/Local_Contexts.thy --- a/Nominal/Ex/Local_Contexts.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/Local_Contexts.thy Mon May 19 16:45:46 2014 +0100 @@ -55,7 +55,7 @@ apply (metis Pair_eqvt perm_supp_eq) done -termination (in name_subst) (eqvt) by lexicographic_order +nominal_termination (in name_subst) (eqvt) by lexicographic_order inductive (in name_subst) beta :: "lam \ lam \ bool" (infix "\\<^sub>\" 90) where diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/Pi.thy --- a/Nominal/Ex/Pi.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/Pi.thy Mon May 19 16:45:46 2014 +0100 @@ -38,7 +38,7 @@ apply(rule_tac y="b" in list.exhaust) by(auto) -termination (eqvt) +nominal_termination (eqvt) by (lexicographic_order) @@ -379,7 +379,7 @@ apply(simp) done -termination (eqvt) +nominal_termination (eqvt) by (lexicographic_order) lemma forget_mix: diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/SFT/Consts.thy --- a/Nominal/Ex/SFT/Consts.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/SFT/Consts.thy Mon May 19 16:45:46 2014 +0100 @@ -99,7 +99,7 @@ by (rule, perm_simp, rule) qed -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma supp_numeral[simp]: "supp \x\ = supp x" @@ -144,7 +144,7 @@ apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev) done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma ltgt_eq_iff[simp]: "\M\ = \N\ \ M = N" diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/SFT/LambdaTerms.thy --- a/Nominal/Ex/SFT/LambdaTerms.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/SFT/LambdaTerms.thy Mon May 19 16:45:46 2014 +0100 @@ -52,7 +52,7 @@ by (rule, perm_simp, rule) qed -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma forget[simp]: shows "atom x \ t \ t[x ::= s] = t" diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/SubstNoFcb.thy --- a/Nominal/Ex/SubstNoFcb.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/SubstNoFcb.thy Mon May 19 16:45:46 2014 +0100 @@ -31,7 +31,7 @@ apply (metis (no_types) Pair_inject lam.distinct)+ done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma lam_rec_cong[fundef_cong]: " (\v. l = Var v \ fv v = fv' v) \ @@ -58,7 +58,7 @@ apply (rule, perm_simp, rule, rule) by pat_completeness auto -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order lemma fresh_fun_eqvt_app3: assumes e: "eqvt f" diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/TypeSchemes1.thy --- a/Nominal/Ex/TypeSchemes1.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/TypeSchemes1.thy Mon May 19 16:45:46 2014 +0100 @@ -89,7 +89,7 @@ apply(simp_all) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma subst_id1: @@ -161,7 +161,7 @@ apply blast done -termination (eqvt) +nominal_termination (eqvt) by (lexicographic_order) @@ -301,7 +301,7 @@ apply(simp) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma better: @@ -412,7 +412,7 @@ apply(simp_all) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma tt: diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/TypeSchemes2.thy --- a/Nominal/Ex/TypeSchemes2.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/TypeSchemes2.thy Mon May 19 16:45:46 2014 +0100 @@ -155,7 +155,7 @@ done -termination (eqvt) by lexicographic_order +nominal_termination (eqvt) by lexicographic_order text {* Some Tests about Alpha-Equality *} diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Nominal2.thy Mon May 19 16:45:46 2014 +0100 @@ -3,7 +3,7 @@ Nominal2_Base Nominal2_Abs Nominal2_FCB keywords "nominal_datatype" :: thy_decl and - "nominal_function" "nominal_inductive" :: thy_goal and + "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and "avoids" "binds" begin diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/nominal_termination.ML --- a/Nominal/nominal_termination.ML Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/nominal_termination.ML Mon May 19 16:45:46 2014 +0100 @@ -103,14 +103,13 @@ val option_parser = (Scan.optional (@{keyword "("} |-- Parse.!!! - ((Parse.reserved "eqvt" >> K (true, true)) || - (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false)) + ((Parse.reserved "eqvt" >> K true) || + (Parse.reserved "no_eqvt" >> K false)) --| @{keyword ")"}) (false)) val _ = - Outer_Syntax.local_theory_to_proof @{command_spec "termination"} - "prove termination of a recursive function" + Outer_Syntax.local_theory_to_proof @{command_spec "nominal_termination"} + "prove termination of a recursive nominal function" (option_parser -- Scan.option Parse.term >> - (fn ((is_nominal, is_eqvt), opt_trm) => - if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm)) + (fn (is_eqvt, opt_trm) => termination_cmd is_eqvt opt_trm)) end diff -r 5ebd327ffb96 -r e2da10806a34 Tutorial/Lambda.thy --- a/Tutorial/Lambda.thy Mon May 19 12:45:26 2014 +0100 +++ b/Tutorial/Lambda.thy Mon May 19 16:45:46 2014 +0100 @@ -47,7 +47,7 @@ apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order @@ -76,7 +76,7 @@ apply(simp add: perm_supp_eq fresh_star_Pair) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma fresh_fact: