# HG changeset patch # User wenzelm # Date 1256073904 -7200 # Node ID 66ef64a5f122f41797683d99d5373ce10621a4bb # Parent fcc77a029bb2867c556d79135464ab2cecde7f84 eliminated THENL -- use THEN RANGE; eliminated TRY' -- use TRY with op o; observe naming convention ctxt: Proof.context; tuned whitespace; diff -r fcc77a029bb2 -r 66ef64a5f122 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Tue Oct 20 22:46:24 2009 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Tue Oct 20 23:25:04 2009 +0200 @@ -7,24 +7,10 @@ (* First some functions that should be in the library *) -(* A tactical which applies a list of int -> tactic to the *) -(* corresponding subgoals present after the application of *) -(* another tactic. *) -(* *) -(* T THENL [A,B,C] is equivalent to T THEN (C 3 THEN B 2 THEN A 1) *) - -infix 1 THENL -fun tac THENL tacs = - tac THEN - (EVERY (map (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1)))) - (* A tactic which only succeeds when the argument *) (* tactic solves completely the specified subgoal *) fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac); -(* A version of TRY for int -> tactic *) -fun TRY' tac i = TRY (tac i); - fun gen_res_inst_tac_term instf tyinst tinst elim th i st = let val thy = theory_of_thm st; @@ -45,10 +31,10 @@ compose_tac (elim, th', nprems_of th) i st end handle Subscript => Seq.empty; -val res_inst_tac_term = +val res_inst_tac_term = gen_res_inst_tac_term (curry Thm.instantiate); -val res_inst_tac_term' = +val res_inst_tac_term' = gen_res_inst_tac_term (K Drule.cterm_instantiate) []; fun cut_inst_tac_term' tinst th = @@ -65,18 +51,18 @@ val fresh_fun_app' = @{thm "fresh_fun_app'"}; val fresh_prod = @{thm "fresh_prod"}; -(* A tactic to generate a name fresh for all the free *) +(* A tactic to generate a name fresh for all the free *) (* variables and parameters of the goal *) fun generate_fresh_tac atom_name i thm = - let + let val thy = theory_of_thm thm; (* the parsing function returns a qualified name, we get back the base name *) val atom_basename = Long_Name.base_name atom_name; val goal = List.nth(prems_of thm, i-1); val ps = Logic.strip_params goal; val Ts = rev (map snd ps); - fun is_of_fs_name T = Sign.of_sort thy (T, Sign.intern_sort thy ["fs_"^atom_basename]); + fun is_of_fs_name T = Sign.of_sort thy (T, Sign.intern_sort thy ["fs_"^atom_basename]); (* rebuild de bruijn indices *) val bvs = map_index (Bound o fst) ps; (* select variables of the right class *) @@ -90,7 +76,7 @@ val exists_fresh' = at_name_inst_thm RS at_exists_fresh'; (* find the variable we want to instantiate *) val x = hd (OldTerm.term_vars (prop_of exists_fresh')); - in + in (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN rtac fs_name_thm 1 THEN etac exE 1) thm @@ -98,18 +84,18 @@ end; fun get_inner_fresh_fun (Bound j) = NONE - | get_inner_fresh_fun (v as Free _) = NONE + | get_inner_fresh_fun (v as Free _) = NONE | get_inner_fresh_fun (v as Var _) = NONE | get_inner_fresh_fun (Const _) = NONE - | get_inner_fresh_fun (Abs (_, _, t)) = get_inner_fresh_fun t - | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u) - = SOME T - | get_inner_fresh_fun (t $ u) = + | get_inner_fresh_fun (Abs (_, _, t)) = get_inner_fresh_fun t + | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u) + = SOME T + | get_inner_fresh_fun (t $ u) = let val a = get_inner_fresh_fun u in - if a = NONE then get_inner_fresh_fun t else a + if a = NONE then get_inner_fresh_fun t else a end; -(* This tactic generates a fresh name of the atom type *) +(* This tactic generates a fresh name of the atom type *) (* given by the innermost fresh_fun *) fun generate_fresh_fun_tac i thm = @@ -117,32 +103,32 @@ val goal = List.nth(prems_of thm, i-1); val atom_name_opt = get_inner_fresh_fun goal; in - case atom_name_opt of + case atom_name_opt of NONE => all_tac thm - | SOME atom_name => generate_fresh_tac atom_name i thm + | SOME atom_name => generate_fresh_tac atom_name i thm end -(* Two substitution tactics which looks for the innermost occurence in +(* Two substitution tactics which looks for the innermost occurence in one assumption or in the conclusion *) -val search_fun = curry (Seq.flat o (uncurry EqSubst.searchf_bt_unify_valid)); +val search_fun = curry (Seq.flat o uncurry EqSubst.searchf_bt_unify_valid); val search_fun_asm = EqSubst.skip_first_asm_occs_search EqSubst.searchf_bt_unify_valid; -fun subst_inner_tac ctx = EqSubst.eqsubst_tac' ctx search_fun; -fun subst_inner_asm_tac_aux i ctx = EqSubst.eqsubst_asm_tac' ctx search_fun_asm i; +fun subst_inner_tac ctxt = EqSubst.eqsubst_tac' ctxt search_fun; +fun subst_inner_asm_tac_aux i ctxt = EqSubst.eqsubst_asm_tac' ctxt search_fun_asm i; -(* A tactic to substitute in the first assumption +(* A tactic to substitute in the first assumption which contains an occurence. *) -fun subst_inner_asm_tac ctx th = - curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux - (1 upto Thm.nprems_of th)))))) ctx th; +fun subst_inner_asm_tac ctxt th = + curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux + (1 upto Thm.nprems_of th)))))) ctxt th; -fun fresh_fun_tac no_asm i thm = +fun fresh_fun_tac no_asm i thm = (* Find the variable we instantiate *) let val thy = theory_of_thm thm; - val ctx = Context.init_proof thy; + val ctxt = ProofContext.init thy; val ss = global_simpset_of thy; val abs_fresh = PureThy.get_thms thy "abs_fresh"; val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app"; @@ -151,45 +137,45 @@ val x = hd (tl (OldTerm.term_vars (prop_of exI))); val goal = nth (prems_of thm) (i-1); val atom_name_opt = get_inner_fresh_fun goal; - val n = List.length (Logic.strip_params goal); + val n = length (Logic.strip_params goal); (* Here we rely on the fact that the variable introduced by generate_fresh_tac *) (* is the last one in the list, the inner one *) in - case atom_name_opt of + case atom_name_opt of NONE => all_tac thm - | SOME atom_name => - let + | SOME atom_name => + let val atom_basename = Long_Name.base_name atom_name; val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename; val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; fun inst_fresh vars params i st = let val vars' = OldTerm.term_vars (prop_of st); val thy = theory_of_thm st; - in case vars' \\ vars of + in case vars' \\ vars of [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st) | _ => error "fresh_fun_simp: Too many variables, please report." end in ((fn st => - let + let val vars = OldTerm.term_vars (prop_of st); val params = Logic.strip_params (nth (prems_of st) (i-1)) - (* The tactics which solve the subgoals generated + (* The tactics which solve the subgoals generated by the conditionnal rewrite rule. *) - val post_rewrite_tacs = + val post_rewrite_tacs = [rtac pt_name_inst, rtac at_name_inst, - TRY' (SOLVEI (NominalPermeq.finite_guess_tac ss'')), + TRY o SOLVEI (NominalPermeq.finite_guess_tac ss''), inst_fresh vars params THEN' - (TRY' (SOLVEI (NominalPermeq.fresh_guess_tac ss''))) THEN' - (TRY' (SOLVEI (asm_full_simp_tac ss'')))] - in + (TRY o SOLVEI (NominalPermeq.fresh_guess_tac ss'')) THEN' + (TRY o SOLVEI (asm_full_simp_tac ss''))] + in ((if no_asm then no_tac else - (subst_inner_asm_tac ctx fresh_fun_app' i THENL post_rewrite_tacs)) + (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) ORELSE - (subst_inner_tac ctx fresh_fun_app' i THENL post_rewrite_tacs)) st + (subst_inner_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) st end)) thm - + end end