Skip to content

Commit f65404a

Browse files
luxin7670luxin7670
committed
changed old open/theory formats in some scripts before remote cleanup
1 parent caf42af commit f65404a

File tree

78 files changed

+697
-640
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

78 files changed

+697
-640
lines changed

‎.hol/make-deps/lastmaker‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/Users/mac/honors/HOL/bin/Holmake

‎richerlang/.hol/logs/envSemTheory‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
<<HOL message: Created theory "envSem">>
2+
<<HOL message: mk_functional:
3+
pattern completion has added 5 clauses to the original specification.>>
4+
<<HOL message: mk_functional:
5+
pattern completion has added 4 clauses to the original specification.>>
6+
Saved definition ____ "eval_exp_def"
7+
Saved induction _____ "eval_exp_ind"
8+
Saved definition ____ "diverges_def"
9+
Saved definition ____ "localise_def"
10+
Saved theorem _______ "result_bind_eq_value"
11+
Saved theorem _______ "result_bind_eq_exn"
12+
Saved theorem _______ "result_bind_eq_typeerr"
13+
Saved theorem _______ "envtype_fdom"
14+
Saved theorem _______ "envtype_submap"
15+
Saved theorem _______ "FLOOKUP_supermap"
16+
Saved theorem _______ "envtype_DRESTRICT"
17+
Saved theorem _______ "submap_domsub2"
18+
Saved theorem _______ "submap_update_same"
19+
Saved theorem _______ "subset_update"
20+
Saved theorem _______ "subset_diff_update"
21+
Saved theorem _______ "subset_diff_same"
22+
Saved theorem _______ "diff_eq_same"
23+
Saved theorem _______ "union_diff_subset_x"
24+
Saved theorem _______ "typecheck_env_submap"
25+
Saved theorem _______ "typecheck_env_fv"
26+
Saved theorem _______ "typecheck_drestrict"
27+
Saved theorem _______ "drestrict_domsub_map"
28+
Saved theorem _______ "drestrict_fupdate_union"
29+
Saved theorem _______ "typecheck_update_sub_fv"
30+
Saved theorem _______ "type_soundness"
31+
Saved theorem _______ "typecheck_value_type"
32+
Saved theorem _______ "clock_value_increment"
33+
Saved theorem _______ "clock_exn_increment"
34+
Saved theorem _______ "clock_typeerr_increment"
35+
Saved theorem _______ "clock_increment"
36+
Saved theorem _______ "clock_eval_exp_unique"
37+
Saved theorem _______ "eval_exp_value_exn_false"
38+
Saved theorem _______ "clock_eval_exp_typeerr_false"
39+
Saved theorem _______ "clock_eval_exp_exn_false"
40+
Saved theorem _______ "localise_fdom"
41+
Saved theorem _______ "localise_fapply"
42+
Saved theorem _______ "localise_flookup"
43+
Saved theorem _______ "localise_fempty"
44+
Saved theorem _______ "localise_update_eqn"
45+
Saved theorem _______ "localise_update_neq"
46+
Saved theorem _______ "submap_localise"
47+
Saved theorem _______ "subset_fdom_localise_state"
48+
Saved theorem _______ "localise_fdom_subset"
49+
Saved theorem _______ "envtype_update"
50+
Saved theorem _______ "eval_no_undefined_vars"
51+
Saved theorem _______ "delete_inter_eq"
52+
Saved theorem _______ "subset_absortion"
53+
Saved theorem _______ "eval_value_type"
54+
Saved theorem _______ "eval_sumv_types"
55+
Saved theorem _______ "eval_bigger_state_type"
56+
Saved theorem _______ "eval_fn_submap_lemma"
57+
Saved theorem _______ "fst_state_union_update_lemma"
58+
Saved theorem _______ "eval_bigger_state_fv"
59+
Saved theorem _______ "eval_bigger_state_exn"
60+
Saved theorem _______ "eval_val_neq"
61+
Saved theorem _______ "typecheck_no_undefined_vars"
62+
Exporting theory "envSem" ... done.
63+
Theory "envSem" took 9.3s to build

