3 |
3 |
4 Provides a tactic to generate fresh names and |
4 Provides a tactic to generate fresh names and |
5 a tactic to analyse instances of the fresh_fun. |
5 a tactic to analyse instances of the fresh_fun. |
6 *) |
6 *) |
7 |
7 |
8 (* FIXME proper ML structure *) |
8 (* FIXME proper ML structure! *) |
9 |
9 |
10 (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *) |
10 (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *) |
11 |
11 |
12 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
12 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
13 fun gen_res_inst_tac_term instf tyinst tinst elim th i st = |
13 fun gen_res_inst_tac_term instf tyinst tinst elim th i st = |
50 val fresh_prod = @{thm "fresh_prod"}; |
50 val fresh_prod = @{thm "fresh_prod"}; |
51 |
51 |
52 (* A tactic to generate a name fresh for all the free *) |
52 (* A tactic to generate a name fresh for all the free *) |
53 (* variables and parameters of the goal *) |
53 (* variables and parameters of the goal *) |
54 |
54 |
55 fun generate_fresh_tac atom_name i thm = |
55 fun generate_fresh_tac ctxt atom_name = SUBGOAL (fn (goal, _) => |
56 let |
56 let |
57 val thy = theory_of_thm thm; |
57 val thy = Proof_Context.theory_of ctxt; |
58 (* the parsing function returns a qualified name, we get back the base name *) |
58 (* the parsing function returns a qualified name, we get back the base name *) |
59 val atom_basename = Long_Name.base_name atom_name; |
59 val atom_basename = Long_Name.base_name atom_name; |
60 val goal = nth (prems_of thm) (i - 1); |
|
61 val ps = Logic.strip_params goal; |
60 val ps = Logic.strip_params goal; |
62 val Ts = rev (map snd ps); |
61 val Ts = rev (map snd ps); |
63 fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]); |
62 fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]); |
64 (* rebuild de bruijn indices *) |
63 (* rebuild de bruijn indices *) |
65 val bvs = map_index (Bound o fst) ps; |
64 val bvs = map_index (Bound o fst) ps; |
74 val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; |
73 val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; |
75 val exists_fresh' = at_name_inst_thm RS at_exists_fresh'; |
74 val exists_fresh' = at_name_inst_thm RS at_exists_fresh'; |
76 (* find the variable we want to instantiate *) |
75 (* find the variable we want to instantiate *) |
77 val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh')); |
76 val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh')); |
78 in |
77 in |
|
78 fn st => |
79 (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN |
79 (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN |
80 rtac fs_name_thm 1 THEN |
80 rtac fs_name_thm 1 THEN |
81 etac exE 1) thm |
81 etac exE 1) st |
82 handle List.Empty => all_tac thm (* if we collected no variables then we do nothing *) |
82 handle List.Empty => all_tac st (* if we collected no variables then we do nothing *) |
83 end; |
83 end) 1; |
84 |
84 |
85 fun get_inner_fresh_fun (Bound j) = NONE |
85 fun get_inner_fresh_fun (Bound j) = NONE |
86 | get_inner_fresh_fun (v as Free _) = NONE |
86 | get_inner_fresh_fun (v as Free _) = NONE |
87 | get_inner_fresh_fun (v as Var _) = NONE |
87 | get_inner_fresh_fun (v as Var _) = NONE |
88 | get_inner_fresh_fun (Const _) = NONE |
88 | get_inner_fresh_fun (Const _) = NONE |
95 end; |
95 end; |
96 |
96 |
97 (* This tactic generates a fresh name of the atom type *) |
97 (* This tactic generates a fresh name of the atom type *) |
98 (* given by the innermost fresh_fun *) |
98 (* given by the innermost fresh_fun *) |
99 |
99 |
100 fun generate_fresh_fun_tac i thm = |
100 fun generate_fresh_fun_tac ctxt = SUBGOAL (fn (goal, _) => |
101 let |
101 let |
102 val goal = nth (prems_of thm) (i - 1); |
|
103 val atom_name_opt = get_inner_fresh_fun goal; |
102 val atom_name_opt = get_inner_fresh_fun goal; |
104 in |
103 in |
105 case atom_name_opt of |
104 case atom_name_opt of |
106 NONE => all_tac thm |
105 NONE => all_tac |
107 | SOME atom_name => generate_fresh_tac atom_name i thm |
106 | SOME atom_name => generate_fresh_tac ctxt atom_name |
108 end |
107 end) 1; |
109 |
108 |
110 (* Two substitution tactics which looks for the innermost occurence in |
109 (* Two substitution tactics which looks for the innermost occurence in |
111 one assumption or in the conclusion *) |
110 one assumption or in the conclusion *) |
112 |
111 |
113 val search_fun = curry (Seq.flat o uncurry EqSubst.searchf_bt_unify_valid); |
112 val search_fun = curry (Seq.flat o uncurry EqSubst.searchf_bt_unify_valid); |
121 |
120 |
122 fun subst_inner_asm_tac ctxt th = |
121 fun subst_inner_asm_tac ctxt th = |
123 curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux |
122 curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux |
124 (1 upto Thm.nprems_of th)))))) ctxt th; |
123 (1 upto Thm.nprems_of th)))))) ctxt th; |
125 |
124 |
126 fun fresh_fun_tac ctxt no_asm i thm = |
125 fun fresh_fun_tac ctxt no_asm = SUBGOAL (fn (goal, i) => |
127 (* Find the variable we instantiate *) |
126 (* Find the variable we instantiate *) |
128 let |
127 let |
129 val thy = theory_of_thm thm; |
128 val thy = Proof_Context.theory_of ctxt; |
130 val abs_fresh = Global_Theory.get_thms thy "abs_fresh"; |
129 val abs_fresh = Global_Theory.get_thms thy "abs_fresh"; |
131 val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app"; |
130 val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app"; |
132 val simp_ctxt = |
131 val simp_ctxt = |
133 ctxt addsimps (fresh_prod :: abs_fresh) |
132 ctxt addsimps (fresh_prod :: abs_fresh) |
134 addsimps fresh_perm_app; |
133 addsimps fresh_perm_app; |
135 val x = hd (tl (Misc_Legacy.term_vars (prop_of exI))); |
134 val x = hd (tl (Misc_Legacy.term_vars (prop_of exI))); |
136 val goal = nth (prems_of thm) (i-1); |
|
137 val atom_name_opt = get_inner_fresh_fun goal; |
135 val atom_name_opt = get_inner_fresh_fun goal; |
138 val n = length (Logic.strip_params goal); |
136 val n = length (Logic.strip_params goal); |
139 (* Here we rely on the fact that the variable introduced by generate_fresh_tac *) |
137 (* Here we rely on the fact that the variable introduced by generate_fresh_tac *) |
140 (* is the last one in the list, the inner one *) |
138 (* is the last one in the list, the inner one *) |
141 in |
139 in |
142 case atom_name_opt of |
140 case atom_name_opt of |
143 NONE => all_tac thm |
141 NONE => all_tac |
144 | SOME atom_name => |
142 | SOME atom_name => |
145 let |
143 let |
146 val atom_basename = Long_Name.base_name atom_name; |
144 val atom_basename = Long_Name.base_name atom_name; |
147 val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename; |
145 val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename; |
148 val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; |
146 val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; |
171 in |
169 in |
172 ((if no_asm then no_tac else |
170 ((if no_asm then no_tac else |
173 (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) |
171 (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) |
174 ORELSE |
172 ORELSE |
175 (subst_inner_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) st |
173 (subst_inner_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) st |
176 end)) thm |
174 end)) |
|
175 end |
|
176 end) |
177 |
177 |
178 end |
|
179 end |
|
180 |
|
181 (* syntax for options, given "(no_asm)" will give back true, without |
|
182 gives back false *) |
|
183 val options_syntax = |
|
184 (Args.parens (Args.$$$ "no_asm") >> (K true)) || |
|
185 (Scan.succeed false); |
|
186 |
|
187 fun setup_generate_fresh x = |
|
188 (Args.goal_spec -- Args.type_name {proper = true, strict = true} >> |
|
189 (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x; |
|
190 |
|
191 fun setup_fresh_fun_simp x = |
|
192 (Scan.lift options_syntax >> (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))) x; |
|
193 |
|