/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | Makefile | 6 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 D | concrRepScript.sml | 67 >- (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 D | waaSimplScript.sml | 17 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 D | ltl2waaScript.sml | 32 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 D | concrGBArepScript.sml | 55 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 D | generalHelpersScript.sml | 10 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 D | gbaSimplScript.sml | 20 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 D | buechiAScript.sml | 51 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 D | concrwaa2gbaScript.sml | 29 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 D | alterAScript.sml | 42 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 D | concrltl2waaScript.sml | 26 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 D | waa2baScript.sml | 21 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 D | for_nd_compileScript.sml | 47 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 D | for_compileScript.sml | 43 \\ 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 D | int_bitwiseScript.sml | 14 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 D | tripleScript.sml | 56 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 D | for_osmallScript.sml | 254 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 D | forSmallScript.sml | 189 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 D | simple_traceScript.sml | 14 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 D | optScript.sml | 43 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 D | cbvScript.sml | 121 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 D | logrelScript.sml | 58 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 D | simpleSexpParseScript.sml | 16 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 D | Formula.sml | 55 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 D | Formula.sml | 55 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...] |