‎richerlang/.hol/logs/numstringTheory‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
<<HOL message: Created theory "numstring">>
2+
Saved definition ____ "int_to_stringHelper_def"
3+
Saved induction _____ "int_to_stringHelper_ind"
4+
Saved definition ____ "int_to_string_def"
5+
Saved definition ____ "string_to_intHelper2_def"
6+
Saved definition ____ "string_to_int2_def"
7+
Saved theorem _______ "i2sHelper_EQ_NIL"
8+
Saved theorem _______ "s2i_inverse"
9+
Saved definition ____ "hnlz_def"
10+
Saved theorem _______ "hnlz_reverse"
11+
Saved theorem _______ "s2iHelper_empty"
12+
Saved theorem _______ "s2iHelper_nonzero"
13+
Saved theorem _______ "i2sHelper_inverse"
14+
Saved theorem _______ "reverse_zero"
15+
Saved theorem _______ "i2s_inverse"
16+
Exporting theory "numstring" ... done.
17+
Theory "numstring" took 0.82631s to build

‎richerlang/.hol/logs/richerLangTheory‎

Lines changed: 179 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,179 @@
1+
<<HOL message: Created theory "richerLang">>
2+
Saved theorem _______ "num2bop_bop2num"
3+
Saved theorem _______ "bop2num_num2bop"
4+
Saved theorem _______ "num2bop_11"
5+
Saved theorem _______ "bop2num_11"
6+
Saved theorem _______ "num2bop_ONTO"
7+
Saved theorem _______ "bop2num_ONTO"
8+
Saved theorem _______ "num2bop_thm"
9+
Saved theorem _______ "bop2num_thm"
10+
Saved theorem _______ "bop_EQ_bop"
11+
Saved theorem _______ "bop_case_def"
12+
Saved theorem _______ "datatype_bop"
13+
Saved theorem _______ "bop_distinct"
14+
Saved theorem _______ "bop_nchotomy"
15+
Saved theorem _______ "bop_Axiom"
16+
Saved theorem _______ "bop_induction"
17+
Saved theorem _______ "bop_case_cong"
18+
Saved theorem _______ "bop_case_eq"
19+
<<HOL message: Defined type: "bop">>
20+
Saved theorem _______ "num2uop_uop2num"
21+
Saved theorem _______ "uop2num_num2uop"
22+
Saved theorem _______ "num2uop_11"
23+
Saved theorem _______ "uop2num_11"
24+
Saved theorem _______ "num2uop_ONTO"
25+
Saved theorem _______ "uop2num_ONTO"
26+
Saved theorem _______ "num2uop_thm"
27+
Saved theorem _______ "uop2num_thm"
28+
Saved theorem _______ "uop_EQ_uop"
29+
Saved theorem _______ "uop_case_def"
30+
Saved theorem _______ "datatype_uop"
31+
Saved theorem _______ "uop_distinct"
32+
Saved theorem _______ "uop_nchotomy"
33+
Saved theorem _______ "uop_Axiom"
34+
Saved theorem _______ "uop_induction"
35+
Saved theorem _______ "uop_case_cong"
36+
Saved theorem _______ "uop_case_eq"
37+
<<HOL message: Defined type: "uop">>
38+
Saved theorem _______ "datatype_type"
39+
Saved theorem _______ "type_11"
40+
Saved theorem _______ "type_distinct"
41+
Saved theorem _______ "type_nchotomy"
42+
Saved theorem _______ "type_Axiom"
43+
Saved theorem _______ "type_induction"
44+
Saved theorem _______ "type_case_cong"
45+
Saved theorem _______ "type_case_eq"
46+
<<HOL message: Defined type: "type">>
47+
Saved theorem _______ "datatype_exp"
48+
Saved theorem _______ "exp_11"
49+
Saved theorem _______ "exp_distinct"
50+
Saved theorem _______ "exp_nchotomy"
51+
Saved theorem _______ "exp_Axiom"
52+
Saved theorem _______ "exp_induction"
53+
Saved theorem _______ "exp_case_cong"
54+
Saved theorem _______ "exp_case_eq"
55+
<<HOL message: Defined type: "exp">>
56+
Saved theorem _______ "num2exn_exn2num"
57+
Saved theorem _______ "exn2num_num2exn"
58+
Saved theorem _______ "num2exn_11"
59+
Saved theorem _______ "exn2num_11"
60+
Saved theorem _______ "num2exn_ONTO"
61+
Saved theorem _______ "exn2num_ONTO"
62+
Saved theorem _______ "num2exn_thm"
63+
Saved theorem _______ "exn2num_thm"
64+
Saved theorem _______ "exn_EQ_exn"
65+
Saved theorem _______ "exn_case_def"
66+
Saved theorem _______ "datatype_exn"
67+
Saved theorem _______ "exn_distinct"
68+
Saved theorem _______ "exn_nchotomy"
69+
Saved theorem _______ "exn_Axiom"
70+
Saved theorem _______ "exn_induction"
71+
Saved theorem _______ "exn_case_cong"
72+
Saved theorem _______ "exn_case_eq"
73+
<<HOL message: Defined type: "exn">>
74+
Saved theorem _______ "datatype_result"
75+
Saved theorem _______ "result_11"
76+
Saved theorem _______ "result_distinct"
77+
Saved theorem _______ "result_nchotomy"
78+
Saved theorem _______ "result_Axiom"
79+
Saved theorem _______ "result_induction"
80+
Saved theorem _______ "result_case_cong"
81+
Saved theorem _______ "result_case_eq"
82+
<<HOL message: Defined type: "result">>
83+
Saved definition ____ "result_bind_def"
84+
<<HOL message: mk_functional:
85+
pattern completion has added 5 clauses to the original specification.>>
86+
Saved definition ____ "getI_def"
87+
Saved induction _____ "getI_ind"
88+
<<HOL message: mk_functional:
89+
pattern completion has added 5 clauses to the original specification.>>
90+
Saved definition ____ "getS_def"
91+
Saved induction _____ "getS_ind"
92+
<<HOL message: mk_functional:
93+
pattern completion has added 5 clauses to the original specification.>>
94+
Saved definition ____ "getB_def"
95+
Saved induction _____ "getB_ind"
96+
Saved theorem _______ "getB_EQ_value"
97+
<<HOL message: mk_functional:
98+
pattern completion has added 5 clauses to the original specification.>>
99+
Saved definition ____ "getP_def"
100+
Saved induction _____ "getP_ind"
101+
Saved definition ____ "binIop_def"
102+
Saved definition ____ "binSop_def"
103+
Saved definition ____ "binBop_def"
104+
Saved definition ____ "eval_bop_def"
105+
Saved definition ____ "eval_uop_def"
106+
Saved theorem _______ "uoptype_rules"
107+
Saved theorem _______ "uoptype_ind"
108+
Saved theorem _______ "uoptype_strongind"
109+
Saved theorem _______ "uoptype_cases"
110+
Saved theorem _______ "uoptype_not"
111+
Saved theorem _______ "uoptype_s2i"
112+
Saved theorem _______ "uoptype_i2s"
113+
Saved theorem _______ "uoptype_fst"
114+
Saved theorem _______ "uoptype_snd"
115+
Saved theorem _______ "uoptype_suml"
116+
Saved theorem _______ "uoptype_sumr"
117+
Saved theorem _______ "boptype_rules"
118+
Saved theorem _______ "boptype_ind"
119+
Saved theorem _______ "boptype_strongind"
120+
Saved theorem _______ "boptype_cases"
121+
Saved theorem _______ "boptype_bint"
122+
Saved theorem _______ "boptype_concat"
123+
Saved theorem _______ "boptype_Less"
124+
Saved theorem _______ "boptype_Eq"
125+
Saved theorem _______ "boptype_pair"
126+
Saved theorem _______ "typecheck_rules"
127+
Saved theorem _______ "typecheck_ind"
128+
Saved theorem _______ "typecheck_strongind"
129+
Saved theorem _______ "typecheck_cases"
130+
Saved theorem _______ "typecheck_var"
131+
Saved theorem _______ "typecheck_if"
132+
Saved theorem _______ "typecheck_StrLit"
133+
Saved theorem _______ "typecheck_IntLit"
134+
Saved theorem _______ "typecheck_BoolLit"
135+
Saved theorem _______ "typecheck_Binop"
136+
Saved theorem _______ "typecheck_Uop"
137+
Saved theorem _______ "typecheck_let"
138+
Saved theorem _______ "typecheck_fn"
139+
Saved theorem _______ "typecheck_app"
140+
Saved theorem _______ "typecheck_case"
141+
Saved theorem _______ "typecheck_var_thm"
142+
Saved theorem _______ "typecheck_strlit_thm"
143+
Saved theorem _______ "typecheck_intlit_thm"
144+
Saved theorem _______ "typecheck_boollit_thm"
145+
Saved theorem _______ "typecheck_binop_thm"
146+
Saved theorem _______ "typecheck_uop_thm"
147+
Saved theorem _______ "typecheck_if_thm"
148+
Saved theorem _______ "typecheck_let_thm"
149+
Saved theorem _______ "typecheck_fn_thm"
150+
Saved theorem _______ "typecheck_app_thm"
151+
Saved theorem _______ "typecheck_case_thm"
152+
<<HOL message: mk_functional:
153+
pattern completion has added 2 clauses to the original specification.>>
154+
Saved definition ____ "free_vars"
155+
Saved induction _____ "free_vars_ind"
156+
Saved theorem _______ "typecheck_vars"
157+
Saved theorem _______ "value_type_rules"
158+
Saved theorem _______ "value_type_ind"
159+
Saved theorem _______ "value_type_strongind"
160+
Saved theorem _______ "value_type_cases"
161+
Saved theorem _______ "value_type_IntV"
162+
Saved theorem _______ "value_type_StrV"
163+
Saved theorem _______ "value_type_BoolV"
164+
Saved theorem _______ "value_type_FnV"
165+
Saved theorem _______ "value_type_PairV"
166+
Saved theorem _______ "value_type_SumLV"
167+
Saved theorem _______ "value_type_SumRV"
168+
Saved definition ____ "envtype_def"
169+
Saved theorem _______ "envtype_lemma"
170+
Saved theorem _______ "valuetype_EQ_intT"
171+
Saved theorem _______ "valuetype_EQ_strT"
172+
Saved theorem _______ "valuetype_EQ_boolT"
173+
Saved theorem _______ "valuetype_EQ_fnT"
174+
Saved theorem _______ "valuetype_EQ_pairT"
175+
Saved theorem _______ "valuetype_EQ_sumT"
176+
Saved theorem _______ "bop_type_soundness"
177+
Saved theorem _______ "uop_type_soundness"
178+
Exporting theory "richerLang" ... done.
179+
Theory "richerLang" took 2.6s to build

