Skip to content

Commit de50eba

Browse files
yutakangyutakang
committed
SeLFiE_For_Top_Down as a separate file.
1 parent c712a74 commit de50eba

4 files changed

Lines changed: 102 additions & 95 deletions

File tree

‎Abduction/Abduction.thy‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ ML_file \<open>Abstract_Same_Term.ML\<close>
1919
ML_file \<open>Remove_Function.ML\<close>
2020
ML_file \<open>Remove_Outermost_Assumption.ML\<close>
2121
ML_file \<open>Replace_Imp_With_Eq.ML\<close>
22+
ML_file \<open>SeLFiE_For_Top_Down.ML\<close>
2223
ML_file \<open>All_Top_Down_Conjecturing.ML\<close>
2324
ML_file \<open>And_Node.ML\<close>
2425
ML_file \<open>Or_Node.ML\<close>

‎Abduction/All_Top_Down_Conjecturing.ML‎

Lines changed: 1 addition & 94 deletions
Original file line numberDiff line numberDiff line change
@@ -5,99 +5,6 @@
55
* Yutaka Nagashima, Daniel Goc Sebastian
66
* Huawei Technologies Research & Development (UK) Limited.
77
*)
8-
(*** SeLFiE_for_Top_Down ***)
9-
structure SeLFiE_for_Top_Down =
10-
struct
11-
12-
open Eval_Syntactic_Sugar;
13-
14-
val fvars_in_prem_should_appear_in_concl =
15-
All ("trm_occ_in_prem", SeLFiE_Util.QOuter_Path,
16-
Imply (
17-
And (
18-
Node_Is_Free (Variable "trm_occ_in_prem"),
19-
Is_A_Meta_Premise_Or_Below (Variable "trm_occ_in_prem")
20-
),
21-
Some ("trm_occ_in_cncl", SeLFiE_Util.QOuter_Path,
22-
Ands [
23-
Has_Same_Prnt_As (Variable "trm_occ_in_prem", Variable "trm_occ_in_cncl"),
24-
Node_Is_Free (Variable "trm_occ_in_cncl"),
25-
Is_A_Meta_Conclusion_Or_Below (Variable "trm_occ_in_cncl")
26-
]
27-
)
28-
)
29-
);
30-
31-
(* Due to the use of simplifier, this might be obsolete.*)
32-
val does_not_have_trivial_equality =
33-
Not (
34-
Some ("equality", SeLFiE_Util.QOuter_Path,
35-
And (
36-
Unode_Has_Print (Variable "equality", Print "HOL.eq"),
37-
Some ("lhs", SeLFiE_Util.QOuter_Path,
38-
And (
39-
Is_Nth_Argument_Of (Variable "lhs", Number 0, Variable "equality"),
40-
Some ("rhs", SeLFiE_Util.QOuter_Path,
41-
And (
42-
Has_Same_Prnt_As (Variable "lhs", Variable "rhs"),
43-
Is_Nth_Argument_Of (Variable "rhs", Number 1, Variable "equality")
44-
)
45-
)
46-
)
47-
)
48-
)
49-
)
50-
);
51-
52-
val has_func_with_three_occs_in_a_row =
53-
Some ("func", SeLFiE_Util.QOuter_Print,
54-
Ands [
55-
Print_Is_Cnst (Variable "func"),
56-
Not (Is_Subprint_Of (Print "Pure", Variable "func")),
57-
Not (Is_Subprint_Of (Print "HOL", Variable "func")),
58-
Some_Of ("func_occ1", Variable "func",
59-
Ands [
60-
Some ("arg_of_func_occ1", SeLFiE_Util.QOuter_Path,
61-
Ands [
62-
Node_Is_App (Variable "arg_of_func_occ1"),
63-
Is_An_Argument_Of (Variable "arg_of_func_occ1", Variable "func_occ1"),
64-
Some_Of ("func_occ2", Variable "func",
65-
Ands [
66-
Is_Nth_Child_Of (Variable "func_occ2", Number 0, Variable "arg_of_func_occ1"),
67-
68-
Some ("arg_of_func_occ2", SeLFiE_Util.QOuter_Path,
69-
Ands [
70-
Node_Is_App (Variable "arg_of_func_occ2"),
71-
Is_An_Argument_Of (Variable "arg_of_func_occ2", Variable "func_occ2"),
72-
Some_Of ("func_occ3", Variable "func",
73-
Ands [
74-
Is_Nth_Child_Of (Variable "func_occ3", Number 0, Variable "arg_of_func_occ2")
75-
]
76-
)
77-
]
78-
)
79-
80-
]
81-
)
82-
]
83-
)
84-
]
85-
)
86-
]
87-
);
88-
89-
fun run_assertion (pst:Proof.state) (assrt:assert) (cnjctr:term) =
90-
let
91-
val outer_path_to_unode_table = Outer_Path_To_Unode.pst_n_trm_to_path_to_unode_table pst cnjctr : Outer_Path_To_Unode.path_to_unode_table;
92-
val gen_path_table = Gen_Path.Outer_Path_To_Unode outer_path_to_unode_table : Gen_Path.gen_path_to_unode_table;
93-
val empty_argument = SeLFiE_Util.Induct_Arguments {ons = [], arbs = [], rules = []} : SeLFiE_Util.induct_arguments;
94-
val outer_domains = Quantifier_Domain.inout_pst_n_trm_n_induct_args_to_domains Quantifier_Domain.Out gen_path_table empty_argument: Quantifier_Domain.domains;
95-
in
96-
eval pst outer_path_to_unode_table outer_domains empty_argument assrt = True
97-
end;
98-
99-
end;
100-
1018
(*** structure All_Top_Down_Conjecturing ***)
1029
structure All_Top_Down_Conjecturing: TOP_DOWN_CONJECTURING =
10310
struct
@@ -158,7 +65,7 @@ fun template_conjectures (ctxt:Proof.context) (trm:term): (string * term) list =
15865
result
15966
end;
16067

