Searched refs:fs (Results 1 - 25 of 209) sorted by relevance

123456789

/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/
H A DMakefile6 ln -fs ../minisat/Proof.o
7 ln -fs ../minisat/File.o
8 ln -fs ../minisat/File.h
9 ln -fs ../minisat/Proof.h
10 ln -fs ../minisat/Global.h
11 ln -fs ../minisat/Sort.h
12 ln -fs ../minisat/SolverTypes.h
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/
H A DconcrRepScript.sml67 >- (Induct_on `pos` >> fs[] >> rpt strip_tac
68 >> fs[char_def]
71 >> simp[SUBSET_DEF] >> rpt strip_tac >> fs[]
73 >- (Induct_on `pos` >> fs[] >> rpt strip_tac
87 >- (Induct_on `neg1` >> fs[MEM_SUBSET_def] >> rpt strip_tac
91 >- (rpt strip_tac >> fs[MEM_SUBSET_def]
101 gen_tac >> Induct_on `p` >> fs[IN_POW] >> rpt strip_tac >> fs[]
102 >> fs[char_def,IN_POW,EQ_IMP_THM] >> rpt strip_tac
111 gen_tac >> Induct_on `n` >> fs[IN_PO
[all...]
H A DwaaSimplScript.sml17 fs[partial_order_def, rrestrict_def, rel_to_reln_def] >> rpt strip_tac
18 >- (fs[domain_def,SUBSET_DEF] >> rpt strip_tac)
19 >- (fs[range_def, SUBSET_DEF] >> rpt strip_tac)
20 >- (fs[transitive_def,SUBSET_DEF,trans_implies_def] >> rpt strip_tac
22 >> fs[trans_implies_def] >> metis_tac[SUBSET_TRANS])
23 >- (fs[reflexive_def,SUBSET_DEF,trans_implies_def] >> rpt strip_tac
24 >> Cases_on `x` >> fs[trans_implies_def] >> metis_tac[SUBSET_REFL])
25 >- (fs[antisym_def,SUBSET_DEF,trans_implies_def] >> rpt strip_tac
27 >> fs[trans_implies_def] >> metis_tac[SUBSET_ANTISYM])
33 fs[finite_prefixes_de
[all...]
H A Dltl2waaScript.sml32 Induct_on `f` >> fs[trans_def, char_def, SUBSET_DEF,d_conj_def]
46 Induct_on `f` >> fs[trans_def, tempDNF_def,BIGUNION,SUBSET_DEF] >> rpt strip_tac
47 >- (qexists_tac `{{}}` >> qexists_tac `{char �� a}` >> fs[])
48 >- (qexists_tac `{{}}` >> qexists_tac `{�� DIFF char �� a}` >> fs[])
51 >- (fs[d_conj_def] >>
67 >> qexists_tac `e ��� e'` >> fs[] >> qexists_tac `t ��� t'`
68 >> dsimp[] >> fs[] >> rpt strip_tac
70 >> qexists_tac `e` >> qexists_tac `e'` >> fs[]
71 >> fs[UNION_DEF] >> rpt strip_tac
78 >> qexists_tac `q` >> qexists_tac `a'''` >> fs[])
[all...]
H A DconcrGBArepScript.sml55 suffices_by fs[]
57 >> Induct_on `s` >> fs[gba_trans_concr_def] >> rpt strip_tac
58 >- (fs[cE_equiv_def,MEM_EQUAL_def,MEM_SUBSET_def])
59 >- (fs[cE_equiv_def,MEM_EQUAL_def,MEM_SUBSET_def]
60 >> fs[d_conj_concr_def,FOLDR_LEMM4] >> qexists_tac `e1` >> simp[]
63 >- (fs[cE_equiv_def,MEM_EQUAL_def,MEM_SUBSET_def]
64 >> fs[d_conj_concr_def,FOLDR_LEMM4]
73 >- (Cases_on `s= []` >> fs[]
74 >- (fs[d_conj_concr_def,FOLDR_CONS,MEM_MAP]
78 >> simp[] >> fs[d_conj_concr_de
[all...]
H A DgeneralHelpersScript.sml10 rpt strip_tac >> fs[] >> qexists_tac `CHOICE s`
15 >> strip_tac >> (fs[SUBSET_DEF,CHOICE_DEF]))
22 rpt strip_tac >> fs[transitive_def, rrestrict_def]
29 rpt strip_tac >> fs[antisym_def, in_rrestrict]
35 rpt strip_tac >> Induct_on `n` >> fs[]
42 strip_tac >> fs[IMAGE_DEF]
45 >> rpt strip_tac >> fs[SUBSET_DEF]
59 fs[UNION_DEF, SUBSET_DEF] >> rpt strip_tac
73 fs[SET_EQ_SUBSET, SUBSET_DEF] >> rpt strip_tac
80 simp[EQ_IMP_THM] >> fs[]
[all...]
H A DgbaSimplScript.sml20 fs[partial_order_def, rrestrict_def, rel_to_reln_def] >> rpt strip_tac
21 >- (fs[domain_def,SUBSET_DEF] >> rpt strip_tac)
22 >- (fs[range_def, SUBSET_DEF] >> rpt strip_tac)
23 >- (fs[transitive_def,SUBSET_DEF] >> rpt strip_tac
24 >> Cases_on `x` >> Cases_on `y` >> Cases_on `z` >> fs[trans_implies_def]
26 >- (fs[reflexive_def,SUBSET_DEF] >> rpt strip_tac >> Cases_on `x`
27 >> fs[trans_implies_def])
28 >- (fs[antisym_def,SUBSET_DEF] >> rpt strip_tac >> Cases_on `x`
29 >> Cases_on `y` >> fs[trans_implies_def]
38 fs[finite_prefixes_de
[all...]
H A DbuechiAScript.sml51 rw[EQ_IMP_THM] >> fs[isAcceptingGBARunFor_def]
53 ��� (a, r (j+1)) ��� aut.trans (r j) ��� at x j ��� a}` by fs[]
63 fs[DIFF_DEF, count_def] >> fs[SET_EQ_SUBSET, SUBSET_DEF]
64 >> rpt strip_tac >> fs[] >> metis_tac[]
72 ��� i ��� j}` by fs[]
77 >> fs[IN_ABS] >> metis_tac[]
91 fs[SET_EQ_SUBSET, SUBSET_DEF] >> rpt strip_tac
109 fs[isValidGBA_def]
121 >> CCONTR_TAC >> fs[]
[all...]
H A Dconcrwaa2gbaScript.sml29 rpt strip_tac >> fs[get_acc_set_def]
34 >> fs[concrEdge_component_equality]
36 >> fs[MEM_EQUAL_SET] >> rw[]
56 simp[EQ_IMP_THM] >> fs[valid_acc_def,concr2Abstr_final_def] >> rpt strip_tac
57 >> fs[MEM_MAP]
58 >- (Cases_on `y` >> fs[] >> rw[] >> rename[`MEM (f,f_trns) acc`]
69 >> fs[until_iff_final_def]
74 >> `(���f1 f2. f = U f1 f2)` by (Cases_on `f` >> fs[is_until_def]) >> simp[]
78 simp[is_until_def] >> fs[until_iff_final_def]
83 simp[graphStates_def,MEM_MAP] >> qexists_tac `(n,x)` >> fs[]
[all...]
H A DalterAScript.sml42 fs[isValidAlterA_def] >> simp[SUBSET_DEF] >> rpt strip_tac
90 rpt gen_tac >> strip_tac >> Induct_on `i` >> fs[infBranchOf_def]
93 >> fs[validAARunFor_def]
104 >> fs[validAARunFor_def, branchRange_def, SUBSET_DEF] >> rpt strip_tac
113 >> fs[]
115 >> qexists_tac `b 0` >> fs[branchRange_def]
149 >> fs[isVeryWeakWithOrder_def, infBranchOf_def, validAARunFor_def]
166 >> fs[linear_order_def, branchRange_def, infBranchOf_def, validAARunFor_def]
167 >> fs[isVeryWeakWithOrder_def]
168 >> fs[domain_de
[all...]
H A Dconcrltl2waaScript.sml26 Induct_on `m2` >> fs[]
27 >> rpt strip_tac >> fs[MEM_MAP] >> rw[] >> simp[EQ_IMP_THM]
35 Induct_on `m2` >> fs[]
36 >> rpt strip_tac >> fs[MEM_MAP] >> rw[] >> simp[EQ_IMP_THM]
45 Induct_on `m1` >> fs[]
46 >> rpt strip_tac >> fs[MEM_MAP] >> rw[] >> simp[EQ_IMP_THM]
55 Induct_on `m1` >> fs[]
56 >> rpt strip_tac >> fs[MEM_MAP] >> rw[] >> simp[EQ_IMP_THM]
64 Induct_on `l` >> rpt strip_tac >> fs[]
79 Induct_on `l` >> fs[concrEdge_component_equalit
[all...]
H A Dwaa2baScript.sml21 fs[rrestrict_def, partial_order_def, tr_less_general_def]
23 >- (fs[domain_def, SUBSET_DEF] >> rpt strip_tac)
24 >- (fs[range_def, SUBSET_DEF] >> rpt strip_tac)
25 >- (fs[transitive_def] >> rpt strip_tac >> rw[]
27 >- (fs[reflexive_def] >> rpt strip_tac
29 >- (fs[antisym_def] >> rpt strip_tac >> rw[] >> metis_tac[SUBSET_ANTISYM])
87 >> fs[finite_prefixes_def, rrestrict_def,d_gen_def] >> rpt strip_tac
90 suffices_by (rpt strip_tac >> fs[])
99 >- (`ITSET (d_conj o SND) v v1 = v1` by metis_tac[ITSET_def] >> fs[])
100 >- (fs[]
[all...]
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/
H A Dfor_nd_compileScript.sml47 fs [sem_t_def,sem_e_def]);
66 \\ fs [sem_e_def,permute_pair_def,LET_DEF,oracle_get_def,
68 \\ ect \\ fs [] \\ rfs [] \\ ect \\ fs [] \\ rfs []);
76 \\ ect \\ fs [PULL_FORALL,STOP_def]
78 \\ fs [dec_clock_def]
89 \\ Cases_on `sem_e s b1` \\ fs []
90 \\ Cases_on `q` \\ fs []
92 \\ Cases_on `sem_t r t` \\ fs []
93 \\ Cases_on `q` \\ fs []
702 local val fs = fsrw_tac[] val rfs = rev_full_simp_tac(srw_ss()) in value
[all...]
H A Dfor_compileScript.sml43 \\ fs [sem_e_def]
44 \\ every_case_tac \\ fs [] \\ rfs []);
53 \\ fs [STOP_def]);
57 fs [semantics_def,phase1_correct]);
66 fs [sem_t_def,sem_e_def]);
88 \\ every_case_tac \\ fs [PULL_FORALL,STOP_def]
90 \\ fs [dec_clock_def]
101 \\ Cases_on `sem_e s b1` \\ fs []
102 \\ Cases_on `q` \\ fs []
104 \\ Cases_on `sem_t r t` \\ fs []
214 local val fs = fsrw_tac[] in value
613 local val rw = srw_tac[] val fs = fsrw_tac[] val rfs = rev_full_simp_tac(srw_ss()) in value
995 val rw = srw_tac[] val fs = fsrw_tac[] value
[all...]
/seL4-l4v-10.1.1/HOL4/src/integer/
H A Dint_bitwiseScript.sml14 srw_tac [] [int_not_def] \\ fs [] \\ intLib.COOPER_TAC);
23 \\ fs [int_not_def] \\ `F` by intLib.COOPER_TAC);
75 srw_tac [] [] \\ fs [ODD_EVEN,EVEN_MOD2]
83 \\ Cases_on `n = 0` \\ fs [num_of_bits_def]
84 \\ Cases_on `ODD n` \\ fs [num_of_bits_def]
85 \\ `n DIV 2 < n` by (fs [DIV_LT_X] \\ decide_tac)
86 \\ res_tac \\ fs []
91 \\ fs []);
95 Induct \\ fs [bits_bitwise_def,LET_DEF]);
99 fs [int_bitwise_de
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DtripleScript.sml56 Cases_on `x1` \\ fs []
62 \\ fs [TERM_TAILREC_def, LET_DEF]
66 \\ fs []
68 \\ fs [FUNPOW])
70 \\ fs []
72 \\ fs []
76 >- (Cases_on `n` \\ fs [FUNPOW] \\ metis_tac [])
78 \\ fs [FUNPOW]
91 >- (fs []
93 \\ fs [TRIPLE_de
[all...]
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/small-step/
H A Dfor_osmallScript.sml254 val etac = (fs[Once step_t_cases]>>fs[Once step_t_cases,Once step_e_cases,conjs_def])
263 ho_match_mp_tac step_e_strongind>>rw[]>>fs[FORALL_PROD]
264 >- (rw[conjs_def]>>fs[Once step_e_cases]>>rfs[])
265 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[]))
266 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[]))
267 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[]))
268 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[]))
272 fs[Once step_e_cases])
274 fs[conjs_de
640 local val rw = srw_tac[] val fs = fsrw_tac[] in value
874 local val rw = srw_tac[] val fs = fsrw_tac[] in value
[all...]
H A DforSmallScript.sml189 val etac = (fs[Once step_t_cases]>>fs[Once step_t_cases,Once step_e_cases])
197 ho_match_mp_tac step_e_strongind>>rw[]>>fs[FORALL_PROD]
199 (fs[Once step_e_cases]>>rfs[])
201 ntac 2(fs[Once step_e_cases]>>rfs[])
205 fs[is_val_e_def,Once step_e_cases]
209 (Cases_on`e1`>>fs[is_val_e_def,Once step_e_cases]))
213 fs[Once step_e_cases]
215 (Cases_on`e1`>>fs[is_val_e_def,Once step_e_cases])
219 ntac 2 (fs[Onc
637 local val rw = srw_tac[] val fs = fsrw_tac[] in value
[all...]
H A Dsimple_traceScript.sml14 fs []
17 fs []) >>
22 fs []);
70 fs [check_trace_def])) >>
74 fs [] >>
76 fs [check_trace_def] >>
94 fs [check_trace_def] >>
97 fs [check_trace_def] >>
109 fs [Once RTC_CASES1] >>
110 fs []) >>
[all...]
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/
H A DoptScript.sml43 fs [] >>
100 fs [] >>
115 fs []);
127 >- (fs [shift_def, sem_def, res_rel_rw] >>
128 fs [state_rel_rw, val_rel_refl])
129 >- (fs [shift_def, sem_def, res_rel_rw] >>
134 fs [LIST_REL_EL_EQN])
135 >- fs [state_rel_rw]
142 fs [LIST_REL_EL_EQN] >>
145 >- fs [state_rel_r
[all...]
H A DcbvScript.sml121 fs[check_clock_def,dec_clock_def] >>
135 rpt strip_tac >> res_tac >> simp[] >> fs[])
153 BasicProvers.EVERY_CASE_TAC >> fs[] >>
165 rw[] >> fs[] >>
184 fs []
186 fs [] >>
188 fs [] >>
190 fs [] >>
192 fs [] >>
194 fs [dec_clock_de
[all...]
H A DlogrelScript.sml58 fs [] >>
81 fs [res_rel_def] >>
134 fs [state_rel_rw])
140 fs [res_rel_def, state_rel_rw]));
151 >- (fs [exec_rel_rw, LET_THM] >>
155 >- (fs [state_rel_rw, LIST_REL_EL_EQN] >>
182 fs [state_rel_rw] >>
189 fs [LIST_REL_EL_EQN] >>
192 fs [] >>
194 >- (fs [state_rel_r
200 local val rw = srw_tac[] val fs = fsrw_tac[] in value
419 local val rw = srw_tac[] val fs = fsrw_tac[] in value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DsimpleSexpParseScript.sml16 Induct \\ simp[] \\ Cases_on`ls`\\fs[])
29 \\ fs[optionTheory.IS_SOME_EXISTS]);
74 \\ Cases_on`h` \\ fs[]
75 \\ Cases_on`n = 57` \\ fs[UNHEX_def]
76 \\ Cases_on`n = 56` \\ fs[UNHEX_def]
77 \\ Cases_on`n = 55` \\ fs[UNHEX_def]
78 \\ Cases_on`n = 54` \\ fs[UNHEX_def]
79 \\ Cases_on`n = 53` \\ fs[UNHEX_def]
80 \\ Cases_on`n = 52` \\ fs[UNHEX_def]
81 \\ Cases_on`n = 51` \\ fs[UNHEX_de
[all...]
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DFormula.sml55 fun funcs fs [] = fs
56 | funcs fs (True :: fms) = funcs fs fms
57 | funcs fs (False :: fms) = funcs fs fms
58 | funcs fs (Atom atm :: fms) =
59 funcs (NameAritySet.union (Atom.functions atm) fs) fms
60 | funcs fs (Not p :: fms) = funcs fs (
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DFormula.sml55 fun funcs fs [] = fs
56 | funcs fs (True :: fms) = funcs fs fms
57 | funcs fs (False :: fms) = funcs fs fms
58 | funcs fs (Atom atm :: fms) =
59 funcs (NameAritySet.union (Atom.functions atm) fs) fms
60 | funcs fs (Not p :: fms) = funcs fs (
[all...]

Completed in 129 milliseconds

123456789