‎richerlang/.hol/logs/typeSNTheory‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
<<HOL message: Created theory "typeSN">>
2+
<<HOL message: mk_functional:
3+
pattern completion has added 34 clauses to the original specification.>>
4+
Saved definition ____ "sn_v_def"
5+
Saved induction _____ "sn_v_ind"
6+
Saved definition ____ "envsn_def"
7+
Saved definition ____ "sn_exec_def"
8+
Saved definition ____ "sn_e_def"
9+
Saved theorem _______ "envsn_fdom"
10+
Saved theorem _______ "envsn_g_domsub_update"
11+
Saved theorem _______ "envsn_fdom_subset"
12+
Saved theorem _______ "flookup_submap_rev"
13+
Saved theorem _______ "envsn_e_submap"
14+
Saved theorem _______ "envsn_e_submap2"
15+
Saved theorem _______ "subset_inter_same"
16+
Saved theorem _______ "subset_inter_same2"
17+
Saved theorem _______ "envsn_g_submap"
18+
Saved theorem _______ "envsn_update"
19+
Saved theorem _______ "envsn_g_domsub"
20+
Saved theorem _______ "drestrict_not_in"
21+
Saved theorem _______ "sn_v_intT"
22+
Saved theorem _______ "sn_v_strT"
23+
Saved theorem _______ "sn_v_boolT"
24+
Saved theorem _______ "sn_v_pairT"
25+
Saved theorem _______ "sn_v_fnT"
26+
Saved theorem _______ "sn_v_sumT"
27+
Saved theorem _______ "bop_sn_lemma"
28+
Saved theorem _______ "uop_sn_lemma"
29+
Saved theorem _______ "drestrict_diff_update"
30+
Saved theorem _______ "sn_lemma"
31+
Saved theorem _______ "richerLang_sn"
32+
Exporting theory "typeSN" ... done.
33+
Theory "typeSN" took 2.8s to build