161-
structure S4TD = SeLFiE_for_Top_Down;
68+
structure S4TD = SeLFiE_For_Top_Down;
16269

16370
fun run_assertion (ctxt:Proof.context) (trm:term) (assert:Eval_Syntactic_Sugar.assert) =
16471
S4TD.run_assertion (Top_Down_Util.mk_pst_to_prove_from_term ctxt trm) assert trm;

‎Abduction/SeLFiE_For_Top_Down.ML‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
(*
2+
* SeLFiE_for_Top_Down.ML
3+
*
4+
* Authors:
5+
* Yutaka Nagashima, Daniel Goc Sebastian
6+
* Huawei Technologies Research & Development (UK) Limited.
7+
*)
8+
(*** SeLFiE_For_Top_Down ***)
9+
structure SeLFiE_For_Top_Down =
10+
struct
11+
12+
open Eval_Syntactic_Sugar;
13+
14+
val fvars_in_prem_should_appear_in_concl =
15+
All ("trm_occ_in_prem", SeLFiE_Util.QOuter_Path,
16+
Imply (
17+
And (
18+
Node_Is_Free (Variable "trm_occ_in_prem"),
19+
Is_A_Meta_Premise_Or_Below (Variable "trm_occ_in_prem")
20+
),
21+
Some ("trm_occ_in_cncl", SeLFiE_Util.QOuter_Path,
22+
Ands [
23+
Has_Same_Prnt_As (Variable "trm_occ_in_prem", Variable "trm_occ_in_cncl"),
24+
Node_Is_Free (Variable "trm_occ_in_cncl"),
25+
Is_A_Meta_Conclusion_Or_Below (Variable "trm_occ_in_cncl")
26+
]
27+
)
28+
)
29+
);
30+
31+
(* Due to the use of simplifier, this might be obsolete.*)
32+
val does_not_have_trivial_equality =
33+
Not (
34+
Some ("equality", SeLFiE_Util.QOuter_Path,
35+
And (
36+
Unode_Has_Print (Variable "equality", Print "HOL.eq"),
37+
Some ("lhs", SeLFiE_Util.QOuter_Path,
38+
And (
39+
Is_Nth_Argument_Of (Variable "lhs", Number 0, Variable "equality"),
40+
Some ("rhs", SeLFiE_Util.QOuter_Path,
41+
And (
42+
Has_Same_Prnt_As (Variable "lhs", Variable "rhs"),
43+
Is_Nth_Argument_Of (Variable "rhs", Number 1, Variable "equality")
44+
)
45+
)
46+
)
47+
)
48+
)
49+
)
50+
);
51+
52+
val has_func_with_three_occs_in_a_row =
53+
Some ("func", SeLFiE_Util.QOuter_Print,
54+
Ands [
55+
Print_Is_Cnst (Variable "func"),
56+
Not (Is_Subprint_Of (Print "Pure", Variable "func")),
57+
Not (Is_Subprint_Of (Print "HOL", Variable "func")),
58+
Some_Of ("func_occ1", Variable "func",
59+
Ands [
60+
Some ("arg_of_func_occ1", SeLFiE_Util.QOuter_Path,
61+
Ands [
62+
Node_Is_App (Variable "arg_of_func_occ1"),
63+
Is_An_Argument_Of (Variable "arg_of_func_occ1", Variable "func_occ1"),
64+
Some_Of ("func_occ2", Variable "func",
65+
Ands [
66+
Is_Nth_Child_Of (Variable "func_occ2", Number 0, Variable "arg_of_func_occ1"),
67+
68+
Some ("arg_of_func_occ2", SeLFiE_Util.QOuter_Path,
69+
Ands [
70+
Node_Is_App (Variable "arg_of_func_occ2"),
71+
Is_An_Argument_Of (Variable "arg_of_func_occ2", Variable "func_occ2"),
72+
Some_Of ("func_occ3", Variable "func",
73+
Ands [
74+
Is_Nth_Child_Of (Variable "func_occ3", Number 0, Variable "arg_of_func_occ2")
75+
]
76+
)
77+
]
78+
)
79+
80+
]
81+
)
82+
]
83+
)
84+
]
85+
)
86+
]
87+
);
88+
89+
fun run_assertion (pst:Proof.state) (assrt:assert) (cnjctr:term) =
90+
let
91+
val outer_path_to_unode_table = Outer_Path_To_Unode.pst_n_trm_to_path_to_unode_table pst cnjctr : Outer_Path_To_Unode.path_to_unode_table;
92+
val gen_path_table = Gen_Path.Outer_Path_To_Unode outer_path_to_unode_table : Gen_Path.gen_path_to_unode_table;
93+
val empty_argument = SeLFiE_Util.Induct_Arguments {ons = [], arbs = [], rules = []} : SeLFiE_Util.induct_arguments;
94+
val outer_domains = Quantifier_Domain.inout_pst_n_trm_n_induct_args_to_domains Quantifier_Domain.Out gen_path_table empty_argument: Quantifier_Domain.domains;
95+
in
96+
eval pst outer_path_to_unode_table outer_domains empty_argument assrt = True
97+
end;
98+
99+
end;

‎Abduction/Seed_Of_Or2And_Edge.ML‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ fun condition_to_filter_out (parent_or:term) (pst:Proof.state) (ag:abduction_gra
117117
fun eq_to_final_goal _ = exists (Top_Down_Util.alpha_eq_over_fvar final_goal) trms : bool;
118118
fun concl_is_eq_to_final_goal _ = exists (concl_is_alpha_eq_to final_goal) trms : bool;
119119
fun has_func_with_three_occs_in_a_row _ = exists
120-
(fn trm => SeLFiE_for_Top_Down.run_assertion (Top_Down_Util.mk_pst_to_prove_from_term (Proof.context_of pst) trm) SeLFiE_for_Top_Down.has_func_with_three_occs_in_a_row trm) trms;
120+
(fn trm => SeLFiE_For_Top_Down.run_assertion (Top_Down_Util.mk_pst_to_prove_from_term (Proof.context_of pst) trm) SeLFiE_For_Top_Down.has_func_with_three_occs_in_a_row trm) trms;
121121
fun has_counter_example_in_prems (pst:Proof.state) (term:term) =
122122
let
123123
val prems = Logic.strip_imp_prems term: terms;

0 commit comments

Comments
 (0)