Loading theory "Timed_Automata.Floyd_Warshall" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.DBM_Zone_Semantics" via "Timed_Automata.DBM_Operations" via "Timed_Automata.DBM_Basics" via "Timed_Automata.DBM") Loading theory "Timed_Automata.Misc" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.Approx_Beta" via "Timed_Automata.Regions_Beta") locale enumerateable fixes T :: "'a set" and less :: "'a \ 'a \ bool" (infix "\" 50) assumes "enumerateable T (\)" Found termination order: "(\p. length (fst p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Proofs for inductive predicate(s) "sorted" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "(\p. length (fst p)) <*mlex*> {}" ### theory "Timed_Automata.Misc" ### 0.646s elapsed time, 1.348s cpu time, 0.000s GC time Loading theory "Timed_Automata.Timed_Automata" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.DBM_Zone_Semantics" via "Timed_Automata.DBM_Operations" via "Timed_Automata.DBM_Basics" via "Timed_Automata.DBM") Found termination order: "(\p. length (fst p)) <*mlex*> {}" class linordered_ab_monoid_add = linordered_ab_semigroup_add + fixes neutral :: "'a" assumes "neutl": "\x. \ + x = x" assumes "neutr": "\x. x + \ = x" class time = linordered_ab_group_add + assumes "dense": "\x y. x < y \ \z>x. z < y" assumes "non_trivial": "\x. x \ (0::'a)" Found termination order: "(\p. size (fst (snd (snd p)))) <*mlex*> (\p. size (fst (snd (snd (snd p))))) <*mlex*> (\p. size (snd (snd (snd (snd p))))) <*mlex*> {}" Found termination order: "(\p. size_list size (snd (snd (snd p)))) <*mlex*> {}" ### theory "Timed_Automata.Floyd_Warshall" ### 3.607s elapsed time, 7.100s cpu time, 0.336s GC time Found termination order: "size <*mlex*> {}" Found termination order: "size <*mlex*> {}" Proofs for inductive predicate(s) "valid_abstraction" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "clock_val" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "(\p. length (fst p)) <*mlex*> {}" Proofs for inductive predicate(s) "step_t" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "step_a" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "step" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "steps" *** exception THM 0 raised (line 328 of "drule.ML"): *** OF: no unifiers *** sorted (sorted_list_of_set ?A) *** finite S *** At command "with" (line 228 of "~~/afp/thys/Timed_Automata/Misc.thy") Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "step_z" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "steps_z" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Timed_Automata.Timed_Automata" ### 4.555s elapsed time, 8.940s cpu time, 0.888s GC time Loading theory "Timed_Automata.DBM" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.DBM_Zone_Semantics" via "Timed_Automata.DBM_Operations" via "Timed_Automata.DBM_Basics") Loading theory "Timed_Automata.Paths_Cycles" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.DBM_Zone_Semantics" via "Timed_Automata.DBM_Operations" via "Timed_Automata.DBM_Basics") Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> {}" Found termination order: "(\p. length (snd p)) <*mlex*> {}" Proofs for inductive predicate(s) "dbm_entry_val" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "{}" Proofs for inductive predicate(s) "dbm_lt" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Timed_Automata.Paths_Cycles" ### 1.298s elapsed time, 2.612s cpu time, 0.000s GC time Loading theory "Timed_Automata.Regions" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.Approx_Beta" via "Timed_Automata.Closure") Found termination order: "{}" instantiation DBMEntry :: (time) linorder less_eq_DBMEntry == less_eq :: 'a DBMEntry \ 'a DBMEntry \ bool less_DBMEntry == less :: 'a DBMEntry \ 'a DBMEntry \ bool instantiation DBMEntry :: (time) linordered_ab_monoid_add neutral_DBMEntry == neutral :: 'a DBMEntry plus_DBMEntry == plus :: 'a DBMEntry \ 'a DBMEntry \ 'a DBMEntry ### Partially applied constant "DBM.dbm_le" on left hand side of equation, in theorem: ### linorder.Min dbm_le (set (?x # ?xs)) \ ### fold linordered_monoid.min ?xs ?x ### Partially applied constant "DBM.dbm_le" on left hand side of equation, in theorem: ### linorder.Max dbm_le (set (?x # ?xs)) \ ### fold linordered_monoid.max ?xs ?x ### Partially applied constant "DBM.dbm_le" on left hand side of equation, in theorem: ### linordered_monoid.sorted_list_of_set (set ?xs) \ ### linordered_monoid.sort (remdups ?xs) ### theory "Timed_Automata.DBM" ### 2.991s elapsed time, 5.948s cpu time, 0.704s GC time Loading theory "Timed_Automata.DBM_Basics" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.DBM_Zone_Semantics" via "Timed_Automata.DBM_Operations") instantiation real :: time Proofs for inductive predicate(s) "valid_intv" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "intv_elem" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "valid_region" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "regionp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "Succp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "{}" Found termination order: "{}" Found termination order: "(\p. size (fst (snd (snd p)))) <*mlex*> (\p. size (fst (snd (snd (snd p))))) <*mlex*> {}" Found termination order: "{}" Proofs for inductive predicate(s) "isConst" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "isIntv" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "isGreater" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Timed_Automata.DBM_Basics" ### 1.041s elapsed time, 2.092s cpu time, 0.000s GC time Loading theory "Timed_Automata.DBM_Normalization" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.Approx_Beta" via "Timed_Automata.Regions_Beta") Found termination order: "{}" Found termination order: "{}" ### Ambiguous input (line 2627 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ("_cargs" ("_position" r) ("_position" c)))) ### ("_Setcompr" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" v) ### ("\<^const>Set.member" ("_position" v) ("_position" R))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ("_cargs" ("_position" r) ("_position" c)))) ### ("_Setcompr" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" v) ### ("\<^const>Set.member" ("_position" v) ("_position" R))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "Timed_Automata.DBM_Normalization" ### 0.174s elapsed time, 0.348s cpu time, 0.000s GC time Loading theory "Timed_Automata.DBM_Operations" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.DBM_Zone_Semantics") ### Ambiguous input (line 2633 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 16 parse trees (10 displayed): ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("_position" c))))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_position" \)) ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("_position" c) ("_position" v)) ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ("_position" c))) ### ("_position" v)) ### ("_position" \)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. Proofs for inductive predicate(s) "step_r" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Ambiguous input (line 2699 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. Found termination order: "{}" Proofs for inductive predicate(s) "steps_r" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "{}" ### theory "Timed_Automata.Regions" ### 3.286s elapsed time, 6.540s cpu time, 0.704s GC time Loading theory "Timed_Automata.Closure" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.Approx_Beta") locale AlphaClosure fixes X :: "'c set" and k :: "'c \ nat" and \ :: "('c \ real) set set" and V :: "('c \ real) set" assumes "AlphaClosure X" defines "\ \ {region X I r |I r. valid_region X k I r}" and "V \ {v. \x\X. 0 \ v x}" Proofs for inductive predicate(s) "step_z_alpha" Found termination order: "(\p. size (fst p)) <*mlex*> {}" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "steps_z_alpha" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "(\p. length (fst (snd (snd p)))) <*mlex*> {}" ### theory "Timed_Automata.Closure" ### 0.814s elapsed time, 1.604s cpu time, 0.572s GC time "as @ x # bs @ x # cs @ x # ds" :: "'a list" Found termination order: "(\p. length (fst (snd p))) <*mlex*> {}" ### theory "Timed_Automata.DBM_Operations" ### 1.874s elapsed time, 3.736s cpu time, 0.572s GC time Loading theory "Timed_Automata.DBM_Zone_Semantics" (required by "Timed_Automata.Normalized_Zone_Semantics") Proofs for inductive predicate(s) "step_z_dbm" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Loading theory "Timed_Automata.Regions_Beta" (required by "Timed_Automata.Normalized_Zone_Semantics" via "Timed_Automata.Approx_Beta") Proving the simplification rules ... Proofs for inductive predicate(s) "steps_z_dbm" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Timed_Automata.DBM_Zone_Semantics" ### 0.312s elapsed time, 0.628s cpu time, 0.000s GC time instantiation real :: time Proofs for inductive predicate(s) "valid_intv" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "valid_intv'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "intv_elem" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "intv'_elem" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "isConst" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "isIntv" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "isGreater" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "valid_region" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "regionp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale Beta_Regions fixes X :: "'c set" and k :: "'c \ nat" and \ :: "('c \ real) set set" and V :: "('c \ real) set" assumes "Beta_Regions X" defines "\ \ {region X I J r |I J r. valid_region X k I J r}" and "V \ {v. \x\X. 0 \ v x}" Found termination order: "{}" Found termination order: "{}" locale Beta_Regions' fixes X :: "'a set" and k :: "'a \ nat" and \ :: "('a \ real) set set" and V :: "('a \ real) set" and v :: "'a \ nat" and n :: "nat" and not_in_X :: "'a" assumes "Beta_Regions' X v n not_in_X" defines "\ \ {region X I J r |I J r. valid_region X k I J r}" and "V \ {v. \x\X. 0 \ v x}" locale Beta_Regions' fixes X :: "'a set" and k :: "'a \ nat" and \ :: "('a \ real) set set" and V :: "('a \ real) set" and v :: "'a \ nat" and n :: "nat" and not_in_X :: "'a" assumes "Beta_Regions' X v n not_in_X" defines "\ \ {region X I J r |I J r. valid_region X k I J r}" and "V \ {v. \x\X. 0 \ v x}" locale Beta_Regions' fixes X :: "'a set" and k :: "'a \ nat" and \ :: "('a \ real) set set" and V :: "('a \ real) set" and v :: "'a \ nat" and n :: "nat" and not_in_X :: "'a" assumes "Beta_Regions' X v n not_in_X" defines "\ \ {region X I J r |I J r. valid_region X k I J r}" and "V \ {v. \x\X. 0 \ v x}" ### theory "Timed_Automata.Regions_Beta" ### 5.941s elapsed time, 11.984s cpu time, 3.764s GC time Loading theory "Timed_Automata.Approx_Beta" (required by "Timed_Automata.Normalized_Zone_Semantics") instantiation real :: linordered_ab_monoid_add neutral_real == neutral :: real locale Regions fixes X :: "'c set" and k :: "'c \ nat" and v :: "'c \ nat" and n :: "nat" and not_in_X :: "'c" assumes "Regions X v n not_in_X" Proofs for inductive predicate(s) "step_z_beta" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "steps_z_beta" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Timed_Automata.Approx_Beta" ### 2.210s elapsed time, 4.152s cpu time, 0.156s GC time Loading theory "Timed_Automata.Normalized_Zone_Semantics" Proofs for inductive predicate(s) "step_z_norm" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "steps_z_norm" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale Regions fixes X :: "'c set" and k :: "'c \ nat" and v :: "'c \ nat" and n :: "nat" and not_in_X :: "'c" assumes "Regions X v n not_in_X" Proofs for inductive predicate(s) "valid_dbm" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale Regions' fixes X :: "'c set" and k :: "'c \ nat" and v :: "'c \ nat" and n :: "nat" and not_in_X :: "'c" assumes "Regions' X v n not_in_X" ### theory "Timed_Automata.Normalized_Zone_Semantics" ### 1.510s elapsed time, 2.980s cpu time, 0.292s GC time ### Metis: Falling back on "metis (mono_tags)"... \(?a, ?b) \ set (arcs ?i ?j ?xs); ?b \ ?j\ \ \c. ?xs = [?b] \ ?a = ?i \ (\ys. ?xs = ?b # c # ys \ ?a = ?i) \ (\ys. ?xs = ys @ [?a, ?b] \ c = ?j) \ (\ys zs. ?xs = ys @ ?a # ?b # c # zs) \ \ ?uu = \ Le ?v \ \ = \ Lt ?v \ \ = \ Le ?a \ Le ?b = Le (?a + ?b) Le ?a \ Lt ?b = Lt (?a + ?b) Lt ?a \ Le ?b = Lt (?a + ?b) Lt ?a \ Lt ?b = Lt (?a + ?b) ### Ambiguous input (line 2641 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" xs) ("_position" c)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" xs) ("_position" c)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2641 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_position" c) ("_position" v)) ### ("_position" \)) ### ("_position" \))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ("_position" c))) ### ("_position" v)) ### ("_position" \)) ### ("_position" \))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2641 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 4 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_position" c) ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_position" c) ("_position" v)) ### ("_position" \)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ("_position" c))) ### ("_position" v)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_position" c) ("_position" v)) ### ("_position" \)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_position" c) ("_position" v)) ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ("_position" c))) ### ("_position" v)) ### ("_position" \)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ("_position" c))) ### ("_position" v)) ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ("_position" c))) ### ("_position" v)) ### ("_position" \)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2643 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("_Update" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_position" c) ("_position" v)) ### ("_updbind" ("_position" x) ("_position" c))) ### ("_Update" ### ("_applC" ### ("_list" ("\<^const>FuncSet.funcset" ("_position" xs) ("_position" c))) ### ("_position" v)) ### ("_updbind" ("_position" x) ("_position" c))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2645 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ("_position" ?v) ("_position" \)) ### ("_applC" ("_position" region_set) ### ("_cargs" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ### ("_applC" ("_position" real) ("_position" c)))) ### ("_position" v)) ### ("_position" \)) ### ("_cargs" ("_position" x) ("_position" c)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ("_position" ?v) ("_position" \)) ### ("_applC" ("_position" region_set) ### ("_cargs" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_applC" ("_position" real) ("_position" c)) ("_position" v)) ### ("_position" \)) ### ("_cargs" ("_position" x) ("_position" c)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2646 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ### ("\<^const>List.list.Cons" ("_position" x) ("_position" xs)) ### ("_applC" ("_position" real) ("_position" c))))) ### ("_applC" ("_position" region_set) ### ("_cargs" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ### ("_applC" ("_position" real) ("_position" c)))) ### ("_position" v)) ### ("_position" \)) ### ("_cargs" ("_position" x) ("_position" c)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ### ("\<^const>List.list.Cons" ("_position" x) ("_position" xs)) ### ("_applC" ("_position" real) ("_position" c))))) ### ("_applC" ("_position" region_set) ### ("_cargs" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_applC" ("_position" real) ("_position" c)) ("_position" v)) ### ("_position" \)) ### ("_cargs" ("_position" x) ("_position" c)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2650 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ### ("_applC" ("_position" real) ("_position" c)))) ### ("_position" u)) ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_applC" ("_position" real) ("_position" c)) ("_position" u)) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2651 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ### ("\<^const>List.list.Cons" ("_position" x) ("_position" xs)) ### ("_applC" ("_position" real) ("_position" c)))) ### ("_position" u)) ### ("_Update" ("_position" ?u) ### ("_updbind" ("_position" x) ### ("_applC" ("_position" real) ("_position" c)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Timed_Automata.clock_set_abbrv" ### ("\<^const>List.list.Cons" ("_position" x) ("_position" xs)) ### ("_applC" ("_position" real) ("_position" c)) ("_position" u)) ### ("_Update" ("_position" ?u) ### ("_updbind" ("_position" x) ### ("_applC" ("_position" real) ("_position" c)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2652 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" ?u) ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" xs) ### ("_applC" ("_position" real) ("_position" c)))) ### ("_position" v)) ### ("_position" \)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" ?u) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" xs) ### ("_applC" ("_position" real) ("_position" c)) ("_position" v)) ### ("_position" \)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2658 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ### ("\<^const>List.list.Cons" ("_position" x) ("_position" xs)) ### ("_applC" ("_position" real) ("_position" c)))) ### ("_position" v)) ### ("_position" ?v))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Timed_Automata.clock_set_abbrv" ### ("\<^const>List.list.Cons" ("_position" x) ("_position" xs)) ### ("_applC" ("_position" real) ("_position" c)) ("_position" v)) ### ("_position" ?v))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2716 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("\<^const>Groups.zero_class.zero")))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("_position" \)) ### ("_applC" ("_position" region_set') ### ("_cargs" ("_position" R) ### ("_cargs" ("_position" r) ("\<^const>Groups.zero_class.zero")))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2716 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("_position" \)) ### ("_position" \))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("_position" \)) ### ("_position" \))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2716 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 4 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("_position" \)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("_position" \)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("_position" \)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("_position" \)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2718 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>Regions.part" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("_position" \)) ### ("\<^const>Regions.part" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("_position" \)) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2734 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" u') ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" u') ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2793 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" v)) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" v)) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2800 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("_position" ?R'))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("_position" ?R'))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2800 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2801 of "~~/afp/thys/Timed_Automata/Regions.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.step" ("_position" A) ("_position" l) ### ("_position" u) ("_position" l') ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.step" ("_position" A) ("_position" l) ### ("_position" u) ("_position" l') ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 87 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" v') ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" v)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" v') ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" v)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 93 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" v)) ### ("_applC" ("_position" zone_set) ### ("_cargs" ("_position" R) ("_position" r))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" v)) ### ("_applC" ("_position" zone_set) ### ("_cargs" ("_position" R) ("_position" r))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 411 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" v') ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" v') ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 428 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u')) ### ("_position" ?R'))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u')) ### ("_position" ?R'))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 428 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u')) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u')) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 430 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.step" ("_position" A) ("_position" l) ### ("_position" u') ("_position" l') ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u')))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.step" ("_position" A) ("_position" l) ### ("_position" u') ("_position" l') ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u')))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 431 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u')) ### ("_position" ?W'))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u')) ### ("_position" ?W'))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 495 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" v') ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" v') ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 512 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u')) ### ("_position" ?R'))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u')) ### ("_position" ?R'))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 512 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u')) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.clock_val" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u')) ### ("_applC" ("_position" inv_of) ### ("_cargs" ("_position" A) ("_position" l'))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 514 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.step" ("_position" A) ("_position" l) ### ("_position" u') ("_position" l') ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u')))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Timed_Automata.step" ("_position" A) ("_position" l) ### ("_position" u') ("_position" l') ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u')))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 515 of "~~/afp/thys/Timed_Automata/Closure.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Timed_Automata.clock_set_abbrv" ("_position" r) ### ("\<^const>Groups.zero_class.zero") ("_position" u')) ### ("_position" ?W'))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("_applC" ### ("_list" ### ("\<^const>FuncSet.funcset" ("_position" r) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" u')) ### ("_position" ?W'))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. theorem split_min: fixes P :: "'b \ bool" and i :: "'b" and j :: "'b" shows "P (min i j) = ((i \ j \ P i) \ (\ i \ j \ P j))" theorem inducts: fixes x1 :: "('a \ ('b, real) cconstraint \ 'd \ 'b list \ 'a) set \ ('a \ ('b, real) cconstraint)" and x2 :: "'a" and x3 :: "nat \ nat \ real DBMEntry" and x4 :: "nat \ nat" and x5 :: "'b \ nat" and x6 :: "nat" and x7 :: "'a" and x8 :: "nat \ nat \ real DBMEntry" and P :: "('a \ ('b, real) cconstraint \ 'd \ 'b list \ 'a) set \ ('a \ ('b, real) cconstraint) \ 'a \ (nat \ nat \ real DBMEntry) \ (nat \ nat) \ ('b \ nat) \ nat \ 'a \ (nat \ nat \ real DBMEntry) \ bool" assumes "x1 \ \x2, x3\ \\<^bsub>x4,x5,x6\<^esub> \x7, x8\" and "\A l D v n l' D' k. A \ \l, D\ \\<^bsub>v,n\<^esub> \l', D'\ \ P A l D k v n l' (DBM_Normalization.norm (FW D' n) (\x. real (k x)) n)" shows "P x1 x2 x3 x4 x5 x6 x7 x8" \?R \ \; ?R' \ \; ?v \ ?R; ?v \ ?R'\ \ ?R = ?R' \?R \ \; ?R' \ \; ?v \ ?R; ?v \ ?R'\ \ ?R = ?R' isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Timed_Automata/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Timed_Automata/outline -o pdf -n outline -t /proof,/ML *** exception THM 0 raised (line 328 of "drule.ML"): *** OF: no unifiers *** sorted (sorted_list_of_set ?A) *** finite S *** At command "with" (line 228 of "~~/afp/thys/Timed_Automata/Misc.thy")