‎richerlang/.hol/logs/valueTheory‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
<<HOL message: Created theory "value">>
2+
Saved definition ____ "IntV0_def"
3+
Saved definition ____ "StrV0_def"
4+
Saved definition ____ "BoolV0_def"
5+
Saved definition ____ "Clos0_def"
6+
Saved definition ____ "PairV0_def"
7+
Saved definition ____ "SumV0_def"
8+
Saved theorem _______ "is_value_rules"
9+
Saved theorem _______ "is_value_ind"
10+
Saved theorem _______ "is_value_strongind"
11+
Saved theorem _______ "is_value_cases"
12+
Saved theorem _______ "is_value_int"
13+
Saved theorem _______ "is_value_str"
14+
Saved theorem _______ "is_value_bool"
15+
Saved theorem _______ "is_value_clos"
16+
Saved theorem _______ "is_value_pair"
17+
Saved theorem _______ "is_value_sumL"
18+
Saved theorem _______ "is_value_sumR"
19+
Saved theorem _______ "is_value_exists"
20+
Proved triviality ___ "is_value_Clos0"
21+
Saved definition ____ "IntV_def"
22+
Saved definition ____ "StrV_def"
23+
Saved definition ____ "BoolV_def"
24+
Saved definition ____ "Clos_def"
25+
Saved definition ____ "PairV_def"
26+
Saved definition ____ "SumLV_def"
27+
Saved definition ____ "SumRV_def"
28+
Saved theorem _______ "FORALL_value"
29+
Saved theorem _______ "value_ind"
30+
Saved theorem _______ "value_ax"
31+
Saved theorem _______ "value_size_thm"
32+
<<HOL message: mk_functional:
33+
pattern completion has added 5 clauses to the original specification.>>
34+
Saved definition ____ "is_BoolV_def"
35+
Saved induction _____ "is_BoolV_ind"
36+
Exporting theory "value" ... done.
37+
Theory "value" took 2.2s to build

‎richerlang/.hol/make-deps/envSemScript.sml.d‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
envSemScript.uo: /Users/mac/honors/HOL/sigobj/DB_dtype.uo /Users/mac/honors/HOL/sigobj/HolKernel.uo /Users/mac/honors/HOL/sigobj/Parse.uo /Users/mac/honors/HOL/sigobj/Q.uo /Users/mac/honors/HOL/sigobj/Theory.uo /Users/mac/honors/HOL/sigobj/TotalDefn.uo /Users/mac/honors/HOL/sigobj/boolLib.uo /Users/mac/honors/HOL/sigobj/bossLib.uo /Users/mac/honors/HOL/sigobj/dep_rewrite.uo /Users/mac/honors/HOL/src/finite_maps/finite_mapTheory.uo /Users/mac/honors/HOL/sigobj/holTheory.uo /Users/mac/honors/HOL/sigobj/optionTheory.uo /Users/mac/honors/HOL/sigobj/pairTheory.uo /Users/mac/honors/HOL/sigobj/pred_setTheory.uo richerLangTheory.uo valueTheory.uo

‎richerlang/.hol/make-deps/envSemTheory.sig.d‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
envSemTheory.ui: /Users/mac/honors/HOL/sigobj/Thm.uo

‎richerlang/.hol/make-deps/envSemTheory.sml.d‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
envSemTheory.uo: envSemTheory.ui /Users/mac/honors/HOL/sigobj/Globals.uo /Users/mac/honors/HOL/sigobj/Symtab.uo /Users/mac/honors/HOL/sigobj/Term.uo /Users/mac/honors/HOL/sigobj/Theory.uo /Users/mac/honors/HOL/sigobj/TheoryReader.uo /Users/mac/honors/HOL/sigobj/Thm.uo /Users/mac/honors/HOL/sigobj/Type.uo richerLangTheory.uo

‎richerlang/.hol/make-deps/lastmaker‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/Users/mac/honors/HOL/bin/Holmake

0 commit comments

Comments
 